weakFieldBranchInvariant
plain-language theorem explainer
The weak-field entangling invariant Δφ for a BMV two-mass, two-branch geometry: the alternating sum of gravitational phases on the four branch pairs LL, RR, LR, RL. Cited by the BMV-positive entanglement package and by the numerical falsifier-band evaluation. Defined as a four-term linear combination of the per-branch weak-field phase.
Claim. For coupling $G$, reduced Planck constant $\hbar$, masses $m_1,m_2$, interaction time $T$, and four branch separations $r_{LL},r_{LR},r_{RL},r_{RR}$, the weak-field entangling invariant is $\Delta\phi = \phi(r_{LL})+\phi(r_{RR})-\phi(r_{LR})-\phi(r_{RL})$, where $\phi(r)$ denotes the weak-field gravitational phase acquired on separation $r$.
background
Module Gravity IV packages Theorem 3 of Gravity from Recognition IV: The Quantum Channel. In the BMV protocol two test masses each carry a Left/Right spatial branch, giving four definite joint branches ${LL,LR,RL,RR}$. After gravitational interaction the joint state picks up a per-branch phase $\phi_{ab}$. The joint pure state is a product state if and only if the entangling combination $\Delta\phi=\phi_{LL}+\phi_{RR}-\phi_{LR}-\phi_{RL}$ is congruent to $0\bmod 2\pi$ (equivalently, the $2\times 2$ branch-amplitude matrix has vanishing determinant).
The linear cost-gradient channel of LedgerSuperposition supplies the weak-field phase on a single separation. The present definition assembles those four phases into $\Delta\phi$. Constants $G$ and $\hbar$ enter as free real parameters here; RS-native and CODATA projections are supplied upstream and are substituted only at numerical use sites.
proof idea
Pure definitional abbreviation: expand as the alternating sum of four calls to the single-branch weak-field phase on $r_{LL}$, $r_{RR}$, $r_{LR}$, and $r_{RL}$. No lemmas, no tactics. The closed-form identity that factors out $(G m_1 m_2 T/\hbar)$ times the geometric bracket $(1/r_{LL}+1/r_{RR}-1/r_{LR}-1/r_{RL})$ is the sibling theorem weakFieldBranchInvariant_eq, not this def.
why it matters
This is the concrete $\Delta\phi$ that Theorem 3 (BMV-positive sign) treats as the entanglement witness. Downstream, BMVPositiveTheorem packages the claim that whenever $\Delta\phi\in(0,2\pi)$ the amplitude-matrix determinant is nonzero and the joint state is entangled. The falsifier-band module instantiates the same def at SI/CODATA values to obtain deltaPhi, then proves the exact rational deltaPhi=26696/47475 (about $0.56$ rad), placing a named laboratory geometry strictly inside the open entanglement window. Without this packaging the weak-field formula of T3 would remain an informal combination of four phases rather than a named real that numerical and algebraic arguments can share.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.