weakFieldBranchInvariant_eq
plain-language theorem explainer
Closed-form evaluation of the weak-field BMV entangling invariant Δφ as (G m₁ m₂ T / ℏ) times the signed sum of inverse branch separations. Anyone assembling the T3 entanglement witness for the two-mass two-branch protocol cites this identity. The proof unfolds the weak-field phase definitions and clears denominators by field simplification.
Claim. Let $G,\hbar,m_1,m_2,T,r_{LL},r_{LR},r_{RL},r_{RR}\in\mathbb{R}$ with $\hbar\neq 0$ and all four separations nonzero. The weak-field entangling invariant equals $\frac{G m_1 m_2 T}{\hbar}\Bigl(\frac{1}{r_{LL}}+\frac{1}{r_{RR}}-\frac{1}{r_{LR}}-\frac{1}{r_{RL}}\Bigr)$.
background
Gravity IV packages Theorem 3 of the quantum-channel paper: in the BMV two-mass, two-branch protocol the linear cost-gradient channel imprints a per-branch gravitational phase φ_ab on the four definite states {LL, LR, RL, RR}. The joint pure state is a product state if and only if the entangling combination Δφ = φ_LL + φ_RR − φ_LR − φ_RL is congruent to 0 mod 2π (equivalently, the 2×2 branch-amplitude matrix has vanishing determinant).
In the weak-field regime each phase is proportional to G m₁ m₂ T / (ℏ r_ab). The module therefore defines a weak-field phase for each branch separation and packages their alternating sum as the weak-field branch invariant. The constants G and ℏ that appear may be either the RS-native projections (G = λ_rec² c³/(π ℏ), ℏ = φ⁻⁵ in native units) or CODATA placeholders; the algebraic identity is independent of that choice.
Upstream, the ledger-superposition channel supplies the linear cost-gradient that justifies writing φ_ab ∝ 1/r_ab. The present lemma simply evaluates the resulting four-term combination in closed form.
proof idea
Term-mode proof by definitional reduction. Unfold the weak-field branch invariant (the alternating sum of the four weak-field phases) and the weak-field phase itself (each phase is G m₁ m₂ T /(ℏ r)). After unfolding, the goal is an equality of rational expressions in the eight real parameters. A single field_simp clears the nonzero denominators (using ℏ ≠ 0 and r_ab ≠ 0) and rearranges to the factored form (G m₁ m₂ T / ℏ) · (1/r_LL + 1/r_RR − 1/r_LR − 1/r_RL).
why it matters
This identity is the weak-field formula slot of the master witness bmvPositiveTheorem, which packages the full algebraic content of T3: determinant formula for the branch-amplitude matrix, entanglement outside the discrete revival set, and the explicit weak-field expression for Δφ. The module doc lists it as branchPhase_weakField: once Δφ is known in closed form, non-degeneracy of the BMV geometry (the parenthesis nonzero) immediately yields Δφ ≠ 0 mod 2π on (0, T_rev), hence det A ≠ 0 and a non-product joint state.
Within Recognition Science the result sits on the gravity side of the quantum channel: the same G and ℏ that appear in the RS-native bridge (G = φ⁵/π, ℏ = φ⁻⁵ in native units) feed the phase, so the entanglement witness is expressed entirely in recognition constants. It does not itself force D = 3 or the eight-tick octave; those enter earlier when the ledger geometry is fixed. The lemma closes the algebraic half of T3; geometric non-degeneracy of concrete BMV separations remains a hypothesis on the r_ab.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.