5.5. Two augmentation lemmas for the completion
Both exceptional cases end with the insertion of an edge whose row is
already in the retained row space, and the insertion must preserve
completion sparsity. The two lemmas of this section give that edge, one for
the outside case and one for the private case. Their proofs are tight-set
arguments in the
completion — the addable-edge lemma and
uncrossing applied to \widehat{G} — and, like those
of the sparsity chapter, they do not use the construction theorem that the
formalization also contains.
Let v \in O have degree three with neighbour set N, and set
Q = \widehat{G} - v. If Q[N] is not complete, some
f \in \binom{N}{2} \setminus E(Q) can be added to Q while preserving
(2,2)-sparsity. If Q[N] is a triangle, then no two vertices of N
belong to the support triple of a common flag, and all three triangle edges
belong to G - v.
(Zheng, 2026, Lemma 3.7)
Lean code for Lemma5.5.1●2 theorems
Associated Lean declarations
-
theoremdefined in RB31EndToEnd/Combinatorics/ProvenanceFlagOutsideMove.leancomplete
theorem RB31E2E.ProvenanceFlag.State.outside_live_neighbour_triangle_complete_or_addable.{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) (hv : S.flagMultiplicity v = 0) (N : RB31E2E.DirectionStress.DegreeThreeNeighbours S.edges v) (hDegree : RB31E2E.edgeSetDegree S.edges v = 3) : RB31E2E.ProvenanceFlag.liftLiveEdge (RB31E2E.simpleEdge N.p N.q ⋯) ∈ S.completionEdges ∧ RB31E2E.ProvenanceFlag.liftLiveEdge (RB31E2E.simpleEdge N.p N.r ⋯) ∈ S.completionEdges ∧ RB31E2E.ProvenanceFlag.liftLiveEdge (RB31E2E.simpleEdge N.q N.r ⋯) ∈ S.completionEdges ∨ ∃ f ∈ {RB31E2E.simpleEdge N.p N.q ⋯, RB31E2E.simpleEdge N.p N.r ⋯, RB31E2E.simpleEdge N.q N.r ⋯}, RB31E2E.ProvenanceFlag.liftLiveEdge f ∉ S.completionEdges ∧ RB31E2E.Sparse22 (insert (RB31E2E.ProvenanceFlag.liftLiveEdge f) (RB31E2E.deleteVertexEdges S.completionEdges (Sum.inl v)))
theorem RB31E2E.ProvenanceFlag.State.outside_live_neighbour_triangle_complete_or_addable.{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) (hv : S.flagMultiplicity v = 0) (N : RB31E2E.DirectionStress.DegreeThreeNeighbours S.edges v) (hDegree : RB31E2E.edgeSetDegree S.edges v = 3) : RB31E2E.ProvenanceFlag.liftLiveEdge (RB31E2E.simpleEdge N.p N.q ⋯) ∈ S.completionEdges ∧ RB31E2E.ProvenanceFlag.liftLiveEdge (RB31E2E.simpleEdge N.p N.r ⋯) ∈ S.completionEdges ∧ RB31E2E.ProvenanceFlag.liftLiveEdge (RB31E2E.simpleEdge N.q N.r ⋯) ∈ S.completionEdges ∨ ∃ f ∈ {RB31E2E.simpleEdge N.p N.q ⋯, RB31E2E.simpleEdge N.p N.r ⋯, RB31E2E.simpleEdge N.q N.r ⋯}, RB31E2E.ProvenanceFlag.liftLiveEdge f ∉ S.completionEdges ∧ RB31E2E.Sparse22 (insert (RB31E2E.ProvenanceFlag.liftLiveEdge f) (RB31E2E.deleteVertexEdges S.completionEdges (Sum.inl v)))
The same alternative with an addable edge returned in the original live vertex type.
-
theoremdefined in RB31EndToEnd/Combinatorics/ProvenanceFlagOutsideRegistration.leancomplete
theorem RB31E2E.ProvenanceFlag.State.outside_complete_triangle_live.{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) (hvOutside : S.flagMultiplicity v = 0) (N : RB31E2E.DirectionStress.DegreeThreeNeighbours S.edges v) (hComplete : RB31E2E.ProvenanceFlag.liftLiveEdge (RB31E2E.simpleEdge N.p N.q ⋯) ∈ S.completionEdges ∧ RB31E2E.ProvenanceFlag.liftLiveEdge (RB31E2E.simpleEdge N.p N.r ⋯) ∈ S.completionEdges ∧ RB31E2E.ProvenanceFlag.liftLiveEdge (RB31E2E.simpleEdge N.q N.r ⋯) ∈ S.completionEdges) : RB31E2E.simpleEdge N.p N.q ⋯ ∈ S.edges ∧ RB31E2E.simpleEdge N.p N.r ⋯ ∈ S.edges ∧ RB31E2E.simpleEdge N.q N.r ⋯ ∈ S.edges
theorem RB31E2E.ProvenanceFlag.State.outside_complete_triangle_live.{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) (hvOutside : S.flagMultiplicity v = 0) (N : RB31E2E.DirectionStress.DegreeThreeNeighbours S.edges v) (hComplete : RB31E2E.ProvenanceFlag.liftLiveEdge (RB31E2E.simpleEdge N.p N.q ⋯) ∈ S.completionEdges ∧ RB31E2E.ProvenanceFlag.liftLiveEdge (RB31E2E.simpleEdge N.p N.r ⋯) ∈ S.completionEdges ∧ RB31E2E.ProvenanceFlag.liftLiveEdge (RB31E2E.simpleEdge N.q N.r ⋯) ∈ S.completionEdges) : RB31E2E.simpleEdge N.p N.q ⋯ ∈ S.edges ∧ RB31E2E.simpleEdge N.p N.r ⋯ ∈ S.edges ∧ RB31E2E.simpleEdge N.q N.r ⋯ ∈ S.edges
Hence every completed edge of the outside neighbour triangle is live.
If Q[N] is not complete, then Q + vN = \widehat{G} is sparse and the
addable-edge lemma applies to Q. Suppose Q[N] is complete and
x, y \in N both lie in the support triple T_\delta of an existing
flag. The tight set T_\delta \cup \{g_\delta\} has four vertices and six
edges; since v is outside every flag, the edges vx and vy give at
least eight edges on T_\delta \cup \{g_\delta, v\}. If the third
neighbour z lies in T_\delta, the edge vz is a ninth edge on five
vertices, violating sparsity; otherwise the five-vertex bound forces the set
to be tight, and adjoining z with its three edges zv, zx, zy violates
sparsity again. This proves (i), and (ii) follows: a triangle edge that was
the restored missing edge of a flag would have both its endpoints in that
flag's support triple, contradicting (i).
The formalization proves the alternative in the completed graph. An outside
vertex meets no restored edge and no ghost star, so its incidence packet in
\widehat{G} is exactly the lift of its live packet, its completed degree
is its live degree, and
degree_three_neighbour_triangle_complete_or_addable —
the dichotomy form of Lemma 2.1 — applies to
\widehat{G} directly. Part (ii) is
outside_complete_triangle_live,
proved by the tight-K_4 argument of the paper, and
outside_complete_or_exists_sparse_insertedChild
states the addable alternative on the smaller flag state directly: the
outside vertex deleted, the edge inserted, and the child completion sparse.
Suppose v \in P satisfies (3.10), its unique flag is \gamma with
T_\gamma = \{v, p, q\} in the pivoted shape, and vz is the base-graph
edge at v other than vp. Set Q = \widehat{G} - \{v, g_\gamma\}.
Then at least one of the edges pz, qz is absent from E(Q) and can
be added to Q while preserving (2,2)-sparsity.
(Zheng, 2026, Lemma 3.8)
Lean code for Lemma5.5.2●1 theorem
Associated Lean declarations
-
theoremdefined in RB31EndToEnd/Combinatorics/ProvenanceFlagPrivateMove.leancomplete
theorem RB31E2E.ProvenanceFlag.State.private_response_edge_addable.{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 z : V) (t : Flag) (hvp : v ≠ p) (hvq : v ≠ q) (hvz : v ≠ z) (hpq : p ≠ q) (hpz : p ≠ z) (hqz : q ≠ z) (hTerminals : S.terminals t = {v, p, q}) (hpqLive : RB31E2E.simpleEdge p q hpq ∈ S.edges) (hvzLive : RB31E2E.simpleEdge v z hvz ∈ S.edges) : ∃ f, (f = RB31E2E.simpleEdge p z hpz ∨ f = RB31E2E.simpleEdge q z hqz) ∧ RB31E2E.ProvenanceFlag.liftLiveEdge f ∉ S.completionEdges ∧ RB31E2E.Sparse22 (insert (RB31E2E.ProvenanceFlag.liftLiveEdge f) (RB31E2E.deleteVertexEdges (RB31E2E.deleteVertexEdges S.completionEdges (Sum.inr t)) (Sum.inl v)))
theorem RB31E2E.ProvenanceFlag.State.private_response_edge_addable.{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 z : V) (t : Flag) (hvp : v ≠ p) (hvq : v ≠ q) (hvz : v ≠ z) (hpq : p ≠ q) (hpz : p ≠ z) (hqz : q ≠ z) (hTerminals : S.terminals t = {v, p, q}) (hpqLive : RB31E2E.simpleEdge p q hpq ∈ S.edges) (hvzLive : RB31E2E.simpleEdge v z hvz ∈ S.edges) : ∃ f, (f = RB31E2E.simpleEdge p z hpz ∨ f = RB31E2E.simpleEdge q z hqz) ∧ RB31E2E.ProvenanceFlag.liftLiveEdge f ∉ S.completionEdges ∧ RB31E2E.Sparse22 (insert (RB31E2E.ProvenanceFlag.liftLiveEdge f) (RB31E2E.deleteVertexEdges (RB31E2E.deleteVertexEdges S.completionEdges (Sum.inr t)) (Sum.inl v)))
In the pivoted private degree-two shape, one of the two virtual response edges is genuinely addable to the completed child after the private terminal and its unique ghost are consumed.
The graph Q contains pq. If both pz and qz belonged to E(Q),
the original K_4 on T_\gamma \cup \{g_\gamma\} together with
vz, pz, qz would put nine edges on five vertices. So suppose one candidate
is missing and cannot be added, say qz; a tight set B containing q
and z blocks it, and if p \notin B the edges pq and pz force
B \cup \{p\} to be tight, so some tight set contains p, q, z. If both
candidates are missing and neither can be added, the two blocking tight sets
meet at z and uncrossing gives a tight set containing p, q, z again.
Restoring v and g_\gamma adds at least the six edges
vp, vq, vz, g_\gamma v, g_\gamma p, g_\gamma q to that set, while two new
vertices permit only four, a contradiction.
The formal statement,
private_response_edge_addable,
is proved on the literal completion with both the private terminal and its
consumed ghost deleted, so the graph it augments is exactly the simultaneous
completion of the child system on which the induction continues. The
blocking argument uses
flagVertices_tight —
the completed K_4 of the old flag is tight — together with
uncrossing and the fact that a tight set with at least
two vertices has at least four. The construction theorem is not used, which
confirms at the level of proofs what
the sparsity chapter claimed from
reachability alone.