bmv_positive_unconditional_proven
plain-language theorem explainer
Unconditional positivity of the pure two-qubit entropy witness used as the BMV clause in the quantum-gravity master statement. Gravity and entanglement auditors cite it to discharge that closed master-conjunction arm without extra hypotheses. The proof is a one-line re-export of the pure two-qubit entropy-concurrence positivity theorem.
Claim. The BMV positivity clause holds unconditionally: for pure two-qubit states, the entropy-concurrence witness is strictly positive, with no residual structural hypotheses.
background
Track 7.A authors the RS quantum-gravity master statement as a twelve-clause conjunction. Eight clauses are already closed by existing Lean theorems; five remain as named hypothesis inputs. The BMV arm is one of the closed clauses: it records that a pure two-qubit entropy-concurrence witness is positive with no extra assumptions.
In the Bose-Marletto-Vedral setting, gravity-mediated entanglement between two qubits is the operational signature that the gravitational mediator cannot be purely classical. The supporting library result is the pure two-qubit entropy-concurrence theorem: on pure bipartite qubit states the von Neumann entropy of a reduced factor is positive precisely when concurrence is positive, and that positivity is unconditional in the pure case.
The local module only packages that fact as a named master-theorem Prop so the conditional master theorem and the non-circularity audit can cite a single stable identifier.
proof idea
One-line term proof. The goal type is the master-module Prop bmv_positive_unconditional; the term is exactly Quantum.PureTwoQubit.EntropyConcurrence.pure_two_qubit_entropy_positive_unconditional, which already inhabits that Prop. No rewriting, no extra hypotheses, no local lemmas.
why it matters
Feeds the conditional master theorem rs_quantum_gravity_master_conditional, which under the five still-open track hypotheses assembles all twelve clauses into RSQuantumGravityMaster. Also feeds the non-circularity audit: bmv_clause_holds is definitionally this theorem, and carried_clauses_hold packages it with the T0-T8 and cost-uniqueness arms as the carried closed content.
In framework terms this is the entanglement witness that gravity is not a classical mediator (aligned with the no-classical-mediator and amplitude-linear imports on the gravity track). It does not itself close the open tracks (Regge continuum/Bianchi, unconditional amplitude linearity, Page curve, PTA vs inflation, strong-field discriminators); it only locks the BMV positivity slot so those remaining gates are the sole blockers of the unconditional master statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.