Theme/Window.lean — FrcCore

1import FrcCore.Nat23/-!4# FrcCore.Theme.Window — the readout window: the pulse accumulator and the framed readout (the relaxation theme; 27 October 2026)56The registered dynamics of one link of 21-gravity, stated on counts alone (reports/relaxation-window-20261027.md):7the Subject's chart is the link's phase reference; each chronon the link's current at the registered mismatch `μ` is8read through the window as a count `M μ` of transfers per window `B`; an accumulator adds `M μ` per chronon and the9chart moves one quantum toward alignment each time it passes `B` (the pulse law of `FRC.Relaxation.pulse_law` with the10rate of the present mismatch). Nothing here uses the shell: the theorems are `Nat` arithmetic, with no axioms.1112* `step`, `run` — the re-registration rule as a function of the state (the mismatch in quanta, the accumulator below the13  window); `run_add` composes runs.14* `step_mu_le`, `step_mu_ge` — the registered mismatch never grows and moves by at most one quantum per chronon;15  `run_acc_lt` — the accumulator stays below the window when every count is at most the window.16* `run_aligned` — alignment is a fixed point: with `M 0 = 0` the link stays aligned.17* `drops_within` — at a mismatch `μ ≥ 1` the chart moves within `k` chronons whenever `k · M μ ≥ B`: the dwell at a18  level is bounded by the window over the count (`⌈B / M μ⌉`, stated without division).19* `terminates` — from any mismatch `μ₀` the link reaches exact alignment within `Σ_{μ = 1}^{μ₀} k μ` chronons, `k μ` any20  bound with `k μ · M μ ≥ B`. The chart's Kuramoto flow has an exponential tail; the registered relaxation ends.21* `IsSqrt`, `isSqrt_unique`, `isSqrt_nest` — the grid bound of the framed readout map (22-quantum, Definition readout:22  `s_n = ⌊√(m g^{2n})⌋` as the two-sided bound `s² ≤ m g^{2n} < (s + 1)²`) and the nesting of the readouts across23  scales; `readoutNum`, `readoutDen`, `count` — the readout of a weight `(u + v√m)/b` at scale `n` as a framed rational,24  and the registered count of `B` runs over the two outcomes by the largest-remainder rule (the residual unit goes to the25  event when its remainder is at least the other's: the half-up rounding of `B R`).26* `readout_c8`, `readout_c12` — the window counts of the link's current on `C_8` and `C_12` at 22-quantum's worked scale27  (`g = 3`, `n = 4`, `B = 81`): 57, 81 and 41, 70, 81, decided by the kernel; `M/B` is the readout of `sin(2πμ/N)`.28* `quiet_run`, `fires_at`, `carry_lt` — the dwell at a level: while the accumulator stays below the window the chart29  does not move and the accumulator is `acc + k · M μ`; the chart moves at exactly the first `k + 1` with30  `B ≤ acc + (k + 1) · M μ`; the carry after a pulse is below the count.31* `dwell_two_values` — with carry `c < M` the dwell `d + 1` is `⌊B/M⌋` or `⌊B/M⌋ + 1`: the registered rate `M/B` and32  the dwell per quantum are the two faces of one window count (21:C7).33* `equivalence_cancel` — `(m g)/m = g`: the cardinality cancels inside the two-shift law (21:C4).3435The quotient face of the division algorithm, `x = p · (x/p) + x % p` (`FRC.Nat.div_spec`) and its uniqueness36(`FRC.Nat.div_unique`), is derived first from the definition of `Nat.div` in `Init.Prelude` (a fuel recursion, as37`Nat.modCore` in `FrcCore.Nat`), since Lean's `Nat.mul_div_cancel_left` and `Nat.div_add_mod` carry `propext`.38-/3940namespace FRC.Nat4142/-! ## The division algorithm, the quotient face: from the definition of `Nat.div` -/4344/-- The fuel of `Nat.div.go` does not matter once it exceeds the dividend. -/45theorem div_go_fuel {y : Nat} (hy : 0 < y) : ∀ (f1 f2 x : Nat) (h1 : x < f1) (h2 : x < f2),46    Nat.div.go y hy f1 x h1 = Nat.div.go y hy f2 x h2 := by47  intro f148  induction f1 with49  | zero => intro f2 x h1; exact absurd h1 (Nat.not_lt_zero x)50  | succ f1 ih =>51    intro f2 x h1 h252    cases f2 with53    | zero => exact absurd h2 (Nat.not_lt_zero x)54    | succ f2 =>55      show (if h : y ≤ x then Nat.div.go y hy f1 (x - y) _ + 1 else 0)56          = (if h : y ≤ x then Nat.div.go y hy f2 (x - y) _ + 1 else 0)57      exact match Nat.decLe y x with58        | .isTrue h => by rw [dite_eq_left h, dite_eq_left h, ih f2 (x - y) _ _]59        | .isFalse h => by rw [dite_eq_right h, dite_eq_right h]6061/-- The recursion of `Nat.div`: `x / y = (x − y) / y + 1` for `y ≤ x`, else `0`. -/62theorem div_eq' (x y : Nat) (hy : 0 < y) : x / y = if y ≤ x then (x - y) / y + 1 else 0 := by63  show Nat.div x y = if y ≤ x then Nat.div (x - y) y + 1 else 064  unfold Nat.div65  rw [dite_eq_left hy]66  show (if h : y ≤ x then Nat.div.go y hy x (x - y) _ + 1 else 0) = _67  exact match Nat.decLe y x with68    | .isTrue h => by69        rw [dite_eq_left h, ite_eq_left h, dite_eq_left hy, div_go_fuel hy x (x - y + 1) (x - y) _ _]70    | .isFalse h => by rw [dite_eq_right h, ite_eq_right h]7172/-- The division algorithm, quotient face: `x = p · (x / p) + x % p`. -/73theorem div_spec (p : Nat) (hp : 0 < p) : ∀ x : Nat, x = p * (x / p) + x % p := by74  intro x75  induction x using Nat.strongRecOn with76  | _ x ih =>77    exact match Nat.decLe p x with78      | .isTrue h => by79          have ih' := ih (x - p) (Nat.sub_lt (Nat.lt_of_lt_of_le hp h) hp)80          rw [div_eq' x p hp, ite_eq_left h, mod_eq_sub_mod hp h, Nat.mul_succ, Nat.add_assoc, Nat.add_comm p,81            ← Nat.add_assoc, ← ih', sub_add_cancel h]82      | .isFalse h => by83          rw [div_eq' x p hp, ite_eq_right h, Nat.mul_zero, Nat.zero_add, mod_eq_of_lt (Nat.lt_of_not_le h)]8485/-- The quotient is determined: if `x = p·q + r` with `r < p`, then `x / p = q`. -/86theorem div_unique {p x q r : Nat} (hr : r < p) (h : x = p * q + r) : x / p = q :=87  quot_unique (Nat.mod_lt x (pos_of_lt hr)) hr (by rw [← div_spec p (pos_of_lt hr) x]; exact h)8889end FRC.Nat9091namespace FRC.Relaxation9293/-! ## The pulse accumulator (21:C28) -/9495/-- The registered state of a link: the mismatch in quanta of the phase cycle and the accumulator, below the window. -/96structure State where97  mu : Nat98  acc : Nat99100/-- One chronon of the re-registration rule: the accumulator gains the window count `M μ` of the present mismatch; when101it reaches the window `B` one pulse fires — the chart moves one quantum toward alignment and the accumulator keeps the102remainder. -/103def step (M : Nat → Nat) (B : Nat) (s : State) : State :=104  if B ≤ s.acc + M s.mu then ⟨s.mu - 1, s.acc + M s.mu - B⟩ else ⟨s.mu, s.acc + M s.mu⟩105106/-- `t` chronons of the rule. -/107def run (M : Nat → Nat) (B : Nat) : Nat → State → State108  | 0, s => s109  | t + 1, s => run M B t (step M B s)110111variable {M : Nat → Nat} {B : Nat}112113theorem run_zero (s : State) : run M B 0 s = s := rfl114115theorem run_succ (t : Nat) (s : State) : run M B (t + 1) s = run M B t (step M B s) := rfl116117/-- Runs compose: `a + b` chronons are `a` chronons and then `b`. -/118theorem run_add (a b : Nat) (s : State) : run M B (a + b) s = run M B b (run M B a s) := by119  induction a generalizing s with120  | zero => rw [Nat.zero_add]; rfl121  | succ a ih =>122    rw [Nat.succ_add, run_succ, run_succ, ih]123124/-- The last chronon of a run. -/125theorem run_succ' (t : Nat) (s : State) : run M B (t + 1) s = step M B (run M B t s) := by126  induction t generalizing s with127  | zero => rfl128  | succ t ih => rw [run_succ, ih]; rfl129130/-- The fired step. -/131theorem step_fire {s : State} (h : B ≤ s.acc + M s.mu) : step M B s = ⟨s.mu - 1, s.acc + M s.mu - B⟩ := by132  unfold step; rw [ite_eq_left h]133134/-- The quiet step. -/135theorem step_quiet {s : State} (h : ¬ B ≤ s.acc + M s.mu) : step M B s = ⟨s.mu, s.acc + M s.mu⟩ := by136  unfold step; rw [ite_eq_right h]137138/-- 21:C28 — the registered mismatch never grows. -/139theorem step_mu_le (s : State) : (step M B s).mu ≤ s.mu := by140  cases Nat.lt_or_ge (s.acc + M s.mu) B with141  | inl h => rw [step_quiet (Nat.not_le_of_lt h)]; exact Nat.le_refl _142  | inr h => rw [step_fire h]; exact Nat.sub_le _ _143144/-- 21:C28 — the registered mismatch moves by at most one quantum per chronon. -/145theorem step_mu_ge (s : State) : s.mu ≤ (step M B s).mu + 1 := by146  cases Nat.lt_or_ge (s.acc + M s.mu) B with147  | inl h => rw [step_quiet (Nat.not_le_of_lt h)]; exact Nat.le_add_right _ _148  | inr h =>149    rw [step_fire h]150    show s.mu ≤ s.mu - 1 + 1151    cases s.mu with152    | zero => exact Nat.zero_le _153    | succ m => exact Nat.le_refl _154155/-- The accumulator stays below the window when every count is at most the window. -/156theorem step_acc_lt (hM : ∀ μ, M μ ≤ B) {s : State} (hs : s.acc < B) : (step M B s).acc < B := by157  cases Nat.lt_or_ge (s.acc + M s.mu) B with158  | inl h => rw [step_quiet (Nat.not_le_of_lt h)]; exact h159  | inr h =>160    rw [step_fire h]161    show s.acc + M s.mu - B < B162    exact FRC.Nat.sub_lt_of_lt_add (Nat.add_lt_add_of_lt_of_le hs (hM _)) h163164theorem run_acc_lt (hM : ∀ μ, M μ ≤ B) (t : Nat) {s : State} (hs : s.acc < B) : (run M B t s).acc < B := by165  induction t generalizing s with166  | zero => exact hs167  | succ t ih => rw [run_succ]; exact ih (step_acc_lt hM hs)168169theorem run_mu_le (t : Nat) (s : State) : (run M B t s).mu ≤ s.mu := by170  induction t generalizing s with171  | zero => exact Nat.le_refl _172  | succ t ih => rw [run_succ]; exact Nat.le_trans (ih _) (step_mu_le s)173174/-- 21:C28 — alignment is a fixed point: with no current at alignment (`M 0 = 0`) the link stays aligned. -/175theorem step_aligned (h0 : M 0 = 0) {s : State} (hs : s.acc < B) (hmu : s.mu = 0) :176    (step M B s).mu = 0 ∧ (step M B s).acc = s.acc := by177  have h : ¬ B ≤ s.acc + M s.mu := by rw [hmu, h0, Nat.add_zero]; exact Nat.not_le_of_lt hs178  rw [step_quiet h]; exact ⟨hmu, by show s.acc + M s.mu = s.acc; rw [hmu, h0, Nat.add_zero]⟩179180/-- 21:C28 — the aligned link stays aligned through every run. -/181theorem run_aligned (h0 : M 0 = 0) (t : Nat) {s : State} (hs : s.acc < B) (hmu : s.mu = 0) :182    (run M B t s).mu = 0 := by183  induction t generalizing s with184  | zero => exact hmu185  | succ t ih =>186    rw [run_succ]187    rcases step_aligned h0 hs hmu with ⟨h1, h2⟩188    exact ih (by rw [h2]; exact hs) h1189190/-- While no pulse has fired the accumulator is `acc + j · M μ`: from a mismatch `μ ≥ 1`, after `j` chronons either191the mismatch has dropped or the state is `⟨μ, acc + j · M μ⟩`. -/192theorem run_dichotomy (j : Nat) {s : State} (hpos : 0 < s.mu) :193    (run M B j s).mu < s.mu ∨ ((run M B j s).mu = s.mu ∧ (run M B j s).acc = s.acc + j * M s.mu) := by194  induction j with195  | zero => exact Or.inr ⟨rfl, by show s.acc = s.acc + 0 * M s.mu; rw [Nat.zero_mul, Nat.add_zero]⟩196  | succ j ih =>197    have e : run M B (j + 1) s = step M B (run M B j s) := run_succ' j s198    rcases ih with h | ⟨hmu, hacc⟩199    · exact Or.inl (Nat.lt_of_le_of_lt (by rw [e]; exact step_mu_le _) h)200    · rw [e]201      cases Nat.lt_or_ge ((run M B j s).acc + M (run M B j s).mu) B with202      | inl hq =>203        rw [step_quiet (Nat.not_le_of_lt hq)]204        exact Or.inr ⟨hmu, by show (run M B j s).acc + M (run M B j s).mu = _; rw [hacc, hmu, Nat.succ_mul, Nat.add_assoc]⟩205      | inr hf =>206        rw [step_fire hf]207        show (run M B j s).mu - 1 < s.mu ∨ _208        rw [hmu]209        exact Or.inl (Nat.sub_lt hpos Nat.zero_lt_one)210211/-- 21:C28 — the dwell at a mismatch `μ ≥ 1` is bounded by the window over the count: the chart moves within `k`212chronons whenever `k · M μ ≥ B`. -/213theorem drops_within (hM : ∀ μ, M μ ≤ B) {s : State} (hpos : 0 < s.mu) (hs : s.acc < B) {k : Nat}214    (hk : B ≤ k * M s.mu) : (run M B k s).mu < s.mu := by215  rcases run_dichotomy k hpos with h | ⟨_, hacc⟩216  · exact h217  · exact absurd (run_acc_lt hM k hs) (by218      rw [hacc]; exact Nat.not_lt_of_le (Nat.le_trans hk (Nat.le_add_left _ _)))219220/-- The chronon budget `Σ_{μ = 1}^{n} k μ`. -/221def budget (k : Nat → Nat) : Nat → Nat222  | 0 => 0223  | n + 1 => k (n + 1) + budget k n224225/-- 21:C28 — the registered relaxation terminates: with no current at alignment and a count of at least one quantum per226window at every other mismatch (`k μ · M μ ≥ B` for a bound `k`), a link at mismatch at most `n` reaches exact alignment227within `budget k n` chronons and stays there. -/228theorem terminates (hM : ∀ μ, M μ ≤ B) (h0 : M 0 = 0) (k : Nat → Nat) (hk : ∀ μ, 0 < μ → B ≤ k μ * M μ) :229    ∀ n, ∀ s : State, s.mu ≤ n → s.acc < B → (run M B (budget k n) s).mu = 0 := by230  intro n231  induction n with232  | zero =>233    intro s hn hs234    exact run_aligned h0 _ hs (Nat.le_antisymm hn (Nat.zero_le _))235  | succ n ih =>236    intro s hn hs237    show (run M B (k (n + 1) + budget k n) s).mu = 0238    rw [run_add]239    have hacc : (run M B (k (n + 1)) s).acc < B := run_acc_lt hM _ hs240    apply ih _ _ hacc241    cases Nat.lt_or_ge s.mu (n + 1) with242    | inl hlt => exact Nat.le_trans (run_mu_le _ _) (Nat.le_of_lt_succ hlt)243    | inr hge =>244      have hmu : s.mu = n + 1 := Nat.le_antisymm hn hge245      have hpos : 0 < s.mu := by rw [hmu]; exact Nat.succ_pos n246      have hd := drops_within hM hpos hs (k := k (n + 1)) (by rw [← hmu]; exact hk _ hpos)247      rw [hmu] at hd248      exact Nat.le_of_lt_succ hd249250/-- 21:C28 — the basin form of `terminates`: the count hypothesis is needed only at the mismatches at or below the start,251since the mismatch never grows. A link starting below the antipode of `C_8` or `C_12`, where the exact window count252vanishes, is covered: it never reaches the antipode. -/253theorem terminates_basin (hM : ∀ μ, M μ ≤ B) (h0 : M 0 = 0) (k : Nat → Nat) :254    ∀ n, (∀ μ, 0 < μ → μ ≤ n → B ≤ k μ * M μ) →255      ∀ s : State, s.mu ≤ n → s.acc < B → (run M B (budget k n) s).mu = 0 := by256  intro n257  induction n with258  | zero =>259    intro _ s hn hs260    exact run_aligned h0 _ hs (Nat.le_antisymm hn (Nat.zero_le _))261  | succ n ih =>262    intro hk s hn hs263    show (run M B (k (n + 1) + budget k n) s).mu = 0264    rw [run_add]265    have hacc : (run M B (k (n + 1)) s).acc < B := run_acc_lt hM _ hs266    apply ih (fun μ hμ hle => hk μ hμ (Nat.le_succ_of_le hle)) _ _ hacc267    cases Nat.lt_or_ge s.mu (n + 1) with268    | inl hlt => exact Nat.le_trans (run_mu_le _ _) (Nat.le_of_lt_succ hlt)269    | inr hge =>270      have hmu : s.mu = n + 1 := Nat.le_antisymm hn hge271      have hpos : 0 < s.mu := by rw [hmu]; exact Nat.succ_pos n272      have hd := drops_within hM hpos hs (k := k (n + 1)) (by rw [← hmu]; exact hk _ hpos hn)273      rw [hmu] at hd274      exact Nat.le_of_lt_succ hd275276/-! ## The framed readout on a real-quadratic stratum (22-quantum, Definition readout; 21:C29) -/277278/-- The grid bound of the readout: `s` is the integer square root of `x`, `s² ≤ x < (s + 1)²`. -/279def IsSqrt (x s : Nat) : Prop := s * s ≤ x ∧ x < (s + 1) * (s + 1)280281instance (x s : Nat) : Decidable (IsSqrt x s) := inferInstanceAs (Decidable (_ ∧ _))282283/-- `a² < b² ⇒ a < b`, without the prelude's classical lemma. -/284theorem lt_of_sq_lt_sq {a b : Nat} (h : a * a < b * b) : a < b := by285  cases Nat.lt_or_ge a b with286  | inl hab => exact hab287  | inr hba => exact absurd (Nat.lt_of_lt_of_le h (Nat.mul_le_mul hba hba)) (Nat.lt_irrefl _)288289/-- 21:C29 — the integer square root is unique: the readout's grid point is determined by its bound. -/290theorem isSqrt_unique {x s s' : Nat} (h : IsSqrt x s) (h' : IsSqrt x s') : s = s' :=291  Nat.le_antisymm (Nat.le_of_lt_succ (lt_of_sq_lt_sq (Nat.lt_of_le_of_lt h.1 h'.2)))292    (Nat.le_of_lt_succ (lt_of_sq_lt_sq (Nat.lt_of_le_of_lt h'.1 h.2)))293294/-- 21:C29 — the readouts nest across scales (22-quantum's grid bound at every scale): if `s` is the root of `x` and295`s'` the root of `x · c²`, then `s c ≤ s' < (s + 1) c`. -/296theorem isSqrt_nest {x s s' c : Nat} (hc : 0 < c) (h : IsSqrt x s) (h' : IsSqrt (x * (c * c)) s') :297    s * c ≤ s' ∧ s' < (s + 1) * c := by298  have e1 : s * c * (s * c) = s * s * (c * c) := by299    rw [Nat.mul_assoc, Nat.mul_left_comm c, ← Nat.mul_assoc]300  have e2 : (s + 1) * c * ((s + 1) * c) = (s + 1) * (s + 1) * (c * c) := by301    rw [Nat.mul_assoc, Nat.mul_left_comm c, ← Nat.mul_assoc]302  constructor303  · -- `(s c)² = s² c² ≤ x c² < (s' + 1)²`304    apply Nat.le_of_lt_succ305    apply lt_of_sq_lt_sq306    rw [e1]307    exact Nat.lt_of_le_of_lt (Nat.mul_le_mul_right _ h.1) h'.2308  · -- `s'² ≤ x c² < (s + 1)² c² = ((s + 1) c)²`309    apply lt_of_sq_lt_sq310    rw [e2]311    exact Nat.lt_of_le_of_lt h'.1 (Nat.mul_lt_mul_of_pos_right h.2 (Nat.mul_pos hc hc))312313/-- The readout of the weight `(u + v√m)/b` at scale `n`: the numerator `u gⁿ + v s` with `s` the root of `m g^{2n}`. -/314def readoutNum (u v s g n : Nat) : Nat := u * g ^ n + v * s315316/-- Its denominator `b gⁿ`. -/317def readoutDen (b g n : Nat) : Nat := b * g ^ n318319/-- The registered count of `B` runs over the two outcomes (the event, its absence) by the largest-remainder rule: the320provisional `⌊B R⌋`, and the residual unit when the event's remainder is at least the other's — the half-up rounding of321`B R = B num/den`. -/322def count (B num den : Nat) : Nat := (2 * B * num + den) / (2 * den)323324/-- 21:C29 — `C_8` at 22-quantum's worked scale (`g = 3`, `n = 4`, `B = 81`): the root `s_4 = 114` of `2 · 3^8`, and the325window counts of the current `|sin(2πμ/8)|` — `√2/2 = (0 + 1·√2)/2` at `μ = 1, 3` reads `114/162`, count 57; `1` at `μ = 2`326reads `81/81`, count 81. -/327theorem readout_c8 :328    IsSqrt (2 * 3 ^ 8) 114 ∧ readoutNum 0 1 114 3 4 = 114 ∧ readoutDen 2 3 4 = 162 ∧329    count 81 (readoutNum 0 1 114 3 4) (readoutDen 2 3 4) = 57 ∧330    count 81 (readoutNum 1 0 114 3 4) (readoutDen 1 3 4) = 81 := by331  decide332333/-- 21:C29 — `C_12` at the same scale: the root `s_4 = 140` of `3 · 3^8`, and the counts of `|sin(2πμ/12)|` — `1/2` at334`μ = 1, 5` reads `81/162`, count 41 (the half unit to the event); `√3/2 = (0 + 1·√3)/2` at `μ = 2, 4` reads `140/162`, count33570; `1` at `μ = 3`, count 81. -/336theorem readout_c12 :337    IsSqrt (3 * 3 ^ 8) 140 ∧338    count 81 (readoutNum 1 0 140 3 4) (readoutDen 2 3 4) = 41 ∧339    count 81 (readoutNum 0 1 140 3 4) (readoutDen 2 3 4) = 70 ∧340    count 81 (readoutNum 1 0 140 3 4) (readoutDen 1 3 4) = 81 := by341  decide342343/-! ## The dwell at a level: the two faces of one window count (21:C7) -/344345/-- 21:C7 — while the accumulator stays below the window the chart does not move and the accumulator grows by `M μ` per346chronon: after `k` chronons with `acc + k · M μ < B` the state is `⟨μ, acc + k · M μ⟩`. -/347theorem quiet_run (s : State) : ∀ k, s.acc + k * M s.mu < B → run M B k s = ⟨s.mu, s.acc + k * M s.mu⟩348  | 0, _ => by show s = ⟨s.mu, s.acc + 0 * M s.mu⟩; rw [Nat.zero_mul, Nat.add_zero]349  | k + 1, h => by350    have hk : s.acc + k * M s.mu < B :=351      Nat.lt_of_le_of_lt (Nat.add_le_add_left (Nat.mul_le_mul_right _ (Nat.le_succ k)) _) h352    have hq : ¬ B ≤ s.acc + k * M s.mu + M s.mu := by353      rw [Nat.add_assoc, ← Nat.succ_mul]; exact Nat.not_le_of_lt h354    rw [run_succ', quiet_run s k hk, step_quiet hq]355    show (⟨s.mu, s.acc + k * M s.mu + M s.mu⟩ : State) = ⟨s.mu, s.acc + (k + 1) * M s.mu⟩356    rw [Nat.succ_mul, Nat.add_assoc]357358/-- The dwell at a level is the least `k + 1` with `B ≤ acc + (k + 1) · M μ`: the chart moves at exactly that chronon,359to `μ − 1`, and the accumulator keeps the carry `acc + (k + 1) · M μ − B`. -/360theorem fires_at (s : State) (k : Nat) (hq : s.acc + k * M s.mu < B) (hf : B ≤ s.acc + (k + 1) * M s.mu) :361    (run M B (k + 1) s).mu = s.mu - 1 ∧ (run M B (k + 1) s).acc = s.acc + (k + 1) * M s.mu - B := by362  have hf' : B ≤ s.acc + k * M s.mu + M s.mu := by rw [Nat.add_assoc, ← Nat.succ_mul]; exact hf363  rw [run_succ', quiet_run s k hq, step_fire hf']364  exact ⟨rfl, by show s.acc + k * M s.mu + M s.mu - B = _; rw [Nat.add_assoc, ← Nat.succ_mul]⟩365366/-- The carry after a pulse is below the count: the next dwell is `⌊B/M⌋` or `⌈B/M⌉` (the Christoffel gaps of Lemma367isopair). -/368theorem carry_lt (s : State) (hacc : s.acc < B) (hfire : B ≤ s.acc + M s.mu) : (step M B s).acc < M s.mu := by369  rw [step_fire hfire]370  show s.acc + M s.mu - B < M s.mu371  exact FRC.Nat.sub_lt_of_lt_add (Nat.add_lt_add_right hacc _) hfire372373/-- 21:C7 — with carry `c < M` and a count `0 < M`, the dwell `d + 1` (the least `k` with `B ≤ c + k M`, so374`c + d M < B ≤ c + (d + 1) M`) satisfies `B / M ≤ d + 1 ≤ B / M + 1`: the dwell is `⌊B/M⌋` or `⌊B/M⌋ + 1`, and the375registered rate `M/B` and the dwell per quantum are the two faces of one window count. Without division:376`d · M < B < (d + 2) · M` (the `h1`, `h2` of the proof). -/377theorem dwell_two_values (M B c d : Nat) (hM : 0 < M) (hc : c < M) (hq : c + d * M < B)378    (hf : B ≤ c + (d + 1) * M) : B / M ≤ d + 1 ∧ d + 1 ≤ B / M + 1 := by379  have hs : B = M * (B / M) + B % M := FRC.Nat.div_spec M hM B380  have hr : B % M < M := Nat.mod_lt B hM381  have h1 : d * M < B := Nat.lt_of_le_of_lt (Nat.le_add_left _ _) hq382  have h2 : B < M * (d + 1 + 1) := by383    rw [Nat.mul_comm, Nat.succ_mul]384    exact Nat.lt_of_le_of_lt hf (by rw [Nat.add_comm c]; exact Nat.add_lt_add_left hc _)385  constructor386  · -- `B / M ≤ d + 1`: else `M (d + 2) ≤ M (B / M) ≤ B < M (d + 2)`387    cases Nat.lt_or_ge (B / M) (d + 1 + 1) with388    | inl h => exact Nat.le_of_lt_succ h389    | inr h =>390      have h3 : M * (d + 1 + 1) ≤ B :=391        calc M * (d + 1 + 1) ≤ M * (B / M) := Nat.mul_le_mul_left M h392          _ ≤ M * (B / M) + B % M := Nat.le_add_right _ _393          _ = B := hs.symm394      exact absurd (Nat.lt_of_le_of_lt h3 h2) (Nat.lt_irrefl _)395  · -- `d ≤ B / M`: else `M (B / M + 1) ≤ M d < B < M (B / M + 1)`396    cases Nat.lt_or_ge (B / M) d with397    | inr h => exact Nat.succ_le_succ h398    | inl h =>399      have h3 : M * (B / M + 1) ≤ M * d := Nat.mul_le_mul_left M h400      have h4 : B < M * (B / M + 1) := by401        rw [Nat.mul_succ]402        calc B = M * (B / M) + B % M := hs403          _ < M * (B / M) + M := Nat.add_lt_add_left hr _404      have h5 : M * d ≤ B := by rw [Nat.mul_comm]; exact Nat.le_of_lt h1405      exact absurd (Nat.lt_of_lt_of_le h4 (Nat.le_trans h3 h5)) (Nat.lt_irrefl B)406407/-- 21:C4, 21:X7 — the equivalence cancellation of the two-shift law: the kick shifts the winding by `m · g` (the `m` of408coherent additivity) and the transport moves the registered position by the winding over `m`; the displacement is `g`,409and the cardinality cancels inside the law. -/410theorem equivalence_cancel (m g : Nat) (hm : 0 < m) : (m * g) / m = g :=411  FRC.Nat.div_unique hm (by rw [Nat.add_zero (m * g)])412413end FRC.Relaxation414