7.2. The ideal and the distinct locus
Fix a root o \in V and set X_o = 0. In the polynomial ring
R = k[\omega_{v,i}, b_{v,i} : v \ne o,\ 1 \le i \le 3], the Split–Klein
isotropic difference ideal of a simple graph F = (V, E_F) is
I_F = \bigl(f_{uv} : uv \in E_F\bigr), \qquad
f_{uv} = q(X_u - X_v) = (\omega_u - \omega_v) \cdot (b_u - b_v),
and the distinct locus U_{\mathrm{dist}} \subseteq \operatorname{Spec} R
is the open complement of the diagonal closed subsets
\{X_u = X_v\} over the pairs u \ne v.
(Zheng, 2026, Equation 1.6 and 5.2)
Lean code for Definition7.2.1●2 definitions
Associated Lean declarations
-
defdefined in RB31EndToEnd/NullCellule/PolynomialModel.leancomplete
def RB31E2E.NullCellulePolynomial.edgeIdeal.{u_1, u_2} {k : Type u_1} {V : Type u_2} [CommRing k] (F : RB31E2E.SimpleEdgeSet V) : Ideal (MvPolynomial (RB31E2E.NullCellulePolynomial.TwistVariable V) k)
def RB31E2E.NullCellulePolynomial.edgeIdeal.{u_1, u_2} {k : Type u_1} {V : Type u_2} [CommRing k] (F : RB31E2E.SimpleEdgeSet V) : Ideal (MvPolynomial (RB31E2E.NullCellulePolynomial.TwistVariable V) k)
The ideal generated by the selected edge quadrics.
-
defdefined in RB31EndToEnd/NullCellule/SelectedNullHeight.leancomplete
def RB31E2E.SelectedNullHeight.coefficientSelectedNullIdeal.{u_1, u_2} {V : Type u_1} {E : Type u_2} [DecidableEq V] [DecidableEq E] (root : V) (src dst : E → V) (active : Finset E) (selected : Finset ↥active) : Ideal (RB31E2E.PinOuterActiveHeight.TwistCoefficientRing root)
def RB31E2E.SelectedNullHeight.coefficientSelectedNullIdeal.{u_1, u_2} {V : Type u_1} {E : Type u_2} [DecidableEq V] [DecidableEq E] (root : V) (src dst : E → V) (active : Finset E) (selected : Finset ↥active) : Ideal (RB31E2E.PinOuterActiveHeight.TwistCoefficientRing root)
The selected null ideal in the literal grounded twist polynomial ring.
The formalization contains two builds of this ideal, and only one of them is
used by the root theorem; the deviation register has the entry. The literal
build, in PolynomialModel.lean, takes six variables at every
vertex, spans the ideal by one orientation-independent quadric per edge, and
proves that its zero locus is exactly the null-difference condition on twist
assignments; the module family's own name for the pair of conditions —
pairwise distinct, and null on every selected edge — is the null cellule,
a name this blueprint has not checked against a primary source.
/-- Membership in the distinct null-difference cellule. -/
def InNullCellule (F : SimpleEdgeSet V) (X : V → Twist k) : Prop :=
IsDistinctConfiguration X ∧ IsNullDifferenceConfiguration F X/-- The orientation-independent Split--Klein quadratic attached to an edge. -/
def edgePolynomial {k V : Type*} [CommRing k]
(e : SimpleEdge V) : MvPolynomial (TwistVariable V) k :=
Sym2.lift ⟨fun u v ↦
Twist.splitKlein (universalTwist u - universalTwist v), k:Type u_1V:Type u_2inst✝:CommRing ke:SimpleEdge V⊢ ∀ (a₁ a₂ : V),
(fun u v => (universalTwist u - universalTwist v).splitKlein) a₁ a₂ =
(fun u v => (universalTwist u - universalTwist v).splitKlein) a₂ a₁
intro u k:Type u_1V:Type u_2inst✝:CommRing ke:SimpleEdge Vu:Vv:V⊢ (fun u v => (universalTwist u - universalTwist v).splitKlein) u v =
(fun u v => (universalTwist u - universalTwist v).splitKlein) v u
All goals completed! 🐙⟩ e.1/-- The ideal generated by the selected edge quadrics. -/
def edgeIdeal {k V : Type*} [CommRing k]
(F : SimpleEdgeSet V) : Ideal (MvPolynomial (TwistVariable V) k) :=
Ideal.span
(edgePolynomial (k := k) '' (F : Set (SimpleEdge V)))
The build the assembly uses is grounded and provenance-labelled. Its ambient
ring has six variables per non-root vertex over \Q, exactly the paper's
R with k = \Q; the root twist is the constant zero rather than a
variable, so grounding is a property of the ring and never has to be imposed
on an ideal. Each generator is the Split–Klein quadric of the relative twist
across one selected pin occurrence:
/-- One selected Split--Klein null equation before either localization and
before any retained pin variables are adjoined. -/
def coefficientNullEquation
{V E : Type*} [DecidableEq V]
(root : V) (src dst : E → V) (e : E) :
TwistCoefficientRing root :=
Twist.splitKlein (coefficientRelativeTwist root src dst e)/-- The selected null ideal in the literal grounded twist polynomial ring. -/
def coefficientSelectedNullIdeal
{V E : Type*} [DecidableEq V] [DecidableEq E]
(root : V) (src dst : E → V) (active : Finset E)
(selected : Finset active) : Ideal (TwistCoefficientRing root) :=
Ideal.span (Set.range (fun e : SelectedOccurrence active selected ↦
coefficientNullEquation root src dst e.1.1))
The distinct locus is likewise handled by element rather than by open set:
for each ordered pair of distinct vertices a distinctness chart picks one
of the six coordinates of the twist difference, the product of the chosen
coordinates over all pairs is a single denominator polynomial, and "the
component of P meets U_{\mathrm{dist}}" is the condition that this
denominator not lie in P. On such a component
mapped_pairDifference_ne_zero
shows every pairwise twist difference is nonzero in the function field
\operatorname{Frac}(R/P), which is the form of "meets the open set" used
in the proofs.