weakFieldPhase
plain-language theorem explainer
Weak-field gravitational interaction phase between two masses at separation r, accumulated over time T: φ = G m₁ m₂ T / (ℏ r). Cited by anyone assembling the four BMV branch phases or the entangling combination Δφ. Pure definition equating the symbol to that monomial; no proof obligations.
Claim. The weak-field gravitational phase between masses $m_1$ and $m_2$ at separation $r$, accumulated over interaction time $T$, is $\varphi = \frac{G\, m_1\, m_2\, T}{\hbar\, r}$.
background
Module Gravity IV (BMV-Positive Sign, Theorem 3) treats the Bose–Marletto–Vedral two-mass, two-branch protocol. Each mass has a Left/Right spatial branch, so the joint configuration space is {LL, LR, RL, RR}. After gravitational interaction the joint amplitude acquires a per-branch phase φ_ab; the state is a product state iff the entangling combination Δφ = φ_LL + φ_RR − φ_LR − φ_RL is congruent to 0 mod 2π.
In the weak-field regime the phase on a single definite branch is the Newtonian interaction phase G m₁ m₂ T / (ℏ r). Here G and ℏ may be either the RS-native constants (G = λ_rec² c³/(π ℏ), ℏ = φ⁻⁵ in native units) or CODATA SI values, depending on the call site. The four branch separations r_ab are the geometric inputs; this definition supplies one scalar phase per separation.
proof idea
Definitional abbreviation only: the body is the single monomial G·m₁·m₂·T/(ℏ·r). No lemmas, tactics, or rewriting are involved.
why it matters
Atomic building block for the weak-field entangling invariant. Downstream, weakFieldBranchInvariant is exactly φ_LL + φ_RR − φ_LR − φ_RL with this phase on each arm, which is the quantity whose nonvanishing mod 2π forces a nonzero 2×2 branch-amplitude determinant and hence entanglement (the algebraic content of T3).
The BMVFalsifierBand module instantiates the same formula at a named SI geometry (phase_LL, phase_LR, phase_RL, phase_RR) and proves the exact rational value Δφ = 26696/47475 ≈ 0.562 rad, placing the protocol inside the open interval of positive entanglement entropy. Without this phase definition the weak-field specialization of the ledger-superposition channel cannot be written down.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.