Trust Budget and TCB Disclosure

The trust budget: what Lean’s kernel trusts, and what TauLib extends it by.

A framework that claims “machine-checked in Lean 4” owes the reader a precise statement of what “machine-checked” means here, because Lean 4 — like every proof assistant — has a trusted computing base (TCB) that sits under every theorem. Theorems in TauLib that rely on native_decide extend that TCB in a specific, named way. This page discloses that extension.

Kernel baseline

Lean 4’s kernel trusts the Calculus of Inductive Constructions (CIC) and its standard axioms (propext, Quot.sound, Classical.choice). That is the irreducible baseline: every Lean theorem ultimately bottoms out at the kernel accepting a term of the claimed type, using only CIC reduction and those axioms.

The kernel is what has been audited over years of community use, what large projects like Mathlib have stress-tested, and what formal-methods reviewers refer to when they speak of “trusted by Lean.” No non-trivial theorem in any Lean library avoids extending the kernel’s baseline — every project’s question is how much and where.

The native_decide extension

TauLib uses native_decide in approximately 1,824 places across the library, including, load-bearingly, the Book II Central Theorem (central_theorem_3_15).

Any reader can check the TCB cost at the Lean REPL:

#print axioms central_theorem_3_15

The output includes, beyond the Mathlib baseline (Classical.choice, propext, Quot.sound):

• Lean.ofReduceBool — trusts that Lean’s definitional reduction of a Bool-valued expression to true commutes with kernel-level equality. Specifically: if the compiled Bool-valued check returns true, the kernel accepts this as a witness that the proposition holds.
• Lean.trustCompiler — trusts Lean’s native compilation pipeline to produce a correct executable from a Lean definition. The native_decide tactic runs the compiled version of a decidable check; Lean.trustCompiler is the axiom that says that compiled run is faithful to the source.

Together, these extend TauLib’s TCB from “Lean’s kernel alone” to “Lean’s kernel plus the native compiler pipeline.”

This is the framework’s honest disclosure: the Book II Central Theorem’s proof chain leans on the correctness of Lean’s native compiler and on the ofReduceBool axiom. A reviewer who does not accept either extension should treat the Central Theorem (and every theorem in the list below) as conditionally verified.

Why we accept this tradeoff

Finite Bool-valued checks of the kinds TauLib uses are intractable for kernel-only reduction in reasonable build time. Concretely:

• Central Theorem at rank (3, 15). The algebraic check at that rank involves a finite but large finite computation over the window-algebra integers. Kernel-only decide would exceed build-time limits by orders of magnitude.
• Window-algebra integers W_n(k). Verification of closed-form identities at bounded (n, k) pairs — including the load-bearing W₃(4) = 5 and W₅(3) = 19 — uses native_decide on the same grounds.
• Axiom finite-envelopes. Each of the three conjectural axioms in Book III ships with a paired *_finite_check theorem verifying the universal claim holds at all configurations up to a stated bound. These checks run via native_decide.

native_decide is used deliberately where the kernel-only decide would not terminate in minutes. The alternative — writing out the finite check as a kernel-reducible proof term — produces objects that exceed Lean’s kernel memory envelope before completing. That is a hard engineering limit, not a shortcut.

What a reviewer should do with this disclosure

1. Run #print axioms on the theorems you care about. The output is authoritative; the tables on this page are a guide, not a replacement.
2. Decide whether to accept the native_decide extension. A Lean 4 reviewer who has audited the compiler pipeline may accept it; one who has not may wish to rebuild the load-bearing finite checks at kernel-level, accepting the build-time cost.
3. Separate the two kinds of cost. The three Book III axioms are mathematical commitments — the universal step the framework declines to prove. The native_decide extension is an engineering commitment — that Lean’s native compiler is faithful. These are independent; accepting one does not require accepting the other.

Why this page exists

This disclosure is the posture we prefer: name the cost, locate it, let the reader decide whether to take it on.

A prior version of the Verify lane warned auditors about native_decide as a red flag on audit checklists — while the headline theorem of Book II was itself proved by it. That was an inconsistency. It is now corrected: the native_decide usage is disclosed in full, the theorems that depend on it are enumerated, and the reader is given the tools to make their own determination.

As of peer-review-fixes-v2 (2026-04-19) the per-theorem #print axioms output is emitted as a CI artifact from every build of TauLib — see the paragraph above “Which theorems depend on native_decide” for the link. Per-registry-entry linking from each claim into that artifact remains a separate, finer-grained improvement on the roadmap; for now, the single machine-attested report covers the headline theorems the TCB partition rests on.

Cross-links

• Release Manifest — pinned commit, overall axiom and sorry inventory
• Custom Axiom Inventory — the three Book III axioms in detail
• Formalization Status — per-book statistics
• Formal Methods Audit Route — step-by-step verification protocol
• Scope Labels — how conjectural-axiom dependencies propagate through the registry