import FrcCore.FrameCore
import FrcCore.Transform
import FrcCore.Theme.Quadratic
import FrcCore.Theme.Extension
import FrcCore.Theme.Drive
import FrcCore.Theme.Horizon
import FrcCore.Theme.Ladder

/-!
# FrcCore.Keys.Horizon — the keyed theorems of the horizon theme (ledger migration, task LM19)

One declaration per key, `FRC.Ledger.p<key>`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem
that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration
`FRC.<Module>.p<key>` as an alias. Every declaration has no axioms (`check_core_axioms.py`).
-/

namespace FRC.Ledger

-- Keys of the horizon theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file)
/-- p20008 — 20:B1. The two frames on one substrate: the Carrier chart $\F_\Omega$, held by no embedded observer, and the Subject $\Fp$ embedded with $\Omega\gg \p^{2}$; what they share is the quarter-turn core $Q_4$ and nothing else, on the laboratory pair $(13,233)$ the cycles $C_{12}$ and $C_{232}$ admit no projection ($12\nmid232$); hardness by register ($\p$-hard, $\Omega$-hard). -/
theorem p20008 : (13 : Nat) * (13 : Nat) < (233 : Nat) ∧ (12 : Nat) % (4 : Nat) = (0 : Nat) ∧ (232 : Nat) % (4 : Nat) = (0 : Nat) ∧ (232 : Nat) % (3 : Nat) ≠ (0 : Nat) ∧ (5 : FRC.Shell (13 : Nat)) * (5 : FRC.Shell (13 : Nat)) = (-1 : FRC.Shell (13 : Nat)) ∧ (89 : FRC.Shell (233 : Nat)) * (89 : FRC.Shell (233 : Nat)) = (-1 : FRC.Shell (233 : Nat)) ∧ (232 : Nat) % (12 : Nat) ≠ (0 : Nat) ∧ (3 : Nat) * (3 : Nat) < (13 : Nat) ∧ (3 : Nat) * (3 : Nat) < (233 : Nat) :=
  @FRC.Horizon.lab_pair
set_option linter.defProp false in
/-- p20009 — 20:B2. Frame coincidence below the horizon: for $n\le\sqrt \p$ the residue $n$ is the same integer in $\Fp$ and $\F_\Omega$, and primality of $n$ equals irreducibility in the Subject chart; the Subject-realised primes $\Pi_\p$ are the primes to $\sqrt \p$. -/
def p20009 := And.intro @FRC.Horizon.window_readback (And.intro @FRC.Horizon.factorisation_iff (@FRC.Horizon.frame_coincidence))
/-- p20011 — 20:B4. Zero-slot: $Z_\Omega(k)=\sum_{x\in\Fx{\Omega}}x^{k}$ vanishes on every nonterminal exponent $1\le k\le\Omega-2$ and equals $-1$ on the full cycle; the nonterminal slots are the universal mode basis. -/
theorem p20011 : ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → (∀ (k : Nat), (0 : Nat) < k → k < p - (1 : Nat) → FRC.Shell.sumRange (fun l => FRC.Shell.ofNat (l + (1 : Nat)) ^ k) (p - (1 : Nat)) = (0 : FRC.Shell p)) ∧ FRC.Shell.sumRange (fun l => FRC.Shell.ofNat (l + (1 : Nat)) ^ (p - (1 : Nat))) (p - (1 : Nat)) = (-1 : FRC.Shell p) :=
  @FRC.Horizon.zero_slot
/-- p20012 — 20:B5. Slot complementarity: $\Phi(k)=-\gen^{\,k}$ bijects the nontrivial spectral slots onto the nonterminal additive slots $\Fx{\Omega}\setminus\{-1\}$, the two removed points being $\mu_2$, the intertwiner the half-cycle element. -/
theorem p20012 : ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → (∀ (i j : Nat), i < p - (1 : Nat) → j < p - (1 : Nat) → -g ^ i = -g ^ j → i = j) ∧ (∀ (k : Nat), (0 : Nat) < k → k < p - (1 : Nat) → -g ^ k ≠ (0 : FRC.Shell p) ∧ -g ^ k ≠ (-1 : FRC.Shell p)) ∧ ∀ (y : FRC.Shell p), y ≠ (0 : FRC.Shell p) → y ≠ (-1 : FRC.Shell p) → ∃ k, (0 : Nat) < k ∧ k < p - (1 : Nat) ∧ -g ^ k = y :=
  @FRC.Horizon.slot_complementarity
