T13Cert
plain-language theorem explainer
T13Cert bundles the topological origin of the Hubble ratio as exactly 13/12 with the numerical check that the predicted late Hubble constant matches the observed value 73.04 to within 0.05 percent. Cosmologists working in the Recognition framework cite the structure to certify that the dual-metric hypothesis accounts for the tension between early and late measurements. The declaration is a plain structure definition that simply records these two properties.
Claim. The T13 certificate consists of the assertions that the topological Hubble ratio equals $13/12$ and that $|H_{late}^{pred} - 73.04| / 73.04 < 0.0005$, where $H_{late}^{pred}$ is defined by scaling the early Hubble constant by the ratio $13/12$.
background
The Cosmology.HubbleTension module derives the Hubble tension from the Dual Metric Hypothesis, which sets the late-to-early ratio at 13/12 because the dynamic ledger carries 12 edges plus one time dimension while the static ledger carries only 12 edges. The experimental late Hubble constant is fixed by definition as 73.04, and the predicted value is obtained by multiplying the early constant by the topological ratio 13/12. The same module also obtains the dark-energy density as the passive-field fraction 11/16 minus alpha/pi, yielding a prediction of 0.6852 that lies within 1 sigma of Planck data.
proof idea
The declaration is a structure definition whose two fields directly encode the required equality and the relative-error inequality. No lemmas are applied and no tactics are executed; the structure simply packages the two statements as its components.
why it matters
T13Cert supplies the certificate that feeds the verified instance t13_verified in the same module, thereby confirming that ledger geometry resolves the Hubble tension. It realizes the T13 step of the Recognition Science cosmology derivation, linking the simplicial ledger and the phi-ladder constants to observable cosmology while relying on the eight-tick octave for the underlying dimensional structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.