Technical Credibility — FAQ

Machine-checked does not mean every prose claim is verified. It means the Lean-encoded theorem or obligation is accepted by the proof checker under the disclosed environment and trust budget.

Lean can check encoded derivations. It cannot by compilation alone prove that a τ-internal object corresponds to a physical observable, that a measurement bridge is adequate, or that a numerical match validates the framework.

The Release Manifest is the authoritative current snapshot for release metrics and pins source revision, Lean version, Mathlib version, counts, custom axioms, and sorry status. Other pages should render those facts from the manifest.

A `sorry` can temporarily accept a theorem without proof. A 0-sorry release is meaningful formalization hygiene, while still not proving bridge adequacy or empirical truth.

A 0-sorry Lean development is stronger than one with placeholder proofs, but it is not a truth certificate for the whole research program. The encoded statements, correspondence to prose, bridge claims, and domain claims remain separate burdens.

A custom axiom is accepted without being proved inside Lean. The site treats the three custom axioms as visible debts, with inventory pages explaining rationale, scope, and review burden.

Reviewers should inspect axiom declarations, run `#print axioms` on downstream declarations, and check whether theorem status labels reflect custom-axiom dependence.

This pattern is explicit debt, not proof. It is acceptable only if named, bounded, reproducible, load-bearing, and reflected in downstream scope labels.

It helps distinguish theorem statements that are fully proven under the disclosed base from statements that depend on classical axioms, custom axioms, native computation trust, or placeholder proof artifacts.

No proof assistant verifies itself from nothing. The question is whether the trust base is disclosed, bounded, and auditable. TauLib’s TCB page names the Lean baseline and native computation costs.

`native_decide` is useful for finite computations, but it depends on native compilation/evaluation. The site should treat it as a named trust-budget extension, not hidden magic.

The precise claim is code-level and should be audited through imports and dependencies. Lean/Mathlib tooling is used, but τ object-level content is intended to be constructed internally rather than imported as mathematical semantics.

If public numbers differ, the Release Manifest determines which count is load-bearing and which filter rule is being used. It is the source of truth for release-state facts.

Registry objects are not Lean modules. Dashboard totals are filtered views. Formalized counts apply status filters. `sorry` count is a source scan. The first question is always which filter rule each page uses.

A registry object is a stable public ID for a Corpus item. A TauLib module is a Lean source file. The meaningful audit question is whether claimed mappings between Registry, Corpus, and TauLib are explicit and inspectable.

Treat the pinned commit as authoritative, not a moving branch. A failed build or unexpected `sorry` is a serious reproducibility issue.

A Result page is not automatically a Lean theorem. The right question is status, Corpus support, formalized component, bridge burden, and external validation route.

Bridge adequacy asks whether a τ-internal construction legitimately transfers to the external target. The site should keep internal proof, bridge claim, and domain validation visibly separate.

A fast audit should confirm commit, build, Lean/Mathlib pins, source scans, custom axioms, TCB disclosure, and theorem dependency traces before inspecting prose correspondence.

Such failures may require correction, retraction, relabeling, or narrowing. They do not all necessarily destroy the entire program, but they must update status labels and public artifacts.