unitBridgeTheorem_inhabited
plain-language theorem explainer
The unit-bridge master witness for Gravity IV Theorem 4 is inhabited: positivity of α_RS, the identity κ_rs·α_RS = G/ℏ in RS-native units, and the SI BMV phase-rate closed form all hold together. Anyone citing the conditional T4 package (calibration input free) uses this existence fact. The proof is a one-constructor term that installs the already-built witness.
Claim. There exists a unit-bridge witness packing three facts: $\alpha_{\mathrm{RS}}>0$, $\kappa_{\mathrm{rs}}\,\alpha_{\mathrm{RS}}=G/\hbar$ in RS-native units, and for every external calibration input $U$ the SI BMV entangling phase rate admits the stated closed form in terms of $\kappa_{\mathrm{rs}}$, $\alpha_{\mathrm{RS}}$, and the geometry factor.
background
Gravity IV (The Quantum Channel) isolates a fourth load-bearing step: convert the dimensionless RS coupling $\kappa_{\mathrm{rs}}=8\varphi^5$, already banded in $(85.6,90.4)$, into a dimensionful BMV entangling phase rate readable in SI. In RS-native units one has $\hbar=\varphi^{-5}$ and $G=\varphi^5/\pi$, so $G/\hbar=\varphi^{10}/\pi$ is fixed by $\varphi$ alone. The BMV rate is $(G m_1 m_2/\hbar),g(r_{LL},r_{LR},r_{RL},r_{RR})$ with $g$ the inverse-distance geometry factor from the branch-phase invariant.
The master structure packages three obligations: positivity of $\alpha_{\mathrm{RS}}=\varphi^5/(8\pi)$; the algebraic identity $\kappa_{\mathrm{rs}},\alpha_{\mathrm{RS}}=G/\hbar$; and a universal SI closed form once an inhabitant of the external calibration type is supplied. Until that anchor is fixed, T4 remains conditional on the calibration input. The concrete witness is assembled upstream from the positivity lemma, the $\kappa\alpha$ identity, and the factored SI rate equality.
proof idea
One-line term proof. The structure is inhabited by the already-constructed value that fills its three fields with alphaRS_pos, kappa_rs_alphaRS_eq_G_over_hbar, and bmvPhaseRateSI_eq_kappa_alpha_factored. Nonemptiness is then the anonymous constructor around that value; no further tactics or rewriting.
why it matters
Closes the existence side of Gravity IV Theorem 4 (unit bridge from $\kappa_{\mathrm{rs}}$ to the SI BMV phase rate). Downstream consumers that need a single packaged T4 object rather than three separate lemmas can take any element of this nonempty type. It sits on the RS-native constants $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$ and on the $\varphi$-forced coupling band, linking Zero-Parameter Gravity to a tabletop quantum-channel observable. The calibration input remains the named open frontier of the dimensional bridge; this declaration does not discharge that anchor, only packages the proved algebraic and positivity content around it. No further used-by edges are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.