Theme/Orbital.lean — FrcCore

1import FrcCore.Orbit2import FrcCore.Sum3import FrcCore.Instances4import FrcCore.Poly56/-!7# FrcCore.Theme.Orbital — the orbital shell's arithmetic (the geometry theme)89The geometry theme holds 2-geometry's exact content above the frame (6 November 2026, the minimal revision of the10paper; moved here from the paper module `FrcCore/Geometry.lean`, every name unchanged): the cell counts of the orbital11shell and its completion (2:C2); the fixed-shell bound of the scale grids, its floor `1/(p+1)` and the `(13, 2)` gap12(2:E3); which reindexings of the phase cycle preserve its adjacency (2:B4); the frame moves the labels of one complex13(2:C4); the Lipschitz budget of a bounded experiment (2:E4); the exponents of the external transport (2:F6). No axioms.14-/1516namespace FRC17namespace Geometry1819/-- 2:C2, 2:C3 (Remark 3.4) — the counts: with `π = m + 1` phases-deep and `n = p − 1` phases,20`|V| − |E| + |F| = 1` for the shell and `2` for its completion, written without subtraction:21`(πn + 1) + πn = 2πn + 1` and `((π−1)n + 2) + πn = (2π−1)n + 2`. -/22theorem euler_characteristic (m n : Nat) :23    ((m + 1) * n + 1) + (m + 1) * n = 2 * ((m + 1) * n) + 1 ∧24    (m * n + 2) + (m + 1) * n = (2 * m + 1) * n + 2 := by25  constructor26  · rw [Nat.two_mul, Nat.add_right_comm]27  · rw [FRC.Nat.add_mul, FRC.Nat.add_mul, Nat.one_mul, FRC.Nat.mul_assoc, Nat.two_mul,28      FRC.Nat.add_add_add_comm, Nat.add_comm 2 n, ← Nat.add_assoc]2930/-- 2:E3 — the fixed-shell gap at `p = 13`, `g = 2` (window `x ≤ 6`): no grid point `x / 2^n`31lies strictly between `3/4` and `1` at any depth `n` — the covering radius of the fixed-shell32refinement in `[0, 1]` is at least `1/8` for every depth. -/33theorem fixed_shell_gap (n x : Nat) (hx : x ≤ 6) : ¬ (3 * 2 ^ n < 4 * x ∧ x < 2 ^ n) := by34  intro h35  match Nat.lt_or_ge n 3 with36  | .inl hn =>37    exact (by decide : ∀ n, n < 3 → ∀ x, x ≤ 6 → ¬ (3 * 2 ^ n < 4 * x ∧ x < 2 ^ n)) n hn x hx h38  | .inr hn =>39    have h8 : 2 ^ 3 ≤ 2 ^ n := Nat.pow_le_pow_right (Nat.zero_lt_succ 1) hn40    have h24 : 4 * x ≤ 4 * 6 := Nat.mul_le_mul_left 4 hx41    have h24' : 3 * 2 ^ 3 ≤ 3 * 2 ^ n := Nat.mul_le_mul_left 3 h842    exact Nat.lt_irrefl _ (Nat.lt_of_lt_of_le (Nat.lt_of_le_of_lt h24' h.1) h24)4344/-- 2:E3 (the fixed-shell bound, every shell) — for `g ≥ 2`, any cut `m`, depth `n` and `x ≤ 2κ` with45`x < g^n` (the grid point `x/g^n` below `1`): either `x/g^n ≤ 1 − g^{−m}`, i.e. `x·g^m + g^n ≤ g^m·g^n`,46or `x/g^n ≤ 2κ·g^{−(m+1)}`, i.e. `x·g^{m+1} ≤ 2κ·g^n`. With `2κ + 1 < g^{m+1}` both bounds are below `1`, so the47covering radius of the fixed-shell refinement in `[0, 1]` is bounded below at every depth. -/48theorem fixed_shell_bound (g κ m n x : Nat) (hg : 2 ≤ g) (hx : x ≤ 2 * κ) (hlt : x < g ^ n) :49    x * g ^ m + g ^ n ≤ g ^ m * g ^ n ∨ x * g ^ (m + 1) ≤ 2 * κ * g ^ n := by50  have hg1 : 1 ≤ g := Nat.le_trans (Nat.le_succ 1) hg51  match Nat.lt_or_ge n (m + 1) with52  | .inl hnm =>53    -- n ≤ m: x + 1 ≤ g^n, so x·g^m + g^m ≤ g^n·g^m, and g^n ≤ g^m54    refine .inl ?_55    have hn : n ≤ m := Nat.le_of_lt_succ hnm56    have h1 : (x + 1) * g ^ m ≤ g ^ n * g ^ m := Nat.mul_le_mul_right _ hlt57    have h2 : g ^ n ≤ g ^ m := Nat.pow_le_pow_right (Nat.lt_of_lt_of_le (Nat.zero_lt_succ 0) hg1) hn58    rw [FRC.Nat.add_mul, Nat.one_mul] at h159    calc x * g ^ m + g ^ n ≤ x * g ^ m + g ^ m := Nat.add_le_add_left h2 _60      _ ≤ g ^ n * g ^ m := h161      _ = g ^ m * g ^ n := Nat.mul_comm _ _62  | .inr hnm =>63    refine .inr ?_64    have h1 : g ^ (m + 1) ≤ g ^ n := Nat.pow_le_pow_right (Nat.lt_of_lt_of_le (Nat.zero_lt_succ 0) hg1) hnm65    exact Nat.mul_le_mul hx h16667/-- The cut `m = ⌊log_g(2κ+1)⌋`, i.e. `2κ + 1 < g^{m+1}`, puts the second bound below `1`68(`2κ·g^n < g^{m+1}·g^n`); the first is below `1` for every `m` (`g^m·g^n − g^n < g^m·g^n`). -/69theorem fixed_shell_bound_lt_one (g κ m n : Nat) (hg : 2 ≤ g) (hm : 2 * κ + 1 < g ^ (m + 1)) :70    2 * κ * g ^ n < g ^ (m + 1) * g ^ n ∧ 0 < g ^ n := by71  have hg1 : 1 ≤ g := Nat.le_trans (Nat.le_succ 1) hg72  have hpos : 0 < g ^ n := Nat.pow_pos (Nat.lt_of_lt_of_le (Nat.zero_lt_succ 0) hg1)73  exact ⟨FRC.Nat.mul_lt_mul_of_lt_of_pos (Nat.lt_of_le_of_lt (Nat.le_succ _) hm) hpos, hpos⟩7475/-! ### 2:B4 — which reindexings of the phase cycle are cellular -/7677/-- `m` and `m'` are adjacent on the phase cycle of length `n`. -/78def Adj (n m m' : Nat) : Prop := (m + 1) % n = m' ∨ (m' + 1) % n = m7980/-- The reindexing `ρ_u : m ↦ u·m mod n`. -/81def rho (n u m : Nat) : Nat := (u * m) % n8283/-- 2:B4, 2:C4 (Prop. 2.8) — `ρ_u` preserves the adjacency of the phase cycle (`n ≥ 3`) exactly when84`u ≡ 1` or `u ≡ −1 (mod n)`. -/85theorem rho_adj_iff (n u : Nat) (hn : 3 ≤ n) :86    (∀ m, m < n → Adj n (rho n u m) (rho n u ((m + 1) % n))) ↔ (u % n = 1 ∨ u % n = n - 1) := by87  have hn0 : 0 < n := Nat.lt_of_lt_of_le (Nat.zero_lt_succ 2) hn88  have h1n : 1 < n := Nat.lt_of_lt_of_le (Nat.lt_succ_self 1) (Nat.le_trans (Nat.le_succ 2) hn)89  constructor90  · intro h91    have h0 := h 0 hn092    unfold rho at h093    rw [Nat.mul_zero, FRC.Nat.zero_mod, Nat.zero_add, FRC.Nat.mod_eq_of_lt h1n, Nat.mul_one] at h094    -- Adj n 0 (u % n): (0 + 1) % n = u % n, or (u % n + 1) % n = 095    match h0 with96    | Or.inl e => exact Or.inl (by rw [Nat.zero_add, FRC.Nat.mod_eq_of_lt h1n] at e; exact e.symm)97    | Or.inr e =>98      refine Or.inr ?_99      have hu := Nat.mod_lt u hn0100      exact match Nat.lt_or_ge (u % n + 1) n with101        | Or.inl hlt => by102            rw [FRC.Nat.mod_eq_of_lt hlt] at e103            exact absurd e (Nat.succ_ne_zero _)104        | Or.inr hge =>105            have : u % n + 1 = n := Nat.le_antisymm hu hge106            calc u % n = (u % n + 1) - 1 := (FRC.Nat.add_sub_cancel _ _).symm107              _ = n - 1 := by rw [this]108  · intro h m hm109    unfold rho Adj110    match h with111    | Or.inl e =>112      -- u ≡ 1: ρ is the identity on residues113      have e1 : ∀ x, x < n → (u * x) % n = x := fun x hx => by114        rw [← FRC.Nat.mod_mul_mod _ _ _ hn0, e, Nat.one_mul, FRC.Nat.mod_eq_of_lt hx]115      rw [e1 m hm, e1 _ (Nat.mod_lt _ hn0)]116      exact Or.inl rfl117    | Or.inr e =>118      -- u ≡ −1: ρ is the reflection m ↦ (n − m) % n, and rev (m+1) + 1 ≡ rev m119      have e1 : ∀ x, x < n → (u * x) % n = Shell.Frame.rev n x := fun x hx => by120        unfold Shell.Frame.rev121        rw [← FRC.Nat.mod_mul_mod _ _ _ hn0, e]122        exact match Nat.decEq x 0 with123          | isTrue hx0 => by rw [hx0, Nat.mul_zero, Nat.sub_zero, FRC.Nat.zero_mod, FRC.Nat.mod_self n hn0]124          | isFalse hx0 => by125              have hx0' := Nat.pos_of_ne_zero hx0126              -- (n − 1)·x = n·(x − 1) + (n − x)127              have : (n - 1) * x = n * (x - 1) + (n - x) := by128                have h1 : (n - 1) * x + x = n * x := by129                  rw [← Nat.succ_mul, Nat.succ_eq_add_one, FRC.Nat.sub_add_cancel (Nat.le_of_lt h1n)]130                have h2 : n * (x - 1) + n = n * x := by131                  rw [← Nat.mul_succ, Nat.succ_eq_add_one, FRC.Nat.sub_add_cancel hx0']132                have h3 : n * (x - 1) + (n - x) + x = n * x := by133                  rw [Nat.add_assoc, FRC.Nat.sub_add_cancel (Nat.le_of_lt hx), h2]134                exact FRC.Nat.add_right_cancel (h1.trans h3.symm)135              rw [this, FRC.Nat.add_mul_mod_self_left _ _ _ hn0]136      rw [e1 m hm, e1 _ (Nat.mod_lt _ hn0)]137      -- rev (m+1 mod n) + 1 ≡ rev m: both ≡ −m138      refine Or.inr ?_139      exact match Nat.lt_or_ge (m + 1) n with140        | Or.inl hlt => by141            rw [FRC.Nat.mod_eq_of_lt hlt]142            exact match Nat.decEq m 0 with143              | isTrue e0 => by144                  rw [e0] at hlt ⊢145                  rw [Shell.Frame.rev_zero _ hn0, Shell.Frame.rev_of_pos hlt (Nat.zero_lt_succ 0), Nat.zero_add,146                    FRC.Nat.sub_add_cancel (Nat.le_of_lt h1n)]147                  exact FRC.Nat.mod_self n hn0148              | isFalse e0 => by149                  have hm0 := Nat.pos_of_ne_zero e0150                  rw [Shell.Frame.rev_of_pos hlt (Nat.zero_lt_succ m), Shell.Frame.rev_of_pos hm hm0]151                  -- (n − (m+1)) + 1 = n − m, below n152                  have : n - (m + 1) + 1 = n - m := by153                    have h1 : n - (m + 1) + (m + 1) = n := FRC.Nat.sub_add_cancel (Nat.le_of_lt hlt)154                    have h2 : n - m + m = n := FRC.Nat.sub_add_cancel (Nat.le_of_lt hm)155                    apply FRC.Nat.add_right_cancel (c := m)156                    rw [h2, Nat.add_assoc, Nat.add_comm 1 m, h1]157                  rw [this]158                  exact FRC.Nat.mod_eq_of_lt (Nat.sub_lt hn0 hm0)159        | Or.inr hge => by160            -- m + 1 = n: m = n − 1, rev 0 + 1 = 1, rev (n−1) = 1161            have hmn : m + 1 = n := Nat.le_antisymm hm hge162            rw [hmn, FRC.Nat.mod_self _ hn0, Shell.Frame.rev_zero _ hn0, Nat.zero_add, FRC.Nat.mod_eq_of_lt h1n]163            have hm0 : 0 < m := by164              refine Nat.lt_of_add_lt_add_right (n := 1) ?_165              rw [Nat.zero_add, hmn]; exact h1n166            rw [Shell.Frame.rev_of_pos hm hm0, ← hmn, FRC.Nat.add_sub_cancel_left]167168/-- 2:B4 — the rotations `m ↦ m + c` preserve adjacency (with `ρ_{±1}` they generate the dihedral maps of B4). -/169theorem rotation_adj (n c m : Nat) (hn : 0 < n) : Adj n ((m + c) % n) (((m + 1) % n + c) % n) := by170  unfold Adj171  refine Or.inl ?_172  rw [FRC.Nat.mod_add_mod _ _ _ hn, FRC.Nat.mod_add_mod _ _ _ hn, Nat.add_right_comm]173174/-! ### 2:C4 — the frame moves the labels of one complex -/175176variable {p : Nat} [Pos p]177178/-- The action reading of the vertex `(a, m)` in the frame with drive `g`: `a · g^m`. -/179def label (g : Shell p) (a : Shell p) (m : Nat) : Shell p := a * g ^ m180181/-- 2:C4 (Prop. 3.5) — the complex is one for every generator; the frame `g' = g^u` moves the182labels by the reindexing `ρ_u`: `label g' (a, m) = label g (a, u·m mod n)`. -/183theorem label_covariance {κ : Nat} {g : Shell p} (F : Shell.Frame p κ g) (u : Nat) (a : Shell p) (m : Nat) :184    label (g ^ u) a m = label g a (rho (p - 1) u m) := by185  unfold label rho186  rw [← Shell.pow_mul, F.pow_mod (u * m)]187188189/-! ### 2:E3 — the floor of the fixed-shell bound -/190191/-- 2:E3 — the floor: with `2κ + 1 < g^{m+1}` the second bound `2κ·g^{−(m+1)}` leaves a gap below `1` longer than192`1/(2κ+1)`, i.e. `g^{m+1} < (g^{m+1} − 2κ)·(2κ + 1)`; with `g^m ≤ 2κ + 1` the first gap `g^{−m}` is at least `1/(2κ+1)`193by hypothesis, so the covering radius is at least `1/(4κ+2) = 1/(p+1)`. -/194theorem fixed_shell_floor (g κ m : Nat) (hκ : 0 < κ) (hm : 2 * κ + 1 < g ^ (m + 1)) :195    g ^ (m + 1) < (g ^ (m + 1) - 2 * κ) * (2 * κ + 1) := by196  have hle : 2 * κ ≤ g ^ (m + 1) := Nat.le_of_lt (Nat.lt_of_le_of_lt (Nat.le_succ _) hm)197  have h2k : 0 < 2 * κ := Nat.mul_pos (Nat.zero_lt_succ 1) hκ198  have hG : g ^ (m + 1) = (g ^ (m + 1) - 2 * κ) + 2 * κ := (FRC.Nat.sub_add_cancel hle).symm199  generalize hT : g ^ (m + 1) - 2 * κ = t at hG ⊢200  have ht : 1 < t := by201    have h' : 1 + 2 * κ < t + 2 * κ := by rw [Nat.add_comm 1, ← hG]; exact hm202    exact Nat.lt_of_add_lt_add_right h'203  rw [hG, Nat.mul_add, Nat.mul_one, Nat.add_comm (t * (2 * κ)) t]204  refine Nat.add_lt_add_left ?_ t205  calc 2 * κ = 1 * (2 * κ) := (Nat.one_mul _).symm206    _ < t * (2 * κ) := Nat.mul_lt_mul_of_pos_right ht h2k207208/-! ### 2:E4 — the Lipschitz budget of a bounded experiment -/209210/-- 2:E4 — the budget: `r ≤ L` marked points, each within `d` of its vertex, move an `L`-Lipschitz observable by at211most `L·(r·d) ≤ L·(L·d)`, the bound `L²·δ_p` of the operational theorem in counts. -/212theorem lipschitz_budget (L r d : Nat) (h : r ≤ L) : L * (r * d) ≤ L * (L * d) :=213  Nat.mul_le_mul_left L (Nat.mul_le_mul_right d h)214215/-! ### 2:F6 — the exponents of the external transport -/216217section transport218variable {p : Nat} [Pos p]219220/-- 2:F6 — the external transport in its exponents: the half-period shifts by `−1`, `g^{m+2κ} = −g^m`; the oriented221quarter-turn shifts by three quarters, `i·g^m = g^{m+3κ}` (with `i = −g^κ`, so `χ(i·g^m) = i·χ(g^m)` in the chart);222and the kernel, `(g^j)^r = g^{jr}`. -/223theorem transport_exponents {κ : Nat} {g : Shell p} (F : Shell.Frame p κ g) (m j r : Nat) :224    g ^ (m + 2 * κ) = -(g ^ m) ∧ Shell.Frame.quarterTurn g κ * g ^ m = g ^ (m + 3 * κ) ∧ (g ^ j) ^ r = g ^ (j * r) := by225  have hh : g ^ (m + 2 * κ) = -(g ^ m) := by226    rw [Shell.pow_add, F.half_period, ← Shell.mul_neg, Shell.mul_one]227  refine ⟨hh, ?_, (Shell.pow_mul g j r).symm⟩228  unfold Shell.Frame.quarterTurn229  have h3 : m + 3 * κ = (m + 2 * κ) + κ := by230    rw [Nat.add_assoc, show 3 * κ = 2 * κ + κ from Nat.succ_mul 2 κ]231  rw [h3, Shell.pow_add, hh, ← Shell.neg_mul, ← Shell.neg_mul, Shell.mul_comm]232233end transport234/-! ### 2:D6 — the two orientation classes on the laboratory shell -/235236set_option maxRecDepth 20000 in237/-- 2:D6 [value] — on `𝔽₁₃` the frame `g = 2` reads `i = 5` (odd: `e^{iπ} = −1`) and the frame `g = 7` reads `i = 8`238(even: `e^{iπ} = +1`); `7 = 2^{11}` with `11 ≡ 3 (mod 4)` flips the orientation. -/239theorem s13_orientation :240    Shell.Frame.quarterTurn (2 : Shell 13) 3 = 5 ∧ Shell.Frame.quarterTurn (7 : Shell 13) 3 = 8 ∧241    ((2 : Shell 13) ^ 5) ^ (5 * 6) = -1 ∧ ((7 : Shell 13) ^ 8) ^ (8 * 6) = 1 ∧242    (2 : Shell 13) ^ 11 = 7 := by decide243244end Geometry245end FRC246