set_option linter.defProp false in
/-- p20013 — 20:B6. Hermitian phase calculus on $K=\F_{\p^{2}}$: norm and trace $\Fp$-valued, the phase circle $U_{\p+1}$ of order $\p+1$ with Frobenius as inversion, the quarter-turn $\im$ Frobenius-fixed and off the circle ($\Nm(\im)=-1$), the trace-zero $\eta$ with $\eta^{2}=\nu$ a nonsquare, $\Tr(a+b\eta)=2a$, $\Nm=a^{2}-\nu b^{2}$. -/
def p20013 := And.intro @FRC.Extension.Ext.mul_conj (And.intro @FRC.Extension.Ext.conj_inv_of_norm_one (And.intro @FRC.Horizon.quarter_turn_off_circle (@FRC.Horizon.circle13)))
/-- p20014 — 20:B7. Flat ground state: the full-modulus Ramanujan sum $c_\p(n)\equiv-1$ for every $n\not\equiv0$; the mode at the spectral origin carries no prime information. -/
theorem p20014 : (∀ {q : Nat} [FRC.Pos q] {κ' : Nat} {h : FRC.Shell q}, FRC.Shell.Frame q κ' h → ∀ {m : Nat}, (0 : Nat) < m → ∀ {ω : FRC.Shell q}, ω.IsPrimitive m → ∀ (n : Nat), n % m ≠ (0 : Nat) → FRC.Shell.sumRange (fun a => ω ^ (n * (a + (1 : Nat)))) (m - (1 : Nat)) = (-1 : FRC.Shell q)) ∧ (∀ (n : Nat), n < (13 : Nat) → (0 : Nat) < n → FRC.Shell.sumRange (fun a => (16 : FRC.Shell (53 : Nat)) ^ (n * (a + (1 : Nat)))) (12 : Nat) = (-1 : FRC.Shell (53 : Nat))) ∧ FRC.Shell.sumRange (fun a => (16 : FRC.Shell (53 : Nat)) ^ ((0 : Nat) * (a + (1 : Nat)))) (12 : Nat) = (12 : FRC.Shell (53 : Nat)) :=
  And.intro @FRC.Horizon.ramanujan_sum (@FRC.Horizon.ramanujan53)
set_option linter.defProp false in
/-- p20015 — 20:B8. The finite critical line: the half-turn $2^{-1}=2\kp+1=-\pi$; $\Tr(z)=1$ exactly on the $\p$ points $z=2^{-1}+\eta\theta$, with energy $\Nm(z)=\tfrac14-\nu\theta^{2}$; de-framed, $2^{-1}/\p=(2\kp+1)/\p\to\half$ from above [chart]. -/
def p20015 := And.intro @FRC.Horizon.half_inverse (And.intro @FRC.Horizon.critical_line (@FRC.Horizon.norm_on_line))
set_option linter.defProp false in
/-- p20016 — 20:B9. The two agreement loci: the Klein four-group $\langle\phi,\rho\rangle$ of Frobenius and the functional-equation half-turn fixes exactly $\Fp$ (the prime meridian), $L_{1/2}$ (the critical line) and their meeting $\{2^{-1}\}$; no other line is fixed. -/
def p20016 := And.intro @FRC.Horizon.klein_four (And.intro @FRC.Extension.Ext.fixed_conj (And.intro @FRC.Horizon.critical_line (@FRC.Horizon.fixed_half_turn)))
/-- p20017 — 20:B10. The Subject constants on the shell: $\pi=2\kp$, $2\pi\equiv-1$, $\im=\gen^{-\kp}$, $\im^{2}\equiv-1$, $\E=\gen^{\,\im}$ on the odd lift, $\gen^{\,\pi}\equiv-1$, $\E^{\,\im\pi}\equiv-1$; on $\F_{13}$: $\gen=2$, $\im=5$, $\E=6$, $\pi=6$. -/
theorem p20017 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → FRC.Shell.ofNat ((2 : Nat) * FRC.Shell.Frame.halfPeriod κ) = (-1 : FRC.Shell p) ∧ g ^ ((3 : Nat) * κ) = FRC.Shell.Frame.quarterTurn g κ ∧ FRC.Shell.Frame.quarterTurn g κ * FRC.Shell.Frame.quarterTurn g κ = (-1 : FRC.Shell p) ∧ g ^ ((2 : Nat) * κ) = (-1 : FRC.Shell p) ∧ ∀ (m : Nat), m % (2 : Nat) = (1 : Nat) → (g ^ m) ^ (m * ((2 : Nat) * κ)) = (-1 : FRC.Shell p)) ∧ ((2 : FRC.Shell (13 : Nat)) * (6 : FRC.Shell (13 : Nat)) = (-1 : FRC.Shell (13 : Nat)) ∧ (2 : FRC.Shell (13 : Nat)) ^ (9 : Nat) = (5 : FRC.Shell (13 : Nat)) ∧ FRC.Shell.Frame.quarterTurn (2 : FRC.Shell (13 : Nat)) (3 : Nat) = (5 : FRC.Shell (13 : Nat)) ∧ (5 : FRC.Shell (13 : Nat)) * (5 : FRC.Shell (13 : Nat)) = (-1 : FRC.Shell (13 : Nat)) ∧ (2 : FRC.Shell (13 : Nat)) ^ (5 : Nat) = (6 : FRC.Shell (13 : Nat)) ∧ (2 : FRC.Shell (13 : Nat)) ^ (6 : Nat) = (-1 : FRC.Shell (13 : Nat)) ∧ (6 : FRC.Shell (13 : Nat)) ^ ((5 : Nat) * (6 : Nat)) = (-1 : FRC.Shell (13 : Nat))) ∧ FRC.Shell.Frame (13 : Nat) (3 : Nat) (2 : FRC.Shell (13 : Nat)) :=
  And.intro @FRC.Horizon.subject_constants (And.intro @FRC.Horizon.constants13 (@FRC.Shell.frame13))
