Pith. sign in
module module moderate

IndisputableMonolith.Gravity.NoGraviton.UnitBridge

show as:
view Lean formalization →

Unit-conversion layer from RS-native BMV phase rates to SI laboratory units, using the forced G/ℏ ratio and the entangling inverse-distance geometry. Gravity and quantum-channel workers cite it when stating no-graviton BMV predictions without free unit parameters. The module defines the native rate and SI factorization, proves positivity of the RS scale factor, and packages band endpoints in a named bridge theorem.

claimThe module introduces the BMV geometric factor $\Lambda=1/r_{LL}+1/r_{RR}-1/r_{LR}-1/r_{RL}$, the RS-native phase rate, the ratio $G/\hbar$ in RS units, and a positive RS scale $\alpha_{\mathrm{RS}}>0$. It proves the SI phase rate factors as $\kappa_{\mathrm{RS}}\,\alpha_{\mathrm{RS}}$ times geometry, records explicit band endpoints, and states the Unit Bridge theorem relating native and SI channels.

background

The Bose–Marletto–Vedral (BMV) protocol places two masses in spatial superpositions and asks whether gravity can generate entanglement. In Recognition Science, gravity is an emergent ledger cost rather than a force carrier (registry G-004, NoGraviton). Upstream, the BMV-Positive module (Gravity IV, Theorem 3) shows that the linear cost-gradient channel produces a generically nonzero entangling phase combination $\Delta\varphi$, so the joint state is non-product.

RS-native units fix $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^{5}/\pi$, with fundamental tick $\tau_0=1$. Laboratory statements need a clean bridge from those units to SI. This module supplies that bridge: the geometric factor is the inverse-distance combination $1/r_{LL}+1/r_{RR}-1/r_{LR}-1/r_{RL}$, and the phase rate is rewritten as a product of an RS coupling, a positive scale $\alpha_{\mathrm{RS}}$, and that geometry.

proof idea

Definitional front matter introduces the geometric factor, the native phase rate, $G/\hbar$ in RS units, and $\alpha_{\mathrm{RS}}$. Short equality lemmas identify the native rate with the RS coupling times geometry and prove $\kappa_{\mathrm{RS}},\alpha_{\mathrm{RS}}=G/\hbar$. Positivity of $\alpha_{\mathrm{RS}}$ is recorded separately. The SI rate is then defined and factored; band-endpoint lemmas bound the numerical window. A final Unit Bridge theorem packages the native-to-SI identification for downstream use. No deep tactic search: algebraic rewriting against Constants and the NoGraviton/BMV-Positive imports.

why it matters in Recognition Science

Feeds the Gravity Track 5.B audit in ZeroFreeParameters, whose doc-comment calls that module a structural theorem closing constants-from-$\varphi$ with zero sorry and zero RS-internal axiom. Without a unit bridge, BMV-positive phase predictions stay trapped in native units and cannot enter a zero-free-parameter ledger. The module therefore sits between G-004 (gravity emergent, no graviton mediator) and Gravity IV Theorem 3 (nonzero entangling $\Delta\varphi$), converting the quantum-channel sign result into SI-ready rates. It is the conversion hinge that lets the no-graviton story quote laboratory phase bands without introducing extra couplings.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (14)