BMV_coupling_pos
plain-language theorem explainer
The Bose–Marletto–Vedral entanglement coupling in RS units is strictly positive, so gravity-mediated entanglement is generated rather than suppressed. Cited by anyone assembling the no-graviton certificate or quoting the BMV rate prediction. Proof is a one-line identification with the already-proved positivity of κ_rs.
Claim. The BMV entanglement coupling equals the RS gravitational coupling $\kappa_{\mathrm{rs}}$, and $0 < \kappa_{\mathrm{rs}}$.
background
Module G-004 formalizes the RS answer to “is there a graviton?”: gravity is emergent ledger curvature, not a spin-2 force carrier. Three concrete claims are packaged: κ algebraic in φ alone, two GW polarizations in D=3, and a falsifiable BMV entanglement rate.
In this file the BMV coupling is defined to be exactly $\kappa_{\mathrm{rs}}$ from ZeroParameterGravity. Upstream, $\kappa_{\mathrm{rs}} = 8\varphi^5$ with $\varphi>0$, and kappa_pos already records $0<\kappa_{\mathrm{rs}}$ by multiplying the positive factors 8 and $\varphi^5$. Positivity is the minimal physical content needed for “entanglement should be generated.”
proof idea
One-line term proof: BMV_coupling unfolds to ZeroParameterGravity.kappa_rs, so the goal is identical to kappa_pos. The declaration is therefore just the alias := ZeroParameterGravity.kappa_pos. No new arithmetic is performed here; the work sits in the upstream proof that unfolds $\kappa_{\mathrm{rs}}$ and applies mul_pos to $8$ and pow_pos phi_pos 5.
why it matters
Feeds the certificate field bmv_pos inside no_graviton_cert, which bundles emergent gravity, algebraic κ, integer-φ power form, two GW polarizations, and BMV positivity into one NoGravitonCert record.
In the module narrative this is claim 3 of G-004: the BMV rate is a concrete RS prediction ($\kappa_{\mathrm{rs}}\approx 88.7$, band roughly (85.6, 90.4) in a sibling comment) that distinguishes emergent ledger gravity from particle-mediated gravity. Positivity is the qualitative half of that prediction: the coupling cannot vanish or flip sign, so an entanglement-generation experiment is in principle sensitive. Landmark link: κ is forced from the cost side (φ-ladder / T6 fixed point), not from a gauge generator, which is why “no graviton” is a category claim rather than a missing particle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.