The Lean module lean/FrcLedger/Pnp.lean of the paper 26-pnp (on Mathlib): 7 theorems (0 definitions): 0 with no axioms, 0 at tier 1 (propext, Quot.sound), 7 at tier 2 (Classical.choice), 0 red; the mark's colour is the library's (violet, Mathlib; red a proof the gate rejects), each declaration's axioms on hover; the small plain glyph marks a definition (no proof, no axioms; on the ledger pages the plain glyph is instead a module cited as a whole). Each declaration is anchored; the ledger predicates cite them by name. ▶ open in Lean Live · axioms.log.
1import Mathlib2import FrcLedger.Theme.Horizon3import FrcLedger.Theme.Chart4import FrcLedger.Keys.Chart56/-!7# 26-pnp — the paper module on Mathlib: the Gauss-sum modulus and the chart rows under the paper's name (16 October 2026)89Rows of the predicate ledger of *P versus NP: Computation as Counting over Finite Relational Substrate* (tree10`26-pnp-20260614`) whose content is read on the Gauss sum or against the continuum: the Gauss-sum product `g(χ)·g(χ⁻¹, ψ⁻¹) = p`11(B5) in `FrcLedger/Theme/Horizon.lean` (`FRC.HorizonML`) and its modulus `|g(χ)|² = p` over the complex numbers (B5) in `FrcLedger/Theme/Chart.lean`; the family's bit length and the decision12table beyond the absolute horizon at the scale import's anchor (C2) and the dilation generator's eigenfunction (B4) in13`FrcLedger/Theme/Chart.lean` (`FRC.Chart`, the chart theme, where the reals live). Every name here is an alias; the14exact content of the paper is the core's (`FrcCore/Pnp.lean` and the themes it cites).15-/1617namespace FRC.Pnp1819open Real2021/-! ## Old names (16 October 2026): every declaration of this module is an alias of a theme's (`FRC.HorizonML`,22`FRC.Chart`), under the paper's name -/2324/-- 26:B5 — the Gauss-sum product on a finite field into any domain (`FRC.HorizonML.gauss_product`,25`Theme/Horizon.lean`). -/26
theorem gauss_product {F : Type*} [Field F] [Fintype F] {R' : Type*} [CommRing R'] [IsDomain R']27 {χ : MulChar F R'} (hχ : χ ≠ 1) {ψ : AddChar F R'} (hψ : ψ.IsPrimitive) :28 gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = Fintype.card F :=29 FRC.HorizonML.gauss_product hχ hψ3031/-- 26:B5 — the Gauss-sum modulus over the complex numbers (`FRC.Chart.gauss_modulus`, `Theme/Chart.lean`). -/32theorem gauss_modulus {F : Type*} [Field F] [Fintype F] {χ : MulChar F ℂ} (hχ : χ ≠ 1) {ψ : AddChar F ℂ}33 (hψ : ψ.IsPrimitive) :34 gaussSum χ ψ * star (gaussSum χ ψ) = Fintype.card F ∧ Complex.normSq (gaussSum χ ψ) = Fintype.card F :=35 FRC.Chart.gauss_modulus hχ hψ3637/-- 26:C2 [chart] — the family's bits and the table beyond the horizon (`FRC.Chart.family_bits`, `Theme/Chart.lean`). -/38theorem family_bits (Λ ℓP r S Ω : ℝ) (hΛ : Λ = 1.088e-52) (hℓ : ℓP = 1.616255e-35)39 (hr2 : r ^ 2 = 3 / Λ) (hS : S = π * (r / ℓP) ^ 2) (hΩ : Ω = 4 * S + 1) :40 (2 : ℝ) ^ 204 < √Ω ∧ √Ω < (2 : ℝ) ^ 205 ∧ (2 : ℝ) ^ 102 < √(√Ω) ∧ √(√Ω) < (2 : ℝ) ^ 103 :=41 FRC.Chart.family_bits Λ ℓP r S Ω hΛ hℓ hr2 hS hΩ4243/-- 26:B4 [chart] — the dilation generator's eigenfunction (`FRC.Chart.dilation_eigen`, `Theme/Chart.lean`). -/44theorem dilation_eigen (ν x : ℝ) (hx : 0 < x) :45 -Complex.I * ((x : ℂ) * deriv (fun t : ℝ => (t : ℂ) ^ (-(1 / 2 : ℂ) + Complex.I * ν)) x46 + (1 / 2 : ℂ) * (x : ℂ) ^ (-(1 / 2 : ℂ) + Complex.I * ν))47 = ν * (x : ℂ) ^ (-(1 / 2 : ℂ) + Complex.I * ν) :=48 FRC.Chart.dilation_eigen ν x hx4950-- Ledger predicates of 26-pnp (generated by make_predicates.py from docs/26-pnp/26-pnp-ledger.json; edit the ledger, not this section)51set_option linter.defProp false in52/-- 26:B4 (p26010) — The continuum reading [chart]: the dilation generator $\HH=-\mathrm i(x\partial_x+\tfrac12)$ has $x^{-1/2+\mathrm i\nu}$ as eigenfunction of eigenvalue $\nu$ on $x>0$, so the frequency index is the spectrum of $\HH$ in the chart of the scale shift (20:E1). -/53def p26010 := @FRC.LedgerML.p2601054/-- 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). -/55theorem p26011 : (∀ {F : Type u_1} [Field F] [Fintype F] {R' : Type u_2} [CommRing R'] [IsDomain R'] {χ : MulChar F R'}, χ ≠ (1 : MulChar F R') → ∀ {ψ : AddChar F R'}, ψ.IsPrimitive → gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = ↑(Fintype.card F)) ∧ ∀ {F : Type u_3} [Field F] [Fintype F] {χ : MulChar F ℂ}, χ ≠ (1 : MulChar F ℂ) → ∀ {ψ : AddChar F ℂ}, ψ.IsPrimitive → gaussSum χ ψ * star (gaussSum χ ψ) = ↑(Fintype.card F) ∧ Complex.normSq (gaussSum χ ψ) = ↑(Fintype.card F) :=56 @FRC.LedgerML.p2601157/-- 26:C2 (p26013) — The family's size and the table beyond the horizon [chart]: at the anchor $2^{204}<\sqrt\Om<2^{205}$, so the shells of the family $P^{2}<\Om$ have at most $205$ bits; $2^{102}<\Om^{1/4}<2^{103}$, so a decision table with one entry per $204$-bit input exceeds the absolute horizon and lies below $\sqrt\Om$. -/58theorem p26013 : ∀ (Λ ℓP r S Ω : ℝ), Λ = 1088e-55 → ℓP = 1616255e-41 → r ^ (2 : ℕ) = (3 : ℝ) / Λ → S = Real.pi * (r / ℓP) ^ (2 : ℕ) → Ω = (4 : ℝ) * S + (1 : ℝ) → (2 : ℝ) ^ (204 : ℕ) < √Ω ∧ √Ω < (2 : ℝ) ^ (205 : ℕ) ∧ (2 : ℝ) ^ (102 : ℕ) < √√Ω ∧ √√Ω < (2 : ℝ) ^ (103 : ℕ) :=59 @FRC.LedgerML.p2601360-- end ledger predicates6162end FRC.Pnp63