/-- p20029 — 20:D5. The cells: the heights of a Carrier's cycle are its residues, residue $y$ the cell from $2\pi y$ to $2\pi(y+1)$; a cell is clean when its zeros lie on the line, which Turing's count decides from the labels below $\sqrt{y+1}$, and passes when the frame's reading certifies it. The hypothesis of the Carrier: every residue has a clean cell. -/
theorem p20029 : (∀ {α : Type} (fixed : α → Bool) (l : List α), (∀ (z : α), z ∈ l → fixed z = true) ↔ FRC.Horizon.fixedCount fixed l = l.length) ∧ ∀ (c n : Nat → Nat) (m : Nat), (∀ (y : Nat), y < m → c y ≤ n y) → ((∀ (y : Nat), y < m → c y = n y) ↔ FRC.Shell.Frame.sumTo c m = FRC.Shell.Frame.sumTo n m) :=
  And.intro @FRC.Horizon.clean_iff_count (@FRC.Horizon.cells_clean_iff_cycle)
/-- p20032 — 20:E1. The scale-evolution generator: on the shell the scale-shift $x\mapsto\gen^{\,r}x$ is a unitary permutation of $\Fx{\p}$ with the complex characters as eigenvectors; in the analytic chart [chart] the dilation group $U_r=e^{ir\Hh}$ has the self-adjoint generator $\Hh=-i(x\partial_x+\half)$ with generalised eigenfunctions $x^{-\bar\rho}$, $\rho=\half+i\gamma$, the symmetrizing $\half$ the half-turn of B8; the chart assignment is used nowhere as a shell identity. -/
theorem p20032 : (∀ {p : Nat} [FRC.Pos p] {g : FRC.Shell p} (r k : Nat) (x : FRC.Shell p), (g ^ r * x) ^ k = (g ^ r) ^ k * x ^ k) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (r : Nat), FRC.Shell.Frame.natCount (fun x => x ≠ (0 : Nat) ∧ g ^ r * FRC.Shell.ofNat x = FRC.Shell.ofNat x) p = if r % (p - (1 : Nat)) = (0 : Nat) then p - (1 : Nat) else (0 : Nat) :=
  And.intro @FRC.Horizon.shift_power_character (@FRC.Horizon.shift_trace)
