The core module lean/FrcCore/Keys/Algebra.lean — the substrate from first principles, no Mathlib, no axioms; one of the core's 137 modules (the index); it rests on 18 modules: Nat, Pigeonhole, Shell, Series, Ring, FrameCore, Frame, Parity, Transform, Orbit, Sum, Theme/Logic, Theme/Field, Theme/Foundation, Poly, Instances, Theme/Framed, Theme/Orbital: 8 theorems (0 definitions): 8 with no axioms, 0 at tier 1 (propext, Quot.sound), 0 at tier 2 (Classical.choice), 0 red; the mark's colour is the library's (green, the core; red a proof the gate rejects), each declaration's axioms on hover; the small plain glyph marks a definition (no proof, no axioms; on the ledger pages the plain glyph is instead a module cited as a whole). Each declaration is anchored; the ledger predicates cite them by name. ▶ open in Lean Live · axioms.log.
1import FrcCore.FrameCore2import FrcCore.Frame3import FrcCore.Theme.Orbital4import FrcCore.Theme.Framed56/-!7# FrcCore.Keys.Algebra — the keyed theorems of the algebra theme (ledger migration, task LM19)89One declaration per key, `FRC.Ledger.p<key>`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem10that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration11`FRC.<Module>.p<key>` as an alias. Every declaration has no axioms (`check_core_axioms.py`).12-/1314namespace FRC.Ledger1516-- Keys of the algebra theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file)17set_option linter.defProp false in18/-- p01011 — 1:C4. Involutions and counts: $M_n(a)=M_{n+2\kap}(-a)$ and $L_a(m)=L_{-a}(m+2\kap)$ since $\gen^{2\kap}=-1$; $\p-1$ distinct meridian lists in $2\kap$ great circles; $2\kap$ latitude pairs; one-sided vertex count $(\p-1)^{2}/2+1$, the double cover $(\p-1)^{2}$. -/19
def p01011 := And.intro @FRC.Shell.Frame.meridian_involution (And.intro @FRC.Shell.Frame.pow_inj (And.intro @FRC.Shell.Frame.sign_pair (And.intro @FRC.Shell.Frame.window_injective (And.intro @FRC.Shell.Frame.window_signed (@FRC.Shell.Frame.vertex_count)))))20/-- p01015 — 1:D4. Scale-periodicity, in the field: $S_n(x)=x\gen^{-n}$ satisfies $S_{n+(\p-1)}=S_n$, and the period is exact: for $x\neq0$, $x\gen^{-m}=x\gen^{-n}$ iff $m\equiv n\pmod{\p-1}$; each grid $G_n$ lists every residue once; the zoom has order $\p-1$. As lists of rationals $x/\gen^{n}$ the grids are not periodic. -/21theorem p01015 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (x : FRC.Shell p) (n : Nat), x * g ^ (n + (p - (1 : Nat))) = x * g ^ n) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g y : FRC.Shell p}, FRC.Shell.Frame p κ g → g * y = (1 : FRC.Shell p) → ∀ (x : FRC.Shell p) (n : Nat), x * y ^ (n + (p - (1 : Nat))) = x * y ^ n) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g y : FRC.Shell p}, FRC.Shell.Frame p κ g → g * y = (1 : FRC.Shell p) → ∀ {x : FRC.Shell p}, x ≠ (0 : FRC.Shell p) → ∀ (m n : Nat), x * y ^ m = x * y ^ n ↔ m % (p - (1 : Nat)) = n % (p - (1 : Nat))) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g y : FRC.Shell p}, FRC.Shell.Frame p κ g → g * y = (1 : FRC.Shell p) → ∀ (k : Nat), (∀ (x : FRC.Shell p), x * y ^ k = x) ↔ k % (p - (1 : Nat)) = (0 : Nat)) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g y : FRC.Shell p}, FRC.Shell.Frame p κ g → g * y = (1 : FRC.Shell p) → ∀ (n : Nat), (∀ (z : FRC.Shell p), z * g ^ n * y ^ n = z) ∧ ∀ (x x' : FRC.Shell p), x * y ^ n = x' * y ^ n → x = x' :=22 And.intro @FRC.Shell.Frame.scale_periodic (And.intro @FRC.Shell.Frame.scale_inv_periodic (And.intro @FRC.Shell.Frame.scale_exact (And.intro @FRC.Shell.Frame.zoom_order (@FRC.Shell.Frame.scale_bijective))))23/-- p01019 — 1:E2. The extension by $X^{2}+1$ is trivial: on the shell $\Fp[X]/(X^{2}+1)$ has zero divisors, $(X+\im)(X-\im)=0$, so it is not a field; $\Fp[X]/(X^{2}+1)$ is a field exactly when $\p\equiv3\pmod4$, every nonzero pair $(a,b)$ having the inverse $(a,-b)/(a^{2}+b^{2})$. -/24theorem p01019 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → FRC.Shell.Frame.cmul (FRC.Shell.Frame.quarterTurn g κ, (1 : FRC.Shell p)) (-FRC.Shell.Frame.quarterTurn g κ, (1 : FRC.Shell p)) = ((0 : FRC.Shell p), (0 : FRC.Shell p)) ∧ (FRC.Shell.Frame.quarterTurn g κ, (1 : FRC.Shell p)) ≠ ((0 : FRC.Shell p), (0 : FRC.Shell p)) ∧ (-FRC.Shell.Frame.quarterTurn g κ, (1 : FRC.Shell p)) ≠ ((0 : FRC.Shell p), (0 : FRC.Shell p))) ∧ ∀ {p : Nat} [FRC.Pos p], FRC.Nat.isPrime p → p % (4 : Nat) = (3 : Nat) → ∀ {x : FRC.Shell p × FRC.Shell p}, x ≠ ((0 : FRC.Shell p), (0 : FRC.Shell p)) → ∃ y, FRC.Shell.Frame.cmul x y = ((1 : FRC.Shell p), (0 : FRC.Shell p)) :=25 And.intro @FRC.Shell.Frame.complex_chart_zero_divisor (@FRC.Shell.Frame.complex_chart_field)26/-- p01028 — 1:E4. Continuous symmetry, the abelian case: $\Fpx\simeq C_{\p-1}$ is a $\pi/(\p-1)$-net of $U(1)$ under $k\mapsto e^{2\pi\im k/(\p-1)}$; the rounding of a framed turn $u/v$ to $C_{\p-1}$ lies within half a step, and its group-law defect is at most one step. -/27theorem p01028 : (∀ (N u v : Nat), (0 : Nat) < v → ∃ k, FRC.Shell.Frame.IsRound N u v k) ∧ ∀ {N u u' v k₁ k₂ k₃ : Nat}, (0 : Nat) < v → FRC.Shell.Frame.IsRound N u v k₁ → FRC.Shell.Frame.IsRound N u' v k₂ → FRC.Shell.Frame.IsRound N (u + u') v k₃ → k₁ + k₂ ≤ k₃ + (1 : Nat) ∧ k₃ ≤ k₁ + k₂ + (1 : Nat) :=28 And.intro @FRC.Shell.Frame.round_exists (@FRC.Shell.Frame.round_defect)29set_option linter.defProp false in30/-- p01035 — 1:D8. The window law for framed rationals: for $2ND<\p$, fractions $a/b$ with $|a|\le N$, $1\le b\le D$ and equal values are equal fractions; products of such fractions with $|a|,b\le H$ read back when $2H^{4}<\p$, sums when $4H^{4}<\p$. -/31def p01035 := And.intro @FRC.Shell.Frame.frac_window (And.intro @FRC.Shell.Frame.frac_window_inv (And.intro @FRC.Shell.Frame.frac_mul_readback (@FRC.Shell.Frame.frac_add_readback)))32set_option linter.defProp false in33/-- p01036 — 1:D9. The scale grid covers the field: for every unit $B$, every element of $\Fp$ is $tB^{-1}$ for exactly one integer $t$ with $|t|\le2\kap$; each grid $\{t/\gen^{n}\}$ lists every element once. -/34def p01036 := And.intro @FRC.Shell.Frame.signed_rep (And.intro @FRC.Shell.Frame.signed_rep_unique (And.intro @FRC.Shell.Frame.grid_cover (@FRC.Shell.Frame.grid_unique)))35/-- p02022 — 2:E2. Base-grid estimate [chart]: every point of $S^{2}$ lies within geodesic distance $\delta_{\p}=\sqrt2\,\pi_{\R}/(\p-1)$ of $\Xi_{\p,\gen}(V(\Sp))$; in counts, every latitude fraction and every phase fraction rounds to a grid index within half a step. Measured covering radius $0.36$ at $\p=13$, bound $0.370$. -/36theorem p02022 : ∀ (N u v : Nat), (0 : Nat) < v → ∃ k, FRC.Shell.Frame.IsRound N u v k :=37 @FRC.Shell.Frame.round_exists38/-- p02024 — 2:E4. Precision at the shell's resolution [chart]: for every $L$-bounded observable family and configuration on $(S^{2})^{r}$, vertex images of $\Sp$ reproduce every observable within $L^{2}\delta_{\p}$; a tolerance $\varepsilon$ is met on every shell with $\p-1>\sqrt2\,\pi_{\R}L^{2}/\varepsilon$, and one such shell has $\p\le2\max(7,\sqrt2\,\pi_{\R}L^{2}/\varepsilon+1)$ (A5). -/39theorem p02024 : (∀ (N u v : Nat), (0 : Nat) < v → ∃ k, FRC.Shell.Frame.IsRound N u v k) ∧ ∀ (L r d : Nat), r ≤ L → L * (r * d) ≤ L * (L * d) :=40 And.intro @FRC.Shell.Frame.round_exists (@FRC.Geometry.lipschitz_budget)41-- end keys4243end FRC.Ledger44