From b99c870a0b19ad42bc2037476d458c4f89bb4d31 Mon Sep 17 00:00:00 2001
From: senegrom <6349874+senegrom@users.noreply.github.com>
Date: Wed, 12 Aug 2026 19:07:09 +0100
Subject: [PATCH] Prove the sharp N+4 state law

---
 .github/workflows/state-law-check.yml         |   6 +-
 README.md                                     |   4 +-
 theory/README.md                              |  32 +-
 theory/lazy-point-theory.md                   |  20 +-
 ...oundaryAbsentPresentWriterElimination.lean | 104 ++++
 .../BoundaryApproachActionElimination.lean    | 446 +++++++++++++++++
 .../BoundaryApproachWrittenElimination.lean   |  53 ++
 .../BoundaryOccurrenceDamageElimination.lean  | 467 ++++++++++++++++++
 theory/lean/README.md                         | 259 +++++-----
 theory/lean/StateLawAxiomAudit.lean           |  15 +-
 theory/lean/StateLawNAddFourSharp.lean        |  74 +++
 theory/lean/lakefile.toml                     |  20 +
 12 files changed, 1321 insertions(+), 179 deletions(-)
 create mode 100644 theory/lean/BoundaryAbsentPresentWriterElimination.lean
 create mode 100644 theory/lean/BoundaryApproachActionElimination.lean
 create mode 100644 theory/lean/BoundaryApproachWrittenElimination.lean
 create mode 100644 theory/lean/BoundaryOccurrenceDamageElimination.lean
 create mode 100644 theory/lean/StateLawNAddFourSharp.lean

diff --git a/.github/workflows/state-law-check.yml b/.github/workflows/state-law-check.yml
index acda425..adc7a0a 100644
--- a/.github/workflows/state-law-check.yml
+++ b/.github/workflows/state-law-check.yml
@@ -1,4 +1,4 @@
-name: State law N+6
+name: State law N+4
 on:
   push:
     branches: [main]
@@ -20,10 +20,10 @@ jobs:
           echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
       - name: Build every library
         run: lake build
-      - name: Audit the axioms of the state law
+      - name: Audit the axioms of the sharp state law
         run: |
           lake build StateLawAxiomAudit 2>&1 | tee audit.log
-          grep "'GeneralN.stateLaw' depends on axioms" audit.log
+          grep "'GeneralN.state_law_N_add_four' depends on axioms" audit.log
           if grep -q "sorryAx" audit.log; then
             echo "sorryAx detected" && exit 1
           fi
diff --git a/README.md b/README.md
index 2d41c6f..cae3830 100644
--- a/README.md
+++ b/README.md
@@ -4,8 +4,8 @@ Model LEGO® DUPLO® train track and find every layout that **loops nicely** —
 pieces you actually own.
 
 The mathematics that grew out of it — the lazy-point switch theorems and the
