5.7. Flag moves and the budget ledger🔗

Lemma5.7.1

Statement uses 2

Statement dependency previews

Preview

Lemma 3.4.2

Loading preview

Statement dependency preview content is loaded from the Blueprint HTML cache.

used by 0✓L∃∀N

Tagslean-only

Each move of the induction — deleting an outside vertex, deleting a private vertex with its flag, inserting a virtual response edge, registering a new flag, pivoting a missing edge — is a constructor producing a literal child state on the exact remaining types, with completion sparsity proved by transporting the child completion into the parent's, and with a budget-lift theorem deriving the parent's budget from the child's. The paper performs the corresponding changes of flag system inside the proof of Theorem 3.9 and needs no such statements.

Lean code for Lemma5.7.1●3 theorems

theoremdefined in RB31EndToEnd/Combinatorics/ProvenanceFlagDeletion.lean

complete

theorem RB31E2E.ProvenanceFlag.State.deleteOutside_completionSparse.{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) (v : V)
  (hv : S.flagMultiplicity v = 0) (hSparse : S.CompletionSparse) :
  (S.deleteOutside v hv).CompletionSparse

theorem RB31E2E.ProvenanceFlag.State.deleteOutside_completionSparse.{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)
  (v : V) (hv : S.flagMultiplicity v = 0)
  (hSparse : S.CompletionSparse) :
  (S.deleteOutside v hv).CompletionSparse

Completion sparsity descends under deletion of an outside vertex.

theoremdefined in RB31EndToEnd/Combinatorics/ProvenanceFlagOutsideRegistration.lean

complete

theorem RB31E2E.ProvenanceFlag.State.registerOutside_completionSparse.{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)
  (hTriangleLive :
    RB31E2E.simpleEdge N.p N.q ⋯ ∈ S.edges ∧
      RB31E2E.simpleEdge N.p N.r ⋯ ∈ S.edges ∧
        RB31E2E.simpleEdge N.q N.r ⋯ ∈ S.edges) :
  (S.registerOutside hSparse v hvOutside N
      hTriangleLive).CompletionSparse

theorem RB31E2E.ProvenanceFlag.State.registerOutside_completionSparse.{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)
  (hTriangleLive :
    RB31E2E.simpleEdge N.p N.q ⋯ ∈
        S.edges ∧
      RB31E2E.simpleEdge N.p N.r ⋯ ∈
          S.edges ∧
        RB31E2E.simpleEdge N.q N.r ⋯ ∈
          S.edges) :
  (S.registerOutside hSparse v hvOutside N
      hTriangleLive).CompletionSparse

Registering the complete outside triangle preserves literal completion
`(2,2)`-sparsity.

theoremdefined in RB31EndToEnd/NullCellule/ProvenanceFlagSemismallness.lean

complete

theorem RB31E2E.ProvenanceFlag.FunctionFieldBranch.semismallBudget_of_deleteOutsideIntrinsic.{u,
    v, w, x}
  {k : Type u} {K : Type v} {V : Type w} {Flag : Type x} [Field k]
  [Field K] [Algebra k K] [Fintype V] [DecidableEq V] [Fintype Flag]
  [DecidableEq Flag] (S : RB31E2E.ProvenanceFlag.State V Flag)
  (Y : RB31E2E.ProvenanceFlag.FunctionFieldBranch S) (v : V)
  (hv : S.flagMultiplicity v = 0)
  (hChild :
    RB31E2E.ProvenanceFlag.FunctionFieldBranch.SemismallBudget
      (S.deleteOutside v hv)
      (RB31E2E.ProvenanceFlag.FunctionFieldBranch.deleteOutsideIntrinsic
        S Y v hv))
  (hNonexceptional :
    RB31E2E.DirectionStress.OutsideNonexceptional S.edges Y.position
      v) :
  RB31E2E.ProvenanceFlag.FunctionFieldBranch.SemismallBudget S Y

theorem RB31E2E.ProvenanceFlag.FunctionFieldBranch.semismallBudget_of_deleteOutsideIntrinsic.{u,
    v, w, x}
  {k : Type u} {K : Type v} {V : Type w}
  {Flag : Type x} [Field k] [Field K]
  [Algebra k K] [Fintype V]
  [DecidableEq V] [Fintype Flag]
  [DecidableEq Flag]
  (S :
    RB31E2E.ProvenanceFlag.State V Flag)
  (Y :
    RB31E2E.ProvenanceFlag.FunctionFieldBranch
      S)
  (v : V) (hv : S.flagMultiplicity v = 0)
  (hChild :
    RB31E2E.ProvenanceFlag.FunctionFieldBranch.SemismallBudget
      (S.deleteOutside v hv)
      (RB31E2E.ProvenanceFlag.FunctionFieldBranch.deleteOutsideIntrinsic
        S Y v hv))
  (hNonexceptional :
    RB31E2E.DirectionStress.OutsideNonexceptional
      S.edges Y.position v) :
  RB31E2E.ProvenanceFlag.FunctionFieldBranch.SemismallBudget
    S Y

**Outside nonexceptional induction step.**  This is the complete
recursive branch: intrinsic child semismallness plus the transparent local
nonexceptional condition implies the parent budget.

The paper's induction modifies one graph in place; the formalization, whose state is defined on exact types, rebuilds the state at every move. The child states are built by four constructors: deleteOutside restricts every field to the subtype of remaining vertices, deletePrivate restricts the flag type as well, insertLiveEdge adds one certified edge, and registerOutside erases one triangle edge and adjoins one flag, with the deleted apex replaced by the new ghost. For each, an edge-for-edge embedding of the child completion into the parent's gives sparsity by transport, and the two deletions strictly decrease the live vertex count, so the strong induction on that count terminates.

On the numerical side, the deletion-ledger module identifies each child's stress dimension with that of the parent's deleted graph and proves the two local budget lifts used in the nonexceptional cases: an outside deletion removes three ambient dimensions, so a payment of u + \delta_v \le 3 suffices (semismallBudget_of_deleteOutsideIntrinsic), while a private deletion removes three ambient dimensions but also one flag term of two, so the allowance is exactly one (semismallBudget_of_deletePrivateIntrinsic). The two exceptional cases are proved by semismallBudget_of_outsideExceptional — in its registered alternative one collinear triangle row is erased and one flag is added, so the stress and flag terms change by exactly two each — and semismallBudget_of_privateExceptional, whose proof first transports the branch across the pivot. The transcendence accounting in all four rests on the tower equality of the base-change infrastructure, and the closing natural-number arithmetic is collected in one module so that no truncated subtraction hides inside graph notation.