hubble_ratio_denominator_origin
plain-language theorem explainer
The equality certifies that the denominator twelve in the normalized early-universe Hubble parameter equals three times four. Cosmologists using the dual-metric ledger cite this step when grounding H_early = 12/12 = 1 in the static ledger. The proof reduces to a single numerical normalization.
Claim. The denominator of the normalized early-universe Hubble parameter satisfies $12 = 3 times 4$, where the factor of three counts the spatial dimensions and four counts the parallel edges along each dimension.
background
The module resolves the Hubble tension by positing two distinct metrics in the RS ledger. The static ledger (early universe) sets H_early = 12/12 = 1, with the twelve arising from the cube edge count in D = 3 dimensions. The dynamic ledger (late universe) yields H_late = 13/12, producing the predicted ratio 13/12 that matches the observed 73.04/67.4 to within 0.04%. The module imports the fundamental period abbreviation T from Breath1024 and the triangular-number definition from Gap45.SyncMinimization.
proof idea
The proof is a one-line wrapper that applies the norm_num tactic to confirm the rational equality.
why it matters
This equality supplies the explicit origin of the denominator in T-001.3 of the Hubble Tension Certificate. It supports the sibling claims hubble_ratio_exact and hubble_tension_is_prediction by anchoring the factor twelve in the three-dimensional geometry of the static ledger. The result aligns with the forcing-chain step that fixes D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.