/-- p20043 — 20:E12, 00:Z10. On every shell $\F_\p\subset\F_{\p^2}$, with no hypothesis, the prime vector's spectral content is the constant mode and the nonterminal quarter-turn modes, the finite zeta vanishing on each (20:E12, 20:B4). Every mode of every vector lies on the self-dual line $\Tr=1$, an eigenvector of the scale-shift with a $(\p-1)$-th root of unity as eigenvalue: no off-line mode, $\Om$-blind. -/
theorem p20043 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → (∀ (k : Nat), (0 : Nat) < k → k < p - (1 : Nat) → FRC.Shell.sumRange (fun l => FRC.Shell.ofNat (l + (1 : Nat)) ^ k) (p - (1 : Nat)) = (0 : FRC.Shell p)) ∧ FRC.Shell.sumRange (fun l => FRC.Shell.ofNat (l + (1 : Nat)) ^ (p - (1 : Nat))) (p - (1 : Nat)) = (-1 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (v : Nat → FRC.Shell p) {j : Nat}, j < p - (1 : Nat) → v j = FRC.Shell.sumRange (fun k => FRC.Horizon.modeCoeff g v k * (g ^ j) ^ k) (p - (1 : Nat))) ∧ (∀ {p : Nat} [FRC.Pos p] {g : FRC.Shell p} (r k : Nat) (x : FRC.Shell p), (g ^ r * x) ^ k = (g ^ r) ^ k * x ^ k) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (r k : Nat), ((g ^ r) ^ k) ^ (p - (1 : Nat)) = (1 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (r : Nat), FRC.Shell.Frame.natCount (fun x => x ≠ (0 : Nat) ∧ g ^ r * FRC.Shell.ofNat x = FRC.Shell.ofNat x) p = if r % (p - (1 : Nat)) = (0 : Nat) then p - (1 : Nat) else (0 : Nat)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (ν θ : FRC.Shell p), (FRC.Horizon.readout ν κ θ).trace = (1 : FRC.Shell p) ∧ (FRC.Horizon.readout ν κ θ).re = FRC.Shell.ofNat ((2 : Nat) * κ + (1 : Nat)) ∧ ∀ (θ' : FRC.Shell p), FRC.Horizon.readout ν κ θ = FRC.Horizon.readout ν κ θ' → θ = θ') ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (k : Nat), (1 : Nat) ≤ k → k ≤ p - (2 : Nat) → -g ^ k ≠ (0 : FRC.Shell p) ∧ -g ^ k ≠ (-1 : FRC.Shell p) :=
  And.intro @FRC.Horizon.zero_slot (And.intro @FRC.Horizon.mode_expansion (And.intro @FRC.Horizon.shift_power_character (And.intro @FRC.Horizon.eigenphase (And.intro @FRC.Horizon.shift_trace (And.intro @FRC.Horizon.readout_on_line (@FRC.Horizon.readout_slot_index))))))
/-- p20047 — 20:F1. \textbf{Turing's count on the shell.} On every cell $C_y\le N^{\mathrm{crit}}_y\le\mathcal N_y$ (A7); the cell is clean when $\mathcal N_y=N^{\mathrm{crit}}_y$, and $C_y=\mathcal N_y$ certifies it, every zero simple. The shell estimates $\mathcal N$ by the comb count (Appendix~\ref{app:comb}; uncertified) and reads $C$ from the main sum's sign changes (A10), zeros on the line. An off-line zero is a phantom, $\mathcal N_y-N^{\mathrm{crit}}_y>0$. -/
theorem p20047 : (∀ {α : Type} (sc onLine : α → Bool) (l : List α), (∀ (z : α), z ∈ l → sc z = true → onLine z = true) → FRC.Horizon.fixedCount sc l ≤ FRC.Horizon.fixedCount onLine l ∧ FRC.Horizon.fixedCount onLine l ≤ l.length) ∧ (∀ {α : Type} (sc onLine : α → Bool) (l : List α), (∀ (z : α), z ∈ l → sc z = true → onLine z = true) → FRC.Horizon.fixedCount sc l = l.length → ∀ (z : α), z ∈ l → onLine z = true ∧ sc z = true) ∧ ∀ {α : Type} (onLine : α → Bool) (l : List α), (∃ z, z ∈ l ∧ onLine z = false) → FRC.Horizon.fixedCount onLine l < l.length :=
  And.intro @FRC.Horizon.turing_chain (And.intro @FRC.Horizon.turing_equal (@FRC.Horizon.turing_phantom))
set_option linter.defProp false in
/-- p20079 — 20:F7. \textbf{The closure of the heights.} A height is a residue on the cycle of the shell that reads it, the largest shell is the Carrier's and there is no height beyond its cycle (A2); no embedded Subject reads the cycle whole (A4). The hypothesis of the Carrier is a statement about the residues of its cycle, one clause per residue. -/
def p20079 := And.intro @FRC.Horizon.closure (@FRC.Horizon.closure_lab)
/-- p20081 — 20:F2. \textbf{The hypothesis on a hosted Carrier.} A cell is decided by the certificate of a shell reading it, an embedded Subject below the largest one, the host above; on the laboratory Carriers $233$, $30\,089$ and $2\,408\,561$ every cell of the cycle is clean, $1\,038$, $280\,186$ and $32\,984\,135$ zeros, all simple; the classical verification cleans every cell below $4.8\times10^{11}$ (A9). -/
theorem p20081 : ((3 : Nat) * (3 : Nat) < (13 : Nat) ∧ (13 : Nat) < (5 : Nat) * (5 : Nat) ∧ (13 : Nat) % (4 : Nat) = (1 : Nat) ∧ FRC.Nat.isPrime (3 : Nat) ∧ FRC.Nat.isPrime (5 : Nat) ∧ FRC.Nat.isPrime (13 : Nat) ∧ ∀ (q : Nat), q < (5 : Nat) → (3 : Nat) < q → ¬FRC.Nat.isPrime q) ∧ ((13 : Nat) * (13 : Nat) < (233 : Nat) ∧ (233 : Nat) < (17 : Nat) * (17 : Nat) ∧ (233 : Nat) % (4 : Nat) = (1 : Nat) ∧ FRC.Nat.isPrime (13 : Nat) ∧ FRC.Nat.isPrime (17 : Nat) ∧ FRC.Nat.isPrime (233 : Nat) ∧ ∀ (q : Nat), q < (17 : Nat) → (13 : Nat) < q → ¬FRC.Nat.isPrime q) ∧ ((173 : Nat) * (173 : Nat) < (30089 : Nat) ∧ (30089 : Nat) < (179 : Nat) * (179 : Nat) ∧ (30089 : Nat) % (4 : Nat) = (1 : Nat) ∧ FRC.Nat.isPrime (173 : Nat) ∧ FRC.Nat.isPrime (179 : Nat) ∧ FRC.Nat.isPrime (30089 : Nat) ∧ ∀ (q : Nat), q < (179 : Nat) → (173 : Nat) < q → ¬FRC.Nat.isPrime q) ∧ (1549 : Nat) * (1549 : Nat) < (2408561 : Nat) ∧ (2408561 : Nat) < (1553 : Nat) * (1553 : Nat) ∧ (2408561 : Nat) % (4 : Nat) = (1 : Nat) ∧ FRC.Nat.isPrime (1549 : Nat) ∧ FRC.Nat.isPrime (1553 : Nat) ∧ FRC.Nat.isPrime (2408561 : Nat) ∧ ∀ (q : Nat), q < (1553 : Nat) → (1549 : Nat) < q → ¬FRC.Nat.isPrime q :=
  @FRC.Horizon.closure_lab
set_option linter.defProp false in
/-- p20083 — 20:D9. The finite negative control: on $\F_{13}(\sqrt2)$ the polynomial $((X-2)^{2}-2)((X+1)^{2}-2)$ has exactly the roots $2\pm\eta$, $-1\pm\eta$, of traces $4$, $4$, $11$, $11$ against the line's $1$, the root set closed under conjugation and under the half-turn; finitude, conjugation and the reflection force no root onto the line. -/
def p20083 := @FRC.Horizon.negative_control13
/-- p26009 — 26:B3. The longitudinal turn on the shell: the multiplicative characters $\chi_\nu(g^t)=g^{\nu t}$ are eigenvectors of the scale shift $x\mapsto gx$, with the $(P-1)$-th roots of unity $g^{\nu}$ as distinct eigenvalues; the shift $x\mapsto g^{r}x$ fixes every unit when $(P-1)\mid r$ and none otherwise. -/
theorem p26009 : (∀ {p : Nat} [FRC.Pos p] {g : FRC.Shell p} (r k : Nat) (x : FRC.Shell p), (g ^ r * x) ^ k = (g ^ r) ^ k * x ^ k) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (r k : Nat), ((g ^ r) ^ k) ^ (p - (1 : Nat)) = (1 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {i j : Nat}, i < p - (1 : Nat) → j < p - (1 : Nat) → g ^ i = g ^ j → i = j) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (r : Nat), FRC.Shell.Frame.natCount (fun x => x ≠ (0 : Nat) ∧ g ^ r * FRC.Shell.ofNat x = FRC.Shell.ofNat x) p = if r % (p - (1 : Nat)) = (0 : Nat) then p - (1 : Nat) else (0 : Nat)) ∧ ∀ (i : Nat), i < (12 : Nat) → ∀ (j : Nat), j < (12 : Nat) → (2 : FRC.Shell (13 : Nat)) ^ i = (2 : FRC.Shell (13 : Nat)) ^ j → i = j :=
  And.intro @FRC.Horizon.shift_power_character (And.intro @FRC.Horizon.eigenphase (And.intro @FRC.Shell.Frame.pow_inj (And.intro @FRC.Horizon.shift_trace (@FRC.Ladder.eigenvalues13))))
/-- p26011 — 26:B5. The Gauss sum couples the two turns: multiplication by a unit permutes the units; $\sum_{t\neq0}\psi(tc)$ is $-1$ for $c\neq0$ and $P-1$ for $c=0$; $\sum_u\chi(u)=0$ for $\chi\neq1$; hence $\lvert g(\chi)\rvert^{2}=P$ for every nontrivial $\chi$ on the shell ($\Om$ on the Carrier). -/
theorem p26011 : (∀ {q : Nat} [FRC.Pos q] {κ' : Nat} {h : FRC.Shell q}, FRC.Shell.Frame q κ' h → ∀ {m : Nat}, (0 : Nat) < m → ∀ {ω : FRC.Shell q}, ω.IsPrimitive m → ∀ (n : Nat), n % m ≠ (0 : Nat) → FRC.Shell.sumRange (fun a => ω ^ (n * (a + (1 : Nat)))) (m - (1 : Nat)) = (-1 : FRC.Shell q)) ∧ (∀ {q : Nat} [FRC.Pos q] (ω : FRC.Shell q) (m : Nat), FRC.Shell.sumRange (fun a => ω ^ ((0 : Nat) * (a + (1 : Nat)))) (m - (1 : Nat)) = FRC.Shell.ofNat (m - (1 : Nat))) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (k : Nat), (0 : Nat) < k → k < p - (1 : Nat) → g ^ (p - (1 : Nat)) = (1 : FRC.Shell p) ∧ FRC.Shell.sumRange (fun j => (g ^ k) ^ j) (p - (1 : Nat)) = (0 : FRC.Shell p) ∧ 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 → ∀ {c : FRC.Shell p}, c ≠ (0 : FRC.Shell p) → (∀ {x y : FRC.Shell p}, c * x = c * y → x = y) ∧ ∀ (y : FRC.Shell p), ∃ x, c * x = y :=
  And.intro @FRC.Horizon.ramanujan_sum (And.intro @FRC.Horizon.ramanujan_zero (And.intro @FRC.Shell.Frame.principal_root (@FRC.Ladder.mul_perm)))
/-- p26025 — 26:E8. Existence is free: for every witness index $m$ of the scale chart the translation $j\mapsto j+(n-m)+1$ of the index cycle is a chart (a bijection of the cycle) that places $g^{m}$ one counting step from the origin, $g=g^{0}\cdot g$. The witness enters only to name the chart. -/
theorem p26025 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {m : Nat}, m < p - (1 : Nat) → g ^ FRC.Ladder.recentre (p - (1 : Nat)) m m = g ∧ g = g ^ (0 : Nat) * g) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (m : Nat) {i j : Nat}, i < p - (1 : Nat) → j < p - (1 : Nat) → FRC.Ladder.recentre (p - (1 : Nat)) m i = FRC.Ladder.recentre (p - (1 : Nat)) m j → i = j) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {m : Nat}, m < p - (1 : Nat) → ∀ {j : Nat}, j < p - (1 : Nat) → ∃ i, i < p - (1 : Nat) ∧ FRC.Ladder.recentre (p - (1 : Nat)) m i = j) ∧ ∀ (m : Nat), m < (12 : Nat) → (2 : FRC.Shell (13 : Nat)) ^ FRC.Ladder.recentre (12 : Nat) m m = (2 : FRC.Shell (13 : Nat)) :=
  And.intro @FRC.Ladder.recentre_witness (And.intro @FRC.Ladder.recentre_inj (And.intro @FRC.Ladder.recentre_surj (@FRC.Ladder.recentre13)))
