Principia Fractalis
Pablo Cohen · ORCID 0009-0002-0734-5565 · github.com/FractalDevTeam/Principia-Fractalis
Headline result (kernel-verified, unconditional)
A machine-checked construction of the uniformly hyperfinite (UHF) C*-algebra M3∞ — the metric completion T∞ of the inductive limit of the matrix tower M3k(ℂ) — together with a canonical tracial state τ verified in the Lean 4 kernel to be additive, unital, 1-Lipschitz, tracial, Hermitian, positive, and faithful:
UHF_trace_faithful
As a corollary the formalization delivers the
C*-simplicity of T∞ — every two-sided ideal
is trivial (Glimm 1960) — as substrate_completion_simple_unconditional.
To the best of our knowledge (after searching mathlib, the Coq opam archive, and
the Isabelle AFP), this is the first formalized simplicity theorem for an
infinite-dimensional C*-algebra and the first machine-checked faithful tracial
state on one; we welcome pointers to prior art.
The proof routes through a trace-preserving level-k expectation map (the tail partial trace), its 2-norm contraction (elementary Cauchy–Schwarz), its operator-norm contraction (isometry decomposition), and an ε-density limit argument — development arc r102–r112, July 2026.
Read the paper
The canonical write-up: constructions, the faithfulness proof, honest scope notes, and full reproducibility data.
Verify it yourself
The result is reproducible from a clean checkout; the kernel — not the author — is the authority.
git clone https://github.com/FractalDevTeam/Principia-Fractalis.git
cd Principia-Fractalis/PF_Lean4_Code
lake build PF # 4,471 jobs at HEAD d5ad2881
# then #print axioms UHF_trace_faithful
# → [propext, Classical.choice, Quot.sound]Repository guide
| Where | What |
|---|---|
| PF_Lean4_Code/ | The Lean 4 corpus. Headline files: PF/SubstrateCompletionFaithful.lean (r112 summit),
PF/SubstrateConditionalExpectation.lean, PF/SubstrateCondExpOpNorm.lean. |
| PF/ForMathlib/ | Three mathlib-ready files (two-sided-ideal closure, cfc into closed ideals, clopen spectral projections), staged for upstream PRs. |
| Papers/ | The canonical paper (above) and prior-work archive. |
| Principia_Fractalis_master_folder/ | The book (919 pp), with a per-claim machine-verification ledger in Chapter 4. |
| REFEREE_QUICKSTART.md | Step-by-step independent verification procedure. |
| README.md | Full project overview, including the broader research framework. |
Scope, honestly
The headline result above is a self-contained operator-algebra theorem, fully machine-checked. The repository also contains a broader research framework (substrate-level reductions relating to the Clay Millennium problems); those reductions are conditional — each names its open hypotheses explicitly — and none constitutes a solution to any Millennium problem. The distinction between kernel-verified theorems and named open hypotheses is maintained throughout the corpus.