Predictions

What This Page Catalogs

This page frames predictions as verification targets. The detailed current prediction catalogue remains in the Results lane, where each prediction is part of a result family and can be read with its domain context.

Required Metadata for a Prediction Target

For each prediction surface, the program should expose:

• prediction ID
• related result ID
• related Corpus support
• domain
• type: structural, empirical, or hybrid
• current status
• linked falsification path where available

Current Public Surfaces

• Physics Predictions Browse
• Prediction Timing Ledger
• Fit-Space Argument
• Falsification Pack

Predictions ↔ Lean linkage (transitive chain)

Every public prediction in the program references a Corpus registry object via its registry_id frontmatter. Every referenced registry object names a TauLib Lean module and a specific Lean theorem name. The prediction → registry → TauLib chain is end-to-end traceable for 100% of currently public predictions.

The chain is transitive (prediction → registry → Lean), not direct (prediction → Lean) — by design. The Corpus registry is the canonical naming layer; predictions are the empirical-projection layer; TauLib is the formal-evidence layer. Linking predictions directly to Lean would couple two layers that should remain independently revisable.

Worked example — the chain in full

One prediction, four hops, no hand-waving. Read top-to-bottom; every line is the canonical identifier.

What the theorem actually says (V.T85, plain reading). For a disk galaxy with exponential surface density, the rotation velocity satisfies v_c(r) → v_∞ = (G · M_b · c² / (2 · ℓ_τ))^(1/4) at large radius — i.e. asymptotically flat rotation curves emerge from the τ-capacity gradient without invoking a dark-matter halo. Raising both sides to the fourth power gives the BTFR v_∞⁴ ∝ M_b with τ-fixed slope = 4 (kernel value; 3.991 is the benchmark-fit estimator over the 20-galaxy table, distinct from the kernel slope by < 0.01). The benchmark binding benchmark_T85_planck discharges V.T85 against the Planck-anchored mass calibration used in V.D258.

Falsification condition (1 line). A pre-registered re-fit on a comparable rotation-curve sample (≥ 20 galaxies, similar mass span) returning a BTFR slope outside [3.85, 4.15], or an RMS scatter > 0.15 dex once measurement floors are subtracted, kills V.T85 at this scope and propagates upward — the τ-BTFR derivation has no free parameter to absorb the residual. Cross-reference the Falsification Pack for the corresponding falsification record.

To audit independently. lake build TauLib.BookV.Astrophysics.RotationCurves resolves both benchmark_T85_planck and FlatRotationCurveTheoremVt37 against the formal kernel; #print axioms Tau.BookV.Astrophysics.benchmark_T85_planck enumerates the disclosed custom axioms (TauLib commits to 0 sorry, with custom axioms tracked in the release manifest). Pin to the manifest commit SHA to reproduce.

What the chain does and does not establish

The chain says: every public prediction lands on a named theorem, in a named module, in a public repo. The Lean work is not parallel to the predictions; it underwrites them. The derivation is version-controlled and pinned to the release manifest — auditable independently from the empirical adjudication.

The chain does not say: that the τ-framework is empirically true, that any single prediction has been confirmed, or that formal-kernel correctness implies physical correctness. Those are separate claims under separate verification regimes — see Scientific Rigor for the boundary discipline.