UnitBridgeInput
plain-language theorem explainer
A unit-bridge input packages the SI conversion scale and tabletop BMV geometry needed to turn the RS-native entangling phase rate into an SI prediction. Anyone citing Gravity IV Theorem 4 (quantum channel unit bridge) uses this bundle as the calibration-and-masses hypothesis. It is a plain structure of positive reals: one conversion factor, two masses, and four nonzero branch separations. No proof content; pure data packaging for conditional T4 statements.
Claim. A unit-bridge input consists of a positive SI conversion scale $U_{\mathrm{conv}} > 0$, two positive test masses $m_1, m_2 > 0$, and four nonzero branch separations $r_{LL}, r_{LR}, r_{RL}, r_{RR} \neq 0$. These data parameterize conversion of the RS-native BMV phase rate into SI units via the external calibration map.
background
Gravity IV formalizes the quantum-channel unit bridge: the dimensionless RS coupling $\kappa_{rs} = 8\varphi^5$ (band $(85.6, 90.4)$) converts to a 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 $(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 SI value needs an external dimensional calibration (seconds per tick, meters per voxel, and so on). That map is the named open frontier in the RS-native units module; the conversion map itself is closed elsewhere, but the numerical anchor is external by dimensional analysis. Until an anchor is supplied, T4 remains conditional on calibration input.
This structure records exactly that input: the positive scale $U_{\mathrm{conv}}$, the two SI masses, and the four nonzero branch separations. Masses are ordinary reals in the RS-native units abbreviation; positivity and nonzeroness are field hypotheses so downstream rate formulas stay well-defined.
proof idea
No proof: this is a structure definition. Fields are four pairs of real data plus positivity or nonzeroness witnesses ($U_{\mathrm{conv}}$, $m_1$, $m_2$ positive; each $r_{ab}$ nonzero). Downstream definitions read the fields directly; there is no algebraic reduction or tactic script at this declaration.
why it matters
This is the hypothesis package for Gravity IV Theorem 4. The SI phase-rate definition multiplies $U_{\mathrm{conv}}$ by the closed-form native rate $(\varphi^{10}/\pi), m_1 m_2 g$. The master closed-form theorem rewrites that product as $U_{\mathrm{conv}}\cdot\kappa_{rs}\cdot\alpha_{RS}\cdot m_1 m_2 g$, and the band-propagation theorem pushes the $\kappa_{rs}$ interval $(85.6,90.4)$ linearly onto an SI rate band at fixed calibration and geometry.
The master witness structure packages positivity of $\alpha_{RS}=\varphi^5/(8\pi)$ and the identity $\kappa_{rs}\cdot\alpha_{RS}=G/\hbar$ together with this input type, making T4 a conditional theorem in the calibration. Framework landmarks in play: RS-native $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$, and the $\varphi$-ladder constants that fix $G/\hbar$ without free parameters. The remaining open question is supplying a concrete external calibration inhabitant; until then every SI numerical claim stays conditional on $U_{\mathrm{conv}}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.