Pith. sign in
module module high

IndisputableMonolith.Gravity.QuantumChannel.BMVPositive

show as:
view Lean formalization →

Formalizes the BMV (Bose–Marletto–Vedral) post-interaction amplitude matrix and proves that a nonzero branch-phase invariant forces entanglement of the joint state. Gravity-channel workers cite it for the certified positivity/entanglement witness used by the SI unit bridge and the falsifier-band package. The argument factors the determinant of the 2×2 branch-amplitude matrix and links det ≠ 0 to a nonzero phase invariant on the four LL/LR/RL/RR branches.

claimIn the BMV protocol the post-interaction joint state is encoded by the $2\times 2$ complex amplitude matrix whose entries are $(1/2)\,e^{-i\varphi_{ab}}$ for branches $(a,b)\in\{LL,LR,RL,RR\}$. The branch-phase invariant is nonzero if and only if $\det$ of that matrix is nonzero, which implies the joint state is entangled. In the weak-field regime the same invariant reduces to an explicit function of the four weak-field phases.

background

The module sits in Gravity IV (The Quantum Channel). Upstream, Ledger Superposition supplies the Hilbert carrier: the recognition state space is a complex Hilbert space and the one-tick update is $\mathbb{C}$-linear, so branch amplitudes and phases are well-defined linear data rather than classical labels.

BMV places two masses, each prepared in a spatial superposition $(|L\rangle+|R\rangle)/\sqrt{2}$, into gravitational interaction and asks whether the joint state becomes entangled. The four classical trajectories LL, LR, RL, RR acquire phases $\varphi_{ab}$. The joint amplitude matrix is then $(1/2)$ times the diagonal of those phase factors in the product basis; entanglement is equivalent to that matrix having nonzero determinant (equivalently, a nonzero branch-phase invariant).

Weak-field specializations replace the abstract phases by the linearized gravitational phases used in tabletop proposals, so the same invariant becomes an explicit weak-field formula.

proof idea

Definitions introduce the branch-amplitude matrix, the scalar branch-phase invariant, and the weak-field phase map. Algebraic lemmas factor the determinant of the amplitude matrix and prove $\det\neq 0$ iff the phase invariant is nonzero. Entanglement theorems then apply the standard criterion that a pure bipartite state with that amplitude matrix is entangled precisely when the determinant (hence the invariant) is nonzero, including an open-period version that keeps the phase away from lattice points. The weak-field block equates the abstract invariant to its linearized expression. The headline BMVPositiveTheorem packages the nonzero-invariant $\Rightarrow$ entangled implication for downstream use.

why it matters in Recognition Science

This module is the certified entanglement witness for the RS quantum-channel story of gravity. UnitBridge imports it to connect the dimensionless RS coupling $\kappa_{rs}=8\varphi^5$ (band from ZeroParameterGravity) to the dimensionful BMV entangling phase rate in SI units (Theorem 4 of Gravity IV). BMVFalsifierBand imports it to build the falsifier floor and certified witness band; that downstream package is explicitly excluded from the pillar-3 discriminator because any quantum mediator predicts BMV entanglement, but it still needs this positivity theorem as the mathematical core of the witness.

Within the broader forcing chain the module does not touch T5–T8 directly; it consumes the ledger-superposition Hilbert structure and feeds the experimental interface of the quantum channel.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (13)