7.5. The height theorem🔗

Theorem7.5.1

Group: The paper's algebraic argument: the form, the ideal, the shear, the dimension formula, and the height theorem. (5)

Group member previews

Preview

Definition 7.1.1

Loading preview

Group member preview content is loaded from the Blueprint HTML cache.

uses 1

Used by 3

Reverse dependency previews

Preview

Corollary 7.6.1

Loading preview

Reverse dependency preview content is loaded from the Blueprint HTML cache.

✓L∃∀N

Tagspaperdeviation

Let V \ne \emptyset and let F be a finite simple (2,2)-sparse graph on V. If P is a minimal prime of I_F whose component V(P) meets the distinct locus, then \operatorname{ht} P = |E_F|; equivalently, with X_o = 0, every component meeting the distinct locus has dimension 6(|V| - 1) - |E_F|. (Zheng, 2026, Theorem 1.3)

Lean code for Theorem7.5.1●4 theorems

theoremdefined in RB31EndToEnd/NullCellule/WittShearDistinctPrime.lean

complete

theorem RB31E2E.WittShearDistinctPrime.coefficientMinimalPrime_height_eq_edgeCard_of_groundedPF.{u,
    v}
  {V : Type u} {E : Type v} [Fintype V] [DecidableEq V] [DecidableEq E]
  (root : V) (src dst : E → V) (active : Finset E)
  (hLoop : ∀ e ∈ active, src e ≠ dst e) (F : RB31E2E.SimpleEdgeSet V)
  (hRepresented :
    ∀ f ∈ F,
      ∃ e,
        RB31E2E.SparseNullIncidence.activeEdge src dst active hLoop e =
          f)
  (chart : RB31E2E.UniversalHomogeneousChart.DistinctnessChart V)
  (P : Ideal (RB31E2E.PinOuterActiveHeight.TwistCoefficientRing root))
  [P.IsPrime]
  (hP :
    P ∈
      (RB31E2E.SelectedNullHeight.coefficientSelectedNullIdeal root src
          dst active
          (RB31E2E.SparseNullIncidence.selectedSkeletonOccurrences src
            dst active hLoop F hRepresented)).minimalPrimes)
  (hden :
    RB31E2E.PinOuterFullProvenanceHeightTransfer.coefficientDistinctnessDenominator
        root chart ∉
      P)
  (hPF :
    ∀ {K : Type u} [inst : Field K] [inst_1 : Algebra ℚ K]
      (a : V → Fin 3 → K),
      a root = 0 →
        Function.Injective a →
          IntermediateField.adjoin ℚ (Set.range fun x ↦ a x.1 x.2) = ⊤ →
            RB31E2E.DirectionStress.directionStressDim F a +
                Cardinal.toNat (Algebra.trdeg ℚ K) ≤
              Nat.card
                (RB31E2E.GroundedTwistSplit.SpatialVariable root)) :
  P.height = ↑(Finset.card F)

theorem RB31E2E.WittShearDistinctPrime.coefficientMinimalPrime_height_eq_edgeCard_of_groundedPF.{u,
    v}
  {V : Type u} {E : Type v} [Fintype V]
  [DecidableEq V] [DecidableEq E]
  (root : V) (src dst : E → V)
  (active : Finset E)
  (hLoop : ∀ e ∈ active, src e ≠ dst e)
  (F : RB31E2E.SimpleEdgeSet V)
  (hRepresented :
    ∀ f ∈ F,
      ∃ e,
        RB31E2E.SparseNullIncidence.activeEdge
            src dst active hLoop e =
          f)
  (chart :
    RB31E2E.UniversalHomogeneousChart.DistinctnessChart
      V)
  (P :
    Ideal
      (RB31E2E.PinOuterActiveHeight.TwistCoefficientRing
        root))
  [P.IsPrime]
  (hP :
    P ∈
      (RB31E2E.SelectedNullHeight.coefficientSelectedNullIdeal
          root src dst active
          (RB31E2E.SparseNullIncidence.selectedSkeletonOccurrences
            src dst active hLoop F
            hRepresented)).minimalPrimes)
  (hden :
    RB31E2E.PinOuterFullProvenanceHeightTransfer.coefficientDistinctnessDenominator
        root chart ∉
      P)
  (hPF :
    ∀ {K : Type u} [inst : Field K]
      [inst_1 : Algebra ℚ K]
      (a : V → Fin 3 → K),
      a root = 0 →
        Function.Injective a →
          IntermediateField.adjoin ℚ
                (Set.range fun x ↦
                  a x.1 x.2) =
              ⊤ →
            RB31E2E.DirectionStress.directionStressDim
                  F a +
                Cardinal.toNat
                  (Algebra.trdeg ℚ K) ≤
              Nat.card
                (RB31E2E.GroundedTwistSplit.SpatialVariable
                  root)) :
  P.height = ↑(Finset.card F)

