8.4. Exceptional pin parameters
From here the paper takes k = \C: the pin parameter space is
P_{\mathrm{pin}} = (\C^3)^E of dimension 3N with N = |E|, and for a
fixed partition \mathcal{P} of the bodies the incidence variety
I_{\mathcal{P}} consists of the grounded, pairwise distinct block twists
together with pin coordinates satisfying every compatibility equation, with
\pi_{\mathcal{P}} : I_{\mathcal{P}} \to P_{\mathrm{pin}} the projection
that forgets the twists.
Proposition 6.5: suppose H satisfies the partition inequality (1.2). For
every partition \mathcal{P} of the bodies with t \ge 2 blocks, the
closure of \pi_{\mathcal{P}}(I_{\mathcal{P}}) is a proper closed subset
of P_{\mathrm{pin}}.
(Zheng, 2026, Proposition 6.5)
Lean code for Lemma8.4.1●3 declarations
Associated Lean declarations
-
defdefined in RB31EndToEnd/Incidence/SmallBundleCertificate.leancomplete
def RB31E2E.SparseNullIncidence.PropernessPrinciple : Prop
def RB31E2E.SparseNullIncidence.PropernessPrinciple : Prop
For any finite provenance-labelled occurrence system, a sparse null skeleton of the exact dimension-budget cardinality forces the image of the distinct incidence locus to lie in a proper integer hypersurface of the pin coordinate space. Inactive occurrences are deliberately retained in the ambient polynomial ring; the resulting polynomial may ignore them, but its nonvanishing is asserted in the full provenance-labelled ring. This proposition contains no body--pin graph, partition, or rigidity predicate.
-
theoremdefined in RB31EndToEnd/Incidence/SmallBundleCertificate.leancomplete
theorem RB31E2E.BodyPinIncidence.hasOnlySmallBundlesAt_or_tripleBundlePartitionCertificate (H : RB31E2E.BodyPinIncidence) (P : H.EqualityPartitionIndex) : H.HasOnlySmallBundlesAt P ∨ Nonempty (H.TripleBundlePartitionCertificate P)
theorem RB31E2E.BodyPinIncidence.hasOnlySmallBundlesAt_or_tripleBundlePartitionCertificate (H : RB31E2E.BodyPinIncidence) (P : H.EqualityPartitionIndex) : H.HasOnlySmallBundlesAt P ∨ Nonempty (H.TripleBundlePartitionCertificate P)
The small/triple dichotomy is exhaustive at the occurrence level. If a fine crossing bundle is not small, its filtered occurrence fibre contains three pairwise distinct pins, which retain enough provenance to build the already verified triple-bundle certificate.
-
theoremdefined in RB31EndToEnd/Incidence/SmallBundleCertificate.leancomplete
theorem RB31E2E.BodyPinIncidence.exists_smallBundlePartitionPolynomial (H : RB31E2E.BodyPinIncidence) (P : H.EqualityPartitionIndex) (hPartition : H.PartitionCondition) (hSmall : H.HasOnlySmallBundlesAt P) (hProper : RB31E2E.SparseNullIncidence.PropernessPrinciple) : ∃ Q, Q ≠ 0 ∧ ∀ (p : H.Pin → RB31E2E.Vec3 ℝ) (X : H.Body → RB31E2E.Twist ℝ), H.ExactBadMotionAt P p X → MvPolynomial.eval₂ (Int.castRingHom ℝ) (RB31E2E.GroundedTwistPolynomial.assignmentOfPins p) Q = 0
theorem RB31E2E.BodyPinIncidence.exists_smallBundlePartitionPolynomial (H : RB31E2E.BodyPinIncidence) (P : H.EqualityPartitionIndex) (hPartition : H.PartitionCondition) (hSmall : H.HasOnlySmallBundlesAt P) (hProper : RB31E2E.SparseNullIncidence.PropernessPrinciple) : ∃ Q, Q ≠ 0 ∧ ∀ (p : H.Pin → RB31E2E.Vec3 ℝ) (X : H.Body → RB31E2E.Twist ℝ), H.ExactBadMotionAt P p X → MvPolynomial.eval₂ (Int.castRingHom ℝ) (RB31E2E.GroundedTwistPolynomial.assignmentOfPins p) Q = 0
For one fixed small-bundle equality partition, the universal sparse null-incidence properness principle constructs the exact nonzero integer polynomial required by `FiniteBadCover`. The empty-stratum case uses the constant polynomial `1`. In the nonempty case, non-diagonality supplies at least two blocks, and all other hypotheses of the properness principle are proved from the partition condition and the literal occurrence data.
Case 1: some pair of blocks is joined by three or more pins. Their relative
twist is nonzero by the definition of the partition, so by the pin-fibre
lemma any three of those pin points are collinear, and collinear triples
form a proper closed subset of (\C^3)^3 cut out by the coordinates of a
cross product; its preimage under the projection to the three pins contains
\pi_{\mathcal{P}}(I_{\mathcal{P}}).
Case 2: every pair is joined by at most two pins. Choose by Lemma 6.3 a
spanning (2,2)-sparse subgraph F with R edges and one
representative pin per edge. The compatibility equation of a representative
pin gives the Split–Klein isotropic-difference equation of its edge, and the
block twists are pairwise distinct, so by
Corollary 5.4 — formally, by the grounded
height theorem it restates — the twist tuples
have dimension at most 6(t-1) - R once one twist is fixed. Each of the
M cross-block pins then adds at most one dimension, since a nonempty pin
fibre is an affine line, and each of the N - M within-block pins has zero
relative twist and adds three; hence
\dim I_{\mathcal{P}} \le 6(t-1) - R + M + 3(N - M). The scaling action is
free on I_{\mathcal{P}} and \pi_{\mathcal{P}} is constant on orbits,
so the orbit drop gives
\dim \pi_{\mathcal{P}}(I_{\mathcal{P}}) \le 3N + (6(t-1) - 2M - R) - 1
\le 3N - 1, since R \ge 6(t-1) - 2M.
The formalization states properness as a certificate. The universal form is a single proposition with no body–pin vocabulary in it:
/-- Point-set incidence semantics used by the elimination statement. The
vertex twists must be pairwise distinct, and every selected occurrence is a
zero of its nonzero relative twist. -/
def IsIncidenceRealization {V E : Type*} [DecidableEq E]
(src dst : E → V) (active : Finset E)
(p : E → Vec3 ℝ) (Y : V → Twist ℝ) : Prop :=
Function.Injective Y ∧
∀ e : active,
Twist.eval (Y (src e.1) - Y (dst e.1)) (p e.1) = 0/--
For any finite provenance-labelled occurrence system, a sparse null
skeleton of the exact dimension-budget cardinality forces the image of the
distinct incidence locus to lie in a proper integer hypersurface of the pin
coordinate space. Inactive occurrences are deliberately retained in the
ambient polynomial ring; the resulting polynomial may ignore them, but its
nonvanishing is asserted in the full provenance-labelled ring.
This proposition contains no body--pin graph, partition, or rigidity
predicate.
-/
def PropernessPrinciple : Prop :=
∀ (V E : Type) [Fintype V] [DecidableEq V]
[Fintype E] [DecidableEq E]
(src dst : E → V) (active : Finset E)
(hLoop : ∀ e ∈ active, src e ≠ dst e)
(F : SimpleEdgeSet V),
2 ≤ Fintype.card V →
Sparse22 F →
(∀ f ∈ F, ∃ e : active,
activeEdge src dst active hLoop e = f) →
F.card = 6 * (Fintype.card V - 1) - 2 * active.card →
∃ Q : MvPolynomial (GroundedTwistPolynomial.PinVariable E) ℤ,
Q ≠ 0 ∧
∀ (p : E → Vec3 ℝ) (Y : V → Twist ℝ),
IsIncidenceRealization src dst active p Y →
MvPolynomial.eval₂ (Int.castRingHom ℝ)
(GroundedTwistPolynomial.assignmentOfPins p) Q = 0
A realization is a pairwise distinct twist assignment satisfying the
selected occurrence equations, and the principle asserts one nonzero integer
polynomial Q in the pin variables vanishing at every real realization,
whenever the selected edges form a sparse graph of exactly the budget
cardinality 6(|V|-1) - 2|\mathrm{active}|. The paper's two cases appear
as a dichotomy at the occurrence level,
hasOnlySmallBundlesAt_or_tripleBundlePartitionCertificate:
either every crossing bundle of the partition has at most two pins, or some
bundle's fibre holds three pairwise distinct pins.
In the triple case the certificate is written down directly, as the
2 \times 2 minor asserting collinearity of three pin points:
/-- One `2×2` minor of the two displacement vectors from `e₀`. -/
def minor01 {E : Type*} (e₀ e₁ e₂ : E) :
MvPolynomial (Variable E) ℤ :=
(coordinate e₁ 0 - coordinate e₀ 0) *
(coordinate e₂ 1 - coordinate e₀ 1) -
(coordinate e₁ 1 - coordinate e₀ 1) *
(coordinate e₂ 0 - coordinate e₀ 0)
By the pin-fibre lemma a nonzero common twist forces
the minor to vanish, and the minor is a nonzero polynomial because the three
occurrence labels are distinct — the witness is the explicit assignment
sending the three pins to 0, e_1, e_2 — so distinctness of provenance
labels, not genericity, gives Q \ne 0. In the small-bundle case
exists_smallBundlePartitionPolynomial
applies the properness principle: the selection lemma above gives the
sparse skeleton at the budget cardinality, and the principle itself is
discharged by the chart layer of the closing section, whose height input is
the theorem of the Split–Klein chapter and
whose dimension bookkeeping (the fibre count and the orbit drop of the
paper's Case 2) is carried out as height accounting in a graded polynomial
ring rather than as dimensions of varieties.