/-- p26027 — 26:E10. The counting distance of a unit along the orbit of $g$ is its index: $m\mapsto g^{m}$ is a bijection of the index cycle onto the units, the distances $1,\dots,P-1$ have mean $P/2$ and maximum $P-1$, between $2^{\ell-1}$ and $2^{\ell}$ for $\ell$ the bit length. -/
theorem p26027 : (∀ {p : Nat} [FRC.Pos p], FRC.Nat.isPrime p → ∃ g, (g ^ (p - (1 : Nat)) = (1 : FRC.Shell p) ∧ ∀ (l : Nat), l < p - (1 : Nat) → (0 : Nat) < l → g ^ l ≠ (1 : FRC.Shell p)) ∧ ∀ (v : Nat), v < p → (0 : Nat) < v → ∃ m, m < p - (1 : Nat) ∧ (g ^ m).val = v) ∧ (∀ {p : Nat} [FRC.Pos p], FRC.Nat.isPrime p → ∀ {g : FRC.Shell p}, g ≠ (0 : FRC.Shell p) → FRC.Shell.Prime.HasOrder g (p - (1 : Nat)) → ∀ {i j : Nat}, i < p - (1 : Nat) → j < p - (1 : Nat) → g ^ i = g ^ j → i = j) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → g.Generates (p - (1 : Nat))) ∧ (∀ (n : Nat), (2 : Nat) * FRC.Ladder.distSum n = n * (n + (1 : Nat))) ∧ (∀ (n k : Nat), k < n → k + (1 : Nat) ≤ n) ∧ ∀ {e : Nat}, (0 : Nat) < e → (2 : Nat) ^ (FRC.Ladder.bits e - (1 : Nat)) ≤ e ∧ e < (2 : Nat) ^ FRC.Ladder.bits e :=
  And.intro @FRC.Shell.Prime.exists_drive (And.intro @FRC.Shell.Prime.primitive_pow_inj (And.intro @FRC.Shell.Frame.generates (And.intro @FRC.Ladder.two_mul_distSum (And.intro @FRC.Ladder.dist_le (@FRC.Ladder.bits_bracket)))))
