Fourier.lean — FrcCore

1import FrcCore.Sum2import FrcCore.Meridian3import FrcCore.Keys.Fourier4import FrcCore.Keys.Frame56/-!7# FrcCore.Fourier — 6-fourier predicates on the core89The predicates of *Scale-Shift and Fractional Fourier Transform as Rotations over Finite Holographic Substrate*10(6-fourier) that the core proves with no axioms, named by their accession keys below and proved in the modules this11one imports through the key files: the frame theme's `Sum` and `Meridian` for 6:B2, 6:B3, 6:B5, 6:B7, 6:D412(the Euler identity, the orientation class, `W² = −J`, `W J = J W`, the meridian scale law with the `p = 13` ladder),13and the fourier theme's eight files for the rest: `Theme/Fourier` (the shell DFT and the fractional family),14`Theme/Fractional` (the projector algebra, faithfulness, the domains: 6:C2, 6:C4, 6:C5, 6:D1, 6:D2, 6:D7),15`Theme/Lifts` (the exponent lifts, the charts, the normalization: 6:B6, 6:C6, 6:C8, 6:C11), `Theme/Dichotomy`16(the multiplicity dichotomy in trace form, 6:C7), `Theme/Rotations` (the rotation group of the label plane: 6:E2,176:E3, 6:E10), `Theme/Heisenberg` (the character sector and the Heisenberg pair: 6:E6, 6:E7), `Theme/Spectra`18(the spectra and the spectral obstruction: 6:E5, 6:E9) and `Theme/Exclusivity` (cardinal exclusivity, 6:E8);196:C3 and 6:C9 are `Theme/Fourier`'s. The Mathlib statements of fifteen of these predicates, for every shell, are20in `FrcLedger/Fourier.lean`; the paper's python witness checks them on six shells.21-/2223namespace FRC.Fourier2425-- Ledger predicates of 6-fourier (generated by make_predicates.py from docs/6-fourier/6-fourier-ledger.json; edit the ledger, not this section)26/-- 6:B2 (p06009) — The Euler identity is a property of the chart class: $e^{\im\pi}=\gen^{2\kap(\im\bmod2)}\equiv-1$ exactly when the quarter-turn residue is odd; the conjugate reframing $(\gen,\im)\mapsto(\gen^{-1},-\im)$ toggles the parity, so one member of each conjugate pair carries it; on $\F_{13}(\chron;0,1,2)$, $\im=5$ and $6^{6}=-1$. Every primitive frame of the six shells. -/27theorem p06009 : ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (i : Nat), (g ^ i) ^ (i * ((2 : Nat) * κ)) = if i % (2 : Nat) = (0 : Nat) then (1 : FRC.Shell p) else (-1 : FRC.Shell p) :=28  @FRC.Ledger.p0600929/-- 6:B3 (p06010) — Chart covariance: under $\gen'=\gen^{u}$, $u\in\Zp^{\times}$, the quarter-turn name flips exactly on $u\equiv3\pmod4$ and the exponential-unit name moves already at $u\equiv1\pmod4$ whenever $\im(u-1)\not\equiv0\pmod{4\kap}$ ($\p=13$, $u=5$: $e'=2\neq6$); the objects of C3, C4 and C9 are invariant. -/30theorem p06010 : ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (u : Nat), (u % (4 : Nat) = (1 : Nat) → -(g ^ u) ^ κ = -g ^ κ) ∧ (u % (4 : Nat) = (3 : Nat) → -(g ^ u) ^ κ = - -g ^ κ) :=31  @FRC.Ledger.p0601032/-- 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}. -/33theorem p06012 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (k j : Nat), FRC.Shell.sumRange (fun l => FRC.Shell.Frame.W g k l * FRC.Shell.Frame.W g l j) (p - (1 : Nat)) = -FRC.Shell.Frame.J (p - (1 : Nat)) k j) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (k j : Nat), FRC.Shell.sumRange (fun l => FRC.Shell.Frame.Fmat g κ k l * FRC.Shell.Frame.Fmat g κ l j) (p - (1 : Nat)) = FRC.Shell.Frame.J (p - (1 : Nat)) k j) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {k j : Nat}, k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.sumRange (fun l => FRC.Shell.Frame.J (p - (1 : Nat)) k l * FRC.Shell.Frame.J (p - (1 : Nat)) l j) (p - (1 : Nat)) = if k = j then (1 : FRC.Shell p) else (0 : FRC.Shell p) :=34  @FRC.Ledger.p0601235/-- 6:B6 (p06013) — The normalization is the unitary constant read in the field: $1/n\equiv-1$, its square roots in $\Fp$ are exactly $\pm\im$, and $(c\Wt)^{2}=J$ if and only if $c=\pm\im$. -/36theorem p06013 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → FRC.Shell.ofNat (p - (1 : Nat)) = (-1 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (x : FRC.Shell p), x * x = (-1 : FRC.Shell p) ↔ x = FRC.Shell.Frame.quarterTurn g κ ∨ x = -FRC.Shell.Frame.quarterTurn g κ) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (c : FRC.Shell p), (∀ (k j : Nat), k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.sumRange (fun l => c * FRC.Shell.Frame.W g k l * (c * FRC.Shell.Frame.W g l j)) (p - (1 : Nat)) = FRC.Shell.Frame.J (p - (1 : Nat)) k j) ↔ c = FRC.Shell.Frame.quarterTurn g κ ∨ c = -FRC.Shell.Frame.quarterTurn g κ :=37  @FRC.Ledger.p0601338/-- 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$. -/39theorem p06014 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {k j : Nat}, k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.sumRange (fun l => FRC.Shell.Frame.W g k l * FRC.Shell.Frame.J (p - (1 : Nat)) l j) (p - (1 : Nat)) = FRC.Shell.sumRange (fun l => FRC.Shell.Frame.J (p - (1 : Nat)) k l * FRC.Shell.Frame.W g l j) (p - (1 : Nat))) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (v : Nat → FRC.Shell p), ∃ vp vm, FRC.Shell.Frame.Symm (p - (1 : Nat)) vp ∧ FRC.Shell.Frame.Antisymm (p - (1 : Nat)) vm ∧ ∀ (k : Nat), k < p - (1 : Nat) → v k = vp k + vm k) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {a b : Nat → FRC.Shell p}, FRC.Shell.Frame.Symm (p - (1 : Nat)) a → FRC.Shell.Frame.Antisymm (p - (1 : Nat)) b → (∀ (k : Nat), k < p - (1 : Nat) → a k + b k = (0 : FRC.Shell p)) → ∀ (k : Nat), k < p - (1 : Nat) → a k = (0 : FRC.Shell p) ∧ b k = (0 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {v w : Nat → FRC.Shell p}, FRC.Shell.Frame.Symm (p - (1 : Nat)) v → FRC.Shell.Frame.Symm (p - (1 : Nat)) w → (∀ (k : Nat), k ≤ (2 : Nat) * κ → v k = w k) → ∀ (k : Nat), k < p - (1 : Nat) → v k = w k) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {v w : Nat → FRC.Shell p}, FRC.Shell.Frame.Antisymm (p - (1 : Nat)) v → FRC.Shell.Frame.Antisymm (p - (1 : Nat)) w → (∀ (k : Nat), (0 : Nat) < k → k < (2 : Nat) * κ → v k = w k) → ∀ (k : Nat), k < p - (1 : Nat) → v k = w k :=40  @FRC.Ledger.p0601441/-- 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$. -/42theorem p06016 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (ℓ : Nat) {k j : Nat}, k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.sumRange (fun l => FRC.Shell.Frame.proj g κ ℓ k l * FRC.Shell.Frame.proj g κ ℓ l j) (p - (1 : Nat)) = FRC.Shell.Frame.proj g κ ℓ k j) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {ℓ m : Nat}, ℓ < (4 : Nat) → m < (4 : Nat) → ℓ ≠ m → ∀ {k j : Nat}, k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.sumRange (fun l => FRC.Shell.Frame.proj g κ ℓ k l * FRC.Shell.Frame.proj g κ m l j) (p - (1 : Nat)) = (0 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (k j : Nat), FRC.Shell.Frame.proj g κ (0 : Nat) k j + FRC.Shell.Frame.proj g κ (1 : Nat) k j + FRC.Shell.Frame.proj g κ (2 : Nat) k j + FRC.Shell.Frame.proj g κ (3 : Nat) k j = FRC.Shell.Frame.idm k j) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (ℓ : Nat) {k j : Nat}, k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.sumRange (fun l => FRC.Shell.Frame.Fmat g κ k l * FRC.Shell.Frame.proj g κ ℓ l j) (p - (1 : Nat)) = FRC.Shell.Frame.quarterTurn g κ ^ ℓ * FRC.Shell.Frame.proj g κ ℓ k j :=43  @FRC.Ledger.p0601644/-- 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$. -/45theorem p06017 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (z : FRC.Shell p) (s r : Nat) {k j : Nat}, k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.Frame.frft g κ z (s + r) k j = FRC.Shell.sumRange (fun l => FRC.Shell.Frame.frft g κ z s k l * FRC.Shell.Frame.frft g κ z r l j) (p - (1 : Nat))) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ (k j : Nat), FRC.Shell.Frame.frft g κ z (0 : Nat) k j = FRC.Shell.Frame.idm k j ∧ FRC.Shell.Frame.frft g κ z κ k j = FRC.Shell.Frame.Fmat g κ k j ∧ FRC.Shell.Frame.frft g κ z ((2 : Nat) * κ) k j = FRC.Shell.Frame.J (p - (1 : Nat)) k j ∧ FRC.Shell.Frame.frft g κ z ((3 : Nat) * κ) k j = FRC.Shell.Frame.FJ g κ k j) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ (s k j : Nat), FRC.Shell.Frame.frft g κ z (s + (p - (1 : Nat))) k j = FRC.Shell.Frame.frft g κ z s k j) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ (s m k j : Nat), k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.Frame.frft g κ z (m * s) k j = FRC.Shell.Frame.mpow (FRC.Shell.Frame.frft g κ z s) m k j :=46  @FRC.Ledger.p0601747/-- 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. -/48theorem p06018 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → (2 : Nat) ≤ κ → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ {s r : Nat}, s < p - (1 : Nat) → r < p - (1 : Nat) → (∀ (k j : Nat), k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.Frame.frft g κ z s k j = FRC.Shell.Frame.frft g κ z r k j) → s = r) ∧ (∀ (g : FRC.Shell (5 : Nat)), g.IsPrimitive (4 : Nat) → g = (2 : FRC.Shell (5 : Nat)) ∨ g = (3 : FRC.Shell (5 : Nat))) ∧ ((∀ (s : Nat), s < (4 : Nat) → ∀ (r : Nat), r < (4 : Nat) → (∀ (k : Nat), k < (4 : Nat) → ∀ (j : Nat), j < (4 : Nat) → FRC.Shell.Frame.frft (2 : FRC.Shell (5 : Nat)) (1 : Nat) (3 : FRC.Shell (5 : Nat)) s k j = FRC.Shell.Frame.frft (2 : FRC.Shell (5 : Nat)) (1 : Nat) (3 : FRC.Shell (5 : Nat)) r k j) → s = r) ∧ ∀ (s : Nat), s < (4 : Nat) → ∀ (r : Nat), r < (4 : Nat) → (∀ (k : Nat), k < (4 : Nat) → ∀ (j : Nat), j < (4 : Nat) → FRC.Shell.Frame.frft (3 : FRC.Shell (5 : Nat)) (1 : Nat) (2 : FRC.Shell (5 : Nat)) s k j = FRC.Shell.Frame.frft (3 : FRC.Shell (5 : Nat)) (1 : Nat) (2 : FRC.Shell (5 : Nat)) r k j) → s = r) ∧ (∀ (k : Nat), k < (4 : Nat) → ∀ (j : Nat), j < (4 : Nat) → FRC.Shell.Frame.proj (2 : FRC.Shell (5 : Nat)) (1 : Nat) (1 : Nat) k j = (0 : FRC.Shell (5 : Nat))) ∧ FRC.Shell.Frame.proj (2 : FRC.Shell (5 : Nat)) (1 : Nat) (3 : Nat) (1 : Nat) (1 : Nat) ≠ (0 : FRC.Shell (5 : Nat)) ∧ (∀ (k : Nat), k < (4 : Nat) → ∀ (j : Nat), j < (4 : Nat) → FRC.Shell.Frame.proj (3 : FRC.Shell (5 : Nat)) (1 : Nat) (3 : Nat) k j = (0 : FRC.Shell (5 : Nat))) ∧ FRC.Shell.Frame.proj (3 : FRC.Shell (5 : Nat)) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) ≠ (0 : FRC.Shell (5 : Nat)) ∧ (∀ (s : Nat), s < (4 : Nat) → ∀ (r : Nat), r < (4 : Nat) → (3 : FRC.Shell (5 : Nat)) ^ ((3 : Nat) * s) = (3 : FRC.Shell (5 : Nat)) ^ ((3 : Nat) * r) → s = r) ∧ ∀ (s : Nat), s < (4 : Nat) → ∀ (r : Nat), r < (4 : Nat) → (2 : FRC.Shell (5 : Nat)) ^ ((1 : Nat) * s) = (2 : FRC.Shell (5 : Nat)) ^ ((1 : Nat) * r) → s = r :=49  @FRC.Ledger.p0601850/-- 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. -/51theorem p06019 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (k j : Nat), FRC.Shell.Frame.proj g κ (0 : Nat) k j + FRC.Shell.Frame.proj g κ (2 : Nat) k j = (-FRC.Shell.ofNat κ + -FRC.Shell.ofNat κ) * (FRC.Shell.Frame.idm k j + FRC.Shell.Frame.J (p - (1 : Nat)) k j)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (k j : Nat), FRC.Shell.Frame.proj g κ (1 : Nat) k j + FRC.Shell.Frame.proj g κ (3 : Nat) k j = (-FRC.Shell.ofNat κ + -FRC.Shell.ofNat κ) * (FRC.Shell.Frame.idm k j + -FRC.Shell.Frame.J (p - (1 : Nat)) k j)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ((1 : FRC.Shell p) + (1 : FRC.Shell p)) * (-FRC.Shell.ofNat κ + -FRC.Shell.ofNat κ) = (1 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → FRC.Shell.Frame.proj g κ (0 : Nat) (0 : Nat) (0 : Nat) ≠ (0 : FRC.Shell p) ∧ FRC.Shell.Frame.proj g κ (2 : Nat) (0 : Nat) (0 : Nat) ≠ (0 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → (2 : Nat) ≤ κ → FRC.Shell.Frame.proj g κ (1 : Nat) (2 : Nat) (1 : Nat) ≠ (0 : FRC.Shell p) ∧ FRC.Shell.Frame.proj g κ (3 : Nat) (2 : Nat) (1 : Nat) ≠ (0 : FRC.Shell p)) ∧ (∀ (g : FRC.Shell (5 : Nat)), g.IsPrimitive (4 : Nat) → g = (2 : FRC.Shell (5 : Nat)) ∨ g = (3 : FRC.Shell (5 : Nat))) ∧ (∀ (k : Nat), k < (4 : Nat) → ∀ (j : Nat), j < (4 : Nat) → FRC.Shell.Frame.proj (2 : FRC.Shell (5 : Nat)) (1 : Nat) (1 : Nat) k j = (0 : FRC.Shell (5 : Nat))) ∧ FRC.Shell.Frame.proj (2 : FRC.Shell (5 : Nat)) (1 : Nat) (3 : Nat) (1 : Nat) (1 : Nat) ≠ (0 : FRC.Shell (5 : Nat)) ∧ (∀ (k : Nat), k < (4 : Nat) → ∀ (j : Nat), j < (4 : Nat) → FRC.Shell.Frame.proj (3 : FRC.Shell (5 : Nat)) (1 : Nat) (3 : Nat) k j = (0 : FRC.Shell (5 : Nat))) ∧ FRC.Shell.Frame.proj (3 : FRC.Shell (5 : Nat)) (1 : Nat) (1 : Nat) (1 : Nat) (1 : Nat) ≠ (0 : FRC.Shell (5 : Nat)) ∧ (∀ (s : Nat), s < (4 : Nat) → ∀ (r : Nat), r < (4 : Nat) → (3 : FRC.Shell (5 : Nat)) ^ ((3 : Nat) * s) = (3 : FRC.Shell (5 : Nat)) ^ ((3 : Nat) * r) → s = r) ∧ ∀ (s : Nat), s < (4 : Nat) → ∀ (r : Nat), r < (4 : Nat) → (2 : FRC.Shell (5 : Nat)) ^ ((1 : Nat) * s) = (2 : FRC.Shell (5 : Nat)) ^ ((1 : Nat) * r) → s = r :=52  @FRC.Ledger.p0601953/-- 6:C6 (p06020) — The projectors are chart data: for $u$ odd and a unit mod $4\kap$ the site relabelling $m\mapsto um$ carries $\Ft(\gen)$ to $\Ft(\gen^{u^{2}})$ by a coordinate permutation, $\Ft(\gen^{u^{2}})_{kj}=\Ft(\gen)_{uk,uj}$; at $\p=13$ the frames $\gen=2$ and $\gen=6$ give the trace tuples $(3,3,4,2)$ and $(4,2,3,3)$, with $\operatorname{Tr}\Ft=4,9$. -/54theorem p06020 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {u : Nat}, u % (2 : Nat) = (1 : Nat) → ∀ (k j : Nat), FRC.Shell.Frame.Fmat (g ^ (u * u)) κ k j = FRC.Shell.Frame.Fmat g κ (u * k % (p - (1 : Nat))) (u * j % (p - (1 : Nat)))) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (2 : FRC.Shell (13 : Nat)) (3 : Nat) (0 : Nat)) (12 : Nat) = (3 : FRC.Shell (13 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (2 : FRC.Shell (13 : Nat)) (3 : Nat) (1 : Nat)) (12 : Nat) = (3 : FRC.Shell (13 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (2 : FRC.Shell (13 : Nat)) (3 : Nat) (2 : Nat)) (12 : Nat) = (4 : FRC.Shell (13 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (2 : FRC.Shell (13 : Nat)) (3 : Nat) (3 : Nat)) (12 : Nat) = (2 : FRC.Shell (13 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (6 : FRC.Shell (13 : Nat)) (3 : Nat) (0 : Nat)) (12 : Nat) = (4 : FRC.Shell (13 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (6 : FRC.Shell (13 : Nat)) (3 : Nat) (1 : Nat)) (12 : Nat) = (2 : FRC.Shell (13 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (6 : FRC.Shell (13 : Nat)) (3 : Nat) (2 : Nat)) (12 : Nat) = (3 : FRC.Shell (13 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (6 : FRC.Shell (13 : Nat)) (3 : Nat) (3 : Nat)) (12 : Nat) = (3 : FRC.Shell (13 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.Fmat (2 : FRC.Shell (13 : Nat)) (3 : Nat)) (12 : Nat) = (4 : FRC.Shell (13 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.Fmat (6 : FRC.Shell (13 : Nat)) (3 : Nat)) (12 : Nat) = (9 : FRC.Shell (13 : Nat)) :=55  @FRC.Ledger.p0602056/-- 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$. -/57theorem p06021 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → FRC.Shell.Frame.trace FRC.Shell.Frame.idm (p - (1 : Nat)) = (-1 : FRC.Shell p) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.Fmat g κ) (p - (1 : Nat)) = FRC.Shell.Frame.quarterTurn g κ * FRC.Shell.Frame.gauss g (p - (1 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.J (p - (1 : Nat))) (p - (1 : Nat)) = (1 : FRC.Shell p) + (1 : FRC.Shell p) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.FJ g κ) (p - (1 : Nat)) = FRC.Shell.Frame.quarterTurn g κ * FRC.Shell.Frame.gauss z (p - (1 : Nat))) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ (ℓ : Nat), FRC.Shell.Frame.trace (FRC.Shell.Frame.proj g κ ℓ) (p - (1 : Nat)) = -FRC.Shell.ofNat κ * (-1 : FRC.Shell p) + -FRC.Shell.ofNat κ * (-FRC.Shell.Frame.quarterTurn g κ) ^ ℓ * (FRC.Shell.Frame.quarterTurn g κ * FRC.Shell.Frame.gauss g (p - (1 : Nat))) + -FRC.Shell.ofNat κ * ((-FRC.Shell.Frame.quarterTurn g κ) ^ ℓ * (-FRC.Shell.Frame.quarterTurn g κ) ^ ℓ) * ((1 : FRC.Shell p) + (1 : FRC.Shell p)) + -FRC.Shell.ofNat κ * ((-FRC.Shell.Frame.quarterTurn g κ) ^ ℓ * (-FRC.Shell.Frame.quarterTurn g κ) ^ ℓ * (-FRC.Shell.Frame.quarterTurn g κ) ^ ℓ) * (FRC.Shell.Frame.quarterTurn g κ * FRC.Shell.Frame.gauss z (p - (1 : Nat)))) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → FRC.Shell.Frame.gauss g (p - (1 : Nat)) * FRC.Shell.Frame.gauss z (p - (1 : Nat)) = -((1 : FRC.Shell p) + (1 : FRC.Shell p))) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ {ε : FRC.Shell p}, ε * ε = (1 : FRC.Shell p) → FRC.Shell.Frame.gauss g (p - (1 : Nat)) = ε * ((1 : FRC.Shell p) + FRC.Shell.Frame.quarterTurn g κ) → FRC.Shell.Frame.gauss z (p - (1 : Nat)) = -(ε * ((1 : FRC.Shell p) + -FRC.Shell.Frame.quarterTurn g κ))) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ {ε : FRC.Shell p}, ε = (1 : FRC.Shell p) ∨ ε = (-1 : FRC.Shell p) → FRC.Shell.Frame.gauss g (p - (1 : Nat)) = ε * ((1 : FRC.Shell p) + FRC.Shell.Frame.quarterTurn g κ) → ε = (1 : FRC.Shell p) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj g κ (0 : Nat)) (p - (1 : Nat)) = FRC.Shell.ofNat κ ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj g κ (1 : Nat)) (p - (1 : Nat)) = FRC.Shell.ofNat κ ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj g κ (2 : Nat)) (p - (1 : Nat)) = FRC.Shell.ofNat κ + (1 : FRC.Shell p) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj g κ (3 : Nat)) (p - (1 : Nat)) = FRC.Shell.ofNat κ + (-1 : FRC.Shell p) ∨ ε = (-1 : FRC.Shell p) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj g κ (0 : Nat)) (p - (1 : Nat)) = FRC.Shell.ofNat κ + (1 : FRC.Shell p) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj g κ (1 : Nat)) (p - (1 : Nat)) = FRC.Shell.ofNat κ + (-1 : FRC.Shell p) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj g κ (2 : Nat)) (p - (1 : Nat)) = FRC.Shell.ofNat κ ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj g κ (3 : Nat)) (p - (1 : Nat)) = FRC.Shell.ofNat κ) ∧ (FRC.Shell.Frame.gauss (2 : FRC.Shell (5 : Nat)) (4 : Nat) = (-1 : FRC.Shell (5 : Nat)) * ((1 : FRC.Shell (5 : Nat)) + FRC.Shell.Frame.quarterTurn (2 : FRC.Shell (5 : Nat)) (1 : Nat)) ∧ FRC.Shell.Frame.gauss (2 : FRC.Shell (13 : Nat)) (12 : Nat) = (1 : FRC.Shell (13 : Nat)) * ((1 : FRC.Shell (13 : Nat)) + FRC.Shell.Frame.quarterTurn (2 : FRC.Shell (13 : Nat)) (3 : Nat)) ∧ FRC.Shell.Frame.gauss (3 : FRC.Shell (17 : Nat)) (16 : Nat) = (1 : FRC.Shell (17 : Nat)) * ((1 : FRC.Shell (17 : Nat)) + FRC.Shell.Frame.quarterTurn (3 : FRC.Shell (17 : Nat)) (4 : Nat)) ∧ FRC.Shell.Frame.gauss (2 : FRC.Shell (29 : Nat)) (28 : Nat) = (1 : FRC.Shell (29 : Nat)) * ((1 : FRC.Shell (29 : Nat)) + FRC.Shell.Frame.quarterTurn (2 : FRC.Shell (29 : Nat)) (7 : Nat)) ∧ FRC.Shell.Frame.gauss (2 : FRC.Shell (37 : Nat)) (36 : Nat) = (1 : FRC.Shell (37 : Nat)) * ((1 : FRC.Shell (37 : Nat)) + FRC.Shell.Frame.quarterTurn (2 : FRC.Shell (37 : Nat)) (9 : Nat)) ∧ FRC.Shell.Frame.gauss (6 : FRC.Shell (41 : Nat)) (40 : Nat) = (1 : FRC.Shell (41 : Nat)) * ((1 : FRC.Shell (41 : Nat)) + FRC.Shell.Frame.quarterTurn (6 : FRC.Shell (41 : Nat)) (10 : Nat))) ∧ (FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (2 : FRC.Shell (5 : Nat)) (1 : Nat) (0 : Nat)) (4 : Nat) = (2 : FRC.Shell (5 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (2 : FRC.Shell (5 : Nat)) (1 : Nat) (1 : Nat)) (4 : Nat) = (0 : FRC.Shell (5 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (2 : FRC.Shell (5 : Nat)) (1 : Nat) (2 : Nat)) (4 : Nat) = (1 : FRC.Shell (5 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (2 : FRC.Shell (5 : Nat)) (1 : Nat) (3 : Nat)) (4 : Nat) = (1 : FRC.Shell (5 : Nat))) ∧ (FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (2 : FRC.Shell (13 : Nat)) (3 : Nat) (0 : Nat)) (12 : Nat) = (3 : FRC.Shell (13 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (2 : FRC.Shell (13 : Nat)) (3 : Nat) (1 : Nat)) (12 : Nat) = (3 : FRC.Shell (13 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (2 : FRC.Shell (13 : Nat)) (3 : Nat) (2 : Nat)) (12 : Nat) = (4 : FRC.Shell (13 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (2 : FRC.Shell (13 : Nat)) (3 : Nat) (3 : Nat)) (12 : Nat) = (2 : FRC.Shell (13 : Nat))) ∧ (FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (3 : FRC.Shell (17 : Nat)) (4 : Nat) (0 : Nat)) (16 : Nat) = (4 : FRC.Shell (17 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (3 : FRC.Shell (17 : Nat)) (4 : Nat) (1 : Nat)) (16 : Nat) = (4 : FRC.Shell (17 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (3 : FRC.Shell (17 : Nat)) (4 : Nat) (2 : Nat)) (16 : Nat) = (5 : FRC.Shell (17 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (3 : FRC.Shell (17 : Nat)) (4 : Nat) (3 : Nat)) (16 : Nat) = (3 : FRC.Shell (17 : Nat))) ∧ (FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (2 : FRC.Shell (29 : Nat)) (7 : Nat) (0 : Nat)) (28 : Nat) = (7 : FRC.Shell (29 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (2 : FRC.Shell (29 : Nat)) (7 : Nat) (1 : Nat)) (28 : Nat) = (7 : FRC.Shell (29 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (2 : FRC.Shell (29 : Nat)) (7 : Nat) (2 : Nat)) (28 : Nat) = (8 : FRC.Shell (29 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (2 : FRC.Shell (29 : Nat)) (7 : Nat) (3 : Nat)) (28 : Nat) = (6 : FRC.Shell (29 : Nat))) ∧ (FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (2 : FRC.Shell (37 : Nat)) (9 : Nat) (0 : Nat)) (36 : Nat) = (9 : FRC.Shell (37 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (2 : FRC.Shell (37 : Nat)) (9 : Nat) (1 : Nat)) (36 : Nat) = (9 : FRC.Shell (37 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (2 : FRC.Shell (37 : Nat)) (9 : Nat) (2 : Nat)) (36 : Nat) = (10 : FRC.Shell (37 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (2 : FRC.Shell (37 : Nat)) (9 : Nat) (3 : Nat)) (36 : Nat) = (8 : FRC.Shell (37 : Nat))) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (6 : FRC.Shell (41 : Nat)) (10 : Nat) (0 : Nat)) (40 : Nat) = (10 : FRC.Shell (41 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (6 : FRC.Shell (41 : Nat)) (10 : Nat) (1 : Nat)) (40 : Nat) = (10 : FRC.Shell (41 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (6 : FRC.Shell (41 : Nat)) (10 : Nat) (2 : Nat)) (40 : Nat) = (11 : FRC.Shell (41 : Nat)) ∧ FRC.Shell.Frame.trace (FRC.Shell.Frame.proj (6 : FRC.Shell (41 : Nat)) (10 : Nat) (3 : Nat)) (40 : Nat) = (9 : FRC.Shell (41 : Nat)) :=58  @FRC.Ledger.p0602159/-- 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}$. -/60theorem p06022 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (z : FRC.Shell p) (a : Nat → Nat) (s r : Nat) {k j : Nat}, k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.sumRange (fun l => FRC.Shell.Frame.lift g κ z a s k l * FRC.Shell.Frame.lift g κ z a r l j) (p - (1 : Nat)) = FRC.Shell.Frame.lift g κ z a (s + r) k j) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ (a : Nat → Nat), (∀ (ℓ : Nat), ℓ < (4 : Nat) → a ℓ % (4 : Nat) = ℓ) → ∀ (m k j : Nat), FRC.Shell.Frame.lift g κ z a (m * κ) k j = FRC.Shell.Frame.frft g κ z (m * κ) k j) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ (a : Nat → Nat), (∀ (ℓ : Nat), ℓ < (4 : Nat) → a ℓ % (4 : Nat) = ℓ) → ∀ (m : Nat) {k j : Nat}, k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.Frame.lift g κ z a (m * κ) k j = FRC.Shell.Frame.mpow (FRC.Shell.Frame.Fmat g κ) m k j :=61  @FRC.Ledger.p0602262/-- 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. -/63theorem p06023 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → FRC.Shell.Frame p κ z) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ {k j : Nat}, k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.Frame.Fmat z κ k j = -FRC.Shell.Frame.FJ g κ k j) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ (ℓ : Nat) {k j : Nat}, k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.Frame.proj z κ ℓ k j = FRC.Shell.Frame.proj g κ (ℓ + (2 : Nat)) k j :=64  @FRC.Ledger.p0602365/-- 6:C11 (p06052) — Charts outside the classified set: for $u$ a unit mod $4\kap$, $\Wt(\gen^{u})=\Wt P_u$ with $P_u$ the site relabelling $j\mapsto uj$, so $\Wt\,\Wt(\gen^{u})=-JP_u$ and $\Wt(\gen^{u})\,\Wt=-JP_{u^{-1}}$, and the two differ at the entry $(-u,1)$ when $u^{2}\not\equiv1\pmod{4\kap}$: a family canonical in such a chart does not commute with $\Ft$; $\p=29$, $u=5$, and every such chart of the six shells of Table~\ref{tab:checks} checked. -/66theorem p06052 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (u k j : Nat), FRC.Shell.Frame.W (g ^ u) k j = FRC.Shell.Frame.W g k (u * j % (p - (1 : Nat)))) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (u k j : Nat), FRC.Shell.sumRange (fun l => FRC.Shell.Frame.W g k l * FRC.Shell.Frame.W (g ^ u) l j) (p - (1 : Nat)) = -if (k + u * j) % (p - (1 : Nat)) = (0 : Nat) then (1 : FRC.Shell p) else (0 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (u k j : Nat), FRC.Shell.sumRange (fun l => FRC.Shell.Frame.W (g ^ u) k l * FRC.Shell.Frame.W g l j) (p - (1 : Nat)) = -if (u * k + j) % (p - (1 : Nat)) = (0 : Nat) then (1 : FRC.Shell p) else (0 : FRC.Shell p)) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {u : Nat}, u * u % (p - (1 : Nat)) ≠ (1 : Nat) → FRC.Shell.sumRange (fun l => FRC.Shell.Frame.W g (FRC.Shell.Frame.rev (p - (1 : Nat)) (u % (p - (1 : Nat)))) l * FRC.Shell.Frame.W (g ^ u) l (1 : Nat)) (p - (1 : Nat)) ≠ FRC.Shell.sumRange (fun l => FRC.Shell.Frame.W (g ^ u) (FRC.Shell.Frame.rev (p - (1 : Nat)) (u % (p - (1 : Nat)))) l * FRC.Shell.Frame.W g l (1 : Nat)) (p - (1 : Nat)) :=67  @FRC.Ledger.p0605268/-- 6:D1 (p06024) — The meridional representation domain $D_s=(\Vt,\mathcal B_s)$, $\mathcal B_s=\Ft^{[s]}\mathcal B_0$, every $\Ft^{[s]}$ invertible with inverse $\Ft^{[n-s]}$; the cardinal domains spatial, spectral, parity, inverse-spectral. -/69theorem p06024 : ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ {s : Nat}, s ≤ p - (1 : Nat) → ∀ {k j : Nat}, k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.sumRange (fun l => FRC.Shell.Frame.frft g κ z s k l * FRC.Shell.Frame.frft g κ z (p - (1 : Nat) - s) l j) (p - (1 : Nat)) = FRC.Shell.Frame.idm k j ∧ FRC.Shell.sumRange (fun l => FRC.Shell.Frame.frft g κ z (p - (1 : Nat) - s) k l * FRC.Shell.Frame.frft g κ z s l j) (p - (1 : Nat)) = FRC.Shell.Frame.idm k j :=70  @FRC.Ledger.p0602471/-- 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. -/72theorem p06025 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → (2 : Nat) ≤ κ → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ {s r : Nat}, s < p - (1 : Nat) → r < p - (1 : Nat) → (∀ (k j : Nat), k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.Frame.frft g κ z s k j = FRC.Shell.Frame.frft g κ z r k j) → s = r) ∧ (∀ (g : FRC.Shell (5 : Nat)), g.IsPrimitive (4 : Nat) → g = (2 : FRC.Shell (5 : Nat)) ∨ g = (3 : FRC.Shell (5 : Nat))) ∧ ((∀ (s : Nat), s < (4 : Nat) → ∀ (r : Nat), r < (4 : Nat) → (∀ (k : Nat), k < (4 : Nat) → ∀ (j : Nat), j < (4 : Nat) → FRC.Shell.Frame.frft (2 : FRC.Shell (5 : Nat)) (1 : Nat) (3 : FRC.Shell (5 : Nat)) s k j = FRC.Shell.Frame.frft (2 : FRC.Shell (5 : Nat)) (1 : Nat) (3 : FRC.Shell (5 : Nat)) r k j) → s = r) ∧ ∀ (s : Nat), s < (4 : Nat) → ∀ (r : Nat), r < (4 : Nat) → (∀ (k : Nat), k < (4 : Nat) → ∀ (j : Nat), j < (4 : Nat) → FRC.Shell.Frame.frft (3 : FRC.Shell (5 : Nat)) (1 : Nat) (2 : FRC.Shell (5 : Nat)) s k j = FRC.Shell.Frame.frft (3 : FRC.Shell (5 : Nat)) (1 : Nat) (2 : FRC.Shell (5 : Nat)) r k j) → s = r) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ (s : Nat) {k j : Nat}, k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.Frame.frft g κ z (s + (2 : Nat) * κ) k j = FRC.Shell.Frame.frft g κ z s k (FRC.Shell.Frame.rev (p - (1 : Nat)) j) :=73  @FRC.Ledger.p0602574/-- 6:D4 (p06027) — Meridian-scale covariance: $S_r(M_m)=M_{m+r}$ for every $(m,r)$, as ordered lists; consecutive entries of $M_m$ differ by the effective step $\gen^{m}$; $S_{r+(\p-1)}=S_r$, the periodicity of A5 in meridian form; at $\p=13$, $\gen=2$ the ladder $M_0,\dots,M_3$ at the steps $1,2,4,8$ (Section~\ref{sec:examples}). -/75theorem p06027 : (∀ {p : Nat} [FRC.Pos p] (g : FRC.Shell p) (κ m r : Nat), List.map (g.scale r) (g.meridian κ m) = g.meridian κ (m + r)) ∧ (∀ {p : Nat} [FRC.Pos p] (g : FRC.Shell p) (m a : Nat), FRC.Shell.ofNat (a + (1 : Nat)) * g ^ m = FRC.Shell.ofNat a * g ^ m + g ^ m) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (r : Nat) (x : FRC.Shell p), g.scale (r + (p - (1 : Nat))) x = g.scale r x) ∧ FRC.Shell.meridian (2 : FRC.Shell (13 : Nat)) (3 : Nat) (0 : Nat) = [(0 : FRC.Shell (13 : Nat)), (1 : FRC.Shell (13 : Nat)), (2 : FRC.Shell (13 : Nat)), (3 : FRC.Shell (13 : Nat)), (4 : FRC.Shell (13 : Nat)), (5 : FRC.Shell (13 : Nat)), (6 : FRC.Shell (13 : Nat))] ∧ FRC.Shell.meridian (2 : FRC.Shell (13 : Nat)) (3 : Nat) (1 : Nat) = [(0 : FRC.Shell (13 : Nat)), (2 : FRC.Shell (13 : Nat)), (4 : FRC.Shell (13 : Nat)), (6 : FRC.Shell (13 : Nat)), (8 : FRC.Shell (13 : Nat)), (10 : FRC.Shell (13 : Nat)), (12 : FRC.Shell (13 : Nat))] ∧ FRC.Shell.meridian (2 : FRC.Shell (13 : Nat)) (3 : Nat) (2 : Nat) = [(0 : FRC.Shell (13 : Nat)), (4 : FRC.Shell (13 : Nat)), (8 : FRC.Shell (13 : Nat)), (12 : FRC.Shell (13 : Nat)), (3 : FRC.Shell (13 : Nat)), (7 : FRC.Shell (13 : Nat)), (11 : FRC.Shell (13 : Nat))] ∧ FRC.Shell.meridian (2 : FRC.Shell (13 : Nat)) (3 : Nat) (3 : Nat) = [(0 : FRC.Shell (13 : Nat)), (8 : FRC.Shell (13 : Nat)), (3 : FRC.Shell (13 : Nat)), (11 : FRC.Shell (13 : Nat)), (6 : FRC.Shell (13 : Nat)), (1 : FRC.Shell (13 : Nat)), (9 : FRC.Shell (13 : Nat))] ∧ (6 : Nat) * (2 : Nat) ^ (1 : Nat) < (13 : Nat) ∧ ¬(6 : Nat) * (2 : Nat) ^ (2 : Nat) < (13 : Nat) :=76  @FRC.Ledger.p0602777/-- 6:D7 (p06053) — The cycle carries exactly $2\kap$ unordered bases: every off-site entry of row $0$ of $\Ft^{[t]}$ is $\tfrac{\im}{2}(1-\gen^{-2t})$, nonzero for $t\notin\{0,2\kap\}$, so $\Ft^{[t]}$ is not monomial and $B_{s+t}\neq B_s$; the six shells of Table~\ref{tab:checks}. -/78theorem p06053 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (z : FRC.Shell p) (t : Nat) {j : Nat}, (0 : Nat) < j → j < p - (1 : Nat) → FRC.Shell.Frame.frft g κ z t (0 : Nat) j = (-FRC.Shell.ofNat κ + -FRC.Shell.ofNat κ) * ((1 : FRC.Shell p) + -(z ^ t * z ^ t)) * FRC.Shell.Frame.quarterTurn g κ) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ {t : Nat}, t < p - (1 : Nat) → t ≠ (0 : Nat) → t ≠ (2 : Nat) * κ → ∀ {j : Nat}, (0 : Nat) < j → j < p - (1 : Nat) → FRC.Shell.Frame.frft g κ z t (0 : Nat) j ≠ (0 : FRC.Shell p) :=79  @FRC.Ledger.p0605380/-- 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. -/81theorem p06031 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ (s : Nat), FRC.Shell.Frame.cs g κ z s * FRC.Shell.Frame.cs g κ z s + FRC.Shell.Frame.ds g κ z s * FRC.Shell.Frame.ds g κ z s = (1 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (z : FRC.Shell p) (s r : Nat), FRC.Shell.Frame.cs g κ z (s + r) = FRC.Shell.Frame.cs g κ z s * FRC.Shell.Frame.cs g κ z r + -(FRC.Shell.Frame.ds g κ z s * FRC.Shell.Frame.ds g κ z r) ∧ FRC.Shell.Frame.ds g κ z (s + r) = FRC.Shell.Frame.cs g κ z s * FRC.Shell.Frame.ds g κ z r + FRC.Shell.Frame.ds g κ z s * FRC.Shell.Frame.cs g κ z r) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ {s r : Nat}, s < p - (1 : Nat) → r < p - (1 : Nat) → FRC.Shell.Frame.cs g κ z s = FRC.Shell.Frame.cs g κ z r → FRC.Shell.Frame.ds g κ z s = FRC.Shell.Frame.ds g κ z r → s = r) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ {c d : FRC.Shell p}, c * c + d * d = (1 : FRC.Shell p) → ∃ s, s < p - (1 : Nat) ∧ c = FRC.Shell.Frame.cs g κ z s ∧ d = FRC.Shell.Frame.ds g κ z s) ∧ FRC.Shell.Frame.countCircle (5 : Nat) (5 : Nat) = (4 : Nat) ∧ FRC.Shell.Frame.countCircle (13 : Nat) (13 : Nat) = (12 : Nat) ∧ FRC.Shell.Frame.countCircle (17 : Nat) (17 : Nat) = (16 : Nat) ∧ FRC.Shell.Frame.countCircle (29 : Nat) (29 : Nat) = (28 : Nat) ∧ FRC.Shell.Frame.countCircle (37 : Nat) (37 : Nat) = (36 : Nat) ∧ FRC.Shell.Frame.countCircle (41 : Nat) (41 : Nat) = (40 : Nat) :=82  @FRC.Ledger.p0603183/-- 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). -/84theorem p06032 : ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → (FRC.Shell.Frame.cs g κ z (0 : Nat) = (1 : FRC.Shell p) ∧ FRC.Shell.Frame.ds g κ z (0 : Nat) = (0 : FRC.Shell p)) ∧ (FRC.Shell.Frame.cs g κ z κ = (0 : FRC.Shell p) ∧ FRC.Shell.Frame.ds g κ z κ = (1 : FRC.Shell p)) ∧ (FRC.Shell.Frame.cs g κ z ((2 : Nat) * κ) = (-1 : FRC.Shell p) ∧ FRC.Shell.Frame.ds g κ z ((2 : Nat) * κ) = (0 : FRC.Shell p)) ∧ (FRC.Shell.Frame.cs g κ z ((3 : Nat) * κ) = (0 : FRC.Shell p) ∧ FRC.Shell.Frame.ds g κ z ((3 : Nat) * κ) = (-1 : FRC.Shell p)) ∧ z ^ κ = FRC.Shell.Frame.quarterTurn g κ :=85  @FRC.Ledger.p0603286/-- 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. -/87theorem p06034 : ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → (2 : Nat) ≤ κ → ∀ (z : FRC.Shell p) (s : Nat) (T T' : Nat → Nat → FRC.Shell p), (∀ (k j : Nat), k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.Frame.mmul T' T (p - (1 : Nat)) k j = FRC.Shell.Frame.idm k j) → (∀ (k j : Nat), k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.Frame.mmul (FRC.Shell.Frame.mmul T (FRC.Shell.Frame.shift p) (p - (1 : Nat))) T' (p - (1 : Nat)) k j = FRC.Shell.Frame.frft g κ z s k j) → False :=88  @FRC.Ledger.p0603489/-- 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}$. -/90theorem p06035 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (z : FRC.Shell p) (s : Nat) {m : Nat}, m < (4 : Nat) → ∀ {k j : Nat}, k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.sumRange (fun l => FRC.Shell.Frame.frft g κ z s k l * FRC.Shell.Frame.proj g κ m l j) (p - (1 : Nat)) = (z ^ s) ^ m * FRC.Shell.Frame.proj g κ m k j) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (z : FRC.Shell p) (s : Nat) (x : FRC.Shell p) {k j : Nat}, k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.sumRange (fun l => FRC.Shell.Frame.frft g κ z s k l * (x * FRC.Shell.Frame.proj g κ (1 : Nat) l j)) (p - (1 : Nat)) = x * (z ^ s * FRC.Shell.Frame.proj g κ (1 : Nat) k j)) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (z : FRC.Shell p) (s : Nat), FRC.Shell.Frame.cs g κ z s * (1 : FRC.Shell p) + -(FRC.Shell.Frame.ds g κ z s * -FRC.Shell.Frame.quarterTurn g κ) = z ^ s * (1 : FRC.Shell p) ∧ FRC.Shell.Frame.ds g κ z s * (1 : FRC.Shell p) + FRC.Shell.Frame.cs g κ z s * -FRC.Shell.Frame.quarterTurn g κ = z ^ s * -FRC.Shell.Frame.quarterTurn g κ :=91  @FRC.Ledger.p0603592/-- 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}$. -/93theorem p06036 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {k j : Nat}, k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.sumRange (fun l => FRC.Shell.Frame.shift p k l * FRC.Shell.Frame.shiftInv p l j) (p - (1 : Nat)) = FRC.Shell.Frame.idm k j ∧ FRC.Shell.sumRange (fun l => FRC.Shell.Frame.shiftInv p k l * FRC.Shell.Frame.shift p l j) (p - (1 : Nat)) = FRC.Shell.Frame.idm k j) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ {k j : Nat}, k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.sumRange (fun l => FRC.Shell.Frame.Fmat g κ k l * FRC.Shell.Frame.shift p l j) (p - (1 : Nat)) = FRC.Shell.sumRange (fun l => FRC.Shell.Frame.modul g k l * FRC.Shell.Frame.Fmat g κ l j) (p - (1 : Nat)) ∧ FRC.Shell.sumRange (fun l => FRC.Shell.Frame.Fmat g κ k l * FRC.Shell.Frame.modul g l j) (p - (1 : Nat)) = FRC.Shell.sumRange (fun l => FRC.Shell.Frame.shiftInv p k l * FRC.Shell.Frame.Fmat g κ l j) (p - (1 : Nat)) ∧ FRC.Shell.sumRange (fun l => FRC.Shell.Frame.J (p - (1 : Nat)) k l * FRC.Shell.Frame.shift p l j) (p - (1 : Nat)) = FRC.Shell.sumRange (fun l => FRC.Shell.Frame.shiftInv p k l * FRC.Shell.Frame.J (p - (1 : Nat)) l j) (p - (1 : Nat)) ∧ FRC.Shell.sumRange (fun l => FRC.Shell.Frame.FJ g κ k l * FRC.Shell.Frame.shift p l j) (p - (1 : Nat)) = FRC.Shell.sumRange (fun l => FRC.Shell.Frame.modul z k l * FRC.Shell.Frame.FJ g κ l j) (p - (1 : Nat))) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (z : FRC.Shell p) (s k j : Nat), FRC.Shell.Frame.frft g κ z s k j = FRC.Shell.Frame.comb g κ (FRC.Shell.Frame.NF0 (-FRC.Shell.ofNat κ) (-FRC.Shell.Frame.quarterTurn g κ) (z ^ s)) (FRC.Shell.Frame.NF1 (-FRC.Shell.ofNat κ) (-FRC.Shell.Frame.quarterTurn g κ) (z ^ s)) (FRC.Shell.Frame.NF2 (-FRC.Shell.ofNat κ) (-FRC.Shell.Frame.quarterTurn g κ) (z ^ s)) (FRC.Shell.Frame.NF3 (-FRC.Shell.ofNat κ) (-FRC.Shell.Frame.quarterTurn g κ) (z ^ s)) k j) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (u : FRC.Shell p), FRC.Shell.Frame.NF0 (-FRC.Shell.ofNat κ) (-FRC.Shell.Frame.quarterTurn g κ) u = -FRC.Shell.ofNat κ * ((1 : FRC.Shell p) + u + u * u + u * u * u) ∧ FRC.Shell.Frame.NF1 (-FRC.Shell.ofNat κ) (-FRC.Shell.Frame.quarterTurn g κ) u = -FRC.Shell.ofNat κ * ((1 : FRC.Shell p) + u * -FRC.Shell.Frame.quarterTurn g κ + u * -FRC.Shell.Frame.quarterTurn g κ * (u * -FRC.Shell.Frame.quarterTurn g κ) + u * -FRC.Shell.Frame.quarterTurn g κ * (u * -FRC.Shell.Frame.quarterTurn g κ) * (u * -FRC.Shell.Frame.quarterTurn g κ)) ∧ FRC.Shell.Frame.NF2 (-FRC.Shell.ofNat κ) (-FRC.Shell.Frame.quarterTurn g κ) u = -FRC.Shell.ofNat κ * ((1 : FRC.Shell p) + u * (-FRC.Shell.Frame.quarterTurn g κ * -FRC.Shell.Frame.quarterTurn g κ) + u * (-FRC.Shell.Frame.quarterTurn g κ * -FRC.Shell.Frame.quarterTurn g κ) * (u * (-FRC.Shell.Frame.quarterTurn g κ * -FRC.Shell.Frame.quarterTurn g κ)) + u * (-FRC.Shell.Frame.quarterTurn g κ * -FRC.Shell.Frame.quarterTurn g κ) * (u * (-FRC.Shell.Frame.quarterTurn g κ * -FRC.Shell.Frame.quarterTurn g κ)) * (u * (-FRC.Shell.Frame.quarterTurn g κ * -FRC.Shell.Frame.quarterTurn g κ))) ∧ FRC.Shell.Frame.NF3 (-FRC.Shell.ofNat κ) (-FRC.Shell.Frame.quarterTurn g κ) u = -FRC.Shell.ofNat κ * ((1 : FRC.Shell p) + u * (-FRC.Shell.Frame.quarterTurn g κ * -FRC.Shell.Frame.quarterTurn g κ * -FRC.Shell.Frame.quarterTurn g κ) + u * (-FRC.Shell.Frame.quarterTurn g κ * -FRC.Shell.Frame.quarterTurn g κ * -FRC.Shell.Frame.quarterTurn g κ) * (u * (-FRC.Shell.Frame.quarterTurn g κ * -FRC.Shell.Frame.quarterTurn g κ * -FRC.Shell.Frame.quarterTurn g κ)) + u * (-FRC.Shell.Frame.quarterTurn g κ * -FRC.Shell.Frame.quarterTurn g κ * -FRC.Shell.Frame.quarterTurn g κ) * (u * (-FRC.Shell.Frame.quarterTurn g κ * -FRC.Shell.Frame.quarterTurn g κ * -FRC.Shell.Frame.quarterTurn g κ)) * (u * (-FRC.Shell.Frame.quarterTurn g κ * -FRC.Shell.Frame.quarterTurn g κ * -FRC.Shell.Frame.quarterTurn g κ)))) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, -FRC.Shell.Frame.quarterTurn g κ = g ^ κ :=94  @FRC.Ledger.p0603695/-- 6:E8 (p06050) — Cardinal exclusivity: the conjugate $\Ft^{[s]}\sigma\Ft^{[s]\,-1}$ of \eqref{eq:conj-expansion} is not monomial for every $s\notin\{0,\kap,2\kap,3\kap\}$ --- off $j\in\{-1,0,1\}$ its row $0$ is $x^{-1}$ times a quadratic in $x=\gen^{j}$ with leading coefficient $\im\,[c_0(s)+c_2(s)]\,c_3(-s)\neq0$, $c_0(s)+c_2(s)=\tfrac12(1+\gen^{-2s})$, so the row vanishes at no three distinct indices off the sites and, by counting, has at least $4\kap-5$ nonzero entries; the count checked on every shell below $200$. -/96theorem p06050 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ (s : Nat) {j : Nat}, j < p - (1 : Nat) → j ≠ (0 : Nat) → j ≠ (1 : Nat) → j ≠ p - (1 : Nat) - (1 : Nat) → FRC.Shell.Frame.mmul (FRC.Shell.Frame.mmul (FRC.Shell.Frame.frft g κ z s) (FRC.Shell.Frame.shift p) (p - (1 : Nat))) (FRC.Shell.Frame.frft g κ z (p - (1 : Nat) - s)) (p - (1 : Nat)) (0 : Nat) j = (FRC.Shell.Frame.NF0 (-FRC.Shell.ofNat κ) (-FRC.Shell.Frame.quarterTurn g κ) (z ^ s) + FRC.Shell.Frame.NF2 (-FRC.Shell.ofNat κ) (-FRC.Shell.Frame.quarterTurn g κ) (z ^ s)) * (FRC.Shell.Frame.NF1 (-FRC.Shell.ofNat κ) (-FRC.Shell.Frame.quarterTurn g κ) (z ^ (p - (1 : Nat) - s)) * FRC.Shell.Frame.quarterTurn g κ * z ^ j + FRC.Shell.Frame.NF3 (-FRC.Shell.ofNat κ) (-FRC.Shell.Frame.quarterTurn g κ) (z ^ (p - (1 : Nat) - s)) * FRC.Shell.Frame.quarterTurn g κ * g ^ j) + (FRC.Shell.Frame.NF1 (-FRC.Shell.ofNat κ) (-FRC.Shell.Frame.quarterTurn g κ) (z ^ s) + FRC.Shell.Frame.NF3 (-FRC.Shell.ofNat κ) (-FRC.Shell.Frame.quarterTurn g κ) (z ^ s)) * FRC.Shell.Frame.quarterTurn g κ * (FRC.Shell.Frame.NF0 (-FRC.Shell.ofNat κ) (-FRC.Shell.Frame.quarterTurn g κ) (z ^ (p - (1 : Nat) - s)) + FRC.Shell.Frame.NF2 (-FRC.Shell.ofNat κ) (-FRC.Shell.Frame.quarterTurn g κ) (z ^ (p - (1 : Nat) - s)))) ∧ (∀ {p : Nat} [FRC.Pos p] (q jj u : FRC.Shell p), FRC.Shell.Frame.NF0 q jj u + FRC.Shell.Frame.NF2 q jj u = (q + q) * ((1 : FRC.Shell p) + u * u)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ {s : Nat}, s < p - (1 : Nat) → s ≠ κ → s ≠ (3 : Nat) * κ → FRC.Shell.Frame.NF0 (-FRC.Shell.ofNat κ) (-FRC.Shell.Frame.quarterTurn g κ) (z ^ s) + FRC.Shell.Frame.NF2 (-FRC.Shell.ofNat κ) (-FRC.Shell.Frame.quarterTurn g κ) (z ^ s) ≠ (0 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ {s : Nat}, s < p - (1 : Nat) → s ≠ (0 : Nat) → s ≠ κ → s ≠ (2 : Nat) * κ → s ≠ (3 : Nat) * κ → FRC.Shell.Frame.NF3 (-FRC.Shell.ofNat κ) (-FRC.Shell.Frame.quarterTurn g κ) (z ^ (p - (1 : Nat) - s)) ≠ (0 : FRC.Shell p)) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ {s : Nat}, s < p - (1 : Nat) → s ≠ (0 : Nat) → s ≠ κ → s ≠ (2 : Nat) * κ → s ≠ (3 : Nat) * κ → ∀ {j1 j2 j3 : Nat}, j1 < p - (1 : Nat) → j2 < p - (1 : Nat) → j3 < p - (1 : Nat) → j1 ≠ (0 : Nat) ∧ j1 ≠ (1 : Nat) ∧ j1 ≠ p - (1 : Nat) - (1 : Nat) → j2 ≠ (0 : Nat) ∧ j2 ≠ (1 : Nat) ∧ j2 ≠ p - (1 : Nat) - (1 : Nat) → j3 ≠ (0 : Nat) ∧ j3 ≠ (1 : Nat) ∧ j3 ≠ p - (1 : Nat) - (1 : Nat) → j1 ≠ j2 → j1 ≠ j3 → j2 ≠ j3 → ¬(FRC.Shell.Frame.mmul (FRC.Shell.Frame.mmul (FRC.Shell.Frame.frft g κ z s) (FRC.Shell.Frame.shift p) (p - (1 : Nat))) (FRC.Shell.Frame.frft g κ z (p - (1 : Nat) - s)) (p - (1 : Nat)) (0 : Nat) j1 = (0 : FRC.Shell p) ∧ FRC.Shell.Frame.mmul (FRC.Shell.Frame.mmul (FRC.Shell.Frame.frft g κ z s) (FRC.Shell.Frame.shift p) (p - (1 : Nat))) (FRC.Shell.Frame.frft g κ z (p - (1 : Nat) - s)) (p - (1 : Nat)) (0 : Nat) j2 = (0 : FRC.Shell p) ∧ FRC.Shell.Frame.mmul (FRC.Shell.Frame.mmul (FRC.Shell.Frame.frft g κ z s) (FRC.Shell.Frame.shift p) (p - (1 : Nat))) (FRC.Shell.Frame.frft g κ z (p - (1 : Nat) - s)) (p - (1 : Nat)) (0 : Nat) j3 = (0 : FRC.Shell p)) :=97  @FRC.Ledger.p0605098/-- 6:E9 (p06054) — The spectra behind E5: every nonzero residue $b$ is an eigenvalue of $\sigma$, with the geometric eigenvector $(b^{-j})_j$ (so $\sigma$ is diagonalizable over $\Fp$ with the $4\kap$ simple eigenvalues $\Fpx$, the Mathlib reading); an eigenvalue of $\Ft^{[s]}=\sum_\ell\gen^{-\ell s}\Pi_\ell$ is one of the four $\gen^{-\ell s}$ ($\Ft^{[1]}$ on the six shells). -/99theorem p06054 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {b : FRC.Shell p}, b ≠ (0 : FRC.Shell p) → ∃ y, b * y = (1 : FRC.Shell p) ∧ FRC.Shell.Frame.IsEigen (FRC.Shell.Frame.shift p) (p - (1 : Nat)) b fun j => y ^ j) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (z : FRC.Shell p) (s : Nat) {lam : FRC.Shell p} {v : Nat → FRC.Shell p}, FRC.Shell.Frame.IsEigen (FRC.Shell.Frame.frft g κ z s) (p - (1 : Nat)) lam v → ∃ ℓ, ℓ < (4 : Nat) ∧ lam = (z ^ s) ^ ℓ :=100  @FRC.Ledger.p06054101/-- 6:E10 (p06056) — The plane as orbits of the cycle: $R_s$ scales $u=x+\im y$ by $z_s$ and $v=x-\im y$ by $z_s^{-1}$, so every point off the origin has a free orbit of size $4\kap=|SO(2,\Fp)|$, and $\p^{2}=1+(4\kap+2)\,4\kap$ is the count of the origin and $4\kap+2$ orbits (the $4\kap$ circles of nonzero norm and the two isotropic lines, by counting); $\dim\Vt=4\kap$. -/102theorem p06056 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (z : FRC.Shell p) (s : Nat) (x y : FRC.Shell p), FRC.Shell.Frame.cs g κ z s * x + -(FRC.Shell.Frame.ds g κ z s * y) + FRC.Shell.Frame.quarterTurn g κ * (FRC.Shell.Frame.ds g κ z s * x + FRC.Shell.Frame.cs g κ z s * y) = z ^ s * (x + FRC.Shell.Frame.quarterTurn g κ * y) ∧ FRC.Shell.Frame.cs g κ z s * x + -(FRC.Shell.Frame.ds g κ z s * y) + -(FRC.Shell.Frame.quarterTurn g κ * (FRC.Shell.Frame.ds g κ z s * x + FRC.Shell.Frame.cs g κ z s * y)) = g ^ s * (x + -(FRC.Shell.Frame.quarterTurn g κ * y))) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {z : FRC.Shell p}, g * z = (1 : FRC.Shell p) → ∀ {x y : FRC.Shell p}, ¬(x = (0 : FRC.Shell p) ∧ y = (0 : FRC.Shell p)) → ∀ {s : Nat}, s < p - (1 : Nat) → FRC.Shell.Frame.cs g κ z s * x + -(FRC.Shell.Frame.ds g κ z s * y) = x ∧ FRC.Shell.Frame.ds g κ z s * x + FRC.Shell.Frame.cs g κ z s * y = y → s = (0 : Nat)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → p * p = (1 : Nat) + ((4 : Nat) * κ + (2 : Nat)) * ((4 : Nat) * κ)) ∧ FRC.Shell.Frame.countCircle (5 : Nat) (5 : Nat) = (4 : Nat) ∧ FRC.Shell.Frame.countCircle (13 : Nat) (13 : Nat) = (12 : Nat) ∧ FRC.Shell.Frame.countCircle (17 : Nat) (17 : Nat) = (16 : Nat) ∧ FRC.Shell.Frame.countCircle (29 : Nat) (29 : Nat) = (28 : Nat) ∧ FRC.Shell.Frame.countCircle (37 : Nat) (37 : Nat) = (36 : Nat) ∧ FRC.Shell.Frame.countCircle (41 : Nat) (41 : Nat) = (40 : Nat) :=103  @FRC.Ledger.p06056104-- end ledger predicates105106end FRC.Fourier107