Pnp.lean — FrcCore

1import FrcCore.Theme.Ladder2import FrcCore.Keys.Foundation3import FrcCore.Keys.Frame4import FrcCore.Keys.Horizon56/-!7# 26-pnp — the paper module: the reference shell `𝔽₁₃` decided by the kernel (16 October 2026)89The finite content of *P versus NP: Computation as Counting over Finite Relational Substrate* (tree `26-pnp-20260614`)10lives in the themes: the longitudinal turn — the characters as eigenvectors of the scale shift, the eigenvalues roots11of unity, the fixed-point count — in `Theme/Horizon.lean` (`FRC.Horizon`, the shell theorem of 20-rh, the master's12Z10); the Gauss-sum telescoping in `Theme/Horizon.lean` (`ramanujan_sum`) and `Transform.lean` (`principal_root`); the13exponential bijection of the index cycle onto the units in `Theme/Drive.lean` (`Prime.exists_drive`,14`primitive_pow_inj`, the master's A12); the exact round trip of the additive transform in `Transform.lean`15(`dft_inverse`); the ladder itself — the index dynamics of the power map, the recentring chart, the bijective and the16compressive power maps, square-and-multiply with its count, baby-step–giant-step with its count — in17`Theme/Ladder.lean` (`FRC.Ladder`, the horizon theme). Every row of the paper's ledger is a key written by18`make_keys.py` from those (`Keys/*.lean`), and this module carries the rows' declarations `FRC.Pnp.p26NNN` as aliases of19the keys (`make_predicates.py`), the worked instances on the paper's reference shape `𝔽₁₃` (`g = 2`, `n = 12`) and on20`𝔽₁₀₁`, decided by the kernel, living in `Theme/Ladder.lean` beside the theorems they instantiate. No theorem is stated here twice. Every declaration is checked to depend21on no axiom (`check_core_axioms.py`).22-/2324namespace FRC.Pnp2526open FRC.Shell FRC.Shell.Frame FRC.Ladder2728-- Ledger predicates of 26-pnp (generated by make_predicates.py from docs/26-pnp/26-pnp-ledger.json; edit the ledger, not this section)29/-- 26:B3 (p26009) — 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. -/30theorem 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 :=31  @FRC.Ledger.p2600932/-- 26:B5 (p26011) — 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). -/33theorem 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 :=34  @FRC.Ledger.p2601135/-- 26:E8 (p26025) — 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. -/36theorem 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)) :=37  @FRC.Ledger.p2602538/-- 26:E10 (p26027) — 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. -/39theorem 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 :=40  @FRC.Ledger.p2602741/-- 26:F2 (p26030) — 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]. -/42theorem 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) :=43  @FRC.Ledger.p2603044/-- 26:F3 (p26031) — 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]. -/45theorem 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 :=46  @FRC.Ledger.p2603147/-- 26:F10 (p26038) — The descent is the inverse coordinate map: $a_P:j\mapsto g^{j}$ is the bijection of $C_{P-1}$ onto $\F_P^{\times}$ carrying the time index to its position, and $d_P=\mathrm{dlog}$ its inverse, a cyclic-group coordinate, not the inverse of the multiplicative Fourier transform (B3). -/48theorem p26038 : (∀ {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)) :=49  @FRC.Ledger.p2603850/-- 26:G2 (p26041) — 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). -/51theorem 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)) :=52  @FRC.Ledger.p2604153/-- 26:G3 (p26042) — 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. -/54theorem 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)) :=55  @FRC.Ledger.p2604256/-- 26:G4 (p26043) — 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]. -/57theorem 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 :=58  @FRC.Ledger.p2604359/-- 26:G5 (p26044) — 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. -/60theorem 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 :=61  @FRC.Ledger.p2604462/-- 26:H3 (p26048) — Fourier-diagonalisable implies $\PC$: the additive transform on the shell is exact and self-inverse, $T^{-1}T=1$ on the full cycle $n=P-1$ (the round trips on the sub-cycles $n=8$, $256$, $2^{16}$ over $\F_{17}$, $\F_{257}$, $\F_{65537}$ [data]); the cyclic convolution costs $n^{2}$ multiplications in the position chart and $\tfrac32n\log_2n+n$ through the transform ($1\,048\,576$ against $16\,384$ at $n=2^{10}$) [data]. -/63theorem p26048 : (∀ {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 => g ^ (l * k) * -g ^ ((p - (1 : Nat) - j) * l)) (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 → ∀ (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) :=64  @FRC.Ledger.p2604865-- end ledger predicates6667end FRC.Pnp68