-Lean 4 proofs of the state law (`N+4 ≤ f(N) ≤ N+5`, sharp constant one unit
-from closed) — lives in [`theory/`](theory/README.md).
+Lean 4 proof of the sharp state law `f(N) = min(2^N, N + 4)` — lives in
+[`theory/`](theory/README.md).
 
 ```
 duplotrain solve --curve 12 --straight 4 --use-all -o out
diff --git a/theory/README.md b/theory/README.md
index 4b2a638..9d0ed82 100644
--- a/theory/README.md
+++ b/theory/README.md
@@ -1,28 +1,30 @@
 # Theory: the lazy-point switch problem
 
 The mathematical side of the project: how many distinct switch settings
-can a single train visit on a layout of N lazy Y-switches?  The
-conjectured law is f(N) = min(2^N, N + 4).  Machine-checked status:
-**N + 4 ≤ f(N) ≤ N + 5 for every N ≥ 3**, fully symbolic in N on both
-sides; the last additive unit is reduced to four explicit residual
-geometries (see `lean/README.md`).
+can a single train visit on a layout of N lazy Y-switches? The sharp law is
+now machine-checked:
+
+**f(N) = min(2^N, N + 4) for every N ≥ 1.**
+
+The symbolic Lean proof gives the `N + 4` upper bound for every `N`; the
+matching construction gives `N + 4` states for every `N ≥ 3`, while the
+finite-state ceiling supplies `2^N` and the exhaustive small cases give
+`f(1) = 2` and `f(2) = 4`.
 
 Contents:
 
 * **`lean/`** — the machine-checked results (Lean 4, no Mathlib):
-  the `N+5` upper bound (`StateLawNAddFive.lean`, via the unconditional
-  known-incoming-edge `N+4` core), the symbolic `N+4` lower-bound
-  family (`StateLawLowerBound.lean`), the sharpened residual frontier
-  for the exact `N+4` law, the exhaustive small-N anchors, and the
-  permanent axiom audit.  `lean/README.md` is the guide.
+  `StateLawNAddFourSharp.lean` proves the sharp raw `N+4` theorem over
+  tracks and switches; `StateLawLowerBound.lean` gives the matching family;
+  the exhaustive small-N anchors and the permanent axiom audit remain
+  separate from the symbolic proof. `lean/README.md` is the guide.
 * **`lazy-point-theory.md`** — the paper trail of the earlier
-  register-machine (echo) program; historical, superseded by the track
-  proofs.
+  register-machine (echo) programme; historical and independent of the
+  completed physical-track proof.
 * **`switch_ceiling_proof.py`** — the perfection exhaustion engine
   (no perfect layout has ≥ 3 switches), used by
   `tests/test_switch_ceiling.py`.
-* **`tools/bstates.py`** — the python state-count prober that
-  discovered the extremal `N+4` family and cross-checks
-  `lean/FamilyLowerBound.lean`.
+* **`tools/bstates.py`** — the Python state-count prober that discovered the
+  extremal `N+4` family and cross-checks `lean/FamilyLowerBound.lean`.
 
 Build the Lean proofs: `cd lean && lake build` (elan; toolchain pinned).
diff --git a/theory/lazy-point-theory.md b/theory/lazy-point-theory.md
index c2447f8..1bb0f2e 100644
--- a/theory/lazy-point-theory.md
+++ b/theory/lazy-point-theory.md
@@ -16,17 +16,15 @@ an active switch flips both ways. Distinct tongue vectors on a cycle with
 > **Cycle theorem.** Every eventual cycle has at most 2 active switches,
 > hence at most 4 distinct tongue vectors.
 
-is reduced to bounding actives. Status: the general raw bound
-`GeneralN.StateLaw`, namely `f(N) ≤ N+6`, is **proved** by
-`GeneralN.stateLaw` in `lean/KnownEdgeNAddFiveAlt.lean`.  Its stronger
-known-incoming-edge core is `N+5`; an arbitrary start costs at most its
-time-zero vector.  The proof is a direct physical-track lasso argument and
-does not assume the echo-machine Gray-tail properties.  The
-separate echo-machine route still reduces the sharper bound to the Gray tail
-(**B**) and one-alternation transient (**C**); those remain open.  Evidence:
-exhaustive for N ≤ 4 on wirings (140,152, in Lean), unbeaten by
-cycle-objective search through N = 7, and exhaustive across all small
-machines (`echo_machine.py`).
+is reduced to bounding actives. Status: the sharp raw bound
+`f(N) ≤ N+4` is **proved** by `GeneralN.state_law_N_add_four` in
+`lean/StateLawNAddFourSharp.lean`, matching the symbolic lower-bound family
+for every `N ≥ 3`. The proof is a direct physical-track lasso/history
+argument and does not assume the echo-machine Gray-tail properties. The
+separate echo-machine route still reduces the same bound to the Gray tail
+(**B**) and one-alternation transient (**C**); those remain open as an
+independent proof route. Evidence includes the exhaustive `N ≤ 4` wiring
+checks in Lean and the historical search sweeps preserved in git history.
 
 ---
 
diff --git a/theory/lean/BoundaryAbsentPresentWriterElimination.lean b/theory/lean/BoundaryAbsentPresentWriterElimination.lean
new file mode 100644
index 0000000..cc5aacd
--- /dev/null
+++ b/theory/lean/BoundaryAbsentPresentWriterElimination.lean
@@ -0,0 +1,104 @@
+import BoundaryResidualSharpening
+
+/-!
+# Elimination of the absent-present-writer residual
+
+A manufactured reflector's construction is switch-simple.  If that
+construction starts at the stem of switch `k0`, then `k0` cannot be a
+productive first writer: time zero is a quiet facing traversal, while a later
+productive write would revisit the switch already used by the first passage.
+This removes the absent-present-writer constructor from the productive-boundary
+frontier.
+-/
+
+namespace GeneralN
+
+/-- A switch-simple trace beginning at the stem of `k0` cannot productively
+first-write `k0` during that trace. -/
+theorem stem_switch_not_mem_firstWriterSwitches_of_simple_trace
+    {w : Wiring} {N e k0 : Nat} {state : Tongues}
+    {route : List Passage} {finish : Nat × Tongues}
+    (hstem : e = 3 * k0)
+    (htrace : PhysicalTrace w (e, state) route finish)
+    (hsimple : SwitchSimple route) :
+    Not (k0 ∈
+      (rawFirstWriterTimes w N (e, state) route.length).map
+        (rawWriterAt w (e, state))) := by
+  intro hm
+  obtain ⟨k, hk, hwriter⟩ := List.mem_map.mp hm
+  have hkData := mem_rawFirstWriterTimes_iff.mp hk
+  have hklt : k < route.length := hkData.1
+  have hprod : RawProductiveAt w N (e, state) k := hkData.2.1
+  by_cases hkzero : k = 0
+  · subst k
+    apply hprod.2
+    rcases Option.isSome_iff_exists.mp hprod.1 with ⟨next, hnext⟩
+    have hnextOne : stepN w 1 (e, state) = some next := by
+      simpa using hnext
+    have hemod : e % 3 = 0 := by omega
+    have hediv : e / 3 = k0 := by omega
+    have harrive : arrive state e =
+        (selectedBranch state k0, state) := by
+      simp [arrive, hemod, hediv, selectedBranch]
+    have hnextState : next.2 = state := by
+      simp only [stepN, step, harrive] at hnextOne
+      cases hlink : w.link (selectedBranch state k0) with
+      | none => simp [hlink] at hnextOne
+      | some q =>
+          simp [hlink] at hnextOne
+          exact (Prod.mk.inj hnextOne.symm).2
+    unfold restrictedTonguesAt tonguesAt
+    rw [hnextOne]
+    simp [hnextState, stepN]
+  · have hkpos : 0 < k := by omega
+    have hzeroInside : 0 < route.length := by omega
+    have hzeroWriter :=
+      htrace.rawWriterAt_eq_passageSwitch_getElem
+        (k := 0) hzeroInside
+    have hkWriter :=
+      htrace.rawWriterAt_eq_passageSwitch_getElem
+        (k := k) hklt
+    have hpair := List.pairwise_iff_getElem.mp hsimple
+    have hzeroMap : 0 < (route.map passageSwitch).length := by
+      simpa using hzeroInside
+    have hkMap : k < (route.map passageSwitch).length := by
+      simpa using hklt
+    have hne := hpair 0 k hzeroMap hkMap hkpos
+    apply hne
+    simp only [List.getElem_map]
+    rw [← hzeroWriter, ← hkWriter]
+    calc
+      rawWriterAt w (e, state) 0 = e / 3 := by
+        simp [rawWriterAt, rawEntryAt, stepN]
+      _ = k0 := by omega
+      _ = rawWriterAt w (e, state) k := hwriter.symm
+
+/-- The construction of a manufactured reflector cannot productively
+first-write its starting switch when the incoming port is that switch's
+stem. -/
+theorem ManufacturedReflector.stem_switch_not_mem_constructionFirstWriterSwitches
+    {w : Wiring} {N g e k0 : Nat}
+    (B : ManufacturedReflector w g e)
+    (hstem : g = 3 * k0) :
+    Not (k0 ∈ B.constructionFirstWriterSwitches N) := by
+  exact stem_switch_not_mem_firstWriterSwitches_of_simple_trace
+    hstem B.exploration_trace B.exploration_simple
+
+/-- The absent-present-writer constructor in `BoundarySharpResidual` is
+empty: the second construction starts at the boundary switch's stem. -/
+theorem BoundarySharpResidual.absentPresentWriter_impossible
+    {w : Wiring} {N : Nat}
+    {S : ProductiveBoundaryNAddFourSavingResidual w N}
+    (R : ManufacturedFlipReflector w S.source.g S.source.e)
+    (_kind : S.A = ManufacturedReflector.flip R)
+    (_absentA : Not (S.source.k0 ∈
+      S.A.exploration.map passageSwitch))
+    (P : PartialSecondReflectorCompletion S.A N)
+    (_supportGrooved : PathGrooves S.A.toSupported.paths
+      P.reflector.preReturn.2)
+    (present : S.source.k0 ∈
+      P.reflector.constructionFirstWriterSwitches N) : False := by
+  exact (P.reflector.stem_switch_not_mem_constructionFirstWriterSwitches
+    S.source.stem) present
+
+end GeneralN
diff --git a/theory/lean/BoundaryApproachActionElimination.lean b/theory/lean/BoundaryApproachActionElimination.lean
new file mode 100644
index 0000000..4233c57
--- /dev/null
+++ b/theory/lean/BoundaryApproachActionElimination.lean
@@ -0,0 +1,446 @@
+import BoundaryChangedContactSaving
+
+/-!
+# Eliminating the action-only approach-written residual
+
+When the changed-contact approach first-writes the old flip action, the local
+forward tail has only one fresh corner (the runway alternative is impossible).
+Consequently the exploration-absent boundary coordinate alone supplies the
+missing ambient reserve: the compressed lead is at most `N+2`, and the whole
+changed-contact run is at most `N+3`.  Thus the only approach-written residual
+left by the productive-boundary saving is a first write of the boundary switch
+itself.
+-/
+
+namespace GeneralN
+
+private theorem baae_nodup_filter_nat (p : Nat -> Bool) :
+    forall {xs : List Nat}, xs.Nodup -> (xs.filter p).Nodup := by
+  intro xs
+  induction xs with
+  | nil =>
+      intro _
+      simp
+  | cons x rest ih =>
+      intro hnd
+      rw [List.nodup_cons] at hnd
+      cases hp : p x with
+      | true =>
+          simp only [List.filter_cons, hp, if_true, List.nodup_cons]
+          exact ⟨fun hm => hnd.1 (List.mem_filter.mp hm).1, ih hnd.2⟩
+      | false =>
+          simp only [List.filter_cons, hp]
+          exact ih hnd.2
+
+private theorem baae_nodup_map_nat_of_injective_on
+    {f : Nat -> Nat} {xs : List Nat}
+    (hinj : forall i, i ∈ xs -> forall j, j ∈ xs ->
+      f i = f j -> i = j)
+    (hnd : xs.Nodup) : (xs.map f).Nodup := by
+  induction xs with
+  | nil => simp
+  | cons x rest ih =>
+      rw [List.nodup_cons] at hnd
+      rw [List.map_cons, List.nodup_cons]
+      constructor
+      · intro hm
+        obtain ⟨y, hy, hfy⟩ := List.mem_map.mp hm
+        have hxy : y = x :=
+          hinj y (List.mem_cons_of_mem _ hy) x List.mem_cons_self hfy
+        rw [hxy] at hy
+        exact hnd.1 hy
+      · exact ih
+          (fun i hi j hj =>
+            hinj i (List.mem_cons_of_mem _ hi)
+              j (List.mem_cons_of_mem _ hj))
+          hnd.2
+
+/-- If the reserved boundary switch is absent both from the old reusable
+support and from productive first writers in the strict approach, it supplies
+one ambient coordinate independently of whether the old action is itself an
+approach writer. -/
+theorem SimpleContinuationChangedContact.reusable_add_approach_writers_add_reserved_le
+    {w : Wiring} {N g e k0 : Nat}
+    (hN : forall p q, w.link p = some q ->
+      p < 3 * N /\ q < 3 * N)
+    {R : ManufacturedFlipReflector w g e}
+    (C : SimpleContinuationChangedContact w
+      (ManufacturedReflector.flip R))
+    (hA : PathGrooves
+      (ManufacturedReflector.flip R).toSupported.paths
+      (ManufacturedReflector.flip R).activatedState)
+    (hk0 : k0 < N)
+    (hreservedExploration : Not (k0 ∈
+      (ManufacturedReflector.flip R).exploration.map passageSwitch))
+    (hreservedApproach : Not (k0 ∈
+      C.approachFirstWriterSwitches N)) :
+    (ManufacturedReflector.flip R).reusableSwitches.length +
+        (rawFirstWriterTimes w N
+          (e, (ManufacturedReflector.flip R).activatedState)
+          C.approach.length).length + 1 <= N := by
+  classical
+  let times := rawFirstWriterTimes w N
+    (e, (ManufacturedReflector.flip R).activatedState)
+    C.approach.length
+  let writers := times.map
+    (rawWriterAt w
+      (e, (ManufacturedReflector.flip R).activatedState))
+  have htimesNodup : times.Nodup := by
+    dsimp [times, rawFirstWriterTimes]
+    exact baae_nodup_filter_nat _ List.nodup_range
+  have hwritersNodup : writers.Nodup := by
+    dsimp [writers]
+    apply baae_nodup_map_nat_of_injective_on
+    · intro i hi j hj hEq
+      have hiData := mem_rawFirstWriterTimes_iff.mp (by
+        simpa [times] using hi)
+      have hjData := mem_rawFirstWriterTimes_iff.mp (by
+        simpa [times] using hj)
+      exact rawFirstWriterAt_injective hiData.2 hjData.2 hEq
+    · exact htimesNodup
+  have hdisjoint :
+      forall oldSwitch,
+        oldSwitch ∈ (ManufacturedReflector.flip R).reusableSwitches ->
+      forall freshSwitch, freshSwitch ∈ writers ->
+        oldSwitch ≠ freshSwitch := by
+    intro oldSwitch hOld freshSwitch hFresh hEq
+    obtain ⟨k, hk, rfl⟩ := List.mem_map.mp hFresh
+    have hkData := mem_rawFirstWriterTimes_iff.mp (by
+      simpa [times] using hk)
+    have houtside :=
+      C.approach_trace.productive_writer_not_reusable_of_endpoint_grooves
+        hN (ManufacturedReflector.flip R) C.approach_simple
+        hA C.old_grooves hkData.1 hkData.2.1
+    apply houtside
+    rw [← hEq]
+    exact hOld
+  let occupied :=
+    (ManufacturedReflector.flip R).reusableSwitches ++ writers
+  have hoccupiedNodup : occupied.Nodup := by
+    dsimp [occupied]
+    exact List.nodup_append.mpr
+      ⟨(ManufacturedReflector.flip R).reusableSwitches_nodup,
+        hwritersNodup, hdisjoint⟩
+  have hreservedNotOccupied : Not (k0 ∈ occupied) := by
+    intro hm
+    rcases List.mem_append.mp hm with hold | hfresh
+    · exact R.reserved_not_mem_reusable hreservedExploration hold
+    · apply hreservedApproach
+      simpa [SimpleContinuationChangedContact.approachFirstWriterSwitches,
+        writers, times] using hfresh
+  have hallNodup : (k0 :: occupied).Nodup := by
+    rw [List.nodup_cons]
+    exact ⟨hreservedNotOccupied, hoccupiedNodup⟩
+  have hallLt : forall switch,
+      switch ∈ k0 :: occupied -> switch < N := by
+    intro switch hswitch
+    rcases List.mem_cons.mp hswitch with rfl | hoccupied
+    · exact hk0
+    rcases List.mem_append.mp hoccupied with hold | hfresh
+    · exact (ManufacturedReflector.flip R).reusableSwitch_lt hN hold
+    · obtain ⟨k, hk, rfl⟩ := List.mem_map.mp hfresh
+      have hkData := mem_rawFirstWriterTimes_iff.mp (by
+        simpa [times] using hk)
+      exact rawProductiveAt_writer_lt hN hkData.2.1
+  have hbound := nodup_nat_lt_length hallNodup hallLt
+  have hlength :
+      (k0 :: occupied).length =
+        (ManufacturedReflector.flip R).reusableSwitches.length +
+          times.length + 1 := by
+    simp [occupied, writers]
+  rw [hlength] at hbound
+  simpa [times] using hbound
+
+/-- Reserving the boundary coordinate alone bounds the changed-contact
+compressed lead by `N+2`, even when the old action is approach-written. -/
+theorem SimpleContinuationChangedContact.compressedLead_length_le_N_add_two_of_reserved_absent
+    {w : Wiring} {N g e k0 : Nat}
+    (hN : forall p q, w.link p = some q ->
+      p < 3 * N /\ q < 3 * N)
+    {R : ManufacturedFlipReflector w g e}
+    (C : SimpleContinuationChangedContact w
+      (ManufacturedReflector.flip R))
+    (hA : PathGrooves
+      (ManufacturedReflector.flip R).toSupported.paths
+      (ManufacturedReflector.flip R).activatedState)
+    (hk0 : k0 < N)
+    (hreservedExploration : Not (k0 ∈
+      (ManufacturedReflector.flip R).exploration.map passageSwitch))
+    (hreservedApproach : Not (k0 ∈
+      C.approachFirstWriterSwitches N)) :
+    (C.compressedLead N).length <= N + 2 := by
+  have hboundary :
+      VectorCount.restrict N
+          (ManufacturedReflector.flip R).activatedState ∈
+        rawFirstWriterHistory w N
+          (e, (ManufacturedReflector.flip R).activatedState)
+          C.approach.length := by
+    simp [rawFirstWriterHistory, restrictedTonguesAt,
+      tonguesAt, stepN]
+  have hcharge :=
+    C.reusable_add_approach_writers_add_reserved_le
+      hN hA hk0 hreservedExploration hreservedApproach
+  unfold SimpleContinuationChangedContact.compressedLead
+  rw [List.length_append, List.length_append,
+    List.length_erase_of_mem hboundary,
+    (ManufacturedReflector.flip R).sharpHistoryCore_length]
+  simp [rawFirstWriterHistory, ManufacturedReflector.exploration,
+    ManufacturedReflector.reusableSwitches] at hcharge ⊢
+  omega
+
+/-- A one-novelty changed-contact tail plus the boundary-reserved `N+2`
+compressed lead gives the required `N+3` global bound. -/
+theorem SimpleContinuationChangedContact.changed_all_run_distinct_le_N_add_three_of_one_novelty_and_reserved_absent
+    {w : Wiring} {N g e k0 : Nat}
+    (hN : forall p q, w.link p = some q ->
+      p < 3 * N /\ q < 3 * N)
+    {R : ManufacturedFlipReflector w g e}
+    (C : SimpleContinuationChangedContact w
+      (ManufacturedReflector.flip R))
+    (hA : PathGrooves
+      (ManufacturedReflector.flip R).toSupported.paths
+      (ManufacturedReflector.flip R).activatedState)
+    (hk0 : k0 < N)
+    (hreservedExploration : Not (k0 ∈
+      (ManufacturedReflector.flip R).exploration.map passageSwitch))
+    (hreservedApproach : Not (k0 ∈
+      C.approachFirstWriterSwitches N))
+    (times : List Nat)
+    (hlive : forall k, k ∈ times ->
+      (stepN w k
+        (g, (ManufacturedReflector.flip R).baseState)).isSome)
+    (hnd : (times.map
+      (restrictedTonguesAt w N
+        (g, (ManufacturedReflector.flip R).baseState))).Nodup)
+    (hlocal : NoveltyCoverOn w N
+      (e, (ManufacturedReflector.flip R).activatedState)
+      (times.map (fun k => k -
+        ((ManufacturedReflector.flip R).exploration.length +
+          (ManufacturedReflector.flip R).runway.length + 1)))
+      (C.compressedLead N) 1) :
+    times.length <= N + 3 := by
+  let firstTravel :=
+    (ManufacturedReflector.flip R).exploration.length +
+      (ManufacturedReflector.flip R).runway.length + 1
+  let localTimes := times.map (fun k => k - firstTravel)
+  have hreach : stepN w firstTravel
+      (g, (ManufacturedReflector.flip R).baseState) =
+        some (e, (ManufacturedReflector.flip R).activatedState) := by
+    simpa [firstTravel] using
+      (ManufacturedReflector.flip R).manufacturing_journey_reaches_activated
+        hA
+  have hlocal' : NoveltyCoverOn w N
+      (e, (ManufacturedReflector.flip R).activatedState)
+      localTimes (C.compressedLead N) 1 := by
+    simpa [localTimes, firstTravel] using hlocal
+  obtain ⟨fresh, hfresh, hmem⟩ := hlocal'
+  have hcover : NoveltyCoverOn w N
+      (g, (ManufacturedReflector.flip R).baseState)
+      times (C.compressedLead N) 1 := by
+    refine ⟨fresh, hfresh, ?_⟩
+    intro k hk
+    by_cases hfirst : k <= firstTravel
+    · unfold SimpleContinuationChangedContact.compressedLead
+      apply List.mem_append_left
+      apply List.mem_append_left
+      apply (ManufacturedReflector.flip R).mem_sharpHistoryCore_of_mem
+      exact (ManufacturedReflector.flip R).manufacturing_journey_mem_sharpHistory
+        hA (by simpa [firstTravel] using hfirst)
+    · let d := k - firstTravel
+      have hdMem : d ∈ localTimes := by
+        dsimp [d, localTimes]
+        exact List.mem_map.mpr ⟨k, hk, rfl⟩
+      have hm := hmem d hdMem
+      have hshift := restrictedTonguesAt_sub_of_reach
+        (N := N) hreach (by omega) (hlive k hk)
+      rw [hshift]
+      exact hm
+  have hcount := noveltyCoverOn_distinct_count hcover hnd
+  have hlength :=
+    C.compressedLead_length_le_N_add_two_of_reserved_absent
+      hN hA hk0 hreservedExploration hreservedApproach
+  omega
+
+/-- With an exploration-absent boundary coordinate that is not approach
+first-written, every changed contact already fits `N+3`.  If the old action is
+first-written, the one-novelty tail and impossibility of the runway residual
+replace the action-coordinate reserve. -/
+theorem SimpleContinuationChangedContact.changed_all_run_distinct_le_N_add_three_of_reserved_absent
+    {w : Wiring} {N g e k0 : Nat}
+    (hN : forall p q, w.link p = some q ->
+      p < 3 * N /\ q < 3 * N)
+    {R : ManufacturedFlipReflector w g e}
+    (C : SimpleContinuationChangedContact w
+      (ManufacturedReflector.flip R))
+    (hA : PathGrooves
+      (ManufacturedReflector.flip R).toSupported.paths
+      (ManufacturedReflector.flip R).activatedState)
+    (hk0 : k0 < N)
+    (hreservedExploration : Not (k0 ∈
+      (ManufacturedReflector.flip R).exploration.map passageSwitch))
+    (hreservedApproach : Not (k0 ∈
+      C.approachFirstWriterSwitches N))
+    (times : List Nat)
+    (hlive : forall k, k ∈ times ->
+      (stepN w k
+        (g, (ManufacturedReflector.flip R).baseState)).isSome)
+    (hnd : (times.map
+      (restrictedTonguesAt w N
+        (g, (ManufacturedReflector.flip R).baseState))).Nodup) :
+    times.length <= N + 3 := by
+  rcases C.direction with hbackward |
+      ⟨hforward, repaired, hrepair, hrestored⟩
+  · exact C.backward_all_run_distinct_le_N_add_three
+      hN hA hbackward times hlive hnd
+  · by_cases haction :
+        R.actionSwitch ∈ C.approachFirstWriterSwitches N
+    · let localTimes := times.map (fun k => k -
+          ((ManufacturedReflector.flip R).exploration.length +
+            (ManufacturedReflector.flip R).runway.length + 1))
+      rcases C.forward_flip_one_novelty_or_runway_residual
+          hforward hrepair hrestored haction localTimes with
+        hone | hresidual
+      · apply C.changed_all_run_distinct_le_N_add_three_of_one_novelty_and_reserved_absent
+          hN hA hk0 hreservedExploration hreservedApproach
+          times hlive hnd
+        simpa [localTimes] using hone
+      · exact (Classical.choice hresidual).impossible hN hA |>.elim
+    · exact C.changed_all_run_distinct_le_N_add_three_of_action_and_reserved_absent
+        hN hA haction hk0 hreservedExploration hreservedApproach
+        times hlive hnd
+
+/-- Sharpened keystone: the only approach-written geometry that can survive
+an exploration-absent boundary saving is a productive first write of the
+boundary switch itself. -/
+theorem PartialSecondRunSharp.ChangedContact.flip_saving_le_N_add_three_or_boundary_written
+    {w : Wiring} {N g e k0 : Nat}
+    (hN : forall p q, w.link p = some q ->
+      p < 3 * N /\ q < 3 * N)
+    {R : ManufacturedFlipReflector w g e}
+    (D : PartialSecondRunSharp.ChangedContact w
+      (ManufacturedReflector.flip R))
+    (hA : PathGrooves
+      (ManufacturedReflector.flip R).toSupported.paths
+      (ManufacturedReflector.flip R).activatedState)
+    (hk0 : k0 < N)
+    (hreservedExploration : Not (k0 ∈
+      (ManufacturedReflector.flip R).exploration.map passageSwitch))
+    (times : List Nat)
+    (hlive : forall k, k ∈ times ->
+      (stepN w k
+        (g, (ManufacturedReflector.flip R).baseState)).isSome)
+    (hnd : (times.map
+      (restrictedTonguesAt w N
+        (g, (ManufacturedReflector.flip R).baseState))).Nodup) :
+    times.length <= N + 3 \/
+      k0 ∈ D.toSimpleContinuationChangedContact.approachFirstWriterSwitches N := by
+  by_cases hk0Written :
+      k0 ∈ D.toSimpleContinuationChangedContact.approachFirstWriterSwitches N
+  · exact Or.inr hk0Written
+  · exact Or.inl
+      (D.toSimpleContinuationChangedContact.changed_all_run_distinct_le_N_add_three_of_reserved_absent
+        hN hA hk0 hreservedExploration hk0Written times hlive hnd)
+
+
+/-- A switch-simple changed-contact approach cannot productively first-write
+its starting switch when the start port is that switch's stem.  Time zero is
+a quiet facing passage; any later occurrence would repeat the first passage's
+switch. -/
+theorem SimpleContinuationChangedContact.stem_switch_not_mem_approachFirstWriterSwitches
+    {w : Wiring} {N g e k0 : Nat}
+    {R : ManufacturedFlipReflector w g e}
+    (C : SimpleContinuationChangedContact w
+      (ManufacturedReflector.flip R))
+    (hstem : e = 3 * k0) :
+    Not (k0 ∈ C.approachFirstWriterSwitches N) := by
+  intro hm
+  unfold SimpleContinuationChangedContact.approachFirstWriterSwitches at hm
+  obtain ⟨k, hk, hwriter⟩ := List.mem_map.mp hm
+  have hkData := mem_rawFirstWriterTimes_iff.mp hk
+  have hklt : k < C.approach.length := hkData.1
+  have hprod : RawProductiveAt w N
+      (e, (ManufacturedReflector.flip R).activatedState) k :=
+    hkData.2.1
+  by_cases hkzero : k = 0
+  · subst k
+    apply hprod.2
+    rcases Option.isSome_iff_exists.mp hprod.1 with ⟨next, hnext⟩
+    have hnextOne : stepN w 1
+        (e, (ManufacturedReflector.flip R).activatedState) = some next := by
+      simpa using hnext
+    have hemod : e % 3 = 0 := by omega
+    have hediv : e / 3 = k0 := by omega
+    have harrive : arrive (ManufacturedReflector.flip R).activatedState e =
+        (selectedBranch (ManufacturedReflector.flip R).activatedState k0,
+          (ManufacturedReflector.flip R).activatedState) := by
+      simp [arrive, hemod, hediv, selectedBranch]
+    have hnextState : next.2 =
+        (ManufacturedReflector.flip R).activatedState := by
+      simp only [stepN, step, harrive] at hnextOne
+      cases hlink : w.link
+          (selectedBranch (ManufacturedReflector.flip R).activatedState k0) with
+      | none => simp [hlink] at hnextOne
+      | some q =>
+          simp [hlink] at hnextOne
+          exact (Prod.mk.inj hnextOne.symm).2
+    unfold restrictedTonguesAt tonguesAt
+    rw [hnextOne]
+    simp [hnextState, stepN]
+  · have hkpos : 0 < k := by omega
+    have hzeroInside : 0 < C.approach.length := by omega
+    have hzeroWriter :=
+      C.approach_trace.rawWriterAt_eq_passageSwitch_getElem
+        (k := 0) hzeroInside
+    have hkWriter :=
+      C.approach_trace.rawWriterAt_eq_passageSwitch_getElem
+        (k := k) hklt
+    have hpair := List.pairwise_iff_getElem.mp C.approach_simple
+    have hzeroMap : 0 < (C.approach.map passageSwitch).length := by
+      simpa using hzeroInside
+    have hkMap : k < (C.approach.map passageSwitch).length := by
+      simpa using hklt
+    have hne := hpair 0 k hzeroMap hkMap hkpos
+    apply hne
+    simp only [List.getElem_map]
+    rw [← hzeroWriter, ← hkWriter]
+    calc
+      rawWriterAt w
+          (e, (ManufacturedReflector.flip R).activatedState) 0 =
+          e / 3 := by simp [rawWriterAt, rawEntryAt, stepN]
+      _ = k0 := by omega
+      _ = rawWriterAt w
+          (e, (ManufacturedReflector.flip R).activatedState) k :=
+        hwriter.symm
+
+
+/-- In the productive-boundary geometry, the shifted run starts at the stem of
+the reserved switch.  Switch simplicity therefore makes the boundary reserve
+automatic, and every changed-contact branch is at most `N+3`. -/
+theorem SimpleContinuationChangedContact.changed_all_run_distinct_le_N_add_three_of_stem_reserved
+    {w : Wiring} {N g e k0 : Nat}
+    (hN : forall p q, w.link p = some q ->
+      p < 3 * N /\ q < 3 * N)
+    {R : ManufacturedFlipReflector w g e}
+    (C : SimpleContinuationChangedContact w
+      (ManufacturedReflector.flip R))
+    (hA : PathGrooves
+      (ManufacturedReflector.flip R).toSupported.paths
+      (ManufacturedReflector.flip R).activatedState)
+    (hk0 : k0 < N)
+    (hstem : e = 3 * k0)
+    (hreservedExploration : Not (k0 ∈
+      (ManufacturedReflector.flip R).exploration.map passageSwitch))
+    (times : List Nat)
+    (hlive : forall k, k ∈ times ->
+      (stepN w k
+        (g, (ManufacturedReflector.flip R).baseState)).isSome)
+    (hnd : (times.map
+      (restrictedTonguesAt w N
+        (g, (ManufacturedReflector.flip R).baseState))).Nodup) :
+    times.length <= N + 3 := by
+  apply C.changed_all_run_distinct_le_N_add_three_of_reserved_absent
+    hN hA hk0 hreservedExploration
+    (C.stem_switch_not_mem_approachFirstWriterSwitches hstem)
+    times hlive hnd
+
+end GeneralN
diff --git a/theory/lean/BoundaryApproachWrittenElimination.lean b/theory/lean/BoundaryApproachWrittenElimination.lean
new file mode 100644
index 0000000..c22b3d5
--- /dev/null
+++ b/theory/lean/BoundaryApproachWrittenElimination.lean
@@ -0,0 +1,53 @@
+import BoundaryResidualSharpening
+import BoundaryApproachActionElimination
+
+/-!
+# Elimination of the approach-written productive-boundary residual
+
+The shifted second run starts at the stem of the boundary switch.  Hence a
+switch-simple strict approach cannot first-write that boundary switch: time
+zero is a quiet facing traversal, while a later visit would repeat its switch.
+If the old action is first-written instead, the forward tail has only one fresh
+corner and the boundary coordinate remains reserved.  In either case the
+changed-contact run has at most `N+3` selected vectors, contradicting boundary
+saturation at `N+4`.
+-/
+
+namespace GeneralN
+
+/-- The approach-written constructor in `BoundarySharpResidual` is empty. -/
+theorem BoundaryApproachWrittenResidual.impossible
+    {w : Wiring} {N : Nat}
+    (hN : forall p q, w.link p = some q ->
+      p < 3 * N /\ q < 3 * N)
+    {S : ProductiveBoundaryNAddFourSavingResidual w N}
+    (D : BoundaryApproachWrittenResidual S) : False := by
+  let C := D.contact.toSimpleContinuationChangedContact
+  have hA : PathGrooves
+      (ManufacturedReflector.flip D.R).toSupported.paths
+      (ManufacturedReflector.flip D.R).activatedState := by
+    rw [← D.kind, ← S.activated]
+    exact S.grooves
+  have hAbase : (ManufacturedReflector.flip D.R).baseState =
+      S.source.base := by
+    simpa [D.kind] using S.reflector_base
+  have hlive : forall k, k ∈ S.source.times ->
+      (stepN w k
+        (S.source.g,
+          (ManufacturedReflector.flip D.R).baseState)).isSome := by
+    intro k hk
+    simpa [hAbase] using S.source.live k hk
+  have hnd : (S.source.times.map
+      (restrictedTonguesAt w N
+        (S.source.g,
+          (ManufacturedReflector.flip D.R).baseState))).Nodup := by
+    have htail := (List.nodup_cons.mp S.source.distinct).2
+    simpa [hAbase] using htail
+  have hbound :=
+    C.changed_all_run_distinct_le_N_add_three_of_stem_reserved
+      hN hA S.source.switch_lt S.source.stem
+      D.absentExploration S.source.times hlive hnd
+  have hsaturated := S.source.saturated
+  omega
+
+end GeneralN
diff --git a/theory/lean/BoundaryOccurrenceDamageElimination.lean b/theory/lean/BoundaryOccurrenceDamageElimination.lean
new file mode 100644
index 0000000..b428e83
--- /dev/null
+++ b/theory/lean/BoundaryOccurrenceDamageElimination.lean
@@ -0,0 +1,467 @@
+import BoundaryResidualSharpening
+import BoundaryApproachActionElimination
+import BoundaryCanonicalGeometry
+import TrackThetaAllTime
+
+/-!
+# Elimination of the occurrence-support-damage residuals
+
+A noncanonical unchanged occurrence supplies a second repeated vector in the
+first manufacturing journey.  Replacing the ordinary sharp history core by
+the existing double-reduced boundary history therefore inserts the arbitrary
+pre-passage vector at no extra cost.  The changed-contact lead has exactly the
+same length as the ordinary compressed lead, while retaining that boundary
+vector.  The existing zero/two/one-novelty contact classification then counts
+time zero inside the `N+4` budget.
+-/
+
+namespace GeneralN
+
+/-- Pairing a grooved flip reflector with itself at equal endpoints collapses
+the general four-phase law to its two action phases. -/
+private theorem ManufacturedFlipReflector.same_endpoint_two_phase
+    {w : Wiring} {g e : Nat}
+    (R : ManufacturedFlipReflector w g e)
+    (hge : g = e)
+    (state : Tongues)
+    (hpaths : PathGrooves
+      (ManufacturedReflector.flip R).toSupported.paths state)
+    (d : Nat) :
+    exists port phase,
+      stepN w d (g, state) = some (port, phase) /\
+        (phase = state \/ phase = flipAt state R.actionSwitch) := by
+  subst e
+  obtain ⟨port, phase, hrun, hphase⟩ :=
+    manufactured_flip_pair_all_time_four_phase
+      R R state hpaths hpaths d
+  refine ⟨port, phase, hrun, ?_⟩
+  simp only [List.mem_cons, List.not_mem_nil, or_false] at hphase
+  rcases hphase with hstate | hfirst | hsecond | hboth
+  · exact Or.inl hstate
+  · exact Or.inr hfirst
+  · exact Or.inr hsecond
+  · exact Or.inl (by simpa [flipAt_flipAt] using hboth)
+
+/-- **The canonical unchanged saturation is impossible.**
+
+Canonicality forces an empty runway and a self-linked source.  The complete
+future after the first manufacture then has only the activated phase and its
+action mate.  Both manufacturing phases, `original`, and that one mate fit in
+a global history of size at most `N + 3`, contradicting saturation and global
+avoidance of `original`. -/
+theorem ProductiveBoundaryNAddFourSavingResidual.false_of_canonical_saturation
+    {w : Wiring} {N : Nat}
+    (S : ProductiveBoundaryNAddFourSavingResidual w N)
+    (hN : forall p q, w.link p = some q ->
+      p < 3 * N /\ q < 3 * N)
+    (R : ManufacturedFlipReflector w S.source.g S.source.e)
+    (hAeq : S.A = ManufacturedReflector.flip R)
+    (O : InitialEntryWriterOccurrence
+      w S.source.g S.source.e S.source.k0
+        (ManufacturedReflector.flip R))
+    (hstay : O.next = O.middle)
+    (hcanonical : O.before.length = R.runway.length) :
+    False := by
+  let A : ManufacturedReflector w S.source.g S.source.e :=
+    ManufacturedReflector.flip R
+  let firstTravel := A.exploration.length + A.runway.length + 1
+  let opposite := VectorCount.restrict N
+    (flipAt A.activatedState R.actionSwitch)
+  let history :=
+    O.reducedBoundaryHistory N S.source.original ++ [opposite]
+
+  have hgeometry := S.canonical_source_self_link R O hcanonical
+  have hge : S.source.g = S.source.e := hgeometry.1
+  have hApathsS : PathGrooves S.A.toSupported.paths
+      S.A.activatedState := by
+    rw [← S.activated]
+    exact S.grooves
+  have hApaths : PathGrooves A.toSupported.paths A.activatedState := by
+    simpa [A, hAeq] using hApathsS
+  have hAbase : A.baseState = S.source.base := by
+    simpa [A, hAeq] using S.reflector_base
+  have hreach : stepN w firstTravel
+      (S.source.g, S.source.base) =
+        some (S.source.e, A.activatedState) := by
+    simpa [firstTravel, A, hAeq, S.activated] using S.reached
+  have hreachSelf : stepN w firstTravel
+      (S.source.g, S.source.base) =
+        some (S.source.g, A.activatedState) := by
+    simpa [hge] using hreach
+
+  have hlengthReduced :=
+    O.reducedBoundaryHistory_length hN S.source.original
+  have hlength : history.length <= N + 3 := by
+    dsimp [history]
+    simp only [List.length_append, List.length_singleton]
+    omega
+  have horiginal : VectorCount.restrict N S.source.original ∈ history := by
+    apply List.mem_append_left
+    exact List.mem_cons_self
+  have hactivated : VectorCount.restrict N A.activatedState ∈
+      O.reducedBoundaryHistory N S.source.original := by
+    apply O.sharp_mem_reduced_of_stay S.source.original hstay
+    unfold ManufacturedReflector.sharpConstructionHistory
+    apply List.mem_append_right
+    exact List.mem_cons_self
+
+  have hglobal : forall d,
+      (stepN w d (S.source.g, S.source.base)).isSome ->
+      restrictedTonguesAt w N (S.source.g, S.source.base) d ∈
+        history := by
+    intro d _hdLive
+    by_cases hprefix : d <= firstTravel
+    · apply List.mem_append_left
+      apply O.sharp_mem_reduced_of_stay S.source.original hstay
+      have hm := A.manufacturing_journey_mem_sharpHistory
+        (N := N) hApaths (j := d)
+          (by simpa [firstTravel] using hprefix)
+      have hmR :
+          restrictedTonguesAt w N (S.source.g, S.source.base) d ∈
+            (ManufacturedReflector.flip R).sharpConstructionHistory N := by
+        simpa only [A, hAbase] using hm
+      exact hmR
+    · let q := d - firstTravel
+      have hdEq : d = firstTravel + q := by
+        dsimp [q]
+        omega
+      have hpathsR : PathGrooves
+          (ManufacturedReflector.flip R).toSupported.paths
+            (ManufacturedReflector.flip R).activatedState := by
+        simpa [A] using hApaths
+      obtain ⟨port, phase, hrun, hphase⟩ :=
+        R.same_endpoint_two_phase hge
+          (ManufacturedReflector.flip R).activatedState hpathsR q
+      have hrunGlobal :
+          stepN w d (S.source.g, S.source.base) =
+            some (port, phase) := by
+        rw [hdEq, stepN_add, hreachSelf]
+        simpa [A] using hrun
+      have hvector :
+          restrictedTonguesAt w N (S.source.g, S.source.base) d =
+            VectorCount.restrict N phase := by
+        simp [restrictedTonguesAt, tonguesAt, hrunGlobal]
+      rw [hvector]
+      rcases hphase with hphase | hphase
+      · apply List.mem_append_left
+        simpa [A, hphase] using hactivated
+      · apply List.mem_append_right
+        simp [opposite, A, hphase]
+
+  exact S.source.false_of_global_history
+    history (by omega) horiginal hglobal
+
+/-- Replace the first reflector's ordinary one-duplicate core in a changed
+contact lead by the two-duplicate boundary history. -/
+noncomputable def InitialEntryWriterOccurrence.doubleReducedContactLead
+    {w : Wiring} {N g e k0 : Nat}
+    {R : ManufacturedFlipReflector w g e}
+    (O : InitialEntryWriterOccurrence w g e k0
+      (ManufacturedReflector.flip R))
+    (C : SimpleContinuationChangedContact w
+      (ManufacturedReflector.flip R))
+    (original : Tongues) : List (List Bool) :=
+  O.doubleReducedBoundaryHistory N original ++
+    ((rawFirstWriterHistory w N
+      (e, (ManufacturedReflector.flip R).activatedState)
+      C.approach.length).erase
+        (VectorCount.restrict N
+          (ManufacturedReflector.flip R).activatedState) ++
+      [VectorCount.restrict N C.nextState])
+
+/-- The replacement lead contains the arbitrary boundary vector. -/
+theorem InitialEntryWriterOccurrence.original_mem_doubleReducedContactLead
+    {w : Wiring} {N g e k0 : Nat}
+    {R : ManufacturedFlipReflector w g e}
+    (O : InitialEntryWriterOccurrence w g e k0
+      (ManufacturedReflector.flip R))
+    (C : SimpleContinuationChangedContact w
+      (ManufacturedReflector.flip R))
+    (original : Tongues) :
+    VectorCount.restrict N original ∈
+      O.doubleReducedContactLead (N := N) C original := by
+  unfold InitialEntryWriterOccurrence.doubleReducedContactLead
+  apply List.mem_append_left
+  exact List.mem_cons_self
+
+/-- A noncanonical occurrence replacement has exactly the same size as the
+ordinary compressed changed-contact lead. -/
+theorem InitialEntryWriterOccurrence.doubleReducedContactLead_length_eq
+    {w : Wiring} {N g e k0 : Nat}
+    {R : ManufacturedFlipReflector w g e}
+    (O : InitialEntryWriterOccurrence w g e k0
+      (ManufacturedReflector.flip R))
+    (C : SimpleContinuationChangedContact w
+      (ManufacturedReflector.flip R))
+    (original : Tongues)
+    (hdifferent : O.before.length ≠ R.runway.length) :
+    (O.doubleReducedContactLead (N := N) C original).length =
+      (C.compressedLead N).length := by
+  unfold InitialEntryWriterOccurrence.doubleReducedContactLead
+  unfold SimpleContinuationChangedContact.compressedLead
+  simp only [List.length_append]
+  rw [O.doubleReducedBoundaryHistory_length original hdifferent,
+    (ManufacturedReflector.flip R).sharpHistoryCore_length]
+
+/-- Every ordinary compressed-lead vector is retained by the occurrence
+replacement. -/
+theorem InitialEntryWriterOccurrence.mem_doubleReducedContactLead_of_mem_compressedLead
+    {w : Wiring} {N g e k0 : Nat}
+    {R : ManufacturedFlipReflector w g e}
+    (O : InitialEntryWriterOccurrence w g e k0
+      (ManufacturedReflector.flip R))
+    (C : SimpleContinuationChangedContact w
+      (ManufacturedReflector.flip R))
+    (original : Tongues)
+    (hstay : O.next = O.middle)
+    (hdifferent : O.before.length ≠ R.runway.length)
+    {x : List Bool}
+    (hx : x ∈ C.compressedLead N) :
+    x ∈ O.doubleReducedContactLead (N := N) C original := by
+  unfold SimpleContinuationChangedContact.compressedLead at hx
+  unfold InitialEntryWriterOccurrence.doubleReducedContactLead
+  rcases List.mem_append.mp hx with hxFirst | hxTail
+  · apply List.mem_append_left
+    apply O.sharp_mem_doubleReducedBoundaryHistory original
+      hstay hdifferent
+    exact List.mem_of_mem_erase hxFirst
+  · exact List.mem_append_right _ hxTail
+
+/-- A local novelty cover over the ordinary compressed lead lifts across the
+first manufacturing journey to the boundary-replacement lead. -/
+theorem InitialEntryWriterOccurrence.doubleReducedContactLead_global_cover
+    {w : Wiring} {N g e k0 budget : Nat}
+    {R : ManufacturedFlipReflector w g e}
+    (O : InitialEntryWriterOccurrence w g e k0
+      (ManufacturedReflector.flip R))
+    (C : SimpleContinuationChangedContact w
+      (ManufacturedReflector.flip R))
+    (original : Tongues)
+    (hstay : O.next = O.middle)
+    (hdifferent : O.before.length ≠ R.runway.length)
+    (hA : PathGrooves
+      (ManufacturedReflector.flip R).toSupported.paths
+      (ManufacturedReflector.flip R).activatedState)
+    (times : List Nat)
+    (hlive : ∀ k ∈ times,
+      (stepN w k
+        (g, (ManufacturedReflector.flip R).baseState)).isSome)
+    (hlocal : NoveltyCoverOn w N
+      (e, (ManufacturedReflector.flip R).activatedState)
+      (times.map (fun k => k -
+        ((ManufacturedReflector.flip R).exploration.length +
+          (ManufacturedReflector.flip R).runway.length + 1)))
+      (C.compressedLead N) budget) :
+    NoveltyCoverOn w N
+      (g, (ManufacturedReflector.flip R).baseState) times
+      (O.doubleReducedContactLead (N := N) C original) budget := by
+  let A : ManufacturedReflector w g e := ManufacturedReflector.flip R
+  let firstTravel := A.exploration.length + A.runway.length + 1
+  let localTimes := times.map (fun k => k - firstTravel)
+  have hreach : stepN w firstTravel (g, A.baseState) =
+      some (e, A.activatedState) := by
+    simpa [firstTravel, A] using
+      A.manufacturing_journey_reaches_activated hA
+  have hlocal' : NoveltyCoverOn w N (e, A.activatedState)
+      localTimes (C.compressedLead N) budget := by
+    simpa [localTimes, firstTravel, A] using hlocal
+  obtain ⟨fresh, hfresh, hlocalMem⟩ := hlocal'
+  refine ⟨fresh, hfresh, ?_⟩
+  intro k hk
+  by_cases hfirst : k ≤ firstTravel
+  · apply List.mem_append_left
+    unfold InitialEntryWriterOccurrence.doubleReducedContactLead
+    apply List.mem_append_left
+    apply O.sharp_mem_doubleReducedBoundaryHistory original
+      hstay hdifferent
+    exact A.manufacturing_journey_mem_sharpHistory hA (by
+      simpa [firstTravel] using hfirst)
+  · let d := k - firstTravel
+    have hdMem : d ∈ localTimes := by
+      dsimp [d, localTimes]
+      exact List.mem_map.mpr ⟨k, hk, rfl⟩
+    have hm := hlocalMem d hdMem
+    have hshift := restrictedTonguesAt_sub_of_reach
+      (N := N) hreach (by omega) (hlive k hk)
+    rw [hshift]
+    rcases List.mem_append.mp hm with hmHistory | hmFresh
+    · apply List.mem_append_left
+      exact O.mem_doubleReducedContactLead_of_mem_compressedLead
+        (N := N) C original hstay hdifferent hmHistory
+    · exact List.mem_append_right _ hmFresh
+
+/-- Count the arbitrary boundary vector together with a changed-contact run
+using the occurrence replacement lead. -/
+theorem InitialEntryWriterOccurrence.doubleReducedContactLead_count
+    {w : Wiring} {N g e k0 budget : Nat}
+    {R : ManufacturedFlipReflector w g e}
+    (O : InitialEntryWriterOccurrence w g e k0
+      (ManufacturedReflector.flip R))
+    (C : SimpleContinuationChangedContact w
+      (ManufacturedReflector.flip R))
+    (original : Tongues)
+    (hstay : O.next = O.middle)
+    (hdifferent : O.before.length ≠ R.runway.length)
+    (hA : PathGrooves
+      (ManufacturedReflector.flip R).toSupported.paths
+      (ManufacturedReflector.flip R).activatedState)
+    (times : List Nat)
+    (hlive : ∀ k ∈ times,
+      (stepN w k
+        (g, (ManufacturedReflector.flip R).baseState)).isSome)
+    (hnd : (VectorCount.restrict N original ::
+      times.map (restrictedTonguesAt w N
+        (g, (ManufacturedReflector.flip R).baseState))).Nodup)
+    (hlocal : NoveltyCoverOn w N
+      (e, (ManufacturedReflector.flip R).activatedState)
+      (times.map (fun k => k -
+        ((ManufacturedReflector.flip R).exploration.length +
+          (ManufacturedReflector.flip R).runway.length + 1)))
+      (C.compressedLead N) budget) :
+    times.length + 1 ≤
+      (O.doubleReducedContactLead (N := N) C original).length + budget := by
+  have hcover := O.doubleReducedContactLead_global_cover
+    (N := N) C original hstay hdifferent hA times hlive hlocal
+  exact novelty_cover_count_with_historical_extra
+    (VectorCount.restrict N original) hcover
+      (O.original_mem_doubleReducedContactLead (N := N) C original) hnd
+
+
+
+/-- A saturated productive boundary cannot contain a changed contact after a
+noncanonical unchanged occurrence of its first flip reflector. -/
+theorem ProductiveBoundaryNAddFourSavingResidual.false_of_noncanonical_occurrence_flip_changed_contact
+    {w : Wiring} {N : Nat}
+    (S : ProductiveBoundaryNAddFourSavingResidual w N)
+    (hN : forall p q, w.link p = some q ->
+      p < 3 * N /\ q < 3 * N)
+    (R : ManufacturedFlipReflector w S.source.g S.source.e)
+    (hAeq : S.A = ManufacturedReflector.flip R)
+    (O : InitialEntryWriterOccurrence
+      w S.source.g S.source.e S.source.k0
+        (ManufacturedReflector.flip R))
+    (hstay : O.next = O.middle)
+    (hdifferent : O.before.length ≠ R.runway.length)
+    (D : PartialSecondRunSharp.ChangedContact w
+      (ManufacturedReflector.flip R)) : False := by
+  let C := D.toSimpleContinuationChangedContact
+  have hApathsS : PathGrooves S.A.toSupported.paths
+      S.A.activatedState := by
+    rw [← S.activated]
+    exact S.grooves
+  have hA : PathGrooves
+      (ManufacturedReflector.flip R).toSupported.paths
+      (ManufacturedReflector.flip R).activatedState := by
+    simpa [hAeq] using hApathsS
+  have hAbase : (ManufacturedReflector.flip R).baseState =
+      S.source.base := by
+    simpa [hAeq] using S.reflector_base
+  have hlive : forall k, k ∈ S.source.times ->
+      (stepN w k
+        (S.source.g,
+          (ManufacturedReflector.flip R).baseState)).isSome := by
+    intro k hk
+    simpa [hAbase] using S.source.live k hk
+  have hnd : (VectorCount.restrict N S.source.original ::
+      S.source.times.map (restrictedTonguesAt w N
+        (S.source.g,
+          (ManufacturedReflector.flip R).baseState))).Nodup := by
+    simpa [hAbase] using S.source.distinct
+  let localTimes := S.source.times.map (fun k => k -
+    ((ManufacturedReflector.flip R).exploration.length +
+      (ManufacturedReflector.flip R).runway.length + 1))
+  have hsaturated := S.source.saturated
+  rcases C.direction with hbackward |
+      ⟨hforward, repaired, hrepair, hrestored⟩
+  · have hlocal := C.backward_all_time_zero_novelty
+      (N := N) hbackward localTimes
+    have hcount := O.doubleReducedContactLead_count
+      (N := N) C S.source.original hstay hdifferent hA
+        S.source.times hlive hnd (by
+          simpa [localTimes] using hlocal)
+    have hlengthEq := O.doubleReducedContactLead_length_eq
+      (N := N) C S.source.original hdifferent
+    have hlength := C.compressedLead_length_le hN hA
+    omega
+  · by_cases haction :
+        R.actionSwitch ∈ C.approachFirstWriterSwitches N
+    · rcases C.forward_flip_one_novelty_or_runway_residual
+          hforward hrepair hrestored haction localTimes with
+        hone | hresidual
+      · have hcount := O.doubleReducedContactLead_count
+          (N := N) C S.source.original hstay hdifferent hA
+            S.source.times hlive hnd (by
+              simpa [localTimes] using hone)
+        have hlengthEq := O.doubleReducedContactLead_length_eq
+          (N := N) C S.source.original hdifferent
+        have hlength := C.compressedLead_length_le hN hA
+        omega
+      · exact (Classical.choice hresidual).impossible hN hA
+    · have hlocal := C.changed_two_novelty (N := N) localTimes
+      have hcount := O.doubleReducedContactLead_count
+        (N := N) C S.source.original hstay hdifferent hA
+          S.source.times hlive hnd (by
+            simpa [localTimes] using hlocal)
+      have hlengthEq := O.doubleReducedContactLead_length_eq
+        (N := N) C S.source.original hdifferent
+      have hlength :=
+        C.compressedLead_length_le_N_add_two_of_action_absent
+          hN hA haction
+      omega
+
+
+
+
+/-- Every changed contact after an unchanged initial-switch occurrence is
+incompatible with a saturated productive boundary.  Stay reflectors already
+have the `N+3` saving; for flip reflectors, the canonical occurrence is the
+existing saturation obstruction and every noncanonical occurrence is covered
+by the double-reduced lead above. -/
+theorem ProductiveBoundaryNAddFourSavingResidual.false_of_occurrence_changed_contact
+    {w : Wiring} {N : Nat}
+    (S : ProductiveBoundaryNAddFourSavingResidual w N)
+    (hN : forall p q, w.link p = some q ->
+      p < 3 * N /\ q < 3 * N)
+    (O : InitialEntryWriterOccurrence
+      w S.source.g S.source.e S.source.k0 S.A)
+    (hstay : O.next = O.middle)
+    (D : PartialSecondRunSharp.ChangedContact w S.A) : False := by
+  generalize hAeq : S.A = A at O hstay D
+  cases A with
+  | stay R =>
+      have hApathsS : PathGrooves S.A.toSupported.paths
+          S.A.activatedState := by
+        rw [← S.activated]
+        exact S.grooves
+      have hA : PathGrooves
+          (ManufacturedReflector.stay R).toSupported.paths
+          (ManufacturedReflector.stay R).activatedState := by
+        simpa [hAeq] using hApathsS
+      have hAbase : (ManufacturedReflector.stay R).baseState =
+          S.source.base := by
+        simpa [hAeq] using S.reflector_base
+      have hlive : forall k, k ∈ S.source.times ->
+          (stepN w k
+            (S.source.g,
+              (ManufacturedReflector.stay R).baseState)).isSome := by
+        intro k hk
+        simpa [hAbase] using S.source.live k hk
+      have hnd : (S.source.times.map
+          (restrictedTonguesAt w N
+            (S.source.g,
+              (ManufacturedReflector.stay R).baseState))).Nodup := by
+        have htail := (List.nodup_cons.mp S.source.distinct).2
+        simpa [hAbase] using htail
+      have hbound := D.stay_saving_all_run_distinct_le_N_add_three
+        hN hA S.source.times hlive hnd
+      have hsaturated := S.source.saturated
+      omega
+  | flip R =>
+      by_cases hcanonical : O.before.length = R.runway.length
+      · exact S.false_of_canonical_saturation
+          hN R hAeq O hstay hcanonical
+      · exact S.false_of_noncanonical_occurrence_flip_changed_contact
+          hN R hAeq O hstay hcanonical D
+
+
+end GeneralN
diff --git a/theory/lean/README.md b/theory/lean/README.md
index a6f6cff..ddf98b7 100644
--- a/theory/lean/README.md
+++ b/theory/lean/README.md
@@ -1,161 +1,136 @@
-# Formal proofs (Lean 4): the state law
+# Formal proofs (Lean 4): the sharp state law
 
-**The state law is proved, from both sides, one unit apart.**  A single
-train on any `N`-switch lazy-point layout visits at most `N + 5`
-distinct tongue vectors, and for every `N ≥ 3` there is a layout on
-which it visits `N + 4`:
+**The state law is sharp.** A single train on any `N`-switch lazy-point
+layout visits at most `N + 4` distinct tongue vectors. For every `N ≥ 3`
+there is a layout on which it visits exactly `N + 4`; the exact small values
+are `f(1) = 2` and `f(2) = 4`. Together with the finite-state ceiling this
+gives
 
 ```
