8.6. The chart layer
Sixteen modules that derive the properness principle from one commutative-algebra hypothesis: in the nested polynomial ring with pin coordinates as coefficients and grounded twist coordinates as outer variables, every homogeneous prime over the chart ideal that avoids the provenance denominator has full height. The largest Lean-only cluster in the development, documented as one node; the module inventory is in the correspondence chapter.
Lean code for Lemma8.6.1●2 declarations
Associated Lean declarations
-
complete
def RB31E2E.UniversalHomogeneousChart.FiniteGenericIncidenceProvenancePrimeHeightCondition.{u_1, u_2} {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] [DecidableEq E] (root : V) (src dst : E → V) (active : Finset E) (hLoop : ∀ e ∈ active, src e ≠ dst e) (angularChart : ↥active → Fin 3) (selected : Finset ↥active) (distinctChart : RB31E2E.UniversalHomogeneousChart.DistinctnessChart V) : Prop
def RB31E2E.UniversalHomogeneousChart.FiniteGenericIncidenceProvenancePrimeHeightCondition.{u_1, u_2} {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] [DecidableEq E] (root : V) (src dst : E → V) (active : Finset E) (hLoop : ∀ e ∈ active, src e ≠ dst e) (angularChart : ↥active → Fin 3) (selected : Finset ↥active) (distinctChart : RB31E2E.UniversalHomogeneousChart.DistinctnessChart V) : Prop
Full twist height is required only for homogeneous primes which meet the complete pairwise-distinct and active-angular chart.
-
theoremdefined in RB31EndToEnd/Incidence/FiniteFullProvenancePropernessAssembly.leancomplete
theorem RB31E2E.SparseNullIncidence.propernessPrinciple_of_finiteGenericFullProvenancePrimeHeights (hHeight : ∀ (V E : Type) [inst : Fintype V] [inst_1 : DecidableEq V] [Fintype E] [inst_3 : DecidableEq E] (src dst : E → V) (active : Finset E) (hLoop : ∀ e ∈ active, src e ≠ dst e) (F : RB31E2E.SimpleEdgeSet V), 2 ≤ Fintype.card V → RB31E2E.Sparse22 F → ∀ (hRepresented : ∀ f ∈ F, ∃ e, RB31E2E.SparseNullIncidence.activeEdge src dst active hLoop e = f), Finset.card F = 6 * (Fintype.card V - 1) - 2 * active.card → ∀ (root : V) (distinctChart : RB31E2E.UniversalHomogeneousChart.DistinctnessChart V) (angularChart : ↥active → Fin 3), RB31E2E.UniversalHomogeneousChart.FiniteGenericIncidenceProvenancePrimeHeightCondition root src dst active hLoop angularChart (RB31E2E.SparseNullIncidence.selectedSkeletonOccurrences src dst active hLoop F hRepresented) distinctChart) : RB31E2E.SparseNullIncidence.PropernessPrinciple
theorem RB31E2E.SparseNullIncidence.propernessPrinciple_of_finiteGenericFullProvenancePrimeHeights (hHeight : ∀ (V E : Type) [inst : Fintype V] [inst_1 : DecidableEq V] [Fintype E] [inst_3 : DecidableEq E] (src dst : E → V) (active : Finset E) (hLoop : ∀ e ∈ active, src e ≠ dst e) (F : RB31E2E.SimpleEdgeSet V), 2 ≤ Fintype.card V → RB31E2E.Sparse22 F → ∀ (hRepresented : ∀ f ∈ F, ∃ e, RB31E2E.SparseNullIncidence.activeEdge src dst active hLoop e = f), Finset.card F = 6 * (Fintype.card V - 1) - 2 * active.card → ∀ (root : V) (distinctChart : RB31E2E.UniversalHomogeneousChart.DistinctnessChart V) (angularChart : ↥active → Fin 3), RB31E2E.UniversalHomogeneousChart.FiniteGenericIncidenceProvenancePrimeHeightCondition root src dst active hLoop angularChart (RB31E2E.SparseNullIncidence.selectedSkeletonOccurrences src dst active hLoop F hRepresented) distinctChart) : RB31E2E.SparseNullIncidence.PropernessPrinciple
Complete-provenance localized height, for every sparse-null input and every finite chart, implies the literal `PropernessPrinciple` consumed by the body--pin sufficiency proof.
The layer works in a single nested ring
\Q[\text{pin variables}][\text{grounded twist variables}], where the
standard grading of the outer ring is the twist grading: each Split–Klein
equation is homogeneous of degree two and each pin-compatibility coordinate
homogeneous of degree one, so the free scaling action of the paper's
Lemma 6.4 appears as homogeneity of the chart ideal. Its interface is one
\mathrm{Prop}-valued definition,
/-- Full twist height is required only for homogeneous primes which meet
the complete pairwise-distinct and active-angular chart. -/
def FiniteGenericIncidenceProvenancePrimeHeightCondition
{V E : Type*} [Fintype V] [DecidableEq V] [DecidableEq E]
(root : V) (src dst : E → V) (active : Finset E)
(hLoop : ∀ e ∈ active, src e ≠ dst e)
(angularChart : active → Fin 3) (selected : Finset active)
(distinctChart : DistinctnessChart V) : Prop :=
∀ (Q : Ideal (FiniteGenericRelativeRing root E)),
Q.IsPrime →
Q.IsHomogeneous
(MvPolynomial.homogeneousSubmodule
(Fin (groundedTwistVariableCount root))
(GenericPinCoefficientField E)) →
finiteGenericUniversalChartIdeal
root src dst active angularChart selected ≤ Q →
finiteGenericIncidenceProvenanceDenominator
root src dst active hLoop distinctChart angularChart ∉ Q →
(groundedTwistVariableCount root : ℕ∞) ≤ Q.height
and the choice of denominator carries the geometry: one nonzero
twist-difference coordinate per ordered pair of distinct bodies removes both
the scaling orbit and every equality-collapse component, replacing the
paper's normalization of a single twist, and one nonzero angular coordinate
per active occurrence makes each pin's two remaining compatibility equations
triangular, so that the active occurrences provably contribute exactly two
units of height each. The selected-null ideal's height, from
the Split–Klein chapter, is the remaining
input; a full-height prime avoiding the denominator is then impossible by
the height-drop lemma, so a power of the
denominator lies in the chart ideal, and clearing denominators and applying
the rational-to-integer descent of
exists_integer_certificate_vanishing_on_real_zeros
leaves the nonzero integer certificate the properness principle asserts.
That derivation is
propernessPrinciple_of_finiteGenericFullProvenancePrimeHeights,
and no module of the layer asserts a rigidity, properness or height fact of
its own.