Keys/Fourier.lean — FrcCore

1import FrcCore.Transform2import FrcCore.Meridian3import FrcCore.Theme.Fourier4import FrcCore.Theme.Fractional5import FrcCore.Theme.Lifts6import FrcCore.Theme.Dichotomy7import FrcCore.Theme.Rotations8import FrcCore.Theme.Heisenberg9import FrcCore.Theme.Spectra10import FrcCore.Theme.Exclusivity1112/-!13# FrcCore.Keys.Fourier — the keyed theorems of the fourier theme (ledger migration, task LM19)1415One declaration per key, `FRC.Ledger.p<key>`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem16that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration17`FRC.<Module>.p<key>` as an alias. Every declaration has no axioms (`check_core_axioms.py`).18-/1920namespace FRC.Ledger2122-- Keys of the fourier theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file)23/-- p00022 — 00:C2. Scale-shift duality: dilation $x\mapsto gx$ is phase evolution of the frame, advancing $t$; over the cycle it is the fractional Fourier transform, whose quarter-turn $Q_4$ is the discrete Fourier transform. -/24theorem p00022 : (∀ {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) → (∀ (m r : Nat), List.map (g.scale r) (g.meridian κ m) = g.meridian κ (m + r)) ∧ (∀ (r : Nat) (x : FRC.Shell p), g.scale (r + (p - (1 : Nat))) x = g.scale r x) ∧ (∀ (s r 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))) ∧ (∀ (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) ∧ (∀ (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) ∧ (∀ (k j : Nat), k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.sumRange (fun l => FRC.Shell.Frame.FJ g κ k l * FRC.Shell.Frame.Fmat g κ l j) (p - (1 : Nat)) = FRC.Shell.Frame.idm k j) ∧ ∀ (k j : Nat), k < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Shell.Frame.mpow (FRC.Shell.Frame.frft g κ z (1 : Nat)) κ k j = FRC.Shell.Frame.Fmat 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 s' : Nat}, g ^ s = g ^ s' → ∀ (k j : Nat), FRC.Shell.Frame.frft g κ z s 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 → ∀ (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)) ∧ (∀ {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) ∧ (∀ {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) :=25  And.intro @FRC.Shell.Frame.scale_shift (And.intro @FRC.Shell.Frame.frft_dilation (And.intro @FRC.Shell.Frame.W_sq' (And.intro @FRC.Shell.Frame.F_sq (And.intro @FRC.Shell.Frame.J_sq (And.intro @FRC.Shell.Frame.frft_add (And.intro @FRC.Shell.Frame.frft_cardinal (And.intro @FRC.Shell.Frame.frft_period (And.intro @FRC.Shell.Frame.frft_pow (And.intro @FRC.Shell.meridian_scale (And.intro @FRC.Shell.meridian_step (And.intro @FRC.Shell.scale_periodic (@FRC.Shell.ladder13))))))))))))26/-- p00189 — 00:C7. \textbf{Orientation is derived, not conventional}: the $c$-square congruence ($\dS$ even, C8) annihilates orientation transport on every Carrier carrying it ($\im^{\dS}\in\{\pm1\}$); the oriented quarter-turn $\im=-\gen^\kap $ is a selection, read by pullback covariance and count positivity; the joint flip $(\gen,\im,s)\mapsto(\gen^{-1},-\im,-s)$ permutes the registration channels. The constants' derivation consumes no selection (B7). Parity marker: C14. The selection by matter content: D16. -/27theorem p00189 : (∀ {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.Pos Ω] (h : FRC.Shell Ω) (S : Nat), h * h = (-1 : FRC.Shell Ω) → S % (2 : Nat) = (0 : Nat) → h ^ S = (1 : FRC.Shell Ω) ∨ h ^ S = (-1 : FRC.Shell Ω)) ∧ z ^ κ = FRC.Shell.Frame.quarterTurn g κ ∧ FRC.Shell.Frame p κ z ∧ FRC.Shell.Frame.quarterTurn z κ = -FRC.Shell.Frame.quarterTurn g κ ∧ (∀ (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) ∧ ∀ (ℓ 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) ∧ (∀ {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 :=28  And.intro @FRC.Shell.Frame.orientation (And.intro @FRC.Shell.Frame.inv_frame (And.intro @FRC.Shell.Frame.Fmat_conj (@FRC.Shell.Frame.proj_conj)))29/-- p06013 — 6:B6. 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$. -/30theorem 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 κ :=31  And.intro @FRC.Shell.Frame.ofNat_n (And.intro @FRC.Shell.Frame.sqrt_neg_one (@FRC.Shell.Frame.scaled_W_sq_iff))32/-- p06016 — 6:C2. $\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$. -/33theorem 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 :=34  And.intro @FRC.Shell.Frame.proj_mul_self (And.intro @FRC.Shell.Frame.proj_mul_ne (And.intro @FRC.Shell.Frame.sum_proj (@FRC.Shell.Frame.Fmat_proj)))35/-- p06017 — 6:C3. 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$. -/36theorem 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 :=37  And.intro @FRC.Shell.Frame.frft_add (And.intro @FRC.Shell.Frame.frft_cardinal (And.intro @FRC.Shell.Frame.frft_period (@FRC.Shell.Frame.frft_pow)))38/-- p06018 — 6:C4. 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. -/39theorem 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 :=40  And.intro @FRC.Shell.Frame.frft_injective (And.intro @FRC.Shell.Frame.five_frames (And.intro @FRC.Shell.Frame.five_faithful (@FRC.Shell.Frame.five_odd_proj)))41/-- p06019 — 6:C5. 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. -/42theorem 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 :=43  And.intro @FRC.Shell.Frame.proj_even_sum (And.intro @FRC.Shell.Frame.proj_odd_sum (And.intro @FRC.Shell.Frame.half (And.intro @FRC.Shell.Frame.even_proj_ne_zero (And.intro @FRC.Shell.Frame.odd_proj_ne_zero (And.intro @FRC.Shell.Frame.five_frames (@FRC.Shell.Frame.five_odd_proj))))))44/-- p06020 — 6:C6. The projectors are chart data: for $u$ odd and a unit mod $4\kap$ the index 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$. -/45theorem 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)) :=46  And.intro @FRC.Shell.Frame.Fmat_chart (@FRC.Shell.Frame.thirteen_tuples)47/-- p06021 — 6:C7. 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$. -/48theorem 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)) :=49  And.intro @FRC.Shell.Frame.trace_powers (And.intro @FRC.Shell.Frame.trace_proj (And.intro @FRC.Shell.Frame.gauss_mul (And.intro @FRC.Shell.Frame.gauss_conj (And.intro @FRC.Shell.Frame.trace_tuples (And.intro @FRC.Shell.Frame.six_signs (@FRC.Shell.Frame.six_tuples))))))50/-- p06022 — 6:C8. 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}$. -/51theorem 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 :=52  And.intro @FRC.Shell.Frame.lift_add (And.intro @FRC.Shell.Frame.lift_cardinal (@FRC.Shell.Frame.lift_pow))53/-- p06023 — 6:C9. The conjugate chart $(\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. -/54theorem 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 :=55  And.intro @FRC.Shell.Frame.inv_frame (And.intro @FRC.Shell.Frame.Fmat_conj (@FRC.Shell.Frame.proj_conj))56/-- p06024 — 6:D1. The meridional 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. -/57theorem 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 :=58  @FRC.Shell.Frame.frft_inverse59/-- p06025 — 6:D2. 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. -/60theorem 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) :=61  And.intro @FRC.Shell.Frame.frft_injective (And.intro @FRC.Shell.Frame.five_frames (And.intro @FRC.Shell.Frame.five_faithful (@FRC.Shell.Frame.frft_half_turn)))62/-- p06031 — 6:E2. $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 phase cycle. -/63theorem 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) :=64  And.intro @FRC.Shell.Frame.rot_circle (And.intro @FRC.Shell.Frame.rot_hom (And.intro @FRC.Shell.Frame.rot_inj (And.intro @FRC.Shell.Frame.rot_surj (@FRC.Shell.Frame.six_circles))))65/-- p06032 — 6:E3. 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). -/66theorem 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 κ :=67  @FRC.Shell.Frame.rot_cardinal68/-- p06034 — 6:E5. 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. -/69theorem 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 :=70  @FRC.Shell.Frame.spectral_obstruction71/-- p06035 — 6:E6. 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}$. -/72theorem 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 κ :=73  And.intro @FRC.Shell.Frame.frft_proj (And.intro @FRC.Shell.Frame.frft_intertwine (@FRC.Shell.Frame.rot_eigenline))74/-- p06036 — 6:E7. 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}$. -/75theorem 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 ^ κ :=76  And.intro @FRC.Shell.Frame.shift_inverse (And.intro @FRC.Shell.Frame.heisenberg (And.intro @FRC.Shell.Frame.frft_eq (And.intro @FRC.Shell.Frame.frft_coeff (@FRC.Shell.Frame.w_eq_pow_kappa))))77/-- p06050 — 6:E8. 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 those three and, by counting, has at least $4\kap-5$ nonzero entries; the count checked on every shell below $200$. -/78theorem 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)) :=79  And.intro @FRC.Shell.Frame.row_entry (And.intro @FRC.Shell.Frame.even_coeff_id (And.intro @FRC.Shell.Frame.even_coeff_ne_zero (And.intro @FRC.Shell.Frame.odd_coeff_ne_zero (@FRC.Shell.Frame.exclusivity))))80/-- p06052 — 6:C11. Charts outside the classified lifts: for $u$ a unit mod $4\kap$, $\Wt(\gen^{u})=\Wt P_u$ with $P_u$ the index 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. -/81theorem 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)) :=82  And.intro @FRC.Shell.Frame.W_chart (And.intro @FRC.Shell.Frame.W_mul_chart (And.intro @FRC.Shell.Frame.chart_mul_W (@FRC.Shell.Frame.chart_noncommute)))83/-- p06053 — 6:D7. The cycle carries exactly $2\kap$ unordered bases: every entry $(0,k)$, $k\neq0$, 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}. -/84theorem 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) :=85  And.intro @FRC.Shell.Frame.frft_row_zero (@FRC.Shell.Frame.frft_row_zero_ne_zero)86/-- p06054 — 6:E9. 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). -/87theorem 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) ^ ℓ :=88  And.intro @FRC.Shell.Frame.shift_eigen (@FRC.Shell.Frame.frft_eigen)89/-- p06056 — 6:E10. 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$. -/90theorem 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) :=91  And.intro @FRC.Shell.Frame.rot_uv (And.intro @FRC.Shell.Frame.orbit_free (And.intro @FRC.Shell.Frame.plane_count (@FRC.Shell.Frame.six_circles)))92-- end keys9394end FRC.Ledger95