-GeneralN.state_law_N_add_five               -- StateLawNAddFive.lean
-GeneralN.knownIncomingEdgeNAddFour          -- KnownEdgeNAddFourComplete.lean
-GeneralN.state_law_lower_bound              -- StateLawLowerBound.lean
-GeneralN.stateLaw              : StateLaw   -- KnownEdgeNAddFiveAlt.lean (N+6 form)
+f(N) = min(2^N, N + 4)       (N ≥ 1).
 ```
 
-The raw statement (`StateLaw.lean`) is over `Wiring`/`stepN` — for every
-wiring `w` on switches `0 … N-1`, every start configuration, and every
-duplicate-free list of live sample times, the sampled restricted tongue
-vectors number at most `N + 5` (`state_law_N_add_five`; the historical
-`N + 6` definition `StateLaw` follows a fortiori).  The lower bound
-produces, for every `N ≥ 3`, a wiring on switches `0 … N-1`, a start
-configuration, and `N + 4` live sample times whose tongue vectors are
-pairwise distinct.  All proofs are fully symbolic in `N`: no small-`N`
-enumeration, no conditional hypothesis, no Mathlib, no `native_decide`,
-no `sorry`.  (The lower bound's `N = 3` base case is checked by kernel
-`decide`; `N ≥ 4` is the symbolic trajectory.)
-
-Two hundred and fifty-seven libraries, all self-contained.  To check
-everything:
+Headline theorems:
 
 ```
