Custom Axiom Inventory — The Compute-Then-Axiomatize Pattern
Honest accounting of the three custom axiom declarations in TauLib beyond Mathlib's trusted base: what each axiom says, what finite computation motivates it, what the universal step being axiomatized is, and what specialist-review would close on each. The fourth axiom shipped in v1 (`central_theorem_physical : True`) was retired in peer-review-fixes-v1.
In plain language
An axiom is something a formal system asks you to take on faith — every theorem provable in the system depends on its axioms being true. Lean and Mathlib already have a small set of widely-trusted axioms. TauLib adds three more, and this page accounts for each of them: what the axiom says in mathematical terms, what specific finite computation gives evidence for the universal claim it makes, and what would need to happen in peer review to either close the gap (turn the axiom into a theorem) or expose it as wrong. Three custom axioms is small — most large formal systems have many more — but the program treats every additional axiom as a debt to be paid down rather than a freebie.
The Release Manifest states, at the headline level, that TauLib contains 3 custom axiom declarations beyond Mathlib’s trusted base: all 3 in Book III (spectral / number-theoretic bridges). A previously shipping fourth axiom central_theorem_physical : True in Book IV was retired in peer-review-fixes-v1 (2026-04-19) — an axiom : True declaration is a no-op (True is inhabited by trivial) and was identified in pre-publication simulated peer review as a null commitment that inflated the axiom inventory from 3 to 4 without adding anything to the theory. This page expands the accounting of the three remaining axioms.
The question a serious reviewer asks — and the April 2026 external assessments asked it explicitly — is: for each custom axiom, what is the justification? Is this honest “compute-then-axiomatize” or is it a hidden load-bearing assumption dressed up as a universal statement?
Registry “Axiom · 7” vs Lean “axiom: 3” — what the difference means
A reviewer browsing the Corpus Registry will see the type filter Axiom · 7. A reviewer running rg "^axiom " TauLib against the pinned commit will see exactly 3 matches. The numbers are not in conflict; they count two different things:
- The Lean kernel sense (count: 3) — only declarations that begin with the keyword
axiomin TauLib source. These are what#print axiomspropagates into the trusted base of any theorem that depends on them. The 3 arebridge_functor_exists,spectral_correspondence_O3, andgrand_grh_adelic, all in Book III. This is the count that matters for trusted-computing-base hygiene. - The Registry “axiom-class” sense (count: 7) — Corpus-level typed claim entries in the Axiom collection, which include the 3 Lean axioms above plus 4 additional postulate-shaped entries that are formalized as
def,structure,instance, orCommitmentdeclarations rather than as Leanaxioms. These 4 are Corpus claim records about kernel-level commitments (e.g. existence-of-structure postulates, the fourCommitmentdeclarations in Book VII that replaced earlier: True := sorryplaceholders, and one structure-shape declaration). They are not Lean axioms; they do not propagate through#print axioms. They appear in the Registry’s Axiom collection because the Corpus typology classifies them as axiom-class commitments at the prose level, not because the Lean kernel treats them that way.
Reviewer takeaway. For trust-boundary purposes (what does Lean force you to accept on faith?), the canonical number is 3. The Registry’s 7 is the broader inventory of “things the Corpus declares without proof” — useful for editorial accountability but not equivalent to the Lean trusted base. We are reviewing whether to rename or split the Registry collection to make this distinction visible at the index level rather than only here.
What “compute-then-axiomatize” means in TauLib
The pattern is:
- A universal claim is stated (the axiom body): “for all X in some class C, property P holds”.
- A finite, decidable check is performed in Lean using
decideornative_decide: the claim is verified to hold for all X up to a specified finite bound B. - The universal step is declared as an axiom: the Lean kernel accepts the universal claim without further proof; downstream theorems rely on it.
This pattern is not a proof. It is an honest surface of a structural conjecture that has been numerically validated for all accessible cases but not formally proved in full generality. The axiom is load-bearing in the sense that downstream theorems cite it.
The pattern is acceptable as long as it is:
- Explicitly declared (not hidden inside a definition or an unfolded lemma),
- Named (the axiom has a stable identifier that
#print axiomssurfaces), - Bounded (the finite check’s bound B is stated and reproducible),
- Load-bearing but marked (downstream theorems referencing it carry a scope label that propagates the conjectural status).
The Mathlib community’s norms on this are strict, and Lean’s #print axioms mechanism is designed to make this pattern inspectable rather than deniable. TauLib commits to the same discipline.
Inspecting the custom axioms
Any reviewer can, at the pinned commit 2261c04:
cd taulib
rg "^axiom " TauLib --stats
Expected output: 3 matches, with their module locations (all in TauLib/BookIII/).
For any downstream theorem T, run in Lean 4:
#print axioms T
Expected output lists:
- Mathlib’s trusted base (
Classical.choice,propext,Quot.sound) - Plus, if T transitively depends on a custom axiom, the custom axiom’s name.
This is the diagnostic. A theorem claimed as “Internally addressed” that transitively depends on one of the three custom axioms should carry a scope label reflecting that dependency. The Formal Methods audit route names this as one of the fail-fast checks.
Headline-theorem axiom-dependency map
The table below summarises which custom axioms each headline theorem transitively depends on at the pinned commit. A reviewer should still run #print axioms locally to verify — this table is the program’s own published claim about the dependency structure and is exactly what an audit would falsify or confirm. Theorems with no custom-axiom dependency are flagged “kernel-only” — they propagate only Mathlib’s trusted base (Classical.choice, propext, Quot.sound) and, where native_decide is invoked, the standard Lean.ofReduceBool + Lean.trustCompiler extension documented on the TCB Disclosure.
| Headline theorem | Lean identifier | bridge_functor_exists |
spectral_correspondence_O3 |
grand_grh_adelic |
Site status |
|---|---|---|---|---|---|
| Central Theorem 𝒪(τ³) ≅ A_spec(𝕃) | central_theorem_3_15 |
— | — | — | Internally addressed |
| Rigidity Aut(τ) = {id} | rigidity_non_omega |
— | — | — | Internally addressed |
| Categoricity (kernel admits one model up to iso) | categoricity_non_omega |
— | — | — | Internally addressed |
| Generation count = 3 | gen_count_three |
— | — | — | Internally addressed |
| Critical Line Theorem (τ-internal ζ-purity) | III.T19 |
— | — | — | Internally addressed |
| Master Schema → classical RH bridge | III.T23 |
✓ | — | — | Partial |
| Higher-order Millennium reformulations | (Book III dictionary extensions) | — | ✓ | — | Partial |
| Grand GRH for higher-rank automorphic L | (Book III adelic extensions) | — | (transitively) | ✓ | Partial |
| τ-Yang–Mills mass gap (τ-internal) | IV.T75 |
— | — | — | Internally addressed |
| Modal-S4 internal logic | modal_S4_theorem |
— | — | — | Internally addressed |
Reading the table. A column entry “✓” means the theorem’s #print axioms output should surface that custom axiom. A “—” means it should not — the theorem closes against the Mathlib trusted base alone (plus native_decide extension where present). The site’s status grammar (Internally addressed vs Partial) correctly propagates the dependency: every Partial-status theorem above carries a custom-axiom dependency that’s the reason for its Partial classification.
Yang–Mills note. The τ-internal mass-gap theorem IV.T75 closes kernel-only — no custom-axiom dependency. It is Internally addressed inside τ. The corresponding Challenge Response carries a Partial status because the bridge layer between the τ-formulation and the Clay Yang–Mills statement on ℝ⁴ is treated separately and not yet formally bridged via Lean. This is the same pattern as the Master Schema → classical RH split: a τ-internal kernel-only result plus an unproven bridge to the orthodox classical statement. The bridge layer is the program’s open work; IV.T75 itself is not axiom-dependent.
What an audit would establish. Run #print axioms <theorem-name> for each row at the pinned commit. The set of custom axioms returned should match the ✓ marks above. Any mismatch is a finding the program wants to hear about (see also the Formal Methods audit route for the canonical reproducible protocol).
Why this map is in the FAQ rather than embedded as live Lean output. The May 2026 self-assessment surfaced as a Tier-A formal-methods finding that the literal #print axioms output for headline theorems is not yet embedded on the public verify page. Embedding live output requires running the Lean toolchain in CI and pasting the result into the build; that’s on the verify-lane polish backlog. Until then, the table above is the program’s own published claim about the dependency structure — and it can be falsified by any reviewer in 10 minutes using the workflow above.
Per-axiom technical detail — universal claim, finite-envelope check, what would close it (technical reviewer detail)
The three custom axioms
The precise Lean identifiers live in the TauLib source at the pinned commit. The specialist should verify them directly there. The descriptions below are at the prose level; the Lean source is authoritative.
Axiom 1 — Bridge functor existence (Book III)
What it says. A structure-preserving functor exists between τ-admissible spectral data and the orthodox classical formulations (Riemann zeta, Dirichlet and Hecke L-functions) such that τ-internal spectral-purity results translate to classical statements on the τ-admissible sub-domain.
What is finite-checked. The functor’s structure-preserving behavior has been verified via native_decide on all τ-admissible spectral data up to a stated finite bound: the trichotomy (III.T14) classifications match for all bounded configurations.
What is axiomatized. The universal extension: the functor exists and preserves spectral purity for all τ-admissible data, not just the finite-check window.
What closes the gap. A constructive proof of the functor’s existence for unbounded spectral data, or a rigorous obstruction argument that shows the finite-check must extend. This is an active research direction.
Where it is load-bearing. The Master Schema Theorem (III.T23, in Book III Chapter 30) — which is the bridge between τ-internal Riemann Hypothesis results and the classical Clay statement — depends on this axiom. Accordingly, the classical-RH claims are marked Partial on the site, not internally addressed. If this axiom is retracted or refuted, the bridge from τ-internal ζ-purity to classical RH falls, but the τ-internal Critical Line Theorem (III.T19) remains.
Axiom 2 — Spectral correspondence at O(3) (Book III)
What it says. The τ-spectral correspondence extends to third-order constructions: degree-3 polynomial spectral sub-structures on the lemniscate boundary preserve the B ↔ I ↔ S triangle structure in the same way degree-1 and degree-2 sub-structures do (which are proved).
What is finite-checked. The correspondence has been verified for all O(3) τ-admissible configurations up to a stated numerical bound.
What is axiomatized. The generalization from finite-checked O(3) configurations to all O(3) spectral data.
What closes the gap. A direct structural proof using the τ-CR operator and the Hartogs-extension principle for order-3 generalization.
Where it is load-bearing. The Book III spectral dictionary extensions (higher-order Millennium reformulations) depend on this axiom. Grand GRH results for higher-rank automorphic L-functions inherit the dependency.
Axiom 3 — Grand Adelic GRH (Book III)
What it says. The Prime Polarity Scaling Theorem (III.T20) extends to all automorphic L-functions in the adelic sense, not just the finite-rank classes checked in Lean.
What is finite-checked. Grand GRH spectral purity has been verified via native_decide for all τ-admissible automorphic data with bounded rank and bounded conductor.
What is axiomatized. The universal extension to unbounded rank and conductor — the full adelic class.
What closes the gap. A rigorous argument that the τ-internal spectral trichotomy (III.T14) applies uniformly across the full adelic class. This is the most ambitious of the three Book III axioms and the least likely to be closed in the near term.
Where it is load-bearing. Grand GRH claims for higher-rank classes (not classical GRH for Dirichlet L, which is finite-checked separately). Any internally addressed-status GRH claim that depends transitively on this axiom should be re-typed to Partial.
Axiom 4 (RETIRED) — central_theorem_physical : True (Book IV)
Status. Retired in peer-review-fixes-v1 (2026-04-19). No longer present in the TauLib source at the current pinned commit.
What it had said. The original declaration was axiom central_theorem_physical : True in BookIV/Arena/BoundaryHolonomy.lean, intended to mark the physical interpretation of the Book II Central Theorem as a named axiomatic hook.
Why it was retired. An axiom of type True is a no-op: True is already inhabited by trivial, so declaring an axiom at that type adds no logical content and names no new commitment. In pre-publication simulated peer review (chair: Leonardo de Moura, reviewer: Joachim Breitner) the declaration was flagged as a null commitment that inflated the visible axiom inventory from 3 to 4 without adding anything to the theory. The correct posture is either (a) state the physical interpretation as a proved theorem referencing the Book II algebraic proof, or (b) omit the declaration. Option (b) was chosen for v2.
Current state. The physical interpretation of the Central Theorem is now carried by the Book II algebraic statement and its guided tour in TauLib/Tour/CentralTheorem.lean; no Book IV axiom mediates the physical reading.
Why this pattern rather than a proof
The honest reason is: the compute-then-axiomatize pattern is faster than producing a full structural proof, and it makes the conjectural step visible to #print axioms. A researcher who proved these three axioms would collapse the Partial/Conjectural status labels that depend on them; until then, the axioms are placeholders for work-in-progress proofs.
This is also exactly the pattern Mathlib and large Lean projects use for deep structural conjectures that admit numerical evidence but not immediate proofs (e.g., the prime-number-theorem bounds, certain analytic-number-theory density results). It is a pattern Lean was designed to surface cleanly.
A framework that hid such axioms inside definitions, used them implicitly in tactic closures, or simply wrote “here we assume” in prose without Lean declarations would be deniable. TauLib’s declarations are inspectable.
What specialist review would establish
A Lean-4 / formal-methods specialist should verify:
- Count correctness. Is the
rg "^axiom"output exactly 3 matches at the pinned commit, all inTauLib/BookIII/? (Claim: yes.) - Axiom chain faithfulness. For each of ~10 headline theorems that the Release Manifest claims as internally addressed, does
#print axiomssurface only the Mathlib trusted base plus (where applicable) thenative_decideTCB extension (Lean.ofReduceBool,Lean.trustCompiler) and no custom axioms? (Claim: yes; see TCB Disclosure.) - Partial-claim axiom propagation. For each claim marked Partial that references one of the three axioms, does
#print axiomssurface the expected custom axiom? (Claim: yes.) - Finite-check reproducibility. For each custom axiom, the stated finite bound is reproducible via
native_decideon the pinned commit. (Claim: yes.) - Honest downstream-status propagation. No internally addressed claim transitively depends on a custom axiom in a way that should have re-typed it to Partial. (Claim: all such dependencies have been re-typed.)
Any finding that violates (1)–(5) should be reported to the program — this would be the single most impactful piece of formal-methods feedback possible.
What this page does NOT claim
- It does not claim the three axioms will be proved in the near term. They are research-open.
- It does not claim the finite-check bounds are adequate to persuade a number-theorist that the universal extension is plausible. The finite checks are Lean-decidable evidence; they are not mathematical proofs of the universal case.
- It does not replace the Formal Methods Audit route — that is the concrete verification protocol for the claims on this page.
- It does not claim that the compute-then-axiomatize pattern is superior to direct proof. It is a transitional form: proofs-in-progress surfaced honestly.
Cross-links
- Release Manifest — headline axiom and
sorrycounts at pinned commit - Formalization Status — per-book formalization dashboard
- Formal Methods Audit Route — step-by-step verification protocol
- Red-team FAQ #3 — short-form answer
- Scope Labels — the 4-tier scope discipline that propagates through axiom dependencies
Save or share this page for inspection
Download a portable dossier, copy a reviewer note, or send this page to someone who can inspect it.