A surviving minimal selected-null component has exactly one unit of
height per selected skeleton edge.

theoremdefined in RB31EndToEnd/NullCellule/SelectedNullHeight.lean

complete

theorem RB31E2E.SelectedNullHeight.coefficientMinimalPrime_height_le_selectedCard.{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)
  (selected : Finset ↥active)
  (P : Ideal (RB31E2E.PinOuterActiveHeight.TwistCoefficientRing root))
  (hP :
    P ∈
      (RB31E2E.SelectedNullHeight.coefficientSelectedNullIdeal root src
          dst active selected).minimalPrimes) :
  P.height ≤ ↑selected.card

theorem RB31E2E.SelectedNullHeight.coefficientMinimalPrime_height_le_selectedCard.{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)
  (selected : Finset ↥active)
  (P :
    Ideal
      (RB31E2E.PinOuterActiveHeight.TwistCoefficientRing
        root))
  (hP :
    P ∈
      (RB31E2E.SelectedNullHeight.coefficientSelectedNullIdeal
          root src dst active
          selected).minimalPrimes) :
  P.height ≤ ↑selected.card

Generalized Krull height theorem for a minimal prime of the literal
selected-null ideal.

theoremdefined in RB31EndToEnd/NullCellule/SelectedDirectionHeight.lean

complete

theorem RB31E2E.SelectedDirectionHeight.splitMinimalPrime_height_ge_edgeCard_of_groundedPF.{u,
    v}
  {V : Type u} {E : Type v} [Fintype V] [DecidableEq V] [DecidableEq E]
  (root : V) (src dst : E → V) (active : Finset E)
  (hLoop : ∀ e ∈ active, src e ≠ dst e) (F : RB31E2E.SimpleEdgeSet V)
  (hRepresented :
    ∀ f ∈ F,
      ∃ e,
        RB31E2E.SparseNullIncidence.activeEdge src dst active hLoop e =
          f)
  (P :
    Ideal
      (MvPolynomial (RB31E2E.GroundedTwistSplit.SpatialVariable root)
        (MvPolynomial (RB31E2E.GroundedTwistSplit.SpatialVariable root)
          ℚ)))
  [P.IsPrime]
  [(RB31E2E.PolynomialPrimeTrdegHeight.coefficientContraction
        P).IsPrime]
  (hP :
    P ∈
      (RB31E2E.SelectedDirectionFibre.splitSelectedNullIdeal root src
          dst active
          (RB31E2E.SparseNullIncidence.selectedSkeletonOccurrences src
            dst active hLoop F hRepresented)).minimalPrimes)
  (hInjective :
    Function.Injective
      (RB31E2E.SelectedDirectionFibre.quotientPlacement root
        (RB31E2E.PolynomialPrimeTrdegHeight.coefficientContraction P)))
  (hPF :
    ∀ {K : Type u} [inst : Field K] [inst_1 : Algebra ℚ K]
      (a : V → Fin 3 → K),
      a root = 0 →
        Function.Injective a →
          IntermediateField.adjoin ℚ (Set.range fun x ↦ a x.1 x.2) = ⊤ →
            RB31E2E.DirectionStress.directionStressDim F a +
                Cardinal.toNat (Algebra.trdeg ℚ K) ≤
              Nat.card
                (RB31E2E.GroundedTwistSplit.SpatialVariable root)) :
  ↑(Finset.card F) ≤ P.height

