t13_verified
plain-language theorem explainer
The t13_verified definition assembles the T13 certificate by supplying the geometric ratio of 13/12 derived from ledger edges plus time and the numerical agreement between predicted and observed late Hubble constant. Cosmologists working within Recognition Science ledger geometry would reference this certificate to close the Hubble tension derivation. The construction is a direct structure instance that pulls the two required fields from prior theorems in the same module.
Claim. The T13 certificate asserts that the Hubble ratio equals $13/12$ from the ledger topology and that $|H_{late,pred} - H_{late,exp}| / H_{late,exp} < 0.0005$.
background
The module derives the Hubble tension from the dual metric hypothesis in which the late-to-early ratio is 13/12, corresponding to the dynamic ledger (12 edges plus one time dimension) over the static ledger (12 edges). Dark energy density follows from the passive field volume fraction corrected by the fine-structure constant. The upstream theorem hubble_ratio_from_ledger establishes the ratio equality by simplification and normalization. The companion theorem hubble_ratio_match confirms the observational agreement to within 0.05 percent by direct computation of the predicted value 67.4 times 13/12 against the observed 73.04.
proof idea
The definition constructs the T13Cert structure by assigning the geometric_origin field to the result of hubble_ratio_from_ledger and the matches_observation field to the result of hubble_ratio_match. No additional tactics are required beyond the structure constructor.
why it matters
This definition supplies the verified instance of the T13 certificate that resolves the Hubble tension via the geometric ratio 13/12 and confirms the dark energy density prediction within one sigma of Planck data. It completes the formalization of the dual metric hypothesis presented in the module documentation. The certificate stands as the terminal object in the HubbleTension module, linking the ledger geometry to observable cosmology parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.