5.4. Private support vertices and missing-edge pivots
Suppose the selected vertex v is a private support vertex, with unique
triple T_\gamma = \{v, p, q\}. The three possible rigidity rows on three
distinct collinear points span the same two-dimensional space —
the observation of Example 2.2 — so the
distinguished missing edge can be moved to an edge incident with v
without changing the completion or the row space. The vertex v and the
flag \gamma are then deleted together, and the retained field L,
configuration a_H, and local numbers u, \delta_v of
the deletion chapter apply verbatim.
Flag collinearity places a_v on the line through a_p and a_q, which
is defined over L, so \delta_v \le 1 at a private support vertex.
After possibly interchanging p and q, and if necessary exchanging one
base-graph edge with the distinguished missing edge, we may arrange that
d_\gamma = vq while vp, pq \in E(G). The exchange leaves the
simultaneous completion, the row space \operatorname{row} D_G(a), and the
self-stress dimension unchanged, and does not increase \deg_G(v).
(Zheng, 2026, Lemma 3.5)
Lean code for Lemma5.4.1●3 declarations
Associated Lean declarations
-
complete
def RB31E2E.ProvenanceFlag.State.pivotPrivateOpposite.{u_1, u_2} {V : Type u_1} {Flag : Type u_2} [Fintype V] [DecidableEq V] [Fintype Flag] [DecidableEq Flag] (S : RB31E2E.ProvenanceFlag.State V Flag) (hSparse : S.CompletionSparse) (v p q : V) (t : Flag) (hvp : v ≠ p) (hvq : v ≠ q) (hpq : p ≠ q) (hOne : S.flagMultiplicity v = 1) (hvt : v ∈ S.terminals t) (hTerminals : S.terminals t = {v, p, q}) (hMissing : S.missing t = RB31E2E.simpleEdge p q hpq) : RB31E2E.ProvenanceFlag.State V Flag
def RB31E2E.ProvenanceFlag.State.pivotPrivateOpposite.{u_1, u_2} {V : Type u_1} {Flag : Type u_2} [Fintype V] [DecidableEq V] [Fintype Flag] [DecidableEq Flag] (S : RB31E2E.ProvenanceFlag.State V Flag) (hSparse : S.CompletionSparse) (v p q : V) (t : Flag) (hvp : v ≠ p) (hvq : v ≠ q) (hpq : p ≠ q) (hOne : S.flagMultiplicity v = 1) (hvt : v ∈ S.terminals t) (hTerminals : S.terminals t = {v, p, q}) (hMissing : S.missing t = RB31E2E.simpleEdge p q hpq) : RB31E2E.ProvenanceFlag.State V Flag
Exchange the opposite missing edge `pq` with the incident edge `vq`. The hypotheses describe only facts derivable from the old literal state.
-
theoremdefined in RB31EndToEnd/Combinatorics/ProvenanceFlagPrivatePivot.leancomplete
theorem RB31E2E.ProvenanceFlag.State.exists_privatePivotData.{u_1, u_2} {V : Type u_1} {Flag : Type u_2} [Fintype V] [DecidableEq V] [Fintype Flag] [DecidableEq Flag] (S : RB31E2E.ProvenanceFlag.State V Flag) (hSparse : S.CompletionSparse) (v : V) (t : Flag) (hOne : S.flagMultiplicity v = 1) (hvt : v ∈ S.terminals t) : Nonempty (RB31E2E.ProvenanceFlag.PrivatePivotData S hSparse v t hOne hvt)
theorem RB31E2E.ProvenanceFlag.State.exists_privatePivotData.{u_1, u_2} {V : Type u_1} {Flag : Type u_2} [Fintype V] [DecidableEq V] [Fintype Flag] [DecidableEq Flag] (S : RB31E2E.ProvenanceFlag.State V Flag) (hSparse : S.CompletionSparse) (v : V) (t : Flag) (hOne : S.flagMultiplicity v = 1) (hvt : v ∈ S.terminals t) : Nonempty (RB31E2E.ProvenanceFlag.PrivatePivotData S hSparse v t hOne hvt)
Every private terminal admits an orientation in which the distinguished missing edge meets `v`. If the old missing edge is already incident to `v`, this only renames endpoints; if it is opposite `v`, the returned state is `pivotPrivateOpposite`.
-
theoremdefined in RB31EndToEnd/Linear/PrivatePivotStress.leancomplete
theorem RB31E2E.DirectionStress.directionStressDim_exchange_collinear_triangle.{u, w} {K : Type u} {V : Type w} [Field K] [Fintype V] [DecidableEq V] (F : RB31E2E.SimpleEdgeSet V) (pos : V → Fin 3 → K) (x y z : V) (hxy : x ≠ y) (hxz : x ≠ z) (hyz : y ≠ z) (hxyMem : RB31E2E.simpleEdge x y hxy ∈ F) (hxzMem : RB31E2E.simpleEdge x z hxz ∈ F) (hyzNotMem : RB31E2E.simpleEdge y z hyz ∉ F) (hpos : Function.Injective pos) (hcol : RB31E2E.PinCollinearity.Collinear (pos x) (pos y) (pos z)) : RB31E2E.DirectionStress.directionStressDim (insert (RB31E2E.simpleEdge y z hyz) (Finset.erase F (RB31E2E.simpleEdge x z hxz))) pos = RB31E2E.DirectionStress.directionStressDim F pos
theorem RB31E2E.DirectionStress.directionStressDim_exchange_collinear_triangle.{u, w} {K : Type u} {V : Type w} [Field K] [Fintype V] [DecidableEq V] (F : RB31E2E.SimpleEdgeSet V) (pos : V → Fin 3 → K) (x y z : V) (hxy : x ≠ y) (hxz : x ≠ z) (hyz : y ≠ z) (hxyMem : RB31E2E.simpleEdge x y hxy ∈ F) (hxzMem : RB31E2E.simpleEdge x z hxz ∈ F) (hyzNotMem : RB31E2E.simpleEdge y z hyz ∉ F) (hpos : Function.Injective pos) (hcol : RB31E2E.PinCollinearity.Collinear (pos x) (pos y) (pos z)) : RB31E2E.DirectionStress.directionStressDim (insert (RB31E2E.simpleEdge y z hyz) (Finset.erase F (RB31E2E.simpleEdge x z hxz))) pos = RB31E2E.DirectionStress.directionStressDim F pos
Stress dimension is invariant under a collinear terminal-edge pivot.
The pivot has a combinatorial and a linear half, and the formalization keeps
them in separate modules. The combinatorial half is the state constructor
pivotPrivateOpposite,
which applies when the old missing edge pq is opposite v: it inserts
pq into the live edges, erases vq, and redeclares the missing edge of
the flag to be vq. The live edge set and the restored-missing packet
swap one edge each, so the completion is literally unchanged
(pivotPrivateOpposite_completionEdges),
and sparsity with it.
/-- Exchange the opposite missing edge `pq` with the incident edge `vq`.
The hypotheses describe only facts derivable from the old literal state. -/
def State.pivotPrivateOpposite
(S : State V Flag) (hSparse : S.CompletionSparse)
(v p q : V) (t : Flag)
(hvp : v ≠ p) (hvq : v ≠ q) (hpq : p ≠ q)
(hOne : S.flagMultiplicity v = 1) (hvt : v ∈ S.terminals t)
(hTerminals : S.terminals t = {v, p, q})
(hMissing : S.missing t = simpleEdge p q hpq) :
State V Flag where
edges := insert (simpleEdge p q hpq) (S.edges.erase (simpleEdge v q hvq))
terminals := S.terminals
missing u := if h : u = t then simpleEdge v q hvq else S.missing u
terminals_card := ⋯
missing_supported u := ⋯
missing_not_live u := ⋯
other_terminal_edges_live u e heT heMissingNew := ⋯
The linear half is
directionStressDim_exchange_collinear_triangle:
on three distinct collinear placed points, each triangle direction row lies
in the span of the other two, so exchanging one live terminal edge for the
missing one preserves the row space, and rank–nullity turns the unchanged
rank and edge count into an unchanged stress dimension.
exists_privatePivotData
states both halves at once: every private terminal admits an orientation
with d_\gamma incident to v, obtained either by renaming p and q
or by the pivot above, together with the facts about the pivoted state that
are used in the private case of the induction.
In the pivoted shape, if \deg_G(v) \le 2, then either the local increment
satisfies u + \delta_v \le 1, or
\delta_v = 1, u = 1, \deg_G(v) = 2,
\operatorname{rank} C_v = 1, \dim_K \ker C_v = 1 and
\ker \partial_v = \ker C_v; in the second case the base-graph edge vz
other than vp has p, q, z pairwise distinct with collinear
configuration points, and
r_{pz}(a_H), r_{qz}(a_H) \in \operatorname{row}_L D_H(a_H).
(Zheng, 2026, Lemma 3.6)
Lean code for Lemma5.4.2●3 theorems
Associated Lean declarations
-
theoremdefined in RB31EndToEnd/Linear/PrivateLocalClassification.leancomplete
theorem RB31E2E.DirectionStress.private_nonexceptional_or_exceptional.{u, v, w} {k : Type u} {K : Type v} {V : Type w} [Field k] [Field K] [Algebra k K] [DecidableEq V] (F : RB31E2E.SimpleEdgeSet V) (pos : V → Fin 3 → K) (v : V) : RB31E2E.DirectionStress.PrivateNonexceptional F pos v ∨ RB31E2E.DirectionStress.PrivateExceptional F pos v
theorem RB31E2E.DirectionStress.private_nonexceptional_or_exceptional.{u, v, w} {k : Type u} {K : Type v} {V : Type w} [Field k] [Field K] [Algebra k K] [DecidableEq V] (F : RB31E2E.SimpleEdgeSet V) (pos : V → Fin 3 → K) (v : V) : RB31E2E.DirectionStress.PrivateNonexceptional F pos v ∨ RB31E2E.DirectionStress.PrivateExceptional F pos v
-
theoremdefined in RB31EndToEnd/Linear/PrivateLocalClassification.leancomplete
theorem RB31E2E.DirectionStress.privateExceptional_classification.{u, v, w} {k : Type u} {K : Type v} {V : Type w} [Field k] [Field K] [Algebra k K] [Fintype V] [DecidableEq V] (F : RB31E2E.SimpleEdgeSet V) (pos : V → Fin 3 → K) (v p q : V) (hvp : v ≠ p) (hvq : v ≠ q) (hpq : p ≠ q) (hvpMem : RB31E2E.simpleEdge v p hvp ∈ F) (hvqNotMem : RB31E2E.simpleEdge v q hvq ∉ F) (hDegree : RB31E2E.edgeSetDegree F v ≤ 2) (hpos : Function.Injective pos) (hcol : RB31E2E.PinCollinearity.Collinear (pos v) (pos p) (pos q)) (hgen : IntermediateField.adjoin k (Set.range fun c ↦ pos c.1 c.2) = ⊤) (hExceptional : RB31E2E.DirectionStress.PrivateExceptional F pos v) : ∃ N, q ≠ N.z ∧ RB31E2E.PinCollinearity.Collinear (pos v) (pos p) (pos N.z) ∧ RB31E2E.DirectionStress.outsideExtensionTrdeg pos v = 1 ∧ RB31E2E.DirectionStress.outsideResponseKernelDim F pos v = 1 ∧ RB31E2E.DirectionStress.outsideLocalKernelDim F pos v = 1 ∧ RB31E2E.DirectionStress.outsideLocalRank F pos v = 1 ∧ RB31E2E.edgeSetDegree F v = 2 ∧ RB31E2E.DirectionStress.deletedConnectingClass F pos v = 0
theorem RB31E2E.DirectionStress.privateExceptional_classification.{u, v, w} {k : Type u} {K : Type v} {V : Type w} [Field k] [Field K] [Algebra k K] [Fintype V] [DecidableEq V] (F : RB31E2E.SimpleEdgeSet V) (pos : V → Fin 3 → K) (v p q : V) (hvp : v ≠ p) (hvq : v ≠ q) (hpq : p ≠ q) (hvpMem : RB31E2E.simpleEdge v p hvp ∈ F) (hvqNotMem : RB31E2E.simpleEdge v q hvq ∉ F) (hDegree : RB31E2E.edgeSetDegree F v ≤ 2) (hpos : Function.Injective pos) (hcol : RB31E2E.PinCollinearity.Collinear (pos v) (pos p) (pos q)) (hgen : IntermediateField.adjoin k (Set.range fun c ↦ pos c.1 c.2) = ⊤) (hExceptional : RB31E2E.DirectionStress.PrivateExceptional F pos v) : ∃ N, q ≠ N.z ∧ RB31E2E.PinCollinearity.Collinear (pos v) (pos p) (pos N.z) ∧ RB31E2E.DirectionStress.outsideExtensionTrdeg pos v = 1 ∧ RB31E2E.DirectionStress.outsideResponseKernelDim F pos v = 1 ∧ RB31E2E.DirectionStress.outsideLocalKernelDim F pos v = 1 ∧ RB31E2E.DirectionStress.outsideLocalRank F pos v = 1 ∧ RB31E2E.edgeSetDegree F v = 2 ∧ RB31E2E.DirectionStress.deletedConnectingClass F pos v = 0
Under the pivoted flag shape, failure of the one-coordinate inequality forces the stated local dimensions and a zero connecting class.
-
theoremdefined in RB31EndToEnd/Linear/PrivateLocalClassification.leancomplete
theorem RB31E2E.DirectionStress.privateExceptional_bothVirtualRows_mem.{u, v, w} {k : Type u} {K : Type v} {V : Type w} [Field k] [Field K] [Algebra k K] [Fintype V] [DecidableEq V] (F : RB31E2E.SimpleEdgeSet V) (pos : V → Fin 3 → K) (v p q : V) (hvp : v ≠ p) (hvq : v ≠ q) (hpq : p ≠ q) (hvpMem : RB31E2E.simpleEdge v p hvp ∈ F) (hpqMem : RB31E2E.simpleEdge p q hpq ∈ F) (hvqNotMem : RB31E2E.simpleEdge v q hvq ∉ F) (hDegree : RB31E2E.edgeSetDegree F v ≤ 2) (hpos : Function.Injective pos) (hcol : RB31E2E.PinCollinearity.Collinear (pos v) (pos p) (pos q)) (hgen : IntermediateField.adjoin k (Set.range fun c ↦ pos c.1 c.2) = ⊤) (hExceptional : RB31E2E.DirectionStress.PrivateExceptional F pos v) : ∃ N, ∃ (hqz : q ≠ N.z), RB31E2E.DirectionStress.directionRow pos (RB31E2E.simpleEdge p N.z ⋯) ∈ RB31E2E.DirectionStress.directionRowSpace (RB31E2E.deleteVertexEdges F v) pos ∧ RB31E2E.DirectionStress.directionRow pos (RB31E2E.simpleEdge q N.z hqz) ∈ RB31E2E.DirectionStress.directionRowSpace (RB31E2E.deleteVertexEdges F v) pos
theorem RB31E2E.DirectionStress.privateExceptional_bothVirtualRows_mem.{u, v, w} {k : Type u} {K : Type v} {V : Type w} [Field k] [Field K] [Algebra k K] [Fintype V] [DecidableEq V] (F : RB31E2E.SimpleEdgeSet V) (pos : V → Fin 3 → K) (v p q : V) (hvp : v ≠ p) (hvq : v ≠ q) (hpq : p ≠ q) (hvpMem : RB31E2E.simpleEdge v p hvp ∈ F) (hpqMem : RB31E2E.simpleEdge p q hpq ∈ F) (hvqNotMem : RB31E2E.simpleEdge v q hvq ∉ F) (hDegree : RB31E2E.edgeSetDegree F v ≤ 2) (hpos : Function.Injective pos) (hcol : RB31E2E.PinCollinearity.Collinear (pos v) (pos p) (pos q)) (hgen : IntermediateField.adjoin k (Set.range fun c ↦ pos c.1 c.2) = ⊤) (hExceptional : RB31E2E.DirectionStress.PrivateExceptional F pos v) : ∃ N, ∃ (hqz : q ≠ N.z), RB31E2E.DirectionStress.directionRow pos (RB31E2E.simpleEdge p N.z ⋯) ∈ RB31E2E.DirectionStress.directionRowSpace (RB31E2E.deleteVertexEdges F v) pos ∧ RB31E2E.DirectionStress.directionRow pos (RB31E2E.simpleEdge q N.z hqz) ∈ RB31E2E.DirectionStress.directionRowSpace (RB31E2E.deleteVertexEdges F v) pos
If the other live terminal edge `pq` is present, both possible response edges from the second neighbour lie in the child row space.
This is the one-flag analogue of the
low-degree classification: deleting a private support vertex also deletes
its flag, so the right-hand side of the budget falls by three while the flag
term falls by two, and the local allowance is u + \delta_v \le 1 in place
of u + \delta_v \le 3. The
formalization states the allowance as the predicate
PrivateNonexceptional
and the exceptional case as its literal negation, exactly as the deletion
chapter does for the outside case; the disjunction
private_nonexceptional_or_exceptional
is then immediate, and the two branches of the induction exhaust all
possibilities by construction.
/-- The response kernel fits in the coordinate budget left by the
one-dimensional flag-line fibre. -/
def PrivateNonexceptional
(F : SimpleEdgeSet V) (pos : V → Fin 3 → K) (v : V) : Prop :=
outsideResponseKernelDim F pos v +
(outsideExtensionTrdeg (k := k) pos v).toNat ≤ 1/-- The private exceptional branch is exactly the negation of the local
payment, not an extra hypothesis carried by the state. -/
def PrivateExceptional
(F : SimpleEdgeSet V) (pos : V → Fin 3 → K) (v : V) : Prop :=
¬ PrivateNonexceptional (k := k) F pos v
privateExceptional_classification
proves that a failure of the allowance has one shape only. Its hypotheses
are the pivoted flag data: vp live, vq missing, degree at most two,
and a_v, a_p, a_q collinear. Its conclusion gives the unique second
neighbour z, the values in (3.10), collinearity of a_v, a_p, a_z, and
the vanishing of
deletedConnectingClass,
which is the statement \ker \partial_v = \ker C_v in the form the
formalization uses. The two rows of the conclusion are
privateExceptional_bothVirtualRows_mem:
the paper's identities (3.11) and (3.12), the two-star relation on the
collinear triple followed by cancellation over K and descent to L, are
carried out on the actual local equilibrium map, and collinearity of
a_p, a_q, a_z descends to L because matrix rank is unchanged under
field extension. Both rows are rows of virtual response edges in the sense of
the deletion chapter, and the private
augmentation lemma below shows one of them can actually be added.