det_ne_zero_iff_branchPhase_ne_zero
plain-language theorem explainer
The 2×2 BMV branch-amplitude determinant is nonzero exactly when the entangling phase combination Δφ is not an integer multiple of 2π. Gravity-channel and entanglement auditors cite this as the algebraic bridge from the phase invariant to non-product joint states. The proof factors the determinant and cancels two never-zero complex prefactors.
Claim. For real branch phases $\varphi_{LL},\varphi_{LR},\varphi_{RL},\varphi_{RR}$, let $\Delta\varphi=\varphi_{LL}+\varphi_{RR}-\varphi_{LR}-\varphi_{RL}$ be the entangling combination. The determinant of the associated $2\times 2$ branch amplitude matrix is nonzero if and only if $\exp(-i\Delta\varphi)\neq 1$ (equivalently, $\Delta\varphi\notin 2\pi\mathbb{Z}$).
background
This sits in Gravity IV (BMV-Positive Sign, Theorem 3). In the Bose–Marletto–Vedral two-mass, two-branch protocol, each mass carries a Left/Right index, giving four definite joint branches ${LL,LR,RL,RR}$. After the gravitational interaction the joint pure state acquires per-branch phases $\varphi_{ab}$.
The branch amplitude matrix packages those four complex amplitudes (normalized by $1/2$) as a $2\times 2$ matrix. Its determinant vanishes precisely when the joint state factors as a product. The entangling invariant is the combination $\Delta\varphi=\varphi_{LL}+\varphi_{RR}-\varphi_{LR}-\varphi_{RL}$. An upstream factorization lemma writes the determinant as $(1/4),e^{-i(\varphi_{LR}+\varphi_{RL})}(\exp(-i\Delta\varphi)-1)$, so nonvanishing reduces to the phase factor not equaling $1$.
The module goal is the algebraic half of T3: nonzero $\Delta\varphi\bmod 2\pi$ yields a non-product two-qubit state (and hence positive entanglement entropy) outside discrete revival times.
proof idea
Rewrite the determinant via the factored form $(1/4)\cdot e^{-i(\varphi_{LR}+\varphi_{RL})}\cdot(\exp(-i\Delta\varphi)-1)$. Record that the constant $1/4$ is nonzero and that the complex exponential never vanishes.
Both directions of the biconditional are then pure ring arithmetic on $\mathbb{C}$. If the determinant is nonzero but $\exp(-i\Delta\varphi)=1$, the factored expression collapses to zero, contradiction. Conversely, if the product vanishes while the two leading factors are nonzero, mul_eq_zero forces $\exp(-i\Delta\varphi)-1=0$, i.e. the phase factor equals $1$. No analysis beyond complex exponential nonvanishing is used.
why it matters
This is the algebraic core of the BMV-positive package. The immediate parent is the entanglement witness: whenever $\exp(-i\Delta\varphi)\neq 1$, the branch amplitude determinant is nonzero, so the corresponding two-qubit pure state is not a product state. That witness is the load-bearing step of Theorem 3 in Gravity from Recognition IV: The Quantum Channel.
Together with the weak-field evaluation of $\Delta\varphi$ (proportional to $Gm_1 m_2 T/\hbar$ times a geometric combination of inverse separations), it converts a nonzero cost-gradient channel into strictly positive entanglement entropy for all interaction times short of revival. In the broader Recognition chain this is the quantum-channel half of the gravity story: ledger superposition produces a branch-dependent phase whose entangling combination is generically nonzero, matching the BMV prediction that gravity can mediate entanglement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.