branchAmplitudeMatrix
plain-language theorem explainer
The 2×2 complex amplitude matrix for the Bose-Marletto-Vedral two-mass protocol after gravitational interaction. Each entry is one-half times a pure phase factor e^{-i φ_ab} on the four branch pairs LL, LR, RL, RR. Downstream entanglement witnesses and the BMV-positive theorem cite this matrix as the joint state in the Left/Right basis. The body is an explicit entrywise construction from the four real phases.
Claim. Given four real branch phases $\varphi_{LL},\varphi_{LR},\varphi_{RL},\varphi_{RR}$, form the $2\times 2$ complex matrix $A$ with entries $A_{ab}=\frac12\exp(-i\varphi_{ab})$ for $(a,b)\in\{L,R\}^2$. This is the post-interaction joint amplitude of two test masses that began in the equal-superposition product state $((|L\rangle+|R\rangle)/\sqrt{2})^{\otimes 2}$.
background
In the BMV two-mass two-branch protocol each test mass carries a Left/Right spatial index, so the joint Hilbert space has four definite branches {LL, LR, RL, RR}. This module packages Theorem 3 of Gravity from Recognition IV: The Quantum Channel: the linear cost-gradient channel of LedgerSuperposition imprints a real per-branch gravitational phase φ_ab, and 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 has vanishing determinant).
The initial product ((|L⟩+|R⟩)/√2) ⊗ ((|L⟩+|R⟩)/√2) puts amplitude 1/2 on every branch. After the interaction those amplitudes become (1/2) e^{-i φ_ab}. All later determinant identities and entanglement witnesses in the module are statements about this single matrix.
proof idea
Pure definition, no lemmas. Rows and columns are indexed by Fin 2 (0 for L, 1 for R). Each entry is the complex scalar 1/2 multiplied by exp(−I · φ), where φ is the matching real phase among the four arguments, selected by a four-way match on the index pair and coerced to ℂ. The construction is entrywise and closed-form.
why it matters
Carrier object for the whole of T3 (BMV-positive sign). Sibling results compute its determinant in closed form and prove det A = 0 iff Δφ ≡ 0 mod 2π, so nonzero determinant is the algebraic entanglement witness for pure two-qubit states. The structure BMVPositiveTheorem packages that witness under the weak-field phase formula.
The falsifier-band suite evaluates the same matrix at the named geometry and at any phases whose entangling invariant sits in [1/2, 7/10]: rs_bmv_witness_band, rs_bmv_geometry_entangled, bmv_band_entanglement, and clean_null_refutes_rs turn a measured product state (zero determinant) into a contradiction. same_branch_phases_same_BMV_witness records that the witness is a function of the four phases alone, so the package cannot discriminate RS from GR+QFT and remains a falsifier rather than a pillar-3 discriminator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.