/-- p26030 — 26:F2. Ascent is feasible: square-and-multiply computes $g^{j}$ in at most $2\,\mathrm{bits}(j)$ modular multiplications, hence at most $2\ell$ for $j<P$; on the three carriers $17$, $26$, $38$ multiplications at $j=P/3$, right to left with the last squaring skipped [data]. -/
theorem p26030 : (∀ {p : Nat} [FRC.Pos p] (b : FRC.Shell p) (e : Nat), (FRC.Ladder.sqmul b e).fst = b ^ e) ∧ (∀ {p : Nat} [FRC.Pos p] (b : FRC.Shell p) (e : Nat), (FRC.Ladder.sqmul b e).snd ≤ (2 : Nat) * FRC.Ladder.bits e) ∧ (∀ {p : Nat} [FRC.Pos p] (b : FRC.Shell p) {e l : Nat}, e < (2 : Nat) ^ l → (FRC.Ladder.sqmul b e).snd ≤ (2 : Nat) * l) ∧ (∀ (e : Nat), e < (64 : Nat) → (FRC.Ladder.sqmul (2 : FRC.Shell (13 : Nat)) e).fst = (2 : FRC.Shell (13 : Nat)) ^ e ∧ (FRC.Ladder.sqmul (2 : FRC.Shell (13 : Nat)) e).snd ≤ (2 : Nat) * FRC.Ladder.bits e) ∧ (FRC.Ladder.sqmul (2 : FRC.Shell (13 : Nat)) (11 : Nat)).snd = (7 : Nat) :=
  And.intro @FRC.Ladder.sqmul_spec (And.intro @FRC.Ladder.sqmul_count (And.intro @FRC.Ladder.sqmul_count_of_lt_pow (@FRC.Ladder.sqmul13)))
