unitBridgeTheorem
plain-language theorem explainer
Packages the three load-bearing facts of the RS-to-SI unit bridge into one witness: positivity of α_RS, the identity κ_rs · α_RS = G/ℏ in RS-native units, and the closed-form SI BMV phase rate under any calibration input. Anyone citing Theorem 4 (Gravity IV quantum channel) uses this bundle. The construction is a pure structure inhabitant wiring three already-proved lemmas.
Claim. There is a unit-bridge witness consisting of: (i) $0 < \alpha_{RS}$ with $\alpha_{RS} = \varphi^5/(8\pi)$; (ii) $\kappa_{rs}\,\alpha_{RS} = G/\hbar$ in RS-native units; (iii) for every calibration input $U$, the SI BMV entangling phase rate equals $U_{\mathrm{conv}}\cdot\kappa_{rs}\cdot\alpha_{RS}\cdot m_1 m_2\cdot g(r_{LL},r_{LR},r_{RL},r_{RR})$.
background
Gravity IV formalizes the unit bridge from the dimensionless RS coupling $\kappa_{rs} = 8\varphi^5$ (band roughly $(85.6, 90.4)$) to the dimensionful BMV entangling phase rate. 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 $d\Phi/dT = (G m_1 m_2/\hbar), g$, where $g$ is the geometry factor from the branch-phase invariant (T3). The SI value composes that native expression with an external calibration $U$ (an inhabitant of ExternalCalibration); until an anchor is fixed, T4 remains conditional on $U$.
The structure being inhabited records three facts: positivity of $\alpha_{RS} = \varphi^5/(8\pi)$, the product identity $\kappa_{rs},\alpha_{RS} = G/\hbar$, and the factored SI closed form $U_{\mathrm{conv}}\cdot\kappa_{rs}\cdot\alpha_{RS}\cdot m_1 m_2\cdot g$.
proof idea
One-line structure construction. Field alpha_pos is filled by alphaRS_pos (unfold $\alpha_{RS}$ and use positivity of $\varphi^5$ and of $8\pi$). Field kappa_alpha_identity is filled by kappa_rs_alphaRS_eq_G_over_hbar, which reduces $(8\varphi^5)\cdot(\varphi^5/(8\pi))$ to $G/\hbar$ via the native identity $G/\hbar = \varphi^{10}/\pi$. Field si_closed_form is filled by bmvPhaseRateSI_eq_kappa_alpha_factored, the T4 master closed form under any UnitBridgeInput.
why it matters
This is the packaged T4 master witness for Gravity IV (the quantum channel paper): the RS-native coupling converts to a tabletop SI BMV phase rate once a calibration input is supplied. Downstream, unitBridgeTheorem_inhabited simply records Nonempty UnitBridgeTheorem by pointing at this definition, so any later development that needs "T4 is inhabited" cites the nonempty theorem rather than the three lemmas separately.
Framework landmarks in play: RS-native constants $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$, and the zero-parameter gravity band on $\kappa_{rs}$. The open frontier remains the external SI anchor; the conversion map itself is closed in the SI-bridge foundation, but the numerical anchor is external by dimensional analysis. This definition does not close that frontier; it only bundles the proved algebraic content of the bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.