theorem RB31E2E.SelectedDirectionHeight.splitMinimalPrime_height_ge_edgeCard_of_groundedPF.{u,
    v}
  {V : Type u} {E : Type v} [Fintype V]
  [DecidableEq V] [DecidableEq E]
  (root : V) (src dst : E → V)
  (active : Finset E)
  (hLoop : ∀ e ∈ active, src e ≠ dst e)
  (F : RB31E2E.SimpleEdgeSet V)
  (hRepresented :
    ∀ f ∈ F,
      ∃ e,
        RB31E2E.SparseNullIncidence.activeEdge
            src dst active hLoop e =
          f)
  (P :
    Ideal
      (MvPolynomial
        (RB31E2E.GroundedTwistSplit.SpatialVariable
          root)
        (MvPolynomial
          (RB31E2E.GroundedTwistSplit.SpatialVariable
            root)
          ℚ)))
  [P.IsPrime]
  [(RB31E2E.PolynomialPrimeTrdegHeight.coefficientContraction
        P).IsPrime]
  (hP :
    P ∈
      (RB31E2E.SelectedDirectionFibre.splitSelectedNullIdeal
          root src dst active
          (RB31E2E.SparseNullIncidence.selectedSkeletonOccurrences
            src dst active hLoop F
            hRepresented)).minimalPrimes)
  (hInjective :
    Function.Injective
      (RB31E2E.SelectedDirectionFibre.quotientPlacement
        root
        (RB31E2E.PolynomialPrimeTrdegHeight.coefficientContraction
          P)))
  (hPF :
    ∀ {K : Type u} [inst : Field K]
      [inst_1 : Algebra ℚ K]
      (a : V → Fin 3 → K),
      a root = 0 →
        Function.Injective a →
          IntermediateField.adjoin ℚ
                (Set.range fun x ↦
                  a x.1 x.2) =
              ⊤ →
            RB31E2E.DirectionStress.directionStressDim
                  F a +
                Cardinal.toNat
                  (Algebra.trdeg ℚ K) ≤
              Nat.card
                (RB31E2E.GroundedTwistSplit.SpatialVariable
                  root)) :
  ↑(Finset.card F) ≤ P.height

A minimal component of the split selected-null system has the full edge
height once the grounded PF function-field inequality is available for all
coordinate-generated distinct placements.

theoremdefined in RB31EndToEnd/NullCellule/SelectedNullHeightPrimewise.lean

complete

theorem RB31E2E.SelectedNullHeightPrimewise.incidenceLocalizedSelectedNullIdealHeight_ge_selectedCard_of_groundedPF.{u,
    v}
  {V : Type u} {E : Type v} [Fintype V] [Fintype E] [DecidableEq V]
  [DecidableEq E] (root : V) (src dst : E → V) (active : Finset E)
  (hLoop : ∀ e ∈ active, src e ≠ dst e) (F : RB31E2E.SimpleEdgeSet V)
  (hRepresented :
    ∀ f ∈ F,
      ∃ e,
        RB31E2E.SparseNullIncidence.activeEdge src dst active hLoop e =
          f)
  (angularChart : ↥active → Fin 3)
  (distinctChart :
    RB31E2E.UniversalHomogeneousChart.DistinctnessChart V)
  (hPF :
    ∀ {K : Type u} [inst : Field K] [inst_1 : Algebra ℚ K]
      (a : V → Fin 3 → K),
      a root = 0 →
        Function.Injective a →
          IntermediateField.adjoin ℚ (Set.range fun x ↦ a x.1 x.2) = ⊤ →
            RB31E2E.DirectionStress.directionStressDim F a +
                Cardinal.toNat (Algebra.trdeg ℚ K) ≤
              Nat.card
                (RB31E2E.GroundedTwistSplit.SpatialVariable root)) :
  have selected :=
    RB31E2E.SparseNullIncidence.selectedSkeletonOccurrences src dst
      active hLoop F hRepresented;
  ↑selected.card ≤
    RB31E2E.PinOuterFullProvenanceHeightTransfer.incidenceLocalizedSelectedNullIdealHeight
      root src dst active angularChart selected distinctChart

theorem RB31E2E.SelectedNullHeightPrimewise.incidenceLocalizedSelectedNullIdealHeight_ge_selectedCard_of_groundedPF.{u,
    v}
  {V : Type u} {E : Type v} [Fintype V]
  [Fintype E] [DecidableEq V]
  [DecidableEq E] (root : V)
  (src dst : E → V) (active : Finset E)
  (hLoop : ∀ e ∈ active, src e ≠ dst e)
  (F : RB31E2E.SimpleEdgeSet V)
  (hRepresented :
    ∀ f ∈ F,
      ∃ e,
        RB31E2E.SparseNullIncidence.activeEdge
            src dst active hLoop e =
          f)
  (angularChart : ↥active → Fin 3)
  (distinctChart :
    RB31E2E.UniversalHomogeneousChart.DistinctnessChart
      V)
  (hPF :
    ∀ {K : Type u} [inst : Field K]
      [inst_1 : Algebra ℚ K]
      (a : V → Fin 3 → K),
      a root = 0 →
        Function.Injective a →
          IntermediateField.adjoin ℚ
                (Set.range fun x ↦
                  a x.1 x.2) =
              ⊤ →
            RB31E2E.DirectionStress.directionStressDim
                  F a +
                Cardinal.toNat
                  (Algebra.trdeg ℚ K) ≤
              Nat.card
                (RB31E2E.GroundedTwistSplit.SpatialVariable
                  root)) :
  have selected :=
    RB31E2E.SparseNullIncidence.selectedSkeletonOccurrences
      src dst active hLoop F hRepresented;
  ↑selected.card ≤
    RB31E2E.PinOuterFullProvenanceHeightTransfer.incidenceLocalizedSelectedNullIdealHeight
      root src dst active angularChart
      selected distinctChart