/-- p26031 — 26:F3. The descent's count: with $m^{2}\ge P-1$ baby steps $1,g,\dots,g^{m-1}$ ($m$ entries, one multiplication per step) and at most $m$ giant steps, baby-step--giant-step recovers from $g^{x}$ an index $y$ with $g^{y}=g^{x}$; at most $2m$ operations, $m=\lfloor\sqrt{P-1}\rfloor+1$; $134$, $1334$, $13334$ on the three carriers [data]. -/
theorem p26031 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {m : Nat}, m ≤ p - (1 : Nat) → p - (1 : Nat) ≤ m * m → ∀ {x : Nat}, x < p - (1 : Nat) → (∃ i j, (FRC.Ladder.bsgs g (g ^ x) (p - (1 : Nat)) m).fst = some (i, j) ∧ j < m ∧ g ^ (j + m * i) = g ^ x) ∧ (FRC.Ladder.bsgs g (g ^ x) (p - (1 : Nat)) m).snd ≤ m) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {m : Nat}, m ≤ p - (1 : Nat) → p - (1 : Nat) ≤ m * m → ∀ {x : Nat}, x < p - (1 : Nat) → m + (FRC.Ladder.bsgs g (g ^ x) (p - (1 : Nat)) m).snd ≤ (2 : Nat) * m) ∧ (∀ {p : Nat} [FRC.Pos p] {g : FRC.Shell p} (j : Nat), g ^ (j + (1 : Nat)) = g ^ j * g) ∧ (∀ {p : Nat} [FRC.Pos p] {g h : FRC.Shell p} {n m : Nat}, FRC.Ladder.descendsB g h n m = true → ∃ i j, (FRC.Ladder.bsgs g h n m).fst = some (i, j) ∧ j < m ∧ g ^ (j + m * i) = h) ∧ (∀ (x : Nat), x < (12 : Nat) → FRC.Ladder.descendsB (2 : FRC.Shell (13 : Nat)) ((2 : FRC.Shell (13 : Nat)) ^ x) (12 : Nat) (4 : Nat) = true) ∧ ∀ (x : Nat), x < (100 : Nat) → FRC.Ladder.descendsB (2 : FRC.Shell (101 : Nat)) ((2 : FRC.Shell (101 : Nat)) ^ x) (100 : Nat) (10 : Nat) = true :=
  And.intro @FRC.Ladder.bsgs_spec (And.intro @FRC.Ladder.bsgs_total (And.intro @FRC.Ladder.baby_step (And.intro @FRC.Ladder.descendsB_spec (@FRC.Ladder.descent13_101))))
/-- p26041 — 26:G2. Ladder closure: the four roles generate the two cyclic structures, $C_P$ additive and $C_{P-1}$ multiplicative, with the bridge $a_P$. A tower exponent $g^{j}$ is read modulo $P-1$, so tetration is exponentiation of a reduced index, and the power map acts on the index as multiplication; no third cyclic structure hosts a fifth role (00:B6). -/
theorem p26041 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (l : Nat), g ^ l = g ^ (l % (p - (1 : Nat)))) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (j : Nat), g ^ (g ^ j).val = g ^ ((g ^ j).val % (p - (1 : Nat)))) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (m k : Nat), (g ^ m) ^ k = g ^ (k * m % (p - (1 : Nat)))) ∧ ∀ (j : Nat), j < (12 : Nat) → (2 : FRC.Shell (13 : Nat)) ^ ((2 : FRC.Shell (13 : Nat)) ^ j).val = (2 : FRC.Shell (13 : Nat)) ^ (((2 : FRC.Shell (13 : Nat)) ^ j).val % (12 : Nat)) :=
  And.intro @FRC.Shell.Frame.pow_mod (And.intro @FRC.Ladder.tower_reduces (And.intro @FRC.Ladder.power_index (@FRC.Ladder.tower13)))
