Geometry.lean — FrcLedger

1import Mathlib2import FrcLedger.Theme.Fourier34/-!5# 2-geometry — the ledger predicates in Lean (2026-09-17)67Predicates of the ledger of *Geometry and Constants in Finite Ring Continuum* (Symmetry 2026, 18, 751;8tree `2-geometry-20260706`). Compiled 17 Sep 2026, standard axioms only (`axioms.log`). Every universal statement is over an9arbitrary finite field `F` with `Fintype.card F = 4κ + 1` (the shell) and a primitive root `g`; the cell counts10are integer identities; the fixed-shell bound is decided over `ℚ` (the `(13, 2)` instance over `ℕ`); the11Fourier inversion is the matrix identity `W · (−W J) = 1` on `Fin (p − 1)`, from the relations of `FrcLedger.Fourier`.12-/1314namespace FRC.Geometry1516open Finset1718section shell1920variable {F : Type*} [Field F] [Fintype F]2122/-- 2:D1 (Prop. 4.1, the shell half-period): `g^π = −1` for `π = 2κ` and every primitive root `g`. -/23theorem half_period (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) (g : F)24    (hg : IsPrimitiveRoot g (Fintype.card F - 1)) : g ^ (2 * κ) = -1 := by25  have h := FRC.DFT.quarter_turn_sq κ hκ g hg26  have : (-(g ^ κ)) ^ 2 = g ^ (2 * κ) := by ring27  rwa [this] at h2829/-- 2:D2 (Prop. 4.3, the quarter-turn structure): `i = −g^κ` squares to `−1`, so `g^κ` has order four. -/30theorem quarter_turn_order (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) (g : F)31    (hg : IsPrimitiveRoot g (Fintype.card F - 1)) :32    (g ^ κ) ^ 2 = -1 ∧ (g ^ κ) ^ 4 = 1 := by33  have h := FRC.DFT.quarter_turn_sq κ hκ g hg34  have h2 : (g ^ κ) ^ 2 = -1 := by rw [← h]; ring35  refine ⟨h2, ?_⟩36  rw [show (4 : ℕ) = 2 * 2 by norm_num, pow_mul, h2]; ring3738/-- 2:D5 (Remark 4.11 — the orientation classes): under `g' = g^u` the oriented quarter-turn39`i' = −g'^κ` equals `i = −g^κ` when `u ≡ 1 (mod 4)` and `−i` when `u ≡ 3 (mod 4)`. -/40theorem orientation_class (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) (g : F)41    (hg : IsPrimitiveRoot g (Fintype.card F - 1)) (u : ℕ) :42    (u % 4 = 1 → -((g ^ u) ^ κ) = -(g ^ κ)) ∧ (u % 4 = 3 → -((g ^ u) ^ κ) = -(-(g ^ κ))) := by43  have h4 : (g ^ κ) ^ 4 = 1 := (quarter_turn_order κ hκ g hg).244  have h2 : (g ^ κ) ^ 2 = -1 := (quarter_turn_order κ hκ g hg).145  have key : (g ^ u) ^ κ = (g ^ κ) ^ u := by rw [← pow_mul, ← pow_mul, mul_comm]46  have hu : (g ^ κ) ^ u = (g ^ κ) ^ (u % 4) := by47    conv_lhs => rw [← Nat.mod_add_div u 4, pow_add, pow_mul, h4, one_pow, mul_one]48  constructor49  · intro h1; rw [key, hu, h1, pow_one]50  · intro h3; rw [key, hu, h3, show (3 : ℕ) = 2 + 1 by norm_num, pow_add, h2, pow_one]; ring5152/-- 2:D6 (the Euler identity on the shell, master C14): with `e = g^i` and `π = 2κ`, `e^(iπ) = (−1)^i`53for any integer reading `i` of the quarter-turn — `−1` exactly when that reading is odd. -/54theorem euler_identity (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) (g : F)55    (hg : IsPrimitiveRoot g (Fintype.card F - 1)) (i : ℕ) :56    (g ^ i) ^ (i * (2 * κ)) = (-1 : F) ^ i := by57  have hπ := half_period κ hκ g hg58  rw [← pow_mul, show i * (i * (2 * κ)) = (2 * κ) * (i * i) by ring, pow_mul, hπ]59  rcases Nat.even_or_odd i with he | ho60  · rw [he.neg_one_pow, (he.mul_right i).neg_one_pow]61  · rw [ho.neg_one_pow, (ho.mul ho).neg_one_pow]6263/-- 2:B3 (Props. 2.7, 4.5, the primitive generators form one orbit): the primitive roots of unity of order64`n = card F − 1` are exactly the `g^u` with `u < n` coprime to `n`. -/65theorem generator_orbit (g : F) (hg : IsPrimitiveRoot g (Fintype.card F - 1)) (h : F) :66    IsPrimitiveRoot h (Fintype.card F - 1) ↔67      ∃ u, u < Fintype.card F - 1 ∧ Nat.Coprime u (Fintype.card F - 1) ∧ h = g ^ u := by68  have hn : 0 < Fintype.card F - 1 := by have := Fintype.one_lt_card (α := F); omega69  have : NeZero (Fintype.card F - 1) := ⟨by omega⟩70  constructor71  · intro hh72    obtain ⟨u, hu, rfl⟩ := hg.eq_pow_of_pow_eq_one hh.pow_eq_one73    exact ⟨u, hu, (hg.pow_iff_coprime hn u).mp hh, rfl⟩74  · rintro ⟨u, -, hcop, rfl⟩75    exact (hg.pow_iff_coprime hn u).mpr hcop7677/-- 2:F1 (Prop. 6.1, root-of-unity facts): `Σ_j g^{jk} = 0` for `0 < k < n`, and `n = card F − 1` reads as78`−1` in `F`. -/79theorem principal_root (g : F) (hg : IsPrimitiveRoot g (Fintype.card F - 1)) (k : ℕ) (hk0 : 0 < k)80    (hk : k < Fintype.card F - 1) :81    (∑ j ∈ range (Fintype.card F - 1), (g ^ k) ^ j = 0) ∧ ((Fintype.card F - 1 : ℕ) : F) = -1 := by82  refine ⟨?_, FRC.DFT.natCast_card_pred_eq_neg_one⟩83  have hne : g ^ k ≠ 1 := fun h => by84    have := hg.pow_eq_one_iff_dvd k |>.mp h85    exact absurd (Nat.le_of_dvd hk0 this) (not_le.mpr hk)86  have hpow : (g ^ k) ^ (Fintype.card F - 1) = 1 := by87    rw [← pow_mul, mul_comm, pow_mul, hg.pow_eq_one, one_pow]88  have h := geom_sum_mul (g ^ k) (Fintype.card F - 1)89  rw [hpow, sub_self] at h90  exact (mul_eq_zero.1 h).resolve_right (sub_ne_zero.2 hne)9192/-- 2:F3 (Prop. 6.3, inversion): on every shell the inverse of the Fourier matrix `W_g` (`W k j = g^{jk}`) is93`−W_g J`, whose entry at `(k, j)` is `−g^{−jk}`: `W_g · (−W_g J) = 1`. -/94theorem dft_inverse (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) (g : F)95    (hg : IsPrimitiveRoot g (Fintype.card F - 1)) :96    haveI : NeZero (Fintype.card F - 1) := ⟨by have := Fintype.one_lt_card (α := F); omega⟩97    (FRC.DFT.W g : Matrix (Fin (Fintype.card F - 1)) (Fin (Fintype.card F - 1)) F) *98        (-(FRC.DFT.W g * FRC.DFT.J)) = 1 ∧99    ∀ k j : Fin (Fintype.card F - 1),100      (-(FRC.DFT.W g * FRC.DFT.J) :101        Matrix (Fin (Fintype.card F - 1)) (Fin (Fintype.card F - 1)) F) k j102        = -(g ^ ((j : ℕ) * (k : ℕ)))⁻¹ := by103  have : NeZero (Fintype.card F - 1) := ⟨by have := Fintype.one_lt_card (α := F); omega⟩104  obtain ⟨hW, -, -, -⟩ := FRC.DFT.shell_relations κ hκ g hg105  constructor106  · rw [mul_neg, ← mul_assoc, ← sq, hW, neg_mul, neg_neg, ← sq, FRC.DFT.J_sq]107  · intro k j108    rw [Matrix.neg_apply, Matrix.mul_apply]109    simp only [FRC.DFT.W_apply, FRC.DFT.J_apply, mul_ite, mul_one, mul_zero]110    rw [Finset.sum_eq_single (-j)]111    · rw [ite_eq_left (by rw [neg_neg]), pow_mul, FRC.DFT.pow_neg_val hg.pow_eq_one j, inv_pow,112        ← pow_mul]113    · intro x _ hx114      rw [ite_eq_right (fun h => hx (by rw [h, neg_neg]))]115    · intro h; exact absurd (Finset.mem_univ _) h116117end shell118119/-- 2:C2 (Remark 3.4, the counts): for the orbital shell, `χ = V − E + F = 1`; for its completion, `χ = 2`120(`π = 2κ`, `n = p − 1`), as integer identities. -/121theorem euler_characteristic (π n : ℤ) :122    (π * n + 1) - 2 * π * n + π * n = 1 ∧ ((π - 1) * n + 2) - (2 * π - 1) * n + π * n = 2 := by123  constructor <;> ring124125/-- 2:E3 (the fixed-shell gap of Prop. 5.5 at `p = 13`, `g = 2`, `H = 6`): no grid point `x / 2^n`126with `0 ≤ x ≤ 6` lies strictly between `3/4` and `1`, at any depth `n` — the covering radius of the127fixed-shell refinement in `[0, 1]` is at least `1/8` for every `N`. -/128theorem fixed_shell_gap (n x : ℕ) (hx : x ≤ 6) : ¬ (3 * 2 ^ n < 4 * x ∧ x < 2 ^ n) := by129  rintro ⟨h1, h2⟩130  have hn : n < 3 := by131    by_contra hn; push Not at hn132    have := Nat.pow_le_pow_right (by norm_num : 0 < 2) hn133    omega134  interval_cases n <;> omega135136/-- The same, read in `ℚ`: no `x / 2^n` with `x ≤ 6` lies in the open interval `(3/4, 1)`. -/137theorem fixed_shell_gap_rat (n x : ℕ) (hx : x ≤ 6) :138    ¬ ((3 / 4 : ℚ) < x / 2 ^ n ∧ (x : ℚ) / 2 ^ n < 1) := by139  rintro ⟨h1, h2⟩140  have h2n : (0 : ℚ) < 2 ^ n := by positivity141  rw [lt_div_iff₀ h2n] at h1142  rw [div_lt_iff₀ h2n] at h2143  apply fixed_shell_gap n x hx144  constructor145  · have : (3 * 2 ^ n : ℚ) < 4 * x := by linarith146    exact_mod_cast this147  · have : (x : ℚ) < 2 ^ n := by linarith148    exact_mod_cast this149150/-- 2:E3 (the fixed-shell bound, every shell): for any depth cut `m`, every grid point `x / g^n` with151`x ≤ 2κ` that lies below `1` is at most `max (1 − g^{−m}) (2κ · g^{−(m+1)})`; with `m = ⌊log_g(2κ+1)⌋`152that bound is below `1` (`fixed_shell_bound_lt_one`), so the interval above it is free at every depth153and the covering radius of the fixed-shell refinement in `[0, 1]` is bounded below independently of `N`. -/154theorem fixed_shell_bound (g κ m n x : ℕ) (hg : 2 ≤ g) (hx : x ≤ 2 * κ)155    (hlt : (x : ℚ) / (g : ℚ) ^ n < 1) :156    (x : ℚ) / (g : ℚ) ^ n ≤ max (1 - 1 / (g : ℚ) ^ m) (2 * (κ : ℚ) / (g : ℚ) ^ (m + 1)) := by157  have hg0 : (0 : ℚ) < g := by exact_mod_cast (by omega : 0 < g)158  have hg1 : (1 : ℚ) ≤ g := by exact_mod_cast (by omega : 1 ≤ g)159  have hgn : (0 : ℚ) < (g : ℚ) ^ n := pow_pos hg0 n160  rcases le_or_gt n m with hnm | hnm161  · refine le_max_of_le_left ?_162    have hxn : x < g ^ n := by163      have h := (div_lt_one hgn).mp hlt164      exact_mod_cast h165    have hx1 : (x : ℚ) ≤ (g : ℚ) ^ n - 1 := by166      have h : ((x + 1 : ℕ) : ℚ) ≤ ((g ^ n : ℕ) : ℚ) := by exact_mod_cast hxn167      push_cast at h; linarith168    have hgm : (0 : ℚ) < (g : ℚ) ^ m := pow_pos hg0 m169    have hnm' : (g : ℚ) ^ n ≤ (g : ℚ) ^ m := pow_le_pow_right₀ hg1 hnm170    have hq : (g : ℚ) ^ n / (g : ℚ) ^ m ≤ 1 := (div_le_one hgm).mpr hnm'171    rw [div_le_iff₀ hgn]172    calc (x : ℚ) ≤ (g : ℚ) ^ n - 1 := hx1173      _ ≤ (g : ℚ) ^ n - (g : ℚ) ^ n / (g : ℚ) ^ m := by linarith174      _ = (1 - 1 / (g : ℚ) ^ m) * (g : ℚ) ^ n := by ring175  · refine le_max_of_le_right ?_176    have hgm1 : (0 : ℚ) < (g : ℚ) ^ (m + 1) := pow_pos hg0 _177    have hpow : (g : ℚ) ^ (m + 1) ≤ (g : ℚ) ^ n := pow_le_pow_right₀ hg1 hnm178    have hx' : (x : ℚ) ≤ 2 * (κ : ℚ) := by exact_mod_cast hx179    calc (x : ℚ) / (g : ℚ) ^ n ≤ (2 * (κ : ℚ)) / (g : ℚ) ^ n :=180          div_le_div_of_nonneg_right hx' hgn.le181      _ ≤ (2 * (κ : ℚ)) / (g : ℚ) ^ (m + 1) :=182          div_le_div_of_nonneg_left (by positivity) hgm1 hpow183184/-- The cut `m = ⌊log_g(2κ+1)⌋` (`2κ + 1 < g^(m+1)`) puts the bound of `fixed_shell_bound` strictly below `1`. -/185theorem fixed_shell_bound_lt_one (g κ m : ℕ) (hg : 2 ≤ g) (hm : 2 * κ + 1 < g ^ (m + 1)) :186    max (1 - 1 / (g : ℚ) ^ m) (2 * (κ : ℚ) / (g : ℚ) ^ (m + 1)) < 1 := by187  have hg0 : (0 : ℚ) < g := by exact_mod_cast (by omega : 0 < g)188  have hgm1 : (0 : ℚ) < (g : ℚ) ^ (m + 1) := pow_pos hg0 _189  refine max_lt ?_ ?_190  · have : (0 : ℚ) < 1 / (g : ℚ) ^ m := by positivity191    linarith192  · rw [div_lt_one hgm1]193    have h : ((2 * κ : ℕ) : ℚ) < ((g ^ (m + 1) : ℕ) : ℚ) := by exact_mod_cast (by omega : 2 * κ < g ^ (m + 1))194    push_cast at h; exact h195196-- Ledger predicates of 2-geometry (generated by make_predicates.py from docs/2-geometry/2-geometry-ledger.json; edit the ledger, not this section)197/-- 2:B3 (p02007) — Primitive generators form one orbit: every generator is $\gen^{u}$ with $u\in\Z_{\p-1}^{\times}$, a torsor for $\operatorname{Aut}(C_{\p-1})$ (Props.~\ref{prop:primitive-orbit}, \ref{prop:no-canonical-e}). -/198theorem p02007 : ∀ {F : Type u_1} [Field F] [Fintype F] (g : F), IsPrimitiveRoot g (Fintype.card F - (1 : ℕ)) → ∀ (h : F), IsPrimitiveRoot h (Fintype.card F - (1 : ℕ)) ↔ ∃ u < Fintype.card F - (1 : ℕ), u.Coprime (Fintype.card F - (1 : ℕ)) ∧ h = g ^ u :=199  @FRC.Geometry.generator_orbit200/-- 2:C2 (p02010) — Counts: $|V|=\pi(\p-1)+1$, $|E|=2\pi(\p-1)$, $|F|=\pi(\p-1)$, $\chi(\Sp)=1$; the completion has $(\pi-1)(\p-1)+2$ vertices, $(2\pi-1)(\p-1)$ edges, $\pi(\p-1)$ faces, $\chi=2$ (Rem.~\ref{rem:cell-counts}). -/201theorem p02010 : ∀ (π n : ℤ), π * n + (1 : ℤ) - (2 : ℤ) * π * n + π * n = (1 : ℤ) ∧ (π - (1 : ℤ)) * n + (2 : ℤ) - ((2 : ℤ) * π - (1 : ℤ)) * n + π * n = (2 : ℤ) :=202  @FRC.Geometry.euler_characteristic203/-- 2:D1 (p02013) — The half-period: $\gen^{\pi}=-1$ for every primitive $\gen$, $\pi=2\kap$ (Prop.~\ref{prop:half-period}); $2\pi\equiv-1$ (00:C1). -/204theorem p02013 : ∀ {F : Type u_1} [Field F] [Fintype F] (κ : ℕ), Fintype.card F = (4 : ℕ) * κ + (1 : ℕ) → ∀ (g : F), IsPrimitiveRoot g (Fintype.card F - (1 : ℕ)) → g ^ ((2 : ℕ) * κ) = (-1 : F) :=205  @FRC.Geometry.half_period206/-- 2:D2 (p02014) — The quarter-turn subgroup $\Qp=\{x:x^{4}=1\}$ is the unique subgroup of order four; $\gen^{\kap}$ has order four with $(\gen^{\kap})^{2}=-1$; $\Qp=\{\pm1,\pm\It\}$ (Def.~\ref{def:quarter-turn-subgroup}, Prop.~\ref{prop:quarter-turn}; 1:B2). -/207theorem p02014 : ∀ {F : Type u_1} [Field F] [Fintype F] (κ : ℕ), Fintype.card F = (4 : ℕ) * κ + (1 : ℕ) → ∀ (g : F), IsPrimitiveRoot g (Fintype.card F - (1 : ℕ)) → (g ^ κ) ^ (2 : ℕ) = (-1 : F) ∧ (g ^ κ) ^ (4 : ℕ) = (1 : F) :=208  @FRC.Geometry.quarter_turn_order209/-- 2:D5 (p02017) — Orientation classes: for $\gen'=\gen^{u}$, $\It'=-\gen'^{\kap}$ equals $\It$ when $u\equiv1\pmod4$ and $-\It$ when $u\equiv3\pmod4$; the oriented quarter-turn is frame-covariant within one class of generators, not under every generator change. -/210theorem p02017 : ∀ {F : Type u_1} [Field F] [Fintype F] (κ : ℕ), Fintype.card F = (4 : ℕ) * κ + (1 : ℕ) → ∀ (g : F), IsPrimitiveRoot g (Fintype.card F - (1 : ℕ)) → ∀ (u : ℕ), (u % (4 : ℕ) = (1 : ℕ) → -(g ^ u) ^ κ = -g ^ κ) ∧ (u % (4 : ℕ) = (3 : ℕ) → -(g ^ u) ^ κ = - -g ^ κ) :=211  @FRC.Geometry.orientation_class212/-- 2:D6 (p02018) — The Euler identity on the shell: $\eu^{\It\pi}=\gen^{2\kap\It^{2}}=(-1)^{\It}$, equal to $-1$ exactly when the representative of $\It$ is odd (00:C14); the oriented frames of a shell are those with $-\gen^{\kap}$ odd --- on $\F_{13}$, $\gen=2$ ($\It=5$) is one, on $\F_{17}$, $\gen=3$ ($\It=4$) is not. -/213theorem p02018 : ∀ {F : Type u_1} [Field F] [Fintype F] (κ : ℕ), Fintype.card F = (4 : ℕ) * κ + (1 : ℕ) → ∀ (g : F), IsPrimitiveRoot g (Fintype.card F - (1 : ℕ)) → ∀ (i : ℕ), (g ^ i) ^ (i * ((2 : ℕ) * κ)) = (-1 : F) ^ i :=214  @FRC.Geometry.euler_identity215/-- 2:E3 (p02023) — Fixed-shell refinement is bounded: with $m=\lfloor\log_{\gen}(2\kap+1)\rfloor$ no point $x/\gen^{n}$, $|x|\le2\kap$, lies in $(\max(1-\gen^{-m},2\kap\gen^{-m-1}),1)$ at any depth, so the covering radius of the scale grid in $[0,1]$ is $\ge\tfrac12\min(\gen^{-m},1-2\kap\gen^{-m-1})$ for every $N$: $1/8$ at $(13,2)$, $5/22$ at $(13,11)$. -/216theorem p02023 : ∀ (g κ m n x : ℕ), (2 : ℕ) ≤ g → x ≤ (2 : ℕ) * κ → ↑x / ↑g ^ n < (1 : ℚ) → ↑x / ↑g ^ n ≤ max ((1 : ℚ) - (1 : ℚ) / ↑g ^ m) ((2 : ℚ) * ↑κ / ↑g ^ (m + (1 : ℕ))) :=217  @FRC.Geometry.fixed_shell_bound218/-- 2:F1 (p02025) — $\gen$ is a principal $n$-th root of unity, $n=\p-1$: $\gen^{n}=1$, $\sum_{j<n}\gen^{jk}=0$ for $0<k<n$, and $n^{-1}=-1$ in $\Fp$ (Prop.~\ref{prop:principal-root}; $2\pi\equiv-1$). -/219theorem p02025 : ∀ {F : Type u_1} [Field F] [Fintype F] (g : F), IsPrimitiveRoot g (Fintype.card F - (1 : ℕ)) → ∀ (k : ℕ), (0 : ℕ) < k → k < Fintype.card F - (1 : ℕ) → ∑ j ∈ Finset.range (Fintype.card F - (1 : ℕ)), (g ^ k) ^ j = (0 : F) ∧ ↑(Fintype.card F - (1 : ℕ)) = (-1 : F) :=220  @FRC.Geometry.principal_root221set_option linter.defProp false in222/-- 2:F3 (p02027) — Inversion: $v_{j}=-\sum_{k<n}\mathcal F_{\gen}(v)_{k}\gen^{-jk}$, i.e.\ $W_{\gen}^{-1}=-(\gen^{-jk})_{jk}=-W_{\gen}J$ (Prop.~\ref{prop:ring-dft-inverse}; 6:B5), exact on every shell. -/223def p02027 := @FRC.Geometry.dft_inverse224-- end ledger predicates225226end FRC.Geometry227