T6T8_To_CosmologyConstants_Bridge
plain-language theorem explainer
A certificate interface packaging how φ-forcing and D=3 forcing feed the active cosmology constants: the exact η_B rung −44 (three routes), the η_B prefactor band, Ω_Λ via 11/16−α/π, and g★=427/4. Cosmologists and RS auditors cite it to separate theorem-backed identities from empirical bands. As a Prop structure it is pure interface; the companion inhabitance theorem fills each field from T6/T8 and the cosmology modules.
Claim. Given that $\varphi$ is forced (unique positive root of $r^2=r+1$) and that spatial dimension $D=3$ is the unique RS-compatible dimension, the following hold as a single bridge certificate: $\varphi$-uniqueness is available for rung cosmology; $D$ is uniquely closed; the baryon asymmetry exact rung equals $-44$ by three agreeing routes (dimension, chirality, fermionic); the $\eta_B$ prefactor is $(1-\varphi^{-8})^2$ with corrected band in $(6.0,6.2)\times 10^{-10}$; $\Omega_\Lambda^{\mathrm{RS}}=11/16-\alpha_{\mathrm{CODATA}}/\pi$ lies in $(0,11/16)$; $g_\star=427/4$ matches the baryogenesis DOF count; and no unnamed B22 surface is promoted.
background
The Unified Forcing Chain module derives T0–T8 as inevitabilities from the Recognition Composition Law plus normalization and calibration. T6 states that in a discrete ledger with self-similar cost, the only positive scaling ratio is $\varphi=(1+\sqrt{5})/2$, the unique solution of $x^2=x+1$. T8 states that spatial dimension is not free: $D=3$ is the unique value compatible with nontrivial linking, the eight-tick $2^D=8$ sync, and gap-45 synchronization.
Cosmology constants in RS sit on the $\varphi$-ladder and on $D$-dependent gap/chirality counts. The baryon asymmetry $\eta_B$ splits into an exact rung identity (three independent routes converge on $-44$) and a separate prefactor surface with an empirical band. $\Omega_\Lambda$ is given by a closed formula that still imports measured $\alpha_{\mathrm{CODATA}}$ as the one external anchor. $g_\star$ is the SM relativistic DOF count at high $T$, assembled as $427/4=106.75$.
This structure does not re-derive those cosmology modules; it records that T6 and T8 supply the scalar and dimensional inputs those surfaces need, and that empirical bands stay labeled as bands.
proof idea
No proof body: the declaration is a structure ... : Prop whose fields are the bridge obligations. Each field is a named proposition (uniqueness of $\varphi$, unique RS-compatible dimension, Nonempty certificates for $\eta_B$ rung and prefactor and $g_\star$, equalities for rung $-44$, prefactor $(1-\varphi^{-8})^2$, $\Omega_\Lambda$ formula and bounds, $g_\star$ match, and a trivial guard True that B22 is not silently promoted).
Inhabitation is deferred to the companion theorem t6_t8_to_cosmology_constants_bridge_holds, which projects phi_unique from the T6 hypothesis and unique_dimension from the T8 hypothesis, then fills the cosmology fields from the corresponding derivation certificates. A Subsingleton instance makes any two inhabitants definitionally equal.
why it matters
In the complete inevitability chain, T6 and T8 are not ornamental: they are the scalar and dimensional sources for rung cosmology. This bridge is the explicit handoff from those forcing levels into $\eta_B$, $\Omega_\Lambda$, and $g_\star$, so the top-level CompleteForcingChain can claim constants are routed through theorem-backed surfaces rather than free parameters.
Framework landmarks in play: T6 $\varphi$ as the self-similar fixed point; T8 $D=3$ (and the linked T7 eight-tick octave $2^3$); mass/asymmetry rungs on the $\varphi$-ladder; $\alpha$ kept as the measured CODATA anchor inside the $\Omega_\Lambda$ formula, consistent with RS treating exact $\alpha$ as a boundary datum. The structure deliberately keeps exact identities (rung $-44$, $g_\star=427/4$, $\Omega_\Lambda$ algebraic form) separate from empirical bands ($\eta_B$ corrected window), and refuses to promote an absent B22 surface.
Downstream, CompleteForcingChain includes this bridge among the forced layers; the inhabitance theorem is the local discharge step auditors check first.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.