bmv_positive_unconditional
plain-language theorem explainer
Names the unconditional BMV clause: any pure two-qubit state with unit Frobenius norm and positive concurrence has strictly positive reduced von Neumann entropy. Gravity-track authors cite it as one of the twelve conjuncts in the RS quantum-gravity master statement. The body is a pure definitional alias of the carried proposition.
Claim. The proposition asserting that for every $2\times 2$ complex matrix $A$ with $\sum_{i,j}|A_{ij}|^2=1$, if the concurrence of $A$ is strictly positive then the von Neumann entropy of the reduced density matrix of $A$ is strictly positive.
background
Gravity Track 7.A authors the master quantum-gravity statement as a twelve-clause conjunction. Closed clauses are inhabited by existing theorems; open ones remain hypothesis inputs. This declaration is the named Prop for the BMV (two-qubit entanglement entropy) positivity clause inside that conjunction.
The carried content quantifies over pure two-qubit amplitude matrices $A\in\mathbb{C}^{2\times 2}$ of unit Frobenius norm. Concurrence is the standard Wootters entanglement monotone; the reduced von Neumann entropy is $S(\rho_A)=-\mathrm{Tr}(\rho_A\log\rho_A)$ after partial trace. The upstream carried proposition states exactly: unit-norm and positive concurrence imply strictly positive reduced entropy.
The witness theorem lives in Quantum.PureTwoQubit.EntropyConcurrence and is already unconditional (no extra RS hypotheses).
proof idea
Definitional one-liner: the Prop is definitionally equal to the carried proposition bmv_positive_unconditional_carried_prop. No tactics, no lemmas applied at this site. Inhabitation is deferred to the sibling theorem that applies pure_two_qubit_entropy_positive_unconditional.
why it matters
Fills the BMV-positivity slot in RSQuantumGravityMaster, the Track 7.A master statement matching the master-plan template verbatim: the third block is (amplitude_linear_forced ∧ bmv_positive_unconditional). Downstream, bmv_positive_unconditional_proven inhabits it, and the non-circularity audit uses both bmv_clause_is_carried (definitional equality) and bmv_clause_holds to certify that this closed clause is genuinely carried rather than a True placeholder.
In the RS gravity program this clause records that entanglement (positive concurrence) forces positive reduced entropy for pure two-qubit states, a quantum-information ingredient of the quantum-gravity discovery package. It does not itself close the five still-open hypothesis inputs (Regge–EH continuum, amplitude linearity unconditional, Page curve, PTA, strong-field tests).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.