The Lean module lean/FrcLedger/Fourier.lean of the paper 6-four (on Mathlib): 51 theorems (3 definitions): 0 with no axioms, 2 at tier 1 (propext, Quot.sound), 49 at tier 2 (Classical.choice), 0 red; the mark's colour is the library's (violet, Mathlib; 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 Mathlib2import FrcLedger.Theme.Fourier3import FrcLedger.Theme.Fractional4import FrcLedger.Keys.Fourier56/-!7# 6-fourier — the shell Fourier operator and its fractional family, for every shell (2026-09-15, extended 2026-09-17)89The shell Fourier matrix `W k j = g^(jk)` on `V = 𝔽_p^{Z_{p−1}}`, `g` a primitive root, the reversal `J`, and the10normalised operator `F = i W` with `i = −g^κ` (`i² = −1`): `W² = −J`, `F² = J`, `F⁴ = I`, `W J = J W` (predicates B5, B7).11The fractional family of the paper — the projectors `Π_ℓ = ¼ Σ_r i^{−ℓr} F^r`, the family `F^{[s]} = Σ_ℓ g^{−ℓs} Π_ℓ`12on `ZMod (4κ)` with its additivity, cardinal values, faithfulness and character sector (C2–C4, C8, C9, E6), the13multiplicities as traces and ranks with their parity sums and the dichotomy from the Gauss sign (C5, C7), the14parity permutation (D2), the rotation group `SO(2, 𝔽_p) ≃ 𝔽_p^×` with its cardinal values and eigenline (E2, E3),15the spectral obstruction (E5) and the shift–modulation covariance (E7) — proved for every prime shell `p = 4κ + 1`16and every primitive root, and where the algebra allows, for any element `f` with `f⁴ = 1` of any algebra over a17field with a quarter-turn. The paper's witness checks these on six shells. Classical (tier 2) on Mathlib's18hierarchy; predicates B2, B3, B5–B7 are also in the core with no axioms.1920Since the ledger migration (task LM36, 7 October 2026) the theorems live in the fourier theme: the shell DFT in21`FrcLedger/Theme/Fourier.lean` (`FRC.DFT`, task LM17) and the fractional family in `FrcLedger/Theme/Fractional.lean`22(`FRC.Fractional`). The old names below are aliases, and the predicate declarations are the aliases of their keys.23-/2425namespace FRC.Fourier2627/-! ## Old names (ledger migration, task LM17): the declarations moved to the themes, each under its old name -/2829section base_aliases30variable {K : Type*} [Field K] {n : ℕ} [NeZero n]3132omit [NeZero n] in33/-- The geometric sum of an `n`-th root of unity `ζ ≠ 1` over `Fin n` vanishes. -/34
lemma sum_pow_eq_zero_of_ne_one {ζ : K} (hζn : ζ ^ n = 1) (hζ : ζ ≠ 1) :35 ∑ j : Fin n, ζ ^ (j : ℕ) = 0 :=36 FRC.DFT.sum_pow_eq_zero_of_ne_one hζn hζ3738/-- The shell Fourier matrix, `W k j = g^(j·k)`. -/39
@[reducible] def W (g : K) : Matrix (Fin n) (Fin n) K :=40 FRC.DFT.W g4142/-- The reversal `J k l = [l = −k]`. -/43@[reducible] def J : Matrix (Fin n) (Fin n) K :=44 FRC.DFT.J4546omit [NeZero n] in47lemma W_apply (g : K) (k j : Fin n) : (W g : Matrix (Fin n) (Fin n) K) k j = g ^ ((j : ℕ) * (k : ℕ)) :=48 FRC.DFT.W_apply g k j4950omit [NeZero n] in51lemma J_apply (k l : Fin n) : (J : Matrix (Fin n) (Fin n) K) k l = if l = -k then 1 else 0 :=52 FRC.DFT.J_apply k l5354/-- `g^((-j).val) = (g^(j.val))⁻¹` for an `n`-th root of unity `g`. -/55lemma pow_neg_val {g : K} (hg : g ^ n = 1) (j : Fin n) :56 g ^ ((-j : Fin n) : ℕ) = (g ^ (j : ℕ))⁻¹ :=57 FRC.DFT.pow_neg_val hg j5859omit [NeZero n] in60/-- `J² = 1`. -/61theorem J_sq : (J : Matrix (Fin n) (Fin n) K) ^ 2 = 1 :=62 FRC.DFT.J_sq6364omit [NeZero n] in65/-- 6:D2 — `J` is a permutation matrix: `(M J) k j = M k (−j)`, so `M J` has the columns of `M`, reindexed by66the parity involution `j ↦ −j`. -/67theorem mul_J_apply (M : Matrix (Fin n) (Fin n) K) (k j : Fin n) :68 (M * (J : Matrix (Fin n) (Fin n) K)) k j = M k (-j) :=69 FRC.DFT.mul_J_apply M k j7071/-- `W² = n • J` for any primitive `n`-th root of unity `g` (the general identity). -/72theorem W_sq (g : K) (hg : IsPrimitiveRoot g n) :73 (W g : Matrix (Fin n) (Fin n) K) ^ 2 = (n : K) • J :=74 FRC.DFT.W_sq g hg7576/-- `W J = J W` for any `n`-th root of unity `g`. -/77theorem W_mul_J_comm (g : K) (hg : g ^ n = 1) :78 (W g : Matrix (Fin n) (Fin n) K) * J = J * W g :=79 FRC.DFT.W_mul_J_comm g hg8081end base_aliases8283section shell_aliases84variable {F : Type*} [Field F] [Fintype F]8586/-- `(card F − 1 : ℕ) = −1` in a finite field `F`. -/87lemma natCast_card_pred_eq_neg_one : ((Fintype.card F - 1 : ℕ) : F) = -1 :=88 FRC.DFT.natCast_card_pred_eq_neg_one8990/-- The quarter-turn `i = −g^κ` squares to `−1` (`g^{2κ}` is a primitive square root of unity). -/91lemma quarter_turn_sq (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) (g : F)92 (hg : IsPrimitiveRoot g (Fintype.card F - 1)) :93 (-(g ^ κ)) ^ 2 = -1 :=94 FRC.DFT.quarter_turn_sq κ hκ g hg9596/-- 6:B5, 6:B7 — every shell: on a field with `p = 4κ + 1` elements, `n = p − 1`,97`g` a primitive root and `F = i • W`: `W² = −J`, `F² = J`, `F⁴ = 1`, `W J = J W`. -/98theorem shell_relations (κ : ℕ) (hκ : Fintype.card F = 4 * κ + 1) (g : F)99 (hg : IsPrimitiveRoot g (Fintype.card F - 1)) [NeZero (Fintype.card F - 1)] :100 (W g : Matrix (Fin (Fintype.card F - 1)) (Fin (Fintype.card F - 1)) F) ^ 2 = -J ∧101 ((-(g ^ κ)) • W g : Matrix (Fin (Fintype.card F - 1)) (Fin (Fintype.card F - 1)) F) ^ 2 = J ∧102 ((-(g ^ κ)) • W g : Matrix (Fin (Fintype.card F - 1)) (Fin (Fintype.card F - 1)) F) ^ 4 = 1 ∧103 (W g : Matrix (Fin (Fintype.card F - 1)) (Fin (Fintype.card F - 1)) F) * J = J * W g :=104 FRC.DFT.shell_relations κ hκ g hg105106/-- 6:B5, 6:B7 on the prime shell `𝔽_p = ZMod p`, an instance: the relations hold there for every prime107`p = 4κ + 1` and primitive root `g`. -/108theorem shell_relations_zmod (p κ : ℕ) [hp : Fact (Nat.Prime p)] (hκ : p = 4 * κ + 1)109 (g : ZMod p) (hg : IsPrimitiveRoot g (p - 1)) :110 haveI : NeZero (Fintype.card (ZMod p) - 1) :=111 ⟨by have := Fintype.one_lt_card (α := ZMod p); omega⟩112 ((-(g ^ κ)) • W g : Matrix (Fin (Fintype.card (ZMod p) - 1))113 (Fin (Fintype.card (ZMod p) - 1)) (ZMod p)) ^ 2 = J :=114 FRC.DFT.shell_relations_zmod p κ hκ g hg115116end shell_aliases117118/-! The declarations moved to the fourier theme's `Theme/Fractional.lean` by task LM36 (`FRC.Fractional`), each under119its old name. -/120121section lm36_aliases122open FRC.Fractional123section124open FRC.DFT125126open Matrix hiding J127open Finset128129130section algebra131132variable {K : Type*} [Field K] {A : Type*} [Ring A] [Algebra K A]133134variable (i : K) (f : A)135136/-- 6:C2 — 6-fourier's name; the theorem is `FRC.Fractional.proj_mul_proj` (task LM36). -/137theorem proj_mul_proj (hi : i ^ 4 = 1) (hne : ∀ d : ZMod 4, d ≠ 0 → chi i d ≠ 1) (h4 : (4 : K) ≠ 0)138 (hf : f ^ 4 = 1) (ℓ m : ZMod 4) :139 proj i f ℓ * proj i f m = if ℓ = m then proj i f ℓ else 0 := by140 apply FRC.Fractional.proj_mul_proj <;> assumption141142/-- 6:C2 — 6-fourier's name; the theorem is `FRC.Fractional.sum_proj` (task LM36). -/143theorem sum_proj (hi : i ^ 4 = 1) (hne : ∀ d : ZMod 4, d ≠ 0 → chi i d ≠ 1) (h4 : (4 : K) ≠ 0) :144 ∑ ℓ : ZMod 4, proj i f ℓ = 1 := by145 apply FRC.Fractional.sum_proj <;> assumption146147end algebra148149section family150151variable {K : Type*} [Field K] {A : Type*} [Ring A] [Algebra K A] {n : ℕ} [NeZero n]152153variable (i z : K) (f : A)154155omit [NeZero n] in156/-- 6:E6 — 6-fourier's name; the theorem is `FRC.Fractional.frft_mul_proj_one` (task LM36). -/157theorem frft_mul_proj_one (hi : i ^ 4 = 1) (hne : ∀ d : ZMod 4, d ≠ 0 → chi i d ≠ 1) (h4 : (4 : K) ≠ 0)158 (hf : f ^ 4 = 1) (s : ZMod n) :159 frft i z f s * proj i f 1 = psi z s • proj i f 1 := by160 apply FRC.Fractional.frft_mul_proj_one <;> assumption161162end family163164section rotation165166variable {K : Type*} [Field K]167168variable (i : K)169170/-- 6:E2 — 6-fourier's name; the theorem is `FRC.Fractional.circle` (task LM36). -/171theorem circle (hi : i ^ 2 = -1) (h2 : (2 : K) ≠ 0) (z : K) (hz : z ≠ 0) : cc z ^ 2 + dd i z ^ 2 = 1 := by172 apply FRC.Fractional.circle <;> assumption173174/-- 6:E2 — 6-fourier's name; the theorem is `FRC.Fractional.rot_mul` (task LM36). -/175theorem rot_mul (hi : i ^ 2 = -1) (h2 : (2 : K) ≠ 0) (z w : K) (hz : z ≠ 0) (hw : w ≠ 0) :176 rot i (z * w) = rot i z * rot i w := by177 apply FRC.Fractional.rot_mul <;> assumption178179/-- 6:E3 — 6-fourier's name; the theorem is `FRC.Fractional.rot_cardinal` (task LM36). -/180theorem rot_cardinal (hi : i ^ 2 = -1) (h2 : (2 : K) ≠ 0) :181 rot i 1 = 1 ∧ rot i i = !![0, -1; 1, 0] ∧ rot i (-1) = -1 ∧ rot i (-i) = !![0, 1; -1, 0] := by182 apply FRC.Fractional.rot_cardinal <;> assumption183184/-- 6:E6 — 6-fourier's name; the theorem is `FRC.Fractional.rot_eigenline` (task LM36). -/185theorem rot_eigenline (hi : i ^ 2 = -1) (h2 : (2 : K) ≠ 0) (z : K) (hz : z ≠ 0) :186 (rot i z).mulVec ![1, -i] = z • ![1, -i] := by187 apply FRC.Fractional.rot_eigenline <;> assumption188189/-- 6:E2 — 6-fourier's name; the definition is `FRC.Fractional.unitsEquivCircle` (task LM36). -/190@[reducible] noncomputable def unitsEquivCircle (hi : i ^ 2 = -1) (h2 : (2 : K) ≠ 0) : Kˣ ≃ Circle K :=191 FRC.Fractional.unitsEquivCircle i hi h2192193/-- 6:E2 — 6-fourier's name; the theorem is `FRC.Fractional.card_circle` (task LM36). -/194theorem card_circle [Fintype K] [DecidableEq K] (hi : i ^ 2 = -1) (h2 : (2 : K) ≠ 0) :195 Fintype.card (Circle K) = Fintype.card K - 1 := by196 apply FRC.Fractional.card_circle <;> assumption197198end rotation199200section gauss201202variable {K : Type*} [Field K] {n : ℕ} [NeZero n]203204open Fin.CommRing in205/-- 6:C7 — 6-fourier's name; the theorem is `FRC.Fractional.gauss_mul_gauss_inv` (task LM36). -/206theorem gauss_mul_gauss_inv (κ : ℕ) [NeZero κ] (g : K) (hg : IsPrimitiveRoot g (4 * κ))207 (hnK : ((4 * κ : ℕ) : K) = -1) : gauss (4 * κ) g * gauss (4 * κ) g⁻¹ = -2 := by208 apply FRC.Fractional.gauss_mul_gauss_inv <;> assumption209210omit [NeZero n] in211/-- 6:C7 — 6-fourier's name; the theorem is `FRC.Fractional.gauss_inv_of_sign` (task LM36). -/212theorem gauss_inv_of_sign {g i : K} (hGG : gauss n g * gauss n g⁻¹ = -2) (hi : i ^ 2 = -1) (h2 : (2 : K) ≠ 0)213 (ε : K) (hε : ε = 1 ∨ ε = -1) (hG : gauss n g = ε * (1 + i)) : gauss n g⁻¹ = -ε * (1 + -i) := by214 apply FRC.Fractional.gauss_inv_of_sign <;> assumption215216end gauss217218219section shellFamily220221variable {F : Type*} [Field F] [Fintype F] (κ : ℕ) [NeZero κ] (g : F)222223variable (hκ : Fintype.card F = 4 * κ + 1) (hg : IsPrimitiveRoot g (4 * κ))224include hκ hg225226/-- 6:C2 — 6-fourier's name; the theorem is `FRC.Fractional.shell_proj` (task LM36). -/227theorem shell_proj (ℓ m : ZMod 4) :228 Fmat κ g * shellProj κ g ℓ = chi (-(g ^ κ)) ℓ • shellProj κ g ℓ ∧229 shellProj κ g ℓ * shellProj κ g m = (if ℓ = m then shellProj κ g ℓ else 0) ∧230 ∑ ℓ : ZMod 4, shellProj κ g ℓ = 1 := by231 apply FRC.Fractional.shell_proj <;> assumption232233/-- 6:C3 — 6-fourier's name; the theorem is `FRC.Fractional.shell_frft_add` (task LM36). -/234theorem shell_frft_add (s r : ZMod (4 * κ)) :235 shellFrft κ g (s + r) = shellFrft κ g s * shellFrft κ g r := by236 apply FRC.Fractional.shell_frft_add <;> assumption237238/-- 6:C3 — 6-fourier's name; the theorem is `FRC.Fractional.shell_frft_cardinal` (task LM36). -/239theorem shell_frft_cardinal (m : ℕ) :240 shellFrft κ g (m • (κ : ZMod (4 * κ))) = Fmat κ g ^ m := by241 apply FRC.Fractional.shell_frft_cardinal <;> assumption242243/-- 6:C3 — 6-fourier's name; the theorem is `FRC.Fractional.shell_frft_values` (task LM36). -/244theorem shell_frft_values :245 shellFrft κ g (κ : ZMod (4 * κ)) = Fmat κ g ∧246 shellFrft κ g (2 • (κ : ZMod (4 * κ))) = J ∧247 shellFrft κ g (1 : ZMod (4 * κ)) ^ κ = Fmat κ g := by248 apply FRC.Fractional.shell_frft_values <;> assumption249250/-- 6:C8 — 6-fourier's name; the theorem is `FRC.Fractional.shell_frftLift` (task LM36). -/251theorem shell_frftLift (a : ZMod 4 → ℕ) (ha : ∀ ℓ, a ℓ % 4 = ℓ.val) (s r : ZMod (4 * κ)) (m : ℕ) :252 frftLift (-(g ^ κ)) g⁻¹ (Fmat κ g) a (s + r)253 = frftLift (-(g ^ κ)) g⁻¹ (Fmat κ g) a s * frftLift (-(g ^ κ)) g⁻¹ (Fmat κ g) a r ∧254 frftLift (-(g ^ κ)) g⁻¹ (Fmat κ g) a (m • (κ : ZMod (4 * κ))) = Fmat κ g ^ m := by255 apply FRC.Fractional.shell_frftLift <;> assumption256257/-- 6:C9 — 6-fourier's name; the theorem is `FRC.Fractional.shell_conj` (task LM36). -/258theorem shell_conj (ℓ : ZMod 4) :259 (-(-(g ^ κ))) • W g⁻¹ = -(Fmat κ g ^ 3) ∧260 proj (-(-(g ^ κ))) (-(Fmat κ g ^ 3)) ℓ = shellProj κ g (ℓ + 2) := by261 apply FRC.Fractional.shell_conj <;> assumption262263/-- 6:D2 — 6-fourier's name; the theorem is `FRC.Fractional.shell_frft_add_two_kappa` (task LM36). -/264theorem shell_frft_add_two_kappa (s : ZMod (4 * κ)) :265 shellFrft κ g (s + 2 • (κ : ZMod (4 * κ))) = shellFrft κ g s * J := by266 apply FRC.Fractional.shell_frft_add_two_kappa <;> assumption267268/-- 6:E7 — 6-fourier's name; the theorem is `FRC.Fractional.shell_heisenberg` (task LM36). -/269theorem shell_heisenberg :270 Fmat κ g * shift = modul g * Fmat κ g ∧ Fmat κ g * modul g = shift' * Fmat κ g ∧271 (shift : Matrix (Fin (4 * κ)) (Fin (4 * κ)) F) * shift' = 1 := by272 apply FRC.Fractional.shell_heisenberg <;> assumption273274/-- 6:E5 — 6-fourier's name; the theorem is `FRC.Fractional.shell_spectral_obstruction` (task LM36). -/275theorem shell_spectral_obstruction [DecidableEq F] (hκ2 : 2 ≤ κ) (s : ZMod (4 * κ)) :276 ¬ ∃ T : Matrix (Fin (4 * κ)) (Fin (4 * κ)) F, IsUnit T ∧ T * shift * T⁻¹ = shellFrft κ g s := by277 apply FRC.Fractional.shell_spectral_obstruction <;> assumption278279/-- 6:C5 — 6-fourier's name; the theorem is `FRC.Fractional.shell_odd_proj_ne_zero` (task LM36). -/280theorem shell_odd_proj_ne_zero (hκ2 : 2 ≤ κ) : shellProj κ g 1 ≠ 0 ∧ shellProj κ g 3 ≠ 0 := by281 apply FRC.Fractional.shell_odd_proj_ne_zero <;> assumption282283/-- 6:C5 — 6-fourier's name; the theorem is `FRC.Fractional.shell_even_proj_ne_zero` (task LM36). -/284theorem shell_even_proj_ne_zero : shellProj κ g 0 ≠ 0 ∧ shellProj κ g 2 ≠ 0 := by285 apply FRC.Fractional.shell_even_proj_ne_zero <;> assumption286287/-- 6:C4, 6:D2 — 6-fourier's name; the theorem is `FRC.Fractional.shell_frft_injective` (task LM36). -/288theorem shell_frft_injective : Function.Injective (shellFrft κ g) := by289 apply FRC.Fractional.shell_frft_injective <;> assumption290291end shellFamily292293section prime294295variable (p κ : ℕ) [hp : Fact p.Prime] [NeZero κ] (hpκ : p = 4 * κ + 1)296include hpκ297298variable (g : ZMod p) (hg : IsPrimitiveRoot g (4 * κ))299include hg300301/-- 6:C5 — 6-fourier's name; the theorem is `FRC.Fractional.shell_multiplicity_sums` (task LM36). -/302theorem shell_multiplicity_sums :303 (shellProj κ g 0).rank + (shellProj κ g 2).rank = 2 * κ + 1 ∧304 (shellProj κ g 1).rank + (shellProj κ g 3).rank = 2 * κ - 1 := by305 apply FRC.Fractional.shell_multiplicity_sums <;> assumption306307/-- 6:C7 — 6-fourier's name; the theorem is `FRC.Fractional.shell_multiplicity_tuple` (task LM36). -/308theorem shell_multiplicity_tuple (ε : ZMod p) (hε : ε = 1 ∨ ε = -1)309 (hG : gauss (4 * κ) g = ε * (1 + -(g ^ κ))) :310 (ε = 1 → (shellProj κ g 0).rank = κ ∧ (shellProj κ g 1).rank = κ ∧311 (shellProj κ g 2).rank = κ + 1 ∧ (shellProj κ g 3).rank = κ - 1) ∧312 (ε = -1 → (shellProj κ g 0).rank = κ + 1 ∧ (shellProj κ g 1).rank = κ - 1 ∧313 (shellProj κ g 2).rank = κ ∧ (shellProj κ g 3).rank = κ) := by314 apply FRC.Fractional.shell_multiplicity_tuple <;> assumption315316end prime317318end319320end lm36_aliases321322-- Ledger predicates of 6-fourier (generated by make_predicates.py from docs/6-fourier/6-fourier-ledger.json; edit the ledger, not this section)323set_option linter.defProp false in324/-- 6:B5 (p06012) — $\Wt^{2}=-J$, $\Ft^{2}=J$, $\Ft^{4}=I$: the normalized operator generates the four-cycle, on the six shells of Table~\ref{tab:checks}. -/325def p06012 := @FRC.LedgerML.p06012326set_option linter.defProp false in327/-- 6:B7 (p06014) — $\Wt J=J\Wt$, hence $\Ft J=J\Ft$; every $v$ is uniquely $v^{+}+v^{-}$ with $Jv^{\pm}=\pm v^{\pm}$, a symmetric vector determined by its $2\kap+1$ entries at $0,\dots,2\kap$ and an antisymmetric one by its $2\kap-1$ entries at $1,\dots,2\kap-1$. -/328def p06014 := @FRC.LedgerML.p06014329/-- 6:C2 (p06016) — $\Pi_\ell^{2}=\Pi_\ell$, $\Pi_\ell\Pi_m=0$ for $\ell\neq m$, $\sum_\ell\Pi_\ell=I$, $\Ft\Pi_\ell=\im^{\ell}\Pi_\ell$. -/330theorem p06016 : (∀ {F : Type u_1} [Field F] [Fintype F] (κ : ℕ) [NeZero κ] (g : F), Fintype.card F = (4 : ℕ) * κ + (1 : ℕ) → IsPrimitiveRoot g ((4 : ℕ) * κ) → ∀ (ℓ m : ZMod (4 : ℕ)), FRC.Fractional.Fmat κ g * FRC.Fractional.shellProj κ g ℓ = FRC.Fractional.chi (-g ^ κ) ℓ • FRC.Fractional.shellProj κ g ℓ ∧ (FRC.Fractional.shellProj κ g ℓ * FRC.Fractional.shellProj κ g m = if ℓ = m then FRC.Fractional.shellProj κ g ℓ else (0 : Matrix (Fin ((4 : ℕ) * κ)) (Fin ((4 : ℕ) * κ)) F)) ∧ ∑ ℓ, FRC.Fractional.shellProj κ g ℓ = (1 : Matrix (Fin ((4 : ℕ) * κ)) (Fin ((4 : ℕ) * κ)) F)) ∧ (∀ {K : Type u_2} [Field K] {A : Type u_3} [Ring A] [Algebra K A] (i : K) (f : A), i ^ (4 : ℕ) = (1 : K) → (∀ (d : ZMod (4 : ℕ)), d ≠ (0 : ZMod (4 : ℕ)) → FRC.Fractional.chi i d ≠ (1 : K)) → (4 : K) ≠ (0 : K) → f ^ (4 : ℕ) = (1 : A) → ∀ (ℓ m : ZMod (4 : ℕ)), FRC.Fractional.proj i f ℓ * FRC.Fractional.proj i f m = if ℓ = m then FRC.Fractional.proj i f ℓ else (0 : A)) ∧ ∀ {K : Type u_4} [Field K] {A : Type u_5} [Ring A] [Algebra K A] (i : K) (f : A), i ^ (4 : ℕ) = (1 : K) → (∀ (d : ZMod (4 : ℕ)), d ≠ (0 : ZMod (4 : ℕ)) → FRC.Fractional.chi i d ≠ (1 : K)) → (4 : K) ≠ (0 : K) → ∑ ℓ, FRC.Fractional.proj i f ℓ = (1 : A) :=331 @FRC.LedgerML.p06016332/-- 6:C3 (p06017) — The exact finite-field FrFT: $s\mapsto\Ft^{[s]}$ is a representation of $\Phit$, $\Ft^{[s+r]}=\Ft^{[s]}\Ft^{[r]}$ for all $s,r$ (every pair on the six shells by the package), with the cardinal values $\Ft^{[0]}=I$, $\Ft^{[\kap]}=\Ft$, $\Ft^{[2\kap]}=J$, $\Ft^{[3\kap]}=\Ft^{-1}$, and $(\Ft^{[1]})^{\kap}=\Ft$. -/333theorem p06017 : (∀ {F : Type u_1} [Field F] [Fintype F] (κ : ℕ) [NeZero κ] (g : F), Fintype.card F = (4 : ℕ) * κ + (1 : ℕ) → IsPrimitiveRoot g ((4 : ℕ) * κ) → ∀ (s r : ZMod ((4 : ℕ) * κ)), FRC.Fractional.shellFrft κ g (s + r) = FRC.Fractional.shellFrft κ g s * FRC.Fractional.shellFrft κ g r) ∧ (∀ {F : Type u_2} [Field F] [Fintype F] (κ : ℕ) [NeZero κ] (g : F), Fintype.card F = (4 : ℕ) * κ + (1 : ℕ) → IsPrimitiveRoot g ((4 : ℕ) * κ) → ∀ (m : ℕ), FRC.Fractional.shellFrft κ g (m • ↑κ) = FRC.Fractional.Fmat κ g ^ m) ∧ ∀ {F : Type u_3} [Field F] [Fintype F] (κ : ℕ) [NeZero κ] (g : F), Fintype.card F = (4 : ℕ) * κ + (1 : ℕ) → IsPrimitiveRoot g ((4 : ℕ) * κ) → FRC.Fractional.shellFrft κ g ↑κ = FRC.Fractional.Fmat κ g ∧ FRC.Fractional.shellFrft κ g ((2 : ℕ) • ↑κ) = FRC.DFT.J ∧ FRC.Fractional.shellFrft κ g (1 : ZMod ((4 : ℕ) * κ)) ^ κ = FRC.Fractional.Fmat κ g :=334 @FRC.LedgerML.p06017335/-- 6:C4 (p06018) — Faithfulness: $s\mapsto\Ft^{[s]}$ is injective on $\Z_{4\kap}$ for every $\kap\ge1$; at $\p=5$ the surviving odd projector carries the faithful character. -/336theorem p06018 : ∀ {F : Type u_1} [Field F] [Fintype F] (κ : ℕ) [NeZero κ] (g : F), Fintype.card F = (4 : ℕ) * κ + (1 : ℕ) → IsPrimitiveRoot g ((4 : ℕ) * κ) → Function.Injective (FRC.Fractional.shellFrft κ g) :=337 @FRC.LedgerML.p06018338/-- 6:C5 (p06019) — The projector sums $\Pi_0+\Pi_2=\tfrac12(I+J)$ and $\Pi_1+\Pi_3=\tfrac12(I-J)$; $\Pi_0,\Pi_2\neq0$ for every $\kap\ge1$ and $\Pi_1,\Pi_3\neq0$ for $\kap\ge2$, each by one explicit entry; at $\p=5$ exactly one of $\Pi_1,\Pi_3$ vanishes. -/339theorem p06019 : (∀ {F : Type u_1} [Field F] [Fintype F] (κ : ℕ) [NeZero κ] (g : F), Fintype.card F = (4 : ℕ) * κ + (1 : ℕ) → IsPrimitiveRoot g ((4 : ℕ) * κ) → (2 : ℕ) ≤ κ → FRC.Fractional.shellProj κ g (1 : ZMod (4 : ℕ)) ≠ (0 : Matrix (Fin ((4 : ℕ) * κ)) (Fin ((4 : ℕ) * κ)) F) ∧ FRC.Fractional.shellProj κ g (3 : ZMod (4 : ℕ)) ≠ (0 : Matrix (Fin ((4 : ℕ) * κ)) (Fin ((4 : ℕ) * κ)) F)) ∧ (∀ {F : Type u_2} [Field F] [Fintype F] (κ : ℕ) [NeZero κ] (g : F), Fintype.card F = (4 : ℕ) * κ + (1 : ℕ) → IsPrimitiveRoot g ((4 : ℕ) * κ) → FRC.Fractional.shellProj κ g (0 : ZMod (4 : ℕ)) ≠ (0 : Matrix (Fin ((4 : ℕ) * κ)) (Fin ((4 : ℕ) * κ)) F) ∧ FRC.Fractional.shellProj κ g (2 : ZMod (4 : ℕ)) ≠ (0 : Matrix (Fin ((4 : ℕ) * κ)) (Fin ((4 : ℕ) * κ)) F)) ∧ ∀ (p κ : ℕ) [hp : Fact (Nat.Prime p)] [NeZero κ], p = (4 : ℕ) * κ + (1 : ℕ) → ∀ (g : ZMod p), IsPrimitiveRoot g ((4 : ℕ) * κ) → (FRC.Fractional.shellProj κ g (0 : ZMod (4 : ℕ))).rank + (FRC.Fractional.shellProj κ g (2 : ZMod (4 : ℕ))).rank = (2 : ℕ) * κ + (1 : ℕ) ∧ (FRC.Fractional.shellProj κ g (1 : ZMod (4 : ℕ))).rank + (FRC.Fractional.shellProj κ g (3 : ZMod (4 : ℕ))).rank = (2 : ℕ) * κ - (1 : ℕ) :=340 @FRC.LedgerML.p06019341/-- 6:C7 (p06021) — The multiplicity dichotomy in trace form: with $G=\sum_{k}\gen^{k^{2}}$ and $G^{*}=\sum_k\gen^{-k^{2}}$ the traces are $\operatorname{Tr}\Ft=\im G$, $\operatorname{Tr}\Ft^{2}=2$, $\operatorname{Tr}\Ft^{3}=\im G^{*}$ and $\operatorname{Tr}\Pi_\ell=\tfrac14\sum_r\im^{-\ell r}\operatorname{Tr}\Ft^{r}$; $GG^{*}=-2$ and $\varepsilon(\gen^{-1})=-\varepsilon(\gen)$; when $G=\varepsilon(1+\im)$ (A3) the tuple of traces is $(\kap,\kap,\kap+1,\kap-1)$ for $\varepsilon=+1$ and $(\kap+1,\kap-1,\kap,\kap)$ for $\varepsilon=-1$, read in $\Fp$; the sign and the tuples on the six shells of Table~\ref{tab:checks}. Exact on the $38$ primitive frames of $\p\in\{5,13,17,29,37\}$ and the $16$ of $\p=41$. -/342theorem p06021 : (∀ {K : Type u_1} [Field K] (κ : ℕ) [NeZero κ] (g : K), IsPrimitiveRoot g ((4 : ℕ) * κ) → ↑((4 : ℕ) * κ) = (-1 : K) → FRC.Fractional.gauss ((4 : ℕ) * κ) g * FRC.Fractional.gauss ((4 : ℕ) * κ) g⁻¹ = (-2 : K)) ∧ (∀ {K : Type u_2} [Field K] {n : ℕ} {g i : K}, FRC.Fractional.gauss n g * FRC.Fractional.gauss n g⁻¹ = (-2 : K) → i ^ (2 : ℕ) = (-1 : K) → (2 : K) ≠ (0 : K) → ∀ (ε : K), ε = (1 : K) ∨ ε = (-1 : K) → FRC.Fractional.gauss n g = ε * ((1 : K) + i) → FRC.Fractional.gauss n g⁻¹ = -ε * ((1 : K) + -i)) ∧ ∀ (p κ : ℕ) [hp : Fact (Nat.Prime p)] [NeZero κ], p = (4 : ℕ) * κ + (1 : ℕ) → ∀ (g : ZMod p), IsPrimitiveRoot g ((4 : ℕ) * κ) → ∀ (ε : ZMod p), ε = (1 : ZMod p) ∨ ε = (-1 : ZMod p) → FRC.Fractional.gauss ((4 : ℕ) * κ) g = ε * ((1 : ZMod p) + -g ^ κ) → (ε = (1 : ZMod p) → (FRC.Fractional.shellProj κ g (0 : ZMod (4 : ℕ))).rank = κ ∧ (FRC.Fractional.shellProj κ g (1 : ZMod (4 : ℕ))).rank = κ ∧ (FRC.Fractional.shellProj κ g (2 : ZMod (4 : ℕ))).rank = κ + (1 : ℕ) ∧ (FRC.Fractional.shellProj κ g (3 : ZMod (4 : ℕ))).rank = κ - (1 : ℕ)) ∧ (ε = (-1 : ZMod p) → (FRC.Fractional.shellProj κ g (0 : ZMod (4 : ℕ))).rank = κ + (1 : ℕ) ∧ (FRC.Fractional.shellProj κ g (1 : ZMod (4 : ℕ))).rank = κ - (1 : ℕ) ∧ (FRC.Fractional.shellProj κ g (2 : ZMod (4 : ℕ))).rank = κ ∧ (FRC.Fractional.shellProj κ g (3 : ZMod (4 : ℕ))).rank = κ) :=343 @FRC.LedgerML.p06021344set_option linter.defProp false in345/-- 6:C8 (p06022) — Exponent lifts: every lift $a_\ell\equiv\ell\pmod4$, $U^{(a)}_s=\sum_\ell\gen^{-a_\ell s}\Pi_\ell$, is additive with the same cardinal skeleton, $U^{(a)}_{s+r}=U^{(a)}_sU^{(a)}_r$ and $U^{(a)}_{m\kap}=\Ft^{m}$. -/346def p06022 := @FRC.LedgerML.p06022347/-- 6:C9 (p06023) — The conjugate reframing $(\gen,\im)\mapsto(\gen^{-1},-\im)$: exactly $\Ft'=-\Ft^{-1}$ and $\Pi'_\ell=\Pi_{\ell+2}$; the operator relations, cardinal values, additivity and faithfulness hold on the conjugate frame, and its trace tuple is the other pattern of C7. -/348theorem p06023 : ∀ {F : Type u_1} [Field F] [Fintype F] (κ : ℕ) [NeZero κ] (g : F), Fintype.card F = (4 : ℕ) * κ + (1 : ℕ) → IsPrimitiveRoot g ((4 : ℕ) * κ) → ∀ (ℓ : ZMod (4 : ℕ)), - -g ^ κ • FRC.DFT.W g⁻¹ = -FRC.Fractional.Fmat κ g ^ (3 : ℕ) ∧ FRC.Fractional.proj (- -g ^ κ) (-FRC.Fractional.Fmat κ g ^ (3 : ℕ)) ℓ = FRC.Fractional.shellProj κ g (ℓ + (2 : ZMod (4 : ℕ))) :=349 @FRC.LedgerML.p06023350set_option linter.defProp false in351/-- 6:D2 (p06025) — The $4\kap$ framed domains are pairwise distinct; read as unordered bases $B_{s+2\kap}=B_s$, since $\Ft^{[s+2\kap]}=\Ft^{[s]}J$ and $J$ permutes the standard basis. -/352def p06025 := @FRC.LedgerML.p06025353/-- 6:E2 (p06031) — $R_s\in SO(2,\Fp)$, and $s\mapsto R_s$ is an isomorphism $\Phit\simeq SO(2,\Fp)$ with $|SO(2,\Fp)|=\p-1=4\kap$: the full rotation group of the $\p^{2}$-point plane is the meridian cycle. Cited definitions (not proofs): FRC.Fourier.unitsEquivCircle. -/354theorem p06031 : (∀ {K : Type u_1} [Field K] (i : K), i ^ (2 : ℕ) = (-1 : K) → (2 : K) ≠ (0 : K) → ∀ (z : K), z ≠ (0 : K) → FRC.Fractional.cc z ^ (2 : ℕ) + FRC.Fractional.dd i z ^ (2 : ℕ) = (1 : K)) ∧ (∀ {K : Type u_2} [Field K] (i : K), i ^ (2 : ℕ) = (-1 : K) → (2 : K) ≠ (0 : K) → ∀ (z w : K), z ≠ (0 : K) → w ≠ (0 : K) → FRC.Fractional.rot i (z * w) = FRC.Fractional.rot i z * FRC.Fractional.rot i w) ∧ ∀ {K : Type u_3} [Field K] (i : K) [Fintype K] [DecidableEq K], i ^ (2 : ℕ) = (-1 : K) → (2 : K) ≠ (0 : K) → Fintype.card (FRC.Fractional.Circle K) = Fintype.card K - (1 : ℕ) :=355 @FRC.LedgerML.p06031356/-- 6:E3 (p06032) — The cardinal-skeleton dictionary $M_s\leftrightarrow s\leftrightarrow z_s\leftrightarrow R_s$ with $R_0=I$, $R_\kap=w$, $R_{2\kap}=-I$, $R_{3\kap}=w^{-1}$ (the $R_\kap$ column of Table~\ref{tab:checks}), $z_\kap=\im$; the shell's family and the Weil family stand in cardinal Weil correspondence, the Weil side by the normalization of A2 (an import). -/357theorem p06032 : ∀ {K : Type u_1} [Field K] (i : K), i ^ (2 : ℕ) = (-1 : K) → (2 : K) ≠ (0 : K) → FRC.Fractional.rot i (1 : K) = (1 : Matrix (Fin (2 : ℕ)) (Fin (2 : ℕ)) K) ∧ FRC.Fractional.rot i i = !![(0 : K), (-1 : K); (1 : K), (0 : K)] ∧ FRC.Fractional.rot i (-1 : K) = (-1 : Matrix (Fin (2 : ℕ)) (Fin (2 : ℕ)) K) ∧ FRC.Fractional.rot i (-i) = !![(0 : K), (1 : K); (-1 : K), (0 : K)] :=358 @FRC.LedgerML.p06032359set_option linter.defProp false in360/-- 6:E5 (p06034) — Spectral obstruction: for $\kap\ge2$ no invertible $T$ on $\Vt$ satisfies $T\sigma T^{-1}=\Ft^{[s]}$ for any $s$; the cyclic groups $\langle\sigma\rangle$ and $\langle\Ft^{[1]}\rangle$, each of order $4\kap$ ($\Ft^{[1]}$ by C4; $\sigma$ permutes the $4\kap$ labels cyclically), are not conjugate. -/361def p06034 := @FRC.LedgerML.p06034362/-- 6:E6 (p06035) — Common character sector: $\Ft^{[s]}\Pi_1=\gen^{-s}\Pi_1$, so on $E_1=\operatorname{im}\Pi_1\neq0$ ($\kap\ge2$) the family acts by the meridian character; the intertwiner $\Ft^{[s]}T_v=T_vS_{-s}$ on every $x\in\Fp$ and $s$, and $R_s(1,-\im)^{\mathsf T}=\gen^{-s}(1,-\im)^{\mathsf T}$. -/363theorem p06035 : (∀ {K : Type u_1} [Field K] {A : Type u_2} [Ring A] [Algebra K A] {n : ℕ} (i z : K) (f : A), i ^ (4 : ℕ) = (1 : K) → (∀ (d : ZMod (4 : ℕ)), d ≠ (0 : ZMod (4 : ℕ)) → FRC.Fractional.chi i d ≠ (1 : K)) → (4 : K) ≠ (0 : K) → f ^ (4 : ℕ) = (1 : A) → ∀ (s : ZMod n), FRC.Fractional.frft i z f s * FRC.Fractional.proj i f (1 : ZMod (4 : ℕ)) = FRC.Fractional.psi z s • FRC.Fractional.proj i f (1 : ZMod (4 : ℕ))) ∧ ∀ {K : Type u_3} [Field K] (i : K), i ^ (2 : ℕ) = (-1 : K) → (2 : K) ≠ (0 : K) → ∀ (z : K), z ≠ (0 : K) → (FRC.Fractional.rot i z).mulVec ![(1 : K), -i] = z • ![(1 : K), -i] :=364 @FRC.LedgerML.p06035365/-- 6:E7 (p06036) — Cardinal Heisenberg covariance: $\Ft\sigma\Ft^{-1}=D_1$, $\Ft D_1\Ft^{-1}=\sigma^{-1}$; $\Ft^{r}\sigma=\sigma_r\Ft^{r}$ with $(\sigma,D_1,\sigma^{-1},D_1^{-1})$; the expansion \eqref{eq:conj-expansion}, $\Ft^{[s]}=\sum_r c_r(s)\Ft^{r}$ with $c_r(s)=\tfrac14\sum_\ell(\gen^{r\kap-s})^{\ell}$. -/366theorem p06036 : ∀ {F : Type u_1} [Field F] [Fintype F] (κ : ℕ) [NeZero κ] (g : F), Fintype.card F = (4 : ℕ) * κ + (1 : ℕ) → IsPrimitiveRoot g ((4 : ℕ) * κ) → FRC.Fractional.Fmat κ g * FRC.Fractional.shift = FRC.Fractional.modul g * FRC.Fractional.Fmat κ g ∧ FRC.Fractional.Fmat κ g * FRC.Fractional.modul g = FRC.Fractional.shift' * FRC.Fractional.Fmat κ g ∧ FRC.Fractional.shift * FRC.Fractional.shift' = (1 : Matrix (Fin ((4 : ℕ) * κ)) (Fin ((4 : ℕ) * κ)) F) :=367 @FRC.LedgerML.p06036368-- end ledger predicates369370end FRC.Fourier371