bmv_positive_unconditional_carried_prop
plain-language theorem explainer
Packages the BMV positivity clause for the quantum-gravity master theorem: every normalized pure two-qubit amplitude matrix with positive Wootters concurrence has strictly positive reduced von Neumann entropy. Gravity-track auditors and the non-circularity certificate cite this as the carried proposition behind that master clause. The body is a pure Prop definition; the content is witnessed externally by the pure two-qubit entropy positivity theorem.
Claim. For every $2\times 2$ complex matrix $A$ with Frobenius norm $\sum_{i,j}|A_{ij}|^2=1$, if the Wootters concurrence $C(A)=2|\det A|$ is strictly positive, then the von Neumann entropy of the reduced density matrix of $A$ is strictly positive.
background
The Gravity.MasterTheorem module authors the twelve-clause master statement of the RS quantum-gravity discovery (Track 7.A). Closed clauses appear as named Props inhabited by existing theorems; open ones remain hypothesis inputs. This definition is the carried form of the BMV positivity clause.
In the pure two-qubit setting, $A\in M_2(\mathbb{C})$ with unit Frobenius norm is a pure bipartite amplitude matrix. Upstream, concurrence is the Wootters quantity $C(A)=2|\det A|$, and reducedDensityVonNeumannEntropy is the von Neumann entropy of one reduced density matrix after partial trace. The BMV claim asserts that positive concurrence forces positive entropy with no extra structural hypotheses.
The doc-comment points to the witnessing theorem pure_two_qubit_entropy_positive_unconditional in Quantum.PureTwoQubit.EntropyConcurrence as the actual proof that this Prop holds.
proof idea
Definition, not a proved theorem. The body is the universal quantification over normalized $2\times 2$ complex matrices linking positive concurrence to positive reduced entropy; no tactics fire. Mathematical content is discharged elsewhere by pure_two_qubit_entropy_positive_unconditional. The sibling alias bmv_positive_unconditional simply renames this Prop for the master conjunction.
why it matters
Feeds the master theorem BMV-positivity clause. Downstream, bmv_positive_unconditional is definitionally equal to this Prop, and bmv_clause_is_carried records that equality by rfl. The non-circularity certificate lists it as item 3: "The BMV-positivity clause carries the pure two-qubit entropy theorem," auditing that the master statement does not smuggle circular assumptions.
Within RS gravity this clause ties bipartite entanglement structure to thermodynamic themes already imported (Hawking temperature, black-hole entropy SI). It is one of the CLOSED clauses among the twelve in the conditional master theorem; five other tracks remain open before an unconditional master statement is available.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.