bmvPositiveTheorem
plain-language theorem explainer
Canonical inhabitant of the T3 package: the three algebraic facts that the 2×2 branch-amplitude determinant factors through the entangling phase Δφ, that Δφ ∈ (0, 2π) forces det ≠ 0 (hence entanglement), and the weak-field closed form for Δφ. Anyone citing Theorem 3 of Gravity IV uses this record. Construction is pure structure assembly of three already-proved lemmas.
Claim. There is a record packing three facts: (i) $\det A(\varphi_{LL},\varphi_{LR},\varphi_{RL},\varphi_{RR}) = \tfrac14 e^{-i(\varphi_{LR}+\varphi_{RL})}(e^{-i\Delta\varphi}-1)$ where $\Delta\varphi=\varphi_{LL}+\varphi_{RR}-\varphi_{LR}-\varphi_{RL}$; (ii) $0<\Delta\varphi<2\pi$ implies $\det A\neq 0$; (iii) in the weak field, $\Delta\varphi=(G m_1 m_2 T/\hbar)(1/r_{LL}+1/r_{RR}-1/r_{LR}-1/r_{RL})$.
background
Gravity IV formalizes the BMV two-mass, two-branch protocol under the linear cost-gradient channel of LedgerSuperposition. Each mass carries a Left/Right index, giving four definite branch states {LL, LR, RL, RR}. After gravitational interaction the joint state acquires per-branch phases φ_ab; the joint pure state is a product state iff the entangling combination Δφ := φ_LL + φ_RR − φ_LR − φ_RL is congruent to 0 mod 2π, equivalently iff the 2×2 amplitude matrix A has vanishing determinant.
The structure being inhabited packages the complete algebraic content of T3: the closed-form det A in terms of Δφ, the open-period entanglement witness (0 < Δφ < 2π ⇒ det A ≠ 0), and the weak-field formula for Δφ. Upstream, det_branchAmplitude_factored supplies the factored determinant; entangled_of_branchPhase_in_open_period is the paper's positivity statement on (0, T_rev); weakFieldBranchInvariant_eq is the Newtonian closed form.
proof idea
One-line structure inhabitant. The three fields of BMVPositiveTheorem are filled by direct assignment: det_formula := det_branchAmplitude_factored, entangled_open_period := entangled_of_branchPhase_in_open_period, and weakField_formula := weakFieldBranchInvariant_eq. No new reasoning; the def only witnesses that the three already-proved lemmas match the structure's field types.
why it matters
This is the canonical T3 package for Gravity IV (The Quantum Channel). Downstream, bmvPositiveTheorem_inhabited uses it to discharge Nonempty BMVPositiveTheorem, so any later development that needs "T3 is available" can cite the inhabited instance rather than reassemble the three lemmas. Within the Recognition gravity chain it sits after the linear cost-gradient channel (T2 / LedgerSuperposition) and before any quantitative entanglement-entropy or experimental-window claims: it converts the algebraic nonvanishing of Δφ into a reusable theorem object. Framework landmarks touched are the weak-field Newtonian phase (G m1 m2 T / ℏ times the inverse-radius combination) and the discrete revival set where entanglement can briefly vanish; the open-period witness is exactly the paper's positivity of entanglement entropy on (0, T_rev).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.