Verify
How to inspect, verify, and challenge the claims of the Panta Rhei Research Program — what can be checked, and what verification does not settle.
Current TauLib, registry, and release-count metrics are pinned in the Release Manifest; scope is tiered — see Filter Rules.
What can be checked
Every theorem in TauLib compiles in Lean 4. Every quantitative prediction has an explicit formula. Every scope claim carries its epistemic label.
What verification does not settle
Compilation proves internal consistency, not truth about the physical world. Bridge claims remain conjectural until independently validated.
How to start
Start from an obligation, a construction step, or a result. Then trace it to Corpus support, Verify surfaces, and any available formalization.
What Verify Means Here
Verify is where building becomes accountable.
Verify is where every obligation, construction step, and result becomes inspectable.
Verification in this program is not one thing. It includes research-form legitimacy, source-policy inspection, construction-step verification, formal proof checking, semantic correspondence, bridge adequacy, domain-specific validation, prediction and falsification surfaces, and structured external assessment.
Metrics context: Release Manifest · Filter Rules · Custom Axiom Inventory · TCB Disclosure
Current manifest snapshot: 512 Lean modules · 142,406 lines · 4,863 theorems/lemmas · 0 sorry assignments · 3 axiom declarations.
The inspection layer at a glance
The Verification Matrix
Verification is not a single operation. It begins with traceability: what obligation is being answered, what construction supports it, what result follows, and how can it be challenged?
Formal checking is essential, but it is not empirical truth.
For the architecture-level audit route, see Building a Public Research Observatory for High-Scope Open Research. It explains how Verify fits into the larger public observatory without claiming that infrastructure validates the scientific theory.
Verify the Construction Spine
Inspect TauLib
Read the Release Manifest
Open Predictions & Falsification
Scientific Rigor
->
Verification Framework
->
Construction Verification
->
Formal Stack
->
Domain Verification
->
Operational Routes
Core Routes
-
Scientific Rigor Whether the program operates as a serious, inspectable research artifact. -
Verification Framework The shared standards: explicitness, traceability, derivability, and domain-appropriate validation. -
Verify the Construction Spine How each of the ten construction steps can be inspected, checked, or challenged. -
Formal Verification Stack Kernel integrity, standard-foundation checks, bridge verification, and current boundaries. -
Domain Verification How verification differs across mathematics, physics, life, and metaphysics. -
Predictions & Falsification Where results become accountable to computation, measurement, contradiction, or failure. -
Assessment Protocols Manual and LLM-assisted review pathways for structured external scrutiny.
Verification status legend
- Formalized — represented in TauLib or another formal artifact.
- Formally checked — compiles under the pinned formalization environment.
- Bridge pending — internal construction exists, but the bridge to standard mathematics, measurement, or domain interpretation remains open.
- Empirical pending — a prediction or comparison exists, but decisive external test or measurement remains open.
- Externally reviewed — discussed or reviewed outside the program.
- Externally accepted — accepted by an external scholarly process or community standard.
These labels describe inspection state. They are related to, but distinct from, Results status labels such as internally addressed, partial, qualitative, or not addressed.
Review Packets & Citable Artifacts
Inspecting a claim or preparing a review typically requires reaching for the publication-class artifacts behind it. The six surfaces most relevant to a Verify reader:
Research Papers
Standalone scholarly papers — the peer-review-ready Hinge series.
Research Notes
Shorter scholarly artifacts — frontier responses, comparative readings, pre-registrations.
Release Artifacts
Version, provenance, correction, manifest, changelog — the release-governance surface.
Errata
The program's open errata stream — corrections recorded as a first-class artifact.
Bibliography
The cross-cutting references — classical and modern sources linked to canonical publisher, DOI, or arXiv record.
How to Cite
Citation guidance for individual monographs, the program as a whole, specific results, and TauLib.
Operational Surfaces
- TauLib is the Lean 4 formalization surface.
- Release Manifest pins the current public release state.
- Filter Rules explain which count means what across site surfaces.
- Custom Axiom Inventory and TCB Disclosure name the trust budget.
- How to Verify gives practical entry points for different reviewers.
Technical Credibility FAQ
A structured set of questions on what TauLib actually proves, what 0 sorry means, what custom axioms are, the role of Mathlib, build reproduction, the Release Manifest, the trusted computing base, and where formal verification ends and bridge claims begin.
What does “machine-checked in Lean” mean here?
It means encoded formal statements compile under the pinned Lean environment, relative to Lean’s trusted kernel, disclosed assumptions, and current TauLib snapshot.
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.
Does TauLib prove the physical claims?
No. TauLib verifies formal obligations where encoded; it does not by itself prove empirical truth, bridge adequacy, semantic correspondence, or external scientific acceptance.
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.
What is the current formalization snapshot?
The current Release Manifest reports 512 Lean modules, 142,406 lines, 4,863 theorem/lemma declarations, 0 sorry assignments, and 3 custom axiom declarations.
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.
What is a `sorry`, and why does 0 `sorry` matter?
In Lean, `sorry` is a placeholder for an unfinished proof. A 0-sorry release means no explicit unfinished-proof placeholders remain in the pinned TauLib source.
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.
Does 0 `sorry` mean the theory is true?
No. It means the formalized Lean proofs have no explicit unfinished-proof placeholders; it does not settle bridge, semantic, empirical, or external-review questions.
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.
What are the custom axioms?
They are three explicit TauLib axiom declarations beyond Mathlib’s trusted base, all located in Book III spectral / number-theoretic bridge territory.
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.
Are the custom axioms hidden?
No. They are exposed through the Release Manifest, Custom Axiom Inventory, TauLib source, and `#print axioms` audit route.
Reviewers should inspect axiom declarations, run `#print axioms` on downstream declarations, and check whether theorem status labels reflect custom-axiom dependence.
What does “compute-then-axiomatize” mean?
It means a universal claim is finite-checked over an explicit computable envelope, but the unbounded universal step is still declared as an axiom rather than proved.
This pattern is explicit debt, not proof. It is acceptable only if named, bounded, reproducible, load-bearing, and reflected in downstream scope labels.
What is `#print axioms`, and why does it matter?
`#print axioms` is a Lean audit command that shows which axioms a declaration depends on, including custom axioms or `sorryAx` where present.
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.
What is the trusted computing base?
The trusted computing base is the underlying machinery a Lean proof depends on: Lean’s kernel, standard axioms, and any disclosed extensions such as `native_decide`.
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.
All 20 Technical Credibility entries →
The Right First Question
The right first question is not “should I already believe this?” The right first question is: is this a serious research program that has earned structured engagement?
Start by checking the research form, then choose an obligation, a construction step, or a result, trace its Corpus support, inspect the available formalization, identify bridge assumptions, and test its domain-specific accountability route.
Report Corrections
Found an error, a broken proof, a mis-stated numerical value, or a scope-label issue? We take corrections seriously and credit corrigendum contributors in the changelog.
Email: [email protected]
For structured review, technical inspection, or institutional review inquiries: [email protected]
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.