-lake build                      # builds all 257 libraries
-lake build StateLawAxiomAudit   # prints the axioms of the headline theorems
+GeneralN.state_law_N_add_four             -- StateLawNAddFourSharp.lean
+GeneralN.knownIncomingEdgeNAddFour        -- KnownEdgeNAddFourComplete.lean
+GeneralN.productiveInitialBoundaryNAddFour -- StateLawNAddFourSharp.lean
+GeneralN.state_law_lower_bound            -- StateLawLowerBound.lean
 ```
 
-`StateLawAxiomAudit.lean` runs `#print axioms` on the headline
-theorems; the output is exactly `[propext, Classical.choice,
-Quot.sound]` — the three standard Lean axioms.  The `state-law-check`
-workflow repeats both steps on every push.
+The raw upper-bound statement (`StateLawNAddFour.lean`) is over
+`Wiring`/`stepN`: for every wiring `w` on switches `0 … N-1`, every start
+configuration, and every duplicate-free list of live sample times, the
+sampled restricted tongue vectors number at most `N + 4`. The proof is fully
+symbolic in `N`: no finite-instance argument, no Mathlib, no `native_decide`,
+and no `sorry`. The lower bound is also symbolic for `N ≥ 4`; its `N = 3`
+base case is checked by kernel `decide`.
+
+There are 262 self-contained Lean libraries. To check everything:
+
+```
+lake build
+lake build StateLawAxiomAudit
+```
+
+`StateLawAxiomAudit.lean` runs `#print axioms` on the headline theorems. The
+sharp upper bound depends only on `[propext, Classical.choice, Quot.sound]`,
+the three standard Lean axioms, and not on `sorryAx`. The
+`state-law-check` workflow repeats the full build and audit on every push to
+`main`.
 
 ## How to read the statement
 
