Body-Pin Rigidity

7.7.Β Weights and initial idealsπŸ”—

Lemma7.7.1
uses 1used by 0βœ“Lβˆƒβˆ€N
Tagslean-only

Provenance weights on the twist variables, the minimum-weight initial component of a polynomial, the resulting weight-initial ideal, and exact weight-layer decompositions of the replaced equations for an edge-to-K_3 and a vertex-to-K_4 move. A height-comparison interface between an ideal and its weight-initial ideal is stated as a proposition and neither assumed nor proved anywhere in the development.

Lean code for Lemma7.7.1●2 definitions
  • defdefined in RB31EndToEnd/NullCellule/WeightInitialIdeal.lean
    complete
    def RB31E2E.NullCellulePolynomial.weightInitialIdeal.{u_1, u_2}
  {k : Type u_1} {Οƒ : Type u_2} [CommRing k] (w : Οƒ β†’ β„•)
  (I : Ideal (MvPolynomial Οƒ k)) : Ideal (MvPolynomial Οƒ k)
    def RB31E2E.NullCellulePolynomial.weightInitialIdeal.{u_1,
    u_2}
  {k : Type u_1} {Οƒ : Type u_2}
  [CommRing k] (w : Οƒ β†’ β„•)
  (I : Ideal (MvPolynomial Οƒ k)) :
  Ideal (MvPolynomial Οƒ k)
    The minimum-weight initial ideal, generated by initial components of
actual elements of `I`.
  • defdefined in RB31EndToEnd/Algebra/FilteredInitialHeight.lean
    complete
    def RB31E2E.NullCellulePolynomial.WeightInitialHeightMonotone.{u_1, u_2}
  {k : Type u_1} {Οƒ : Type u_2} [CommRing k] : Prop
    def RB31E2E.NullCellulePolynomial.WeightInitialHeightMonotone.{u_1,
    u_2}
  {k : Type u_1} {Οƒ : Type u_2}
  [CommRing k] : Prop
    Height monotonicity from a weighted initial ideal to its source ideal.

Four NullCellule modules and part of a fifth develop a degeneration apparatus with no paper counterpart: variables are weighted by provenance, the minimum nonzero weighted-homogeneous component of a polynomial is singled out, and for two replacement moves β€” an edge replaced by a K_3 and a vertex replaced by a K_4 β€” the exact weight-zero, -one and -two layers of every replaced Split–Klein equation are computed, over \Q, together with the identity that the weight-zero layer of a replaced equation is the original equation.

/-- `g` is the minimum nonzero `w`-weighted homogeneous component of `f`. The witnessing degree is retained, while all strictly smaller natural-number components are required to vanish. -/ def IsInitialComponent (w : Οƒ β†’ β„•) (f g : MvPolynomial Οƒ k) : Prop := βˆƒ d : β„•, weightedHomogeneousComponent w d f = g ∧ g β‰  0 ∧ βˆ€ e < d, weightedHomogeneousComponent w e f = 0/-- The minimum-weight initial ideal, generated by initial components of actual elements of `I`. -/ def weightInitialIdeal (w : Οƒ β†’ β„•) (I : Ideal (MvPolynomial Οƒ k)) : Ideal (MvPolynomial Οƒ k) := Ideal.span {g | βˆƒ f ∈ I, IsInitialComponent w f g}/-- Height monotonicity from a weighted initial ideal to its source ideal. -/ def WeightInitialHeightMonotone : Prop := βˆ€ (w : Οƒ β†’ β„•) (I : Ideal (MvPolynomial Οƒ k)), (weightInitialIdeal w I).height ≀ I.height

The last quoted definition is the reason the apparatus ends where it does. FilteredInitialHeight.lean states the height comparison \operatorname{ht}(\operatorname{in}_w I) \le \operatorname{ht} I as a named proposition and proves the parts of the bridge that follow from the graded decomposition alone; its own comment records that Mathlib's Rees algebra currently covers powers of a single ideal and not the flat one-parameter family of an arbitrary weight filtration, and the proposition is never assumed and never discharged. None of the weight modules is reachable from the root theorem β€” 157 declarations across the four pure weight modules reach it not at all β€” so the apparatus is a parallel development, like the construction theorem of the sparsity chapter; the module-by-module accounting appears in the correspondence chapter. What the root theorem does take from these files is vocabulary: the coordinate-ideal block of FilteredInitialHeight.lean, whose prime-chain height bound the linear-form ideal height of the theorem above rests on.