The core module lean/FrcCore/Meridian.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): 6 theorems (2 definitions): 6 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.Frame23/-!4# 6-fourier — the meridians and the meridian-scale map (predicate D4), no axioms56The meridian `M_m = (a g^m)_{a = 0..π}`, `π = 2κ`, as an ordered list of `2κ + 1` entries, and the7meridian-scale map `S_r(x) = g^r x`: `S_r(M_m) = M_{m+r}` as ordered lists, consecutive entries of `M_m`8differ by the effective step `g^m`, and `S_{r + (p−1)} = S_r` (the `(p−1)`-periodicity of the framed-rational9zoom). The `p = 13`, `g = 2` ladder `M_0, …, M_3` at steps `1, 2, 4, 8`, decided by computation: unwrapped10while `π g^r < p` (`r ≤ 1`), wrapping from `M_2`.11-/1213namespace FRC.Shell1415variable {p : Nat} [Pos p]1617/-- 6:D3 — the meridian `M_m = (0, g^m, 2g^m, …, π g^m)`, `π = 2κ`, as an ordered list. -/18
def meridian (g : Shell p) (κ m : Nat) : List (Shell p) :=19 (List.range (2 * κ + 1)).map (fun a => ofNat a * g ^ m)2021/-- 6:D3 — the meridian-scale map `S_r(x) = g^r x`. -/22def scale (g : Shell p) (r : Nat) (x : Shell p) : Shell p := g ^ r * x2324/-- The scale map on a list of multiples, entry by entry: `g^r (a g^m) = a g^{m+r}`. -/25
theorem map_scale_aux (g : Shell p) (m r : Nat) : ∀ l : List Nat,26 (l.map (fun a => ofNat a * g ^ m)).map (scale g r) = l.map (fun a => ofNat a * g ^ (m + r))27 | [] => rfl28 | a :: l => by29 rw [List.map_cons, List.map_cons, List.map_cons, map_scale_aux g m r l]30 show scale g r (ofNat a * g ^ m) :: _ = (ofNat a * g ^ (m + r)) :: _31 rw [scale, pow_add, mul_left_comm, mul_comm (g ^ m)]3233/-- 6:D4 — meridian-scale covariance: `S_r(M_m) = M_{m+r}` as ordered lists, for every `m, r`. -/34theorem meridian_scale (g : Shell p) (κ m r : Nat) :35 (meridian g κ m).map (scale g r) = meridian g κ (m + r) :=36 map_scale_aux g m r (List.range (2 * κ + 1))3738/-- `ofNat (a + 1) = ofNat a + 1` in the shell. -/39theorem ofNat_succ (a : Nat) : (ofNat (a + 1) : Shell p) = ofNat a + 1 := by40 apply ext41 rw [val_add, val_ofNat, val_ofNat, val_one]42 exact Nat.add_mod a 1 p hp4344/-- 6:D4 — the effective step: consecutive entries of `M_m` differ by `g^m`,45`(a + 1) g^m = a g^m + g^m`. -/46theorem meridian_step (g : Shell p) (m a : Nat) :47 (ofNat (a + 1) : Shell p) * g ^ m = ofNat a * g ^ m + g ^ m := by48 rw [ofNat_succ, right_distrib, one_mul]4950/-- 6:D4 — `S_{r + (p−1)} = S_r`: the meridian-scale map is `(p − 1)`-periodic in `r` (the periodicity of the51framed-rational zoom, A5). -/52theorem scale_periodic {κ : Nat} {g : Shell p} (F : Frame p κ g) (r : Nat) (x : Shell p) :53 scale g (r + (p - 1)) x = scale g r x := by54 unfold scale55 rw [pow_add, F.pow_n, mul_one]5657/-- 6:D4 — the `p = 13`, `g = 2`, `κ = 3` ladder: `M_0, M_1, M_2, M_3` at the effective steps `1, 2, 4, 8`;58`M_0` and `M_1` are unwrapped (`π g^r = 6 g^r < 13` for `r ≤ 1`), `M_2` wraps (`6 · 4 = 24 ≥ 13`: its entries59`0, 4, 8, 12, 3, 7, 11` return through the seam). -/60theorem ladder13 :61 meridian (2 : Shell 13) 3 0 = [0, 1, 2, 3, 4, 5, 6] ∧62 meridian (2 : Shell 13) 3 1 = [0, 2, 4, 6, 8, 10, 12] ∧63 meridian (2 : Shell 13) 3 2 = [0, 4, 8, 12, 3, 7, 11] ∧64 meridian (2 : Shell 13) 3 3 = [0, 8, 3, 11, 6, 1, 9] ∧65 (6 * 2 ^ 1 < 13) ∧ ¬ (6 * 2 ^ 2 < 13) := by66 decide6768end FRC.Shell69