The selected-null localized lower-height bound required by the incidence
transfer follows directly from grounded PF semismallness.  No
`SurvivingSelectedFunctionFieldBudget`, selected-null height, or generic
fibre identity is a premise.

Proof for Theorem 7.5.1

Proof uses 3

Proof dependency previews

Preview

Lemma 6.3.1

Loading preview

Proof dependency preview content is loaded from the Blueprint HTML cache.

Fix the minimal prime P and its component Z = V(P). First apply the Witt shear of Z: the coordinate change a = b + S_Z \omega preserves every generator, so it takes P to a minimal prime P' of I_F of the same height, and the configuration a is pairwise distinct in \operatorname{Frac}(R/P'). Second, contract to the coefficient ring: write R \cong A[\omega] with A = k[a_{v,i} : v \ne o], set \mathfrak{p} = P' \cap A and K = \operatorname{Frac}(A/\mathfrak{p}), so that K is generated by the coordinates of a and the configuration stays pairwise distinct in K^3. With s = \dim_K \ker D_F(a)^T and r = \operatorname{rank}_K D_F(a), the matrix has m rows, so r + s = m; the dimension formula gives \operatorname{ht} \mathfrak{p} + \trdeg_k K = 3n_0, and the grounded inequality (4.7) gives s + \trdeg_k K \le 3n_0, so s \le \operatorname{ht} \mathfrak{p}. Third, pass to the generic fibre over K: substituting y = \omega in the motion equations shows the fibre of P' is the prime linear ideal L_F generated by the rows of D_{F,o}(a), of height r, and minimality of P' forces the fibre to equal L_F. The relative height equality for \mathfrak{p} \subseteq P' then gives \operatorname{ht} P' = \operatorname{ht} \mathfrak{p} + \operatorname{ht} L_F \ge s + r = m, while P' is a minimal prime of an ideal with m generators, so Krull's height theorem gives \operatorname{ht} P' \le m.

The formal route has the same three steps, with the lower bound as its only conclusion. The shear step is exists_splitMinimalPrime_with_injective_placement: one rational shear parameter, produced by the common-shear lemma applied to the pairwise differences in the function field, turns P into an equal-height minimal prime whose induced placement a : V \to K^3 is injective. The contraction and fibre steps run through the angular/translational split of the ambient ring recorded on the grounded-model node: splitSelectedNullIdeal_eq_linearFormIdealOver identifies the transported ideal with the linear-form ideal of the grounded direction rows — the paper's L_F — over the translational coefficient ring; polynomialPrime_height_eq_contractionHeight_add_fractionFibreHeight is the relative height equality \operatorname{ht} P' = \operatorname{ht} \mathfrak{p} + \operatorname{ht} L_F; finrank_span_le_linearFormIdeal_height bounds \operatorname{ht} L_F below by the rank r; the grounded inequality, supplied as the semismallness hypothesis, bounds \operatorname{ht} \mathfrak{p} below by s; and rank–nullity closes with s + r = |E_F|. The composite is splitMinimalPrime_height_ge_edgeCard_of_groundedPF, and incidenceLocalizedSelectedNullIdealHeight_ge_selectedCard_of_groundedPF transports the bound through the two localizations and the adjunction of the retained pin variables into the form the assembly of the next chapter reads. The equality of Theorem 1.3 is proved too. coefficientMinimalPrime_height_le_selectedCard is the generalized Krull height theorem applied to the selected generators: a minimal prime of an ideal generated by m elements has height at most m, and the selected occurrences number |E_F|. Combining it with the lower bound, coefficientMinimalPrime_height_eq_edgeCard_of_groundedPF gives \operatorname{ht} P = |E_F| outright. Proposition 6.5 still reads only the lower bound, so the equality is stated and proved without the assembly depending on it. What remains between the paper's theorem and this one is the ambient ring, and the register records it.