Theme/Static.lean — FrcCore

1import FrcCore.Theme.Field2import FrcCore.Theme.Drift3import FrcCore.Theme.Window45/-!6# FrcCore.Theme.Static — the cut form of the static profile, the winding grading and the leakage count (the relaxation theme; 27 October 2026)78Three exact faces of 21-gravity's relaxation revision (reports/relaxation-window-20261027.md), on counts and on the9prime shell, with no axioms:1011* `Static`, `static_iff`, `slip_of_exceeds` — the cut form of the exact static profile (Proposition exactprofile):12  a link carries at most `κ` quanta per chronon, a cut of `A r` links at most `κ · A r`, and a static locked transfer13  balances the enclosed demand `Q r` through every cut (the Gauss law of `FRC.Drift.gauss_law`); a static state exists14  exactly when `Q r ≤ κ · A r` at every cut, and slips wherever `Q r > κ · A r`.15* `cutArea`, `cutArea_mono`, `exterior_of_sq`, `slip_of_sq`, `slip_instance` — the cut weight `6(2r² + 2r + 1)` of the16  graph ball of radius `r` in the cubic chart (`FRC.Drift.cut_area_monotone`), monotone; a demand `m ≤ 12 κ r²` has its17  static exterior at `r`, a demand `m > 30 κ r²` (for `r ≥ 1`) slips there: the slip radius `r_*` sits between18  `√(m/30κ)` and `⌈√(m/12κ)⌉` (the chart's `r_* = √(Gm)` with `A_r = 4πr²` is the [chart] reading; the core carries the19  cut form exactly); the instance `m = 10⁴` at unit capacity, exterior from `r = 29`, decided by the kernel.20* `Graded`, `graded_mul`, `graded_const`, `equivariant_graded`, `selection` — the winding grading of the nonlinear21  completion (Theorem branch (i)): a sequence on the drive's orbit has grade `k` when one chronon multiplies it by22  `g^k`; grades add under products, a stationary offset has grade `0`, a drive-equivariant linear operation preserves23  the grade, and a sequence of grade `0` and of a grade `m` with `g^m ≠ 1` vanishes — no function of stationary offsets24  constitutes new onsite winding demand (21:C11).25* `leakage`, `returns`, `leakage_add_returns`, `returns_eq_div`, `leakage_eq` — the leakage count on the cycle (T14):26  the chronons below `T` at which the relative cycle of defect `a` on `C_L` fails to close are exactly the chronons off27  the return chain; the returns below `T ≥ 1` are `0` and the multiples of the first return, `⌊(T − 1)/T_def⌋ + 1`28  (`FRC.Drift.return_iff`), and the leakage is the rest. The count of multiples is pinned without division first29  (`count_multiples_spec`: `T ≤ c · d < T + d`), then read through `FRC.Nat.div_unique`.30-/3132namespace FRC.Static3334open FRC.Shell FRC.Shell.Frame3536/-! ## The cut form of the exact static profile (21:C12) -/3738/-- A static locked transfer on a radial partition: the cut `r` carries `t r` quanta per chronon, at most `κ` per link39over its `A r` links, and the transfer balances the enclosed demand `Q r` (the Gauss law of `FRC.Drift.gauss_law`). -/40def Static (κ : Nat) (A Q t : Nat → Nat) : Prop := (∀ r, t r ≤ κ * A r) ∧ (∀ r, t r = Q r)4142/-- 21:C12 — a static locked state exists exactly when every cut can carry its enclosed demand, `Q r ≤ κ · A r`:43Proposition exactprofile's `ϰ A_r sin δ_r = Q_r` in its cut form. -/44theorem static_iff (κ : Nat) (A Q : Nat → Nat) : (∃ t, Static κ A Q t) ↔ ∀ r, Q r ≤ κ * A r :=45  ⟨fun ⟨t, ht⟩ r => by rw [← ht.2 r]; exact ht.1 r, fun h => ⟨Q, h, fun _ => rfl⟩⟩4647/-- 21:C12 — slip exactly where the demand exceeds the cut's capacity: no static state through a cut with48`κ · A r < Q r`. -/49theorem slip_of_exceeds (κ : Nat) (A Q : Nat → Nat) (r : Nat) (h : κ * A r < Q r) : ¬ ∃ t, Static κ A Q t :=50  fun ht => Nat.lt_irrefl _ (Nat.lt_of_lt_of_le h ((static_iff κ A Q).mp ht r))5152/-- The cut weight of the graph ball of radius `r` in the cubic chart, `6(2r² + 2r + 1)`53(`FRC.Drift.cut_area_monotone`). -/54def cutArea (r : Nat) : Nat := 6 * (2 * r * r + 2 * r + 1)5556/-- 21:C12 — the cut weight grows with the radius. -/57theorem cutArea_mono (r : Nat) : cutArea r ≤ cutArea (r + 1) := Nat.le_of_lt (FRC.Drift.cut_area_monotone r).25859/-- 21:C12 — the static exterior exists wherever `12 κ r² ≥ m`: `cutArea r = 12r² + 12r + 6 ≥ 12 r²`, so the cut at60`r` carries the demand `m`. -/61theorem exterior_of_sq (κ m r : Nat) (h : m ≤ 12 * κ * (r * r)) : m ≤ κ * cutArea r := by62  have e : κ * (6 * (2 * r * r)) = 12 * κ * (r * r) := by63    rw [FRC.Nat.mul_assoc 2 r r, ← FRC.Nat.mul_assoc 6 2, FRC.Nat.mul_left_comm κ, ← FRC.Nat.mul_assoc]64  have h1 : 2 * r * r ≤ 2 * r * r + 2 * r + 1 := Nat.le_trans (Nat.le_add_right _ _) (Nat.le_add_right _ _)65  exact Nat.le_trans h (by rw [← e]; exact Nat.mul_le_mul_left κ (Nat.mul_le_mul_left 6 h1))6667/-- 21:C12 — the static exterior fails wherever `30 κ r² < m` (for `r ≥ 1`): `12r + 6 ≤ 18 r²`, so68`cutArea r ≤ 30 r²` and the cut at `r` cannot carry the demand `m`. -/69theorem slip_of_sq (κ m r : Nat) (hr : 1 ≤ r) (h : 30 * κ * (r * r) < m) : κ * cutArea r < m := by70  have h2r : 2 * r ≤ 2 * (r * r) := by71    have := Nat.mul_le_mul_left (2 * r) hr72    rw [Nat.mul_one, FRC.Nat.mul_assoc] at this; exact this73  have hrr : 1 ≤ r * r := Nat.mul_le_mul hr hr74  have hcut : cutArea r ≤ 6 * (5 * (r * r)) := by75    show 6 * (2 * r * r + 2 * r + 1) ≤ 6 * (5 * (r * r))76    apply Nat.mul_le_mul_left 677    have e : 2 * (r * r) + 2 * (r * r) + 1 * (r * r) = 5 * (r * r) := by78      rw [← FRC.Nat.add_mul, ← FRC.Nat.add_mul]79    rw [← e, FRC.Nat.mul_assoc 2 r r]80    exact Nat.add_le_add (Nat.add_le_add (Nat.le_refl _) h2r) (by rw [Nat.one_mul]; exact hrr)81  have e30 : κ * (6 * (5 * (r * r))) = 30 * κ * (r * r) := by82    rw [← FRC.Nat.mul_assoc 6 5, FRC.Nat.mul_left_comm κ, ← FRC.Nat.mul_assoc]83  exact Nat.lt_of_le_of_lt (by rw [← e30]; exact Nat.mul_le_mul_left κ hcut) h8485/-- 21:C12 — a demand of `10⁴` at unit capacity: the cut at `r = 29` carries it (`cutArea 29 = 10446`) and the cut at86`r = 28` does not (`cutArea 28 = 9750`); the static exterior ends at `r = 29`, decided by the kernel. -/87theorem slip_instance : (10000 ≤ 1 * cutArea 29) ∧ (1 * cutArea 28 < 10000) := by decide8889/-! ## The winding grading of the nonlinear completion (21:C11) -/9091variable {p : Nat} [Pos p]9293/-- A sequence on the drive's orbit has grade `k` when one chronon multiplies it by `g ^ k`. -/94def Graded (g : Shell p) (k : Nat) (f : Nat → Shell p) : Prop := ∀ x, f (x + 1) = g ^ k * f x9596/-- 21:C11 — grades add under products: sources of grades `a` and `b` compose to grade `a + b`97(`FRC.Drift.character_composition`). -/98theorem graded_mul (g : Shell p) {a b : Nat} {f h : Nat → Shell p} (hf : Graded g a f) (hh : Graded g b h) :99    Graded g (a + b) (fun x => f x * h x) := fun x => by100  show f (x + 1) * h (x + 1) = g ^ (a + b) * (f x * h x)101  rw [hf x, hh x, pow_add, mul_mul_mul_comm]102103/-- 21:C11 — a stationary relative-offset configuration carries grade `0`. -/104theorem graded_const (g : Shell p) (c : Shell p) : Graded g 0 (fun _ => c) := fun _ => by105  show c = g ^ 0 * c106  rw [pow_zero, one_mul]107108/-- 21:C11 — an operation that commutes with the drive (`T f (x + 1) = T (f ∘ succ) x`, the hypothesis `hT`) and is109homogeneous of degree one pointwise (whenever `f'` is `c · f` at every chronon, `T f'` is `c · T f` at every chronon,110the hypothesis `hlin`, stated pointwise so that no function extensionality is used) sends grade-`k` sequences to111grade-`k` sequences: an adjacency-local drive-equivariant operation sends invariants to invariants. -/112theorem equivariant_graded (g : Shell p) (k : Nat) (T : (Nat → Shell p) → (Nat → Shell p))113    (hT : ∀ f x, T f (x + 1) = T (fun y => f (y + 1)) x)114    (hlin : ∀ (c : Shell p) (f f' : Nat → Shell p), (∀ y, f' y = c * f y) → ∀ x, T f' x = c * T f x)115    {f : Nat → Shell p} (hf : Graded g k f) : Graded g k (T f) := fun x => by116  rw [hT f x]117  exact hlin (g ^ k) f (fun y => f (y + 1)) hf x118119/-- 21:C11, 21:X4 — character selection: a sequence of grade `0` that also has grade `m` with `g ^ m ≠ 1` vanishes120identically — a stationary offset configuration carries no winding demand. On the prime shell `(g^m − 1) f x = 0`121with `g^m − 1 ≠ 0` forces `f x = 0` (`FRC.Shell.Prime.mul_eq_zero`). -/122theorem selection (hp : FRC.Nat.isPrime p) (g : Shell p) (m : Nat) (hm : g ^ m ≠ 1) {f : Nat → Shell p}123    (h0 : Graded g 0 f) (hm' : Graded g m f) : ∀ x, f x = 0 := fun x => by124  have e : g ^ m * f x = f x := by rw [← hm' x, h0 x, pow_zero, one_mul]125  have hz : (g ^ m + -1) * f x = 0 := by rw [right_distrib, neg_one_mul, e, add_neg]126  rcases Prime.mul_eq_zero hp hz with h | h127  · exact absurd (Prime.eq_of_sub_eq_zero h) hm128  · exact h129130/-! ## The leakage count on the cycle (21:C21, T14) -/131132/-- The chronons below `T` at which the relative cycle of defect `a` on `C_L` does not return: the leakage count of the133window. -/134def leakage (L a T : Nat) : Nat := natCount (fun t => (t * a) % L ≠ 0) T135136/-- The returns below `T`. -/137def returns (L a T : Nat) : Nat := natCount (fun t => (t * a) % L = 0) T138139/-- 21:C21 — every chronon below `T` is a return or a leak: the leakage tally is the registered mismatch over the140window. -/141theorem leakage_add_returns (L a T : Nat) : leakage L a T + returns L a T = T := by142  rw [leakage, returns, ← FRC.Grav.natCount_or (fun t => (t * a) % L ≠ 0) (fun t => (t * a) % L = 0) (fun _ h => h) T]143  exact (natCount_congr _ _ T (fun x _ => ⟨fun _ => trivial, fun _ =>144    match Nat.decEq ((x * a) % L) 0 with145    | isTrue h => Or.inr h146    | isFalse h => Or.inl h⟩)).trans (FRC.Grav.natCount_true T)147148/-- One chronon of the count of multiples of `d`: from `T ≤ c · d < T + d` for the count `c` below `T` to the same149bounds at `T + 1` for the count below `T + 1`. -/150theorem ceil_step (d T c : Nat) (hd : 0 < d) (h1 : T ≤ c * d) (h2 : c * d < T + d) :151    T + 1 ≤ (c + if T % d = 0 then 1 else 0) * d ∧ (c + if T % d = 0 then 1 else 0) * d < T + 1 + d :=152  match Nat.decEq (T % d) 0 with153  | isTrue h => by154    rw [ite_eq_left h]155    obtain ⟨q, hq⟩ := FRC.Nat.mod_spec d hd T156    rw [h, Nat.add_zero (d * q)] at hq157    -- `T = d q` and `d q ≤ c d < d q + d` pin the count: `c = q`158    have hcq : c = q := by159      apply Nat.le_antisymm160      · cases Nat.lt_or_ge c (q + 1) with161        | inl hlt => exact Nat.le_of_lt_succ hlt162        | inr hge =>163          have h3 : d * (q + 1) ≤ d * c := Nat.mul_le_mul_left d hge164          rw [Nat.mul_succ, ← hq, Nat.mul_comm d c] at h3165          exact absurd (Nat.lt_of_lt_of_le h2 h3) (Nat.lt_irrefl _)166      · cases Nat.lt_or_ge c q with167        | inr hge => exact hge168        | inl hlt =>169          have h3 : d * (c + 1) ≤ d * q := Nat.mul_le_mul_left d hlt170          rw [Nat.mul_succ, ← hq, Nat.mul_comm d c] at h3171          exact absurd (Nat.lt_of_lt_of_le (Nat.lt_add_of_pos_right hd) (Nat.le_trans h3 h1)) (Nat.lt_irrefl _)172    rw [hcq, Nat.succ_mul, Nat.mul_comm q d, ← hq]173    exact ⟨Nat.add_le_add_left hd T, Nat.add_lt_add_right (Nat.lt_succ_self T) d⟩174  | isFalse h => by175    rw [ite_eq_right h, Nat.add_zero c]176    refine ⟨?_, Nat.lt_of_lt_of_le h2 (Nat.add_le_add_right (Nat.le_succ T) d)⟩177    -- `T ≠ c d` since `c d ≡ 0`, so `T < c d`178    exact Nat.lt_of_le_of_ne h1 (fun e => h (by179      rw [e]; exact FRC.Nat.mod_unique (q := c) hd (by rw [Nat.mul_comm c d, Nat.add_zero (d * c)])))180181/-- The multiples of `d` below `T`, counted, are `⌈T/d⌉`, stated without division: the count `c` has182`T ≤ c · d < T + d`. -/183theorem count_multiples_spec (d : Nat) (hd : 0 < d) :184    ∀ T, T ≤ natCount (fun t => t % d = 0) T * d ∧ natCount (fun t => t % d = 0) T * d < T + d185  | 0 => by186    show 0 ≤ 0 * d ∧ 0 * d < 0 + d187    rw [Nat.zero_mul, Nat.zero_add]; exact ⟨Nat.le_refl 0, hd⟩188  | T + 1 =>189    match count_multiples_spec d hd T with190    | ⟨h1, h2⟩ => ceil_step d T (natCount (fun t => t % d = 0) T) hd h1 h2191192/-- The count below `T + 1` with `T + 1 ≤ c · d < T + 1 + d` is `⌊T/d⌋ + 1` (`FRC.Nat.div_unique`). -/193theorem floor_of_ceil (d T c : Nat) (h1 : T + 1 ≤ c * d) (h2 : c * d < T + 1 + d) : c = T / d + 1 :=194  match c, h1, h2 with195  | 0, h1, _ => by rw [Nat.zero_mul] at h1; exact absurd h1 (Nat.not_succ_le_zero T)196  | c' + 1, h1, h2 => by197    rw [Nat.succ_mul] at h1 h2198    have h3 : d * c' ≤ T := by rw [Nat.mul_comm]; exact Nat.le_of_lt_succ (Nat.lt_of_add_lt_add_right h2)199    have h4 : T < d * c' + d := by rw [Nat.mul_comm]; exact h1200    rw [FRC.Nat.div_unique (FRC.Nat.sub_lt_of_lt_add h4 h3) (FRC.Nat.add_sub_of_le h3).symm]201202/-- 21:C21 — the returns are the multiples of the first return (`FRC.Drift.return_iff`). -/203theorem returns_eq_count (L a T : Nat) (hL : 0 < L) :204    returns L a T = natCount (fun t => t % FRC.Drift.firstReturn L a = 0) T :=205  natCount_congr _ _ T (fun t _ =>206    (FRC.Drift.return_iff L a t hL).trans (FRC.Nat.dvd_iff_mod (FRC.Drift.firstReturn_pos L a)))207208/-- 21:C21, T14 — the returns below `T ≥ 1` are `0` and the multiples of the first return below `T`:209`⌊(T − 1)/T_def⌋ + 1`. -/210theorem returns_eq_div (L a T : Nat) (hL : 0 < L) (hT : 1 ≤ T) :211    returns L a T = (T - 1) / FRC.Drift.firstReturn L a + 1 :=212  match T, hT with213  | 0, hT => absurd hT (Nat.not_succ_le_zero 0)214  | T + 1, _ => by215    rw [returns_eq_count L a (T + 1) hL, FRC.Nat.add_sub_cancel T 1]216    obtain ⟨h1, h2⟩ := count_multiples_spec (FRC.Drift.firstReturn L a) (FRC.Drift.firstReturn_pos L a) (T + 1)217    exact floor_of_ceil _ _ _ h1 h2218219/-- 21:C21, T14 — the leakage count of the window `T ≥ 1`: the chronons off the return chain,220`T − (⌊(T − 1)/T_def⌋ + 1)`. -/221theorem leakage_eq (L a T : Nat) (hL : 0 < L) (hT : 1 ≤ T) :222    leakage L a T = T - ((T - 1) / FRC.Drift.firstReturn L a + 1) := by223  have e := leakage_add_returns L a T224  rw [← returns_eq_div L a T hL hT]225  calc leakage L a T = leakage L a T + returns L a T - returns L a T := (FRC.Nat.add_sub_cancel _ _).symm226    _ = T - returns L a T := by rw [e]227228end FRC.Static229