The core module lean/FrcCore/Theme/Lattice.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): 5 theorems (5 definitions): 5 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.Theme.Shift23/-!4# FrcCore.Theme.Lattice — difference operators on the cycle (the gravity theme; 21-gravity, 10 October 2026)56On the cycle of `n` sites (`FRC.Cycle.cyc`, the fourier theme's `Theme/Shift.lean`): the central difference7`(Δf)(i) = f(i + 1) − f(i − 1)` is anti-self-adjoint, `Σ_i (Δf)(i) g(i) = −Σ_i f(i) (Δg)(i)`8(`central_difference_adjoint`, 21:C9) — the identity carrying the exact gauge invariance of the discrete Fierz–Pauli9functional, whose symbol lines are `Theme/Symbol.lean`'s (00:E1); the one-sided difference's adjoint is the negative10backward difference (`forward_difference_adjoint`); and the cycle Laplacian `f(i + 1) + f(i − 1) − 2f(i)` acts on the11character `χ_k(i) = g^{ki}` as the symbol `g^k + g^{−k} − 2` (`laplacian_symbol`, 21:C15; the pattern of 8:F4). The12sums are reindexed by the cycle's shift (`sum_shift`). No axioms.13-/1415namespace FRC.Lattice1617open FRC.Shell FRC.Cycle1819variable {p : Nat} [Pos p]2021/-- The central difference on the cycle: `(Δf)(i) = f(i + 1) − f(i − 1)`, with `i − 1` read as `i + (n − 1)`. -/22
def cdiff (n : Nat) (f : Nat → Shell p) (i : Nat) : Shell p := cyc n f (i + 1) + -(cyc n f (i + (n - 1)))2324/-- The forward difference `(∂f)(i) = f(i + 1) − f(i)` and the backward difference `(∂̄f)(i) = f(i) − f(i − 1)`. -/25def fdiff (n : Nat) (f : Nat → Shell p) (i : Nat) : Shell p := cyc n f (i + 1) + -(cyc n f i)26def bdiff (n : Nat) (f : Nat → Shell p) (i : Nat) : Shell p := cyc n f i + -(cyc n f (i + (n - 1)))2728/-- The cycle Laplacian `(Δ_Φ f)(i) = f(i + 1) + f(i − 1) − 2 f(i)`. -/29def lap (n : Nat) (f : Nat → Shell p) (i : Nat) : Shell p :=30 cyc n f (i + 1) + cyc n f (i + (n - 1)) + -((1 + 1) * cyc n f i)3132/-- `Σ_i f(i + 1) g(i) = Σ_i f(i) g(i + (n − 1))` on the cycle: the summation by parts. -/33
theorem sum_shift_pair (n : Nat) (hn : 0 < n) (f g : Nat → Shell p) :34 sumRange (fun i => cyc n f (i + 1) * cyc n g i) n = sumRange (fun i => cyc n f i * cyc n g (i + (n - 1))) n := by35 rw [← sum_shift n hn (fun i => cyc n f (i + 1) * cyc n g i) (n - 1)]36 apply sum_congr; intro j _37 show cyc n f ((j + (n - 1)) % n + 1) * cyc n g ((j + (n - 1)) % n) = cyc n f j * cyc n g (j + (n - 1))38 rw [cyc_add_mod n hn, cyc_mod n hn]39 have e : j + (n - 1) + 1 = j + n := by40 rw [Nat.add_assoc, FRC.Nat.sub_add_cancel (Nat.succ_le_of_lt hn)]41 rw [e, cyc_add_n n hn]4243/-- 21:C9 — the central difference is anti-self-adjoint on the cycle: `Σ_i (Δf)(i) g(i) = −Σ_i f(i) (Δg)(i)`. -/44theorem central_difference_adjoint (n : Nat) (hn : 0 < n) (f g : Nat → Shell p) :45 sumRange (fun i => cdiff n f i * cyc n g i) n = -(sumRange (fun i => cyc n f i * cdiff n g i) n) := by46 have L : sumRange (fun i => cdiff n f i * cyc n g i) n =47 sumRange (fun i => cyc n f (i + 1) * cyc n g i) n + -(sumRange (fun i => cyc n f (i + (n - 1)) * cyc n g i) n) := by48 rw [← sum_neg, ← sum_add]; apply sum_congr; intro l _; simp only [cdiff]; rw [right_distrib, neg_mul]49 have R : sumRange (fun i => cyc n f i * cdiff n g i) n =50 sumRange (fun i => cyc n f i * cyc n g (i + 1)) n + -(sumRange (fun i => cyc n f i * cyc n g (i + (n - 1))) n) := by51 rw [← sum_neg, ← sum_add]; apply sum_congr; intro l _; simp only [cdiff]; rw [left_distrib, mul_neg]52 have A := sum_shift_pair n hn f g53 have B : sumRange (fun i => cyc n f (i + (n - 1)) * cyc n g i) n = sumRange (fun i => cyc n f i * cyc n g (i + 1)) n := by54 have h := sum_shift_pair n hn g f55 calc sumRange (fun i => cyc n f (i + (n - 1)) * cyc n g i) n56 = sumRange (fun i => cyc n g i * cyc n f (i + (n - 1))) n := sum_congr n (fun i _ => mul_comm _ _)57 _ = sumRange (fun i => cyc n g (i + 1) * cyc n f i) n := h.symm58 _ = sumRange (fun i => cyc n f i * cyc n g (i + 1)) n := sum_congr n (fun i _ => mul_comm _ _)59 rw [L, R, A, B, neg_add_rev, neg_neg, add_comm]6061/-- 21:C9 — the adjoint of the forward difference is the negative backward difference:62`Σ_i (∂f)(i) g(i) = −Σ_i f(i) (∂̄g)(i)`. -/63theorem forward_difference_adjoint (n : Nat) (hn : 0 < n) (f g : Nat → Shell p) :64 sumRange (fun i => fdiff n f i * cyc n g i) n = -(sumRange (fun i => cyc n f i * bdiff n g i) n) := by65 have L : sumRange (fun i => fdiff n f i * cyc n g i) n =66 sumRange (fun i => cyc n f (i + 1) * cyc n g i) n + -(sumRange (fun i => cyc n f i * cyc n g i) n) := by67 rw [← sum_neg, ← sum_add]; apply sum_congr; intro l _; simp only [fdiff]; rw [right_distrib, neg_mul]68 have R : sumRange (fun i => cyc n f i * bdiff n g i) n =69 sumRange (fun i => cyc n f i * cyc n g i) n + -(sumRange (fun i => cyc n f i * cyc n g (i + (n - 1))) n) := by70 rw [← sum_neg, ← sum_add]; apply sum_congr; intro l _; simp only [bdiff]; rw [left_distrib, mul_neg]71 rw [L, R, sum_shift_pair n hn f g, neg_add_rev, neg_neg, add_comm]7273/-! ## The character and the Laplacian's symbol (21:C15) -/7475/-- The character `χ_k(i) = g^{ki}` on the cycle, read mod `n`. -/76def chi (n : Nat) (g : Shell p) (k : Nat) (i : Nat) : Shell p := g ^ (k * (i % n))7778theorem chi_cyc (n : Nat) (hn : 0 < n) (g : Shell p) (k i : Nat) : cyc n (chi n g k) i = chi n g k i := by79 show g ^ (k * (i % n % n)) = g ^ (k * (i % n)); rw [FRC.Nat.mod_mod i n hn]8081/-- 21:C15 — on a character `g` with `gⁿ = 1`, the cycle Laplacian acts on `χ_k` as the symbol82`g^k + g^{k(n−1)} − 2` (`g^{k(n−1)} = g^{−k}` on the cycle): `(Δ_Φ χ_k)(i) = (g^k + g^{−k} − 2) χ_k(i)`,83the dispersion relation `2 − g^k − g^{−k}` of 8:F4, whose chart is `2 − 2 cos k = 4 sin²(k/2)`. -/84theorem laplacian_symbol (n : Nat) (hn : 0 < n) {g : Shell p} (hg : g ^ n = 1) (k i : Nat) :85 lap n (chi n g k) i = (g ^ k + g ^ (k * (n - 1)) + -(1 + 1)) * chi n g k i := by86 have hk : (g ^ k) ^ n = 1 := by rw [pow_mul_comm, hg, one_pow]87 have e1 : cyc n (chi n g k) (i + 1) = g ^ k * chi n g k i := by88 rw [chi_cyc n hn]89 show g ^ (k * ((i + 1) % n)) = g ^ k * g ^ (k * (i % n))90 rw [pow_mul, pow_mul, ← pow_mod n hn hk (i + 1), ← pow_mod n hn hk i, pow_succ, mul_comm]91 have e2 : cyc n (chi n g k) (i + (n - 1)) = g ^ (k * (n - 1)) * chi n g k i := by92 rw [chi_cyc n hn]93 show g ^ (k * ((i + (n - 1)) % n)) = g ^ (k * (n - 1)) * g ^ (k * (i % n))94 rw [pow_mul, pow_mul, pow_mul, ← pow_mod n hn hk (i + (n - 1)), ← pow_mod n hn hk i, pow_add, mul_comm]95 show cyc n (chi n g k) (i + 1) + cyc n (chi n g k) (i + (n - 1)) + -((1 + 1) * cyc n (chi n g k) i) = _96 rw [e1, e2, chi_cyc n hn, right_distrib (g ^ k + g ^ (k * (n - 1))) (-(1 + 1)) (chi n g k i),97 right_distrib (g ^ k) (g ^ (k * (n - 1))) (chi n g k i), neg_mul]9899end FRC.Lattice100