Prove the sharp N+4 state law

.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

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

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).

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.
 
 ---
 

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