-* A **wiring** `w` is a track layout: switch `k` owns three ports — its
-  stem `3*k`, its left branch `3*k+1`, its right branch `3*k+2` — and
-  `w.link` records which port is track-connected to which (symmetric,
-  because physical track is).
+* A **wiring** `w` is a track layout: switch `k` owns three ports — its stem
+  `3*k`, left branch `3*k+1`, and right branch `3*k+2` — while `w.link`
+  records the symmetric physical track connection.
 * `hN` says the layout uses only switches `0 … N-1`.
-* `stepN` drives the single train one track-piece at a time under the
-  **lazy-point rule**: entering a switch at its stem follows the tongue
-  unchanged; entering at a branch always exits at the stem and, if the
-  tongue pointed at the other branch, flips it.
-* `tonguesAt`/`restrictedTonguesAt` read off the `N` tongue directions at
-  a given time — the *tongue vector*, the machine state of the layout.
-
-## Shape of the lower bound
-
-`StateLawLowerBound.lean` wires the extremal family symbolically: switch
-`0` is a teardrop (branches tied, stem wired to switch `1`'s stem),
-switches `1 … N-3` form a branch-to-stem chain, and switches
-`N-2, N-1` are doubly linked (branch1–stem and branch2–branch2).  A cold
-run started into branch 2 of switch `N-2` flips the chain down to the
-teardrop — one fresh vector per switch — rides back, closes the far
-switch, and then walks a four-corner Gray oscillation on switches `N-2`
-and `0`.  The `N + 4` sample times are
-`0, 1, …, N-2, N, 2N-1, 2N, 3N-1, 4N-1`; the trajectory is proved by
-phase inductions, and pairwise distinctness by explicit witnessing
-coordinates.
-
-## Shape of the upper bound
-
-The core theorem (`knownIncomingEdgeNAddFour`, assembled in
-`KnownEdgeNAddFourComplete.lean` from `ProtectedPairNAddFour.lean` and
-`KnownEdgeNAddFourChangedClosed.lean`) bounds every run whose incoming
-physical edge is known by `N + 4`, with no liveness horizon: wherever
-the run dies, the samples so far are covered by the same histories.
-Its branches — first death, settling on a stable cycle, a first
-support-changing contact after one manufactured reflector, and a
-support-protected pair of opposite reflectors — are all charged into
-**one shared `N`-coordinate construction history**; in the formerly
-limiting protected-pair branch the activated state, the pre-return
-state, *and* the action-flipped pre-return state are all historical, so
-the repair tail contributes at most one fresh vector.  Lifting an
-arbitrary start past its first successful step
-(`arbitrary_start_distinct_le_succ_of_all_known_edge`) costs at most
-the time-zero vector: `N + 5` (`state_law_N_add_five`).  The older
-`N + 5` known-edge core `known_edge_all_run_distinct_le_N_add_five`
-and its `N + 6` assembly `stateLaw` are kept as the historical route.
-
-The supporting layers, bottom to top: the raw track dynamics and
-first-revisit normal forms (`TrackTrace`, `TrackLobe`,
-`TrackNormalForm`, `TrackTheta`); manufactured reflectors, their repairs
-and quantitative lassos (`TrackGlobalRepair`, `TrackQuantitative*`);
-pointwise tongue-phase laws — every traversal shows two phases, every
-capture two, every repairing traversal three, every reflector pair four
-corners, protected repair prefixes two
-(`ManufacturedPairNovelty`, `TrackThetaPointwiseCore`,
-`TrackThetaAllTime`, `RepairLeadTwoPhase`, `TrackStayContactAllTime`,
-`TrackStaySpliceAllTime`); constant tongue counts for every repair
-branch (`*Constant`, `*Count*`, `ProtectedRepair*`); and the history
-assemblies that share one `N`-coordinate budget across branches
-(`TwoHistoryUnionCharge`, `StateLawTwoSixUltra`,
-`StateLawCoefficientOneTop`, `KnownEdgeNAddFiveAlt`).
+* `stepN` drives the train one track piece at a time under the lazy-point
+  rule: entering at a stem follows the tongue unchanged; entering at a
+  branch exits at the stem and flips the tongue when necessary.
+* `tonguesAt` / `restrictedTonguesAt` read the `N` tongue directions at a
+  given time — the machine state of the layout.
+
+## Lower bound
+
+`StateLawLowerBound.lean` wires the extremal family symbolically. Switch `0`
+is a teardrop; switches `1 … N-3` form a branch-to-stem chain; and switches
+`N-2, N-1` are doubly linked. A cold run flips the chain down to the
+teardrop, rides back, closes the far switch, and then walks a four-corner
+Gray oscillation on switches `N-2` and `0`.
+
+The `N + 4` sample times are
+
+```
+0, 1, …, N-2, N, 2N-1, 2N, 3N-1, 4N-1.
+```
+
+Their trajectory is proved by phase inductions and their pairwise
+distinctness by explicit witnessing coordinates.
+
+## Upper bound
+
+The known-incoming-edge core (`knownIncomingEdgeNAddFour`) already bounded
+every shifted run by `N + 4`. Its death, stable-cycle, support-changing
+contact, and protected-reflector-pair branches are charged into one shared
+`N`-coordinate construction history.
+
+The only remaining issue was an arbitrary productive first passage: could
+its time-zero vector be genuinely new on top of the shifted known-edge
+budget? `BoundaryResidualSharpening.lean` reduced that question to four
+constructors. The new closing files eliminate all four:
+
+* `BoundaryApproachActionElimination.lean` proves that a strict simple
+  approach from the boundary stem cannot first-write the boundary switch.
+  If it first-writes the old flip action instead, the tail has only one new
+  corner, so the reserved boundary coordinate still yields `N + 3`.
+* `BoundaryApproachWrittenElimination.lean` packages that charge to rule out
+  the complete approach-written residual.
+* `BoundaryAbsentPresentWriterElimination.lean` proves that the second
+  manufacture, which also starts at the boundary stem, cannot productively
+  first-write that switch. This kills the absent-present writer residual.
+* `BoundaryOccurrenceDamageElimination.lean` handles both remaining support
+  damage cases. A canonical unchanged occurrence forces a self-linked first
+  reflector whose future has only two action phases, so a global `N+3`
+  history contradicts saturation. A noncanonical occurrence gives two
+  duplicate positions in the first manufacturing journey; the double-reduced
+  boundary history has exactly the ordinary compressed lead's length but also
+  contains the arbitrary time-zero vector. The existing zero/two/one-novelty
+  changed-contact classification therefore fits time zero inside `N + 4`.
+
+`StateLawNAddFourSharp.lean` combines these eliminations with
+`productiveInitialBoundaryNAddFour_iff_no_sharp_residual`, then applies the
+exact arbitrary-start wrapper from `StateLawNAddFourTop.lean`.
 
 ## Auxiliary files
 
-* `DuplotrainProofs.lean` — the exhaustive small-`N` results (by
-  `native_decide`, deliberately outside the symbolic proof): the exact
-  state counts `f(1) = 2`, `f(2) = 4`, `f(3) = 7`, `f(4) = 8`, the
-  perfect-layout classification, and the ≥3-switch imperfection sweep.
-  These are the empirical anchors of the remaining conjecture.
-* `FamilyLowerBound.lean` — `native_decide` instances of the same
-  family for `N = 3 … 8`, checking the *exact* maximum: over all starts
-  the family realizes exactly `N+4` distinct vectors (the symbolic
-  theorem only exhibits `N+4`; these instances confirm the family
-  itself does no better).  Discovered and cross-checked by
-  `../tools/bstates.py`; a 60,000-wiring random probe at `N = 5` found
-  nothing above `N+4`.
-* `StateLawAxiomAudit.lean` — the permanent axiom check described above.
-
-## What remains open
-
-The conjectured sharp form is `f(N) = min(2^N, N + 4)`; the proved
-bounds are `N + 4 ≤ f(N) ≤ N + 5` for every `N ≥ 3` (exhaustively
-sharp at `N + 4` for `N ≤ 4`).  The remaining gap is exactly **one
-additive unit**: the time-zero vector of the arbitrary-start lift.
-Since the known-edge bound is already `N + 4`, the sharp law is
-equivalent to showing that a *productive* first passage (one that flips
-a switch on its very first step) cannot add a genuinely new vector
-beyond the shifted known-edge budget.  `StateLawNAddFour.lean` states
-the sharp target as a `def`; `StateLawNAddFourTop.lean` proves it from
-the single residual obligation `ProductiveInitialBoundaryNAddFour`;
-`ProductiveBoundaryNAddFourComplete.lean` proves that obligation
-equivalent to eliminating three concrete residual geometries; and
-`BoundaryChangedContactSaving.lean` /
-`BoundaryResidualSharpening.lean` sharpen the frontier further
-(`productiveInitialBoundaryNAddFour_iff_no_sharp_residual`).  The
-keystone: reserving both the flip action switch and the
-exploration-absent boundary switch lowers a changed contact's budget to
-`N+3`, so under the absent saving both support-damage residuals
-collapse into one geometry.  What remains is exactly four constructors:
-
-1. an **approach-written flip contact** — a flip first reflector whose
-   changed contact productively first-writes its action switch or the
-   boundary switch during the strict approach;
-2. / 3. **support damage under the occurrence saving** (the boundary
-   switch is stay-crossed inside the first exploration) — the cycle and
-   opposite-reflector damage cases;
-4. the **absent-present writer** — a flip-first protected pair whose
-   boundary switch reappears among the second construction's first
-   writers.
-
-Killing those four constructors is the entire remaining distance to
-`f(N) = N + 4`.
+* `DuplotrainProofs.lean` exhaustively checks the small values
+  `f(1) = 2`, `f(2) = 4`, `f(3) = 7`, and `f(4) = 8`, as well as the
+  perfect-layout classification. These finite results deliberately use
+  `native_decide`; they are separate from the symbolic upper bound.
+* `FamilyLowerBound.lean` checks instances of the extremal family for
+  `N = 3 … 8`; the general construction is proved in
+  `StateLawLowerBound.lean`.
+* The older `N+5` and `N+6` routes remain in the tree as independently
+  checked historical proofs.
+
+## Independent open directions
+
+The sharp state-count law itself is closed. The echo-machine programme in
+`../lazy-point-theory.md` still contains open Gray-tail and transient lemmas;
+those would provide a different proof and stronger structural information,
+but are no longer needed for the `N + 4` bound.
 
 ## History
 
-This proof is the end of a bound-tightening campaign
-(`26N+3 → 24N+5 → 18N+3 → 17N+5 → 15N+7 → 14N+9 → 8N+7 → 5N+9 → 3N+7 →
-2N+9 → N+7 → N+6 → N+5`).  The full 391-library development — including
-the superseded linear-bound stages and the echo-machine/four-beat-law
-program aimed at the sharp constant — is preserved in git history;
-commit `2b75dd8` is the last state before the big cleanup.
+The bound-tightening campaign is now complete:
+
+```
+26N+3 → 24N+5 → 18N+3 → 17N+5 → 15N+7 → 14N+9
+→ 8N+7 → 5N+9 → 3N+7 → 2N+9 → N+7 → N+6 → N+5 → N+4.
+```
+
+The superseded stages and the echo-machine/four-beat-law programme remain
+available in git history; commit `2b75dd8` is the last state before the large
+cleanup of those historical libraries.
diff --git a/theory/lean/StateLawAxiomAudit.lean b/theory/lean/StateLawAxiomAudit.lean
index 30b6e25..3e9f421 100644
--- a/theory/lean/StateLawAxiomAudit.lean
+++ b/theory/lean/StateLawAxiomAudit.lean
@@ -1,22 +1,25 @@
+import StateLawNAddFourSharp
 import StateLawNAddFive
 import StateLawLowerBound
 
 /-!
 # Axiom audit for the state law
 
-`#print axioms` on the headline theorems — the `N + 5` upper bound, its
-known-incoming-edge `N + 4` core, the historical `StateLaw` target, and
-the `N + 4` lower bound.  The expected output is at most the three
-standard Lean axioms (`propext`, `Classical.choice`, `Quot.sound`) — in
-particular **no** `sorryAx`.
+`#print axioms` on the sharp `N + 4` upper bound, its known-incoming-edge
+core, the historical `N + 5` / `StateLaw` routes, and the matching `N + 4`
+lower bound. The expected output is at most the three standard Lean axioms
+(`propext`, `Classical.choice`, `Quot.sound`) — in particular **no**
+`sorryAx`.
 -/
 
 namespace GeneralN
 
-#print axioms state_law_N_add_five
+#print axioms state_law_N_add_four
 
 #print axioms knownIncomingEdgeNAddFour
 
+#print axioms state_law_N_add_five
+
 #print axioms stateLaw_via_N_add_five
 
 #print axioms state_law_lower_bound
diff --git a/theory/lean/StateLawNAddFourSharp.lean b/theory/lean/StateLawNAddFourSharp.lean
new file mode 100644
index 0000000..ff62dd4
--- /dev/null
+++ b/theory/lean/StateLawNAddFourSharp.lean
@@ -0,0 +1,74 @@
+import BoundaryApproachWrittenElimination
+import BoundaryAbsentPresentWriterElimination
+import BoundaryOccurrenceDamageElimination
+
+/-!
+# Sharp `N+4` state law
+
+This file eliminates the four residual constructors isolated by
+`BoundaryResidualSharpening` and closes the remaining arbitrary-start unit.
+The known-incoming-edge theorem was already `N+4`; the result below proves
+that the time-zero vector of a productive first passage is always historical.
+-/
+
+namespace GeneralN
+
+/-- Every constructor in the final productive-boundary residual is
+physically impossible. -/
+theorem BoundarySharpResidual.impossible
+    {w : Wiring} {N : Nat}
+    (hN : forall p q, w.link p = some q ->
+      p < 3 * N /\ q < 3 * N)
+    {S : ProductiveBoundaryNAddFourSavingResidual w N}
+    (D : BoundarySharpResidual S) : False := by
+  cases D with
+  | approachWritten D =>
+      exact D.impossible hN
+  | occurrenceCycleDamage O hstay C damage =>
+      have hA : PathGrooves S.A.toSupported.paths
+          S.A.activatedState := by
+        rw [← S.activated]
+        exact S.grooves
+      obtain ⟨contact⟩ :=
+        PartialSecondRunSharp.ManufacturedReflector.changedContact_of_broken_simple
+          S.A hA C.lead_trace C.lead_simple damage
+      exact S.false_of_occurrence_changed_contact
+        hN O hstay contact
+  | occurrenceReflectorDamage O hstay P damage =>
+      have hA : PathGrooves S.A.toSupported.paths
+          S.A.activatedState := by
+        rw [← S.activated]
+        exact S.grooves
+      have htrace : PhysicalTrace w
+          (S.source.e, S.A.activatedState)
+          P.reflector.exploration P.reflector.preReturn := by
+        simpa [P.base] using P.reflector.exploration_trace
+      obtain ⟨contact⟩ :=
+        PartialSecondRunSharp.ManufacturedReflector.changedContact_of_broken_simple
+          S.A hA htrace P.reflector.exploration_simple damage
+      exact S.false_of_occurrence_changed_contact
+        hN O hstay contact
+  | absentPresentWriter R kind absentA P supportGrooved present =>
+      exact BoundarySharpResidual.absentPresentWriter_impossible
+        R kind absentA P supportGrooved present
+
+/-- The productive arbitrary-start boundary fits the exact `N+4` budget. -/
+theorem productiveInitialBoundaryNAddFour
+    {w : Wiring} {N : Nat}
+    (hN : forall p q, w.link p = some q ->
+      p < 3 * N /\ q < 3 * N) :
+    ProductiveInitialBoundaryNAddFour w N := by
+  apply (productiveInitialBoundaryNAddFour_iff_no_sharp_residual hN).2
+  intro S D
+  exact D.impossible hN
+
+/-- **Sharp state law.**  A single train on any finite `N`-switch lazy-point
+layout visits at most `N+4` pairwise-distinct tongue vectors. -/
+theorem state_law_N_add_four : StateLawNAddFour := by
+  apply stateLawNAddFour_of_known_edge_and_productive_boundary
+  · intro w N hN
+    exact knownIncomingEdgeNAddFour hN
+  · intro w N hN
+    exact productiveInitialBoundaryNAddFour hN
+
+end GeneralN
diff --git a/theory/lean/lakefile.toml b/theory/lean/lakefile.toml
index 5816e8d..dbf8510 100644
--- a/theory/lean/lakefile.toml
+++ b/theory/lean/lakefile.toml
@@ -12,11 +12,15 @@ defaultTargets = [
   "BlockSparseFixedCountCore",
   "BoundaryAbsentProtectedPair",
   "BoundaryAbsentSecondWriter",
+  "BoundaryAbsentPresentWriterElimination",
+  "BoundaryApproachActionElimination",
+  "BoundaryApproachWrittenElimination",
   "BoundaryCanonicalGeometry",
   "BoundaryCanonicalOriginalOverlap",
   "BoundaryChangedContactSaving",
   "BoundaryDoubleDuplicate",
   "BoundaryNAddFourSaturation",
+  "BoundaryOccurrenceDamageElimination",
   "BoundaryOverlapTailCount",
   "BoundaryPresentSecondWriter",
   "BoundaryResidualCharge",
@@ -183,6 +187,7 @@ defaultTargets = [
   "StateLawLowerBound",
   "StateLawNAddFive",
   "StateLawNAddFour",
+  "StateLawNAddFourSharp",
   "StateLawNAddFourTop",
   "StateLawThreeSharp",
   "StateLawTwoCandidate",
@@ -295,6 +300,15 @@ name = "BoundaryAbsentProtectedPair"
 [[lean_lib]]
 name = "BoundaryAbsentSecondWriter"
 
+[[lean_lib]]
+name = "BoundaryAbsentPresentWriterElimination"
+
+[[lean_lib]]
+name = "BoundaryApproachActionElimination"
+
+[[lean_lib]]
+name = "BoundaryApproachWrittenElimination"
+
 [[lean_lib]]
 name = "BoundaryCanonicalGeometry"
 
@@ -310,6 +324,9 @@ name = "BoundaryDoubleDuplicate"
 [[lean_lib]]
 name = "BoundaryNAddFourSaturation"
 
+[[lean_lib]]
+name = "BoundaryOccurrenceDamageElimination"
+
 [[lean_lib]]
 name = "BoundaryOverlapTailCount"
 
@@ -808,6 +825,9 @@ name = "StateLawNAddFive"
 [[lean_lib]]
 name = "StateLawNAddFour"
 
+[[lean_lib]]
+name = "StateLawNAddFourSharp"
+
 [[lean_lib]]
 name = "StateLawNAddFourTop"