The core module lean/FrcCore/Keys/Numbers.lean — the substrate from first principles, no Mathlib, no axioms (the modules in order: Nat, Pigeonhole, Shell, Series, Cycle, Ring, FrameCore, Frame, Parity, Transform, Orbit, Sum, Theme/Projective, Theme/Fourier, Theme/Fractional, Theme/Lifts, Theme/Dichotomy, Theme/Rotations, Theme/Heisenberg, Theme/Spectra, Theme/Exclusivity, Theme/Quadratic, Theme/Extension, Theme/Tally, Theme/Numbers, Theme/Logic, Theme/SecondOrder, Theme/Formation, Theme/Field, Theme/Foundation, Theme/Drive, Theme/Carrier, Theme/Subject, Theme/Pair, Theme/Hopf, Theme/Symbol, Theme/Gravity, Theme/Quantum, Theme/Unitary, Theme/Interactions, Theme/Horizon, Theme/Shift, Theme/Lattice, Theme/Drift, Theme/Observation, Theme/Interference, Theme/Composite, Theme/Ladder, Meridian, Fourier, Algebra, Epi, Dimensions, Poly, Quaternion, Causality, Representation, Reductio, Godel, Finitism, Geometry, Complex, Instances, Rh, Entropy, Dirac, Gravity, S13, Qm, Pnp, Keys/Frame, Keys/Extension, Keys/Projective, Keys/Fourier, Keys/Numbers, Keys/Logic, Keys/Foundation, Keys/Carrier, Keys/Subject, Keys/Gravity, Keys/Quantum, Keys/Interactions, Keys/Horizon): 1 theorems (0 definitions): 1 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.Orbit2import FrcCore.Theme.Numbers34/-!5# FrcCore.Keys.Numbers — the keyed theorems of the numbers theme (ledger migration, task LM19)67One declaration per key, `FRC.Ledger.p<key>`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem8that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration9`FRC.<Module>.p<key>` as an alias. Every declaration has no axioms (`check_core_axioms.py`).10-/1112namespace FRC.Ledger1314-- Keys of the numbers theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file)15/-- p01026 — 1:E3. Solving in the substrate (first clause): $f\in\Fp[X]$ has a root in $\Fp$ iff $f$ and $X^{\p}-X=\prod_{a}(X-a)$ are not coprime; the gcd counts the distinct roots and Cantor--Zassenhaus splitting finds them, exactly. An equation without a root in $\Fp$ is recognised, not extended (E2). -/16theorem p01026 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {f : FRC.Shell.Poly p} {n : Nat}, f.Bound n → ((∃ a, f.eval n a = (0 : FRC.Shell p)) ↔ FRC.Shell.Poly.Frame.CommonFactor f n FRC.Shell.Poly.xpx p)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (n : Nat) (f : FRC.Shell.Poly p), f.Bound n → ∀ (r : Nat → FRC.Shell p), (∀ (i j : Nat), i ≤ n → j ≤ n → r i = r j → i = j) → (∀ (i : Nat), i ≤ n → f.eval n (r i) = (0 : FRC.Shell p)) → ∀ (i : Nat), f i = (0 : FRC.Shell p)) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (x : FRC.Shell p), x ^ p = x :=17 And.intro @FRC.Shell.Poly.Frame.root_iff_common_factor (And.intro @FRC.Shell.Poly.Frame.root_bound (@FRC.Shell.Frame.fermat))18-- end keys1920end FRC.Ledger21