entangled_of_branchPhase_nonzero
plain-language theorem explainer
Algebraic entanglement witness for the BMV two-mass protocol: if the entangling phase combination Δφ is not an integer multiple of 2π, the 2×2 branch amplitude matrix has nonzero determinant, so the joint two-qubit pure state is not a product state. Anyone proving positivity of entanglement entropy outside revival times (paper Theorem 3) cites this. Proof is a one-line rewrite through the determinant–phase equivalence lemma.
Claim. For real branch phases $\varphi_{LL},\varphi_{LR},\varphi_{RL},\varphi_{RR}$, write $\Delta\varphi=\varphi_{LL}+\varphi_{RR}-\varphi_{LR}-\varphi_{RL}$. If $\exp(-i\Delta\varphi)\neq 1$, then the determinant of the corresponding $2\times 2$ branch amplitude matrix is nonzero (hence the joint pure state is not a product state).
background
This module packages the algebraic content of Gravity IV Theorem 3 (BMV-positive sign). Two test masses each carry a Left/Right branch index, giving four definite branch states {LL, LR, RL, RR}. After the gravitational interaction the joint state acquires per-branch phases φ_ab. 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 amplitude matrix built from the four complex branch amplitudes has vanishing determinant.
The sibling definitions supply the matrix and the invariant: the branch amplitude matrix has entries proportional to exp(−i φ_ab), and the branch-phase invariant is exactly Δφ. An upstream factorization shows that the determinant equals (1/4)(e^{−i(φ_LL+φ_RR)} − e^{−i(φ_LR+φ_RL)}), so det = 0 precisely when exp(−i Δφ) = 1. The present theorem is the entanglement-direction half of that equivalence: nonzero phase exponential forces nonzero determinant.
proof idea
One-line term proof. Rewrite the goal by the sibling biconditional that the branch-amplitude determinant is nonzero if and only if exp(−i Δφ) ≠ 1; the hypothesis is then exactly the rewritten goal. No further arithmetic is needed.
why it matters
This is the algebraic entanglement witness named in the module doc: the joint state is non-product whenever Δφ ≠ 0 mod 2π. It is the immediate parent of entangled_of_branchPhase_in_open_period, which specializes to the open interval 0 < Δφ < 2π and is the form used in the paper's Theorem 3 (strict positivity of entanglement entropy on (0, T_rev)). Together with the weak-field evaluation of Δφ (proportional to G m1 m2 T/ℏ times the usual BMV distance combination), it closes the chain from the linear cost-gradient channel of LedgerSuperposition to a concrete non-product two-qubit state outside discrete revival times. In the broader RS gravity program it is the pure-state half of the claim that the recognition channel produces observable entanglement, not merely a classical phase.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.