bmvGeometryFactor
plain-language theorem explainer
The BMV geometric factor is the inverse-distance combination g = 1/r_LL + 1/r_RR − 1/r_LR − 1/r_RL on the four branch separations of the Bose–Marletto–Vedral protocol. Anyone deriving the RS-native or SI entangling phase rate cites it as the pure geometry multiplier in front of G m1 m2 / ℏ. It is a one-line definition with no proof obligations.
Claim. For real branch separations $r_{LL}, r_{LR}, r_{RL}, r_{RR}$, the BMV geometric factor is $g(r_{LL},r_{LR},r_{RL},r_{RR}) = \frac{1}{r_{LL}} + \frac{1}{r_{RR}} - \frac{1}{r_{LR}} - \frac{1}{r_{RL}}$.
background
Module Gravity IV (Unit Bridge) packages Theorem 4 of Gravity from Recognition IV: The Quantum Channel: convert the dimensionless RS coupling $\kappa_{rs} = 8\varphi^5$ into a dimensionful BMV entangling phase rate via an explicit RS-native-to-SI bridge.
In that setting the entangling invariant from T3 is $(G m_1 m_2 T/\hbar)\cdot g$, so the per-time rate is $(G m_1 m_2/\hbar)\cdot g$. Here $g$ is exactly the inverse-distance combination on the four branch pairs (LL, LR, RL, RR). RS-native constants fix $G=\varphi^5/\pi$ and $\hbar=\varphi^{-5}$, hence $G/\hbar=\varphi^{10}/\pi$ closed-form in $\varphi$ alone.
The four radii are treated as free real parameters; positivity and non-degeneracy are left to callers that assemble a full UnitBridgeInput.
proof idea
Pure definition: the body is the arithmetic expression $1/r_{LL}+1/r_{RR}-1/r_{LR}-1/r_{RL}$. No lemmas, no tactics, no unfolding.
why it matters
This factor is the geometry slot in every T4 rate formula. Downstream, BMVPhaseRateNative multiplies $(G m_1 m_2/\hbar)$ by it; bmv_phase_rate_native_eq rewrites that product as $(\varphi^{10}/\pi),m_1 m_2,g$; the SI master identity factors the rate as $U_{\mathrm{conv}}\cdot\kappa_{rs}\cdot\alpha_{RS}\cdot m_1 m_2,g$; and the band-endpoint theorem propagates the $\kappa_{rs}\in(85.6,90.4)$ interval linearly through the same $g$. The packaged UnitBridgeTheorem witness therefore depends on $g$ as the only geometry-dependent scalar. Without a named $g$, the closed-form and band claims cannot even be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.