The machine-verified core of Pisot Dimensional Theory. A Lean 4 + Mathlib formalization that verifies, in the kernel, the complex-number arithmetic underlying single-qubit quantum kinematics, and checks the number-theoretic bedrock the theory rests on through Mathlib's genuine API, not hand-substituted values.
206 declarations · 15 modules · no
sorry, nonative_decide. Composition (per the adversarial audit): approximately 96 substantive results, ~40 API wrappers/plumbing, ~33 disclosed elementary numeral identities, plus the cross-module identification lemmas, all kernel-clean over the three standard axioms (propext,Classical.choice,Quot.sound). (147 of the 206 use thetheoremkeyword; the rest arelemmahelpers.) The one-command verifier below builds the project and prints PASS with the full axiom trace — or fails loudly.
Pisot Dimensional Theory is a parameter-free program: it aims to derive the constants — the fine-structure constant, the gauge couplings, the fermion-mass ratios — from the arithmetic of just two polynomials,
x³ − x − 1 (root ρ, the plastic number) and x⁴ − x − 1 (root Q),
with zero adjustable parameters. The full theory develops those numerical derivations and matches them to measurement. This repository is the part a proof kernel can certify outright.
The complex-number kinematics, kernel-checked. The kernel verifies the ℂ-arithmetic underlying single-qubit kinematics: the Born form (z·z̄).re = |z|² (the square forced by [ℂ:ℝ] = 2), positivity, the dagger as complex conjugation, Hermitian ⟹ real (the pointer basis), unitary ⟹ norm-preserving, and that two normalized amplitudes give probabilities that are |z|², non-negative, and sum to one (QM_from_Q). These are theorems about ℂ. QisHilbert : H ≃ₗ[ℝ] ℂ names the physical posit — that a state space is this complex line, Q's complex place — but the proofs establish the ℂ-facts directly and do not transport through it; the identification with physical QM (and with Q) is interpretive, not kernel-checked.
The arithmetic bedrock, through the real Mathlib API. Independently of any posit, the kernel verifies — via Mathlib's genuine Algebra.norm, Algebra.discr, Algebra.traceForm/Algebra.traceMatrix (not asserted values) — the facts the theory is built on: the genuine field norms N(Q) = −1 and N(ρ) = 1 (via Algebra.norm); the discriminants −23 and −283 of the power bases of AdjoinRoot(x³−x−1) / AdjoinRoot(x⁴−x−1), equivalently the polynomial discriminants (these are field discriminants once one adds prime ⇒ squarefree ⇒ maximal-order — a standard step carried in prose, not in the kernel); Sylvester congruence certificates over ℚ pinning the (3,1) Lorentzian and (2,1) spatial trace-form signatures (the base-change to ℝ and Sylvester's law of inertia is the standard final step, in prose); the irreducibility of both polynomials; and the classical-vs-quantum Bell gap — CHSH ≤ 2 classically, Tsirelson 2√2 quantum-mechanically, saturated by an explicit real-Pauli tuple. The compositum norm N(ρQ) = −1 is not an Algebra.norm statement here — the compositum ℚ(ρ,Q) is unformalized; it is disclosed below as the numeral identity 1⁴·(−1)³ = −1.
| File | What it proves |
|---|---|
| PdtQm | Single-system QM kinematics — Born rule = |z|², dagger = Galois conjugation, Hermitian = Galois-fixed ⟹ real (pointer basis), unitary ⟹ norm-preserving, and the capstone QM_from_Q (Born probabilities as |z|², non-negative, summing to one) — all theorems about ℂ. QisHilbert : H ≃ₗ[ℝ] ℂ is the named physical posit; the proofs do not use it. |
| PdtNorm / PdtDiscriminant / PdtTraceForm / PdtIrreducible | The arithmetic through the genuine Mathlib number-theory API, not hand-substituted identities: Algebra.norm ℚ Q = −1, Algebra.norm ℚ ρ = 1; Algebra.discr of the power basis = −23 / −283; the trace-form Gram matrix as Algebra.traceForm over AdjoinRoot; x³−x−1 and x⁴−x−1 proved Irreducible over ℚ by reduction mod 2 (Gauss's lemma lift). (The direct answer to "the content is just in the names.") |
| PdtSignature / PdtSignatureRho | For ℚ[x]/(x⁴−x−1) the kernel checks a Sylvester congruence certificate over ℚ: PᵀMP = diag(4,4,−9/4,283/36) with P unimodular and det M = −283. Base-change to ℝ and the sign-count (Sylvester's law of inertia) — a standard step, in prose — give signature (3,1) (spacetime); likewise (2,1) (3-space) for the cubic. The hand-written matrices are linked to the genuine Algebra.traceForm / Algebra.traceMatrix Gram matrices in PdtLinks (M_eq_M4, Mρ_eq_traceMatrix_fin3). |
| PdtSymplectic | The complex place, two forms and one rotation: the dagger identity G_Born = G_trace ∘ σ (the Born form is the trace form precomposed with conjugation); the same J = mult-by-i is a Born isometry (the unitary phase) and a trace anti-isometry (the Lorentzian time-rotation); and the companion form ω = Jᵀ G_Born = Im(z̄w) is alternating and nondegenerate — a symplectic form — while the trace companion is symmetric. The linear-algebra core of the Fault-Line-A / Proposition 1 result: g(J·,·) is alternating iff g is J-invariant, and it is the Born metric (not the trace form) that is J-invariant. |
| PdtTsirelson / PdtBellClassical | The Tsirelson bound 2√2 (Mathlib's tsirelson_inequality) is saturated by an explicit real-Pauli IsCHSHTuple; the classical CHSH bound is ≤ 2; the gap 2 < 2√2 is strict. |
| PdtPisotBoundary | The settle/spiral dichotomy, kernel-checked from the polynomials alone: every non-real root of x³−x−1 has modulus < 1 (ρ is Pisot — settles) and every non-real root of x⁴−x−1 has modulus > 1 (Q is non-Pisot — spirals), by a single Vieta reduction on the conjugate pair — no root-finding, no polynomial API; packaged as pisot_boundary_dichotomy. Upgrades the computed moduli 0.869 / 1.063 to a theorem. |
| PdtClock | The β-clock's tick word m(n) = ⌊(n+1)β⌋ − ⌊nβ⌋ is two-valued (for 0 < β < 1), of density exactly β (exact telescoping to ⌊Nβ⌋), aperiodic (for irrational β, carried as an explicit hypothesis), and balanced — any two equal-length windows differ by at most one tick. Aperiodic but not random, kernel-checked. |
| PdtGolden / PdtArithmetic | The same bedrock re-expressed as elementary integer identities (decide/norm_num; the genuine field invariants are the API row above): disc(x³−x−1) = −23 = dim 𝔰𝔲(3)+𝔰𝔲(4); disc(x⁴−x−1) = −283; 23, 283 prime; N(2Q−1) = −23; the norm-tower product N(ρQ) = N(ρ)⁴·N(Q)³ = 1⁴·(−1)³ = −1, an elementary numeral identity (the compositum ℚ(ρ,Q) is not formalized); dim 𝔰𝔲(4) = 15. |
A clickable dependency graph (built with leanblueprint) is published on this repo's GitHub Pages — every theorem green, with the lone node the kernel does not check (the identification) set apart.
The kernel certifies the mathematics and logic — exactly, with nothing hidden. Two things sit deliberately outside it, and naming them is what makes the verified part trustworthy:
- The physics is an identification, not a theorem. The kernel verifies the ℂ-arithmetic; that this ℂ is physical quantum mechanics, and is Q's complex place, is the interpretive posit — not evaluated here. The verified facts stand on their own; the identification is named and kept outside the kernel.
- The numerical predictions are matched separately. The theory's high-precision results (α, the mass spectrum, the glueball mass) are checked against measurement by independent computation, not in the kernel.
That is the whole discipline: one named assumption, a hard boundary around it, and a machine confirming that everything inside depends on nothing but the standard axioms of mathematics.
Google Colab — one cell (most robust): open a blank Colab notebook, paste the entire contents of colab_oneshot.py into a single cell, and run. Pure Python — it installs the toolchain, writes the project, builds against pinned Mathlib, and self-certifies. (Do not paste a .ipynb into a cell.) The first line it prints is a version banner; the last is PASS with the axiom trace, or a labelled failure.
Colab — the notebook: in Colab choose File → Upload notebook, select PdtQm_Colab.ipynb, then Run all (CPU is fine).
Locally:
curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y
export PATH="$HOME/.elan/bin:$PATH"
lake exe cache get # respects the pinned manifest — do NOT run `lake update`
lake build # green = kernel-verifiedCode: MIT (see LICENSE).
Citation (all versions): Stephanie Alexander (ORCID 0009-0003-7727-2565), PDT-Lean: a kernel-verified Lean 4 formalization of the Pisot Dimensional Theory core, Zenodo, DOI 10.5281/zenodo.21210683 (concept DOI — always resolves to the latest release).
Feedback on the formalization and on the precision of the scope statement above is exactly what this repository invites.