/-- p26042 — 26:G3. Phase-index dynamics: in the scale chart $x=g^{m}$ the power map acts by $P_k(g^{m})=g^{km}$ and its iterates by $P_k^{\,r}(g^{m})=g^{k^{r}m}$, the exponents read modulo $P-1$; the ascent is the orbit traversal $g^{j+1}=g\cdot g^{j}$, one multiplication per counted step. -/
theorem p26042 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (m k : Nat), (g ^ m) ^ k = g ^ (k * m % (p - (1 : Nat)))) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (k r m : Nat), FRC.Ladder.iter (fun x => x ^ k) r (g ^ m) = g ^ (k ^ r * m % (p - (1 : Nat)))) ∧ (∀ {p : Nat} [FRC.Pos p] {g : FRC.Shell p} (j : Nat), g ^ (j + (1 : Nat)) = g ^ j * g) ∧ ∀ (m : Nat), m < (12 : Nat) → FRC.Ladder.iter (fun x => x ^ (3 : Nat)) (2 : Nat) ((2 : FRC.Shell (13 : Nat)) ^ m) = (2 : FRC.Shell (13 : Nat)) ^ ((9 : Nat) * m % (12 : Nat)) ∧ FRC.Ladder.iter (fun x => x ^ (2 : Nat)) (3 : Nat) ((2 : FRC.Shell (13 : Nat)) ^ m) = (2 : FRC.Shell (13 : Nat)) ^ ((8 : Nat) * m % (12 : Nat)) :=
  And.intro @FRC.Ladder.power_index (And.intro @FRC.Ladder.phase_index (And.intro @FRC.Ladder.ascent_step (@FRC.Ladder.phase13)))
/-- p26043 — 26:G4. The one-way function is the inverse of the last role: each forward role costs one modular operation, the ascent at most $2\ell$ multiplications; the descent recovers the index, the position in the counted orbit of the fourth role. The descent/ascent operation ratio at the three carriers is $134/17$, $1334/26$, $13334/38$ [data]. -/
theorem p26043 : (∀ {p : Nat} [FRC.Pos p] (b : FRC.Shell p) {e l : Nat}, e < (2 : Nat) ^ l → (FRC.Ladder.sqmul b e).snd ≤ (2 : Nat) * l) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {m : Nat}, m ≤ p - (1 : Nat) → p - (1 : Nat) ≤ m * m → ∀ {x : Nat}, x < p - (1 : Nat) → (∃ i j, (FRC.Ladder.bsgs g (g ^ x) (p - (1 : Nat)) m).fst = some (i, j) ∧ j < m ∧ g ^ (j + m * i) = g ^ x) ∧ (FRC.Ladder.bsgs g (g ^ x) (p - (1 : Nat)) m).snd ≤ m) ∧ ∀ {p : Nat} [FRC.Pos p] {g : FRC.Shell p} (j : Nat), g ^ (j + (1 : Nat)) = g ^ j * g :=
  And.intro @FRC.Ladder.sqmul_count_of_lt_pow (And.intro @FRC.Ladder.bsgs_spec (@FRC.Ladder.ascent_step))
/-- p26044 — 26:G5. The power map $P_k$ is a bijection of $\F_P^{\times}$ iff $k$ is invertible modulo $P-1$, inverted by $x\mapsto x^{a}$ with $ak\equiv1$; otherwise its image is the cycle of $g^{d}$, $d=\gcd(k,P-1)$, of exactly $(P-1)/d$ elements. -/
theorem p26044 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {a k : Nat}, a * k % (p - (1 : Nat)) = (1 : Nat) → ∀ (m : Nat), ((g ^ m) ^ k) ^ a = g ^ m ∧ ((g ^ m) ^ a) ^ k = g ^ m) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {d e c a b k : Nat}, p - (1 : Nat) = d * e → k = d * c → a * k = b * (p - (1 : Nat)) + d → (∀ (m : Nat), (g ^ m) ^ k = (g ^ d) ^ (m * c)) ∧ (∀ (i : Nat), ((g ^ a) ^ i) ^ k = (g ^ d) ^ i) ∧ ∀ (i j : Nat), i < e → j < e → (g ^ d) ^ i = (g ^ d) ^ j → i = j) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {d e c k : Nat}, p - (1 : Nat) = d * e → k = d * c → ∀ (m : Nat), ∃ i, i < e ∧ (g ^ m) ^ k = (g ^ d) ^ i) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {d e : Nat}, p - (1 : Nat) = d * e → (1 : Nat) < d → e < p - (1 : Nat)) ∧ (∀ (m : Nat), m < (12 : Nat) → (((2 : FRC.Shell (13 : Nat)) ^ m) ^ (5 : Nat)) ^ (5 : Nat) = (2 : FRC.Shell (13 : Nat)) ^ m) ∧ (∀ (m : Nat), m < (12 : Nat) → ∃ i, i < (3 : Nat) ∧ ((2 : FRC.Shell (13 : Nat)) ^ m) ^ (4 : Nat) = ((2 : FRC.Shell (13 : Nat)) ^ (4 : Nat)) ^ i) ∧ ∀ (i : Nat), i < (3 : Nat) → ∃ m, m < (12 : Nat) ∧ ((2 : FRC.Shell (13 : Nat)) ^ m) ^ (4 : Nat) = ((2 : FRC.Shell (13 : Nat)) ^ (4 : Nat)) ^ i :=
  And.intro @FRC.Ladder.power_bijective_of_unit (And.intro @FRC.Ladder.power_image (And.intro @FRC.Ladder.power_image_index (And.intro @FRC.Ladder.compressive_of_gcd (@FRC.Ladder.powers13))))
-- end keys

end FRC.Ledger