bmv_clause_is_carried
plain-language theorem explainer
The BMV-positivity slot of the quantum-gravity master theorem is definitionally the pure two-qubit von Neumann entropy positivity proposition (normalized 2×2 matrices with positive concurrence have positive reduced entropy). Non-circularity auditors cite this to show the slot is not a True placeholder and does not smuggle in the master conclusion. Proof is reflexivity: the clause was defined equal to that carried proposition.
Claim. The unconditional BMV-positivity field of the master theorem is definitionally equal to the proposition that every $2\times 2$ complex matrix $A$ with $\sum_{i,j}|A_{ij}|^2=1$ and positive concurrence has positive reduced von Neumann entropy.
background
This module is a field-by-field non-circularity audit of the unconditional quantum-gravity master theorem. A referee objection is that witness structures of shape $\Sigma(P:\mathrm{Prop}),P$ are inhabited by $\langle\mathrm{True},\mathrm{trivial}\rangle$, so the master statement is only as strong as the concrete propositions in its slots. For each atom the audit discloses, by definitional equality, what proposition is actually carried, then proves that proposition holds without assuming any master clause.
The BMV slot is one of three formerly-placeholder clauses upgraded after M1–M3. Its carried content is the pure two-qubit entropy positivity statement: for every normalized $2\times 2$ complex matrix with positive concurrence, the reduced-density von Neumann entropy is strictly positive. That statement is witnessed upstream by the pure two-qubit entropy–concurrence theorem; the master field is defined to be exactly this proposition, not a vacuous True.
proof idea
One-line term proof by rfl. The unconditional BMV-positivity field is defined to be the carried pure two-qubit entropy proposition, so definitional equality is immediate. No lemmas are applied; the audit only records that equality for inspection.
why it matters
Feeds the single non-circularity certificate, which conjoins: T0–T8 carries the forcing-chain surface; cost-uniqueness carries universal $J$-cost uniqueness; BMV-positivity carries the pure two-qubit entropy theorem; six closed certificate clauses hold by inhabitation; five witness inputs hold unconditionally; and the D4 Page field is non-vacuous. Without this disclosure, a referee could claim the BMV slot is either True or secretly the master conclusion. With it, the master conjunction is assembled from independently named, non-self-referential physics propositions. Landmark contact is indirect: the slot is quantum-information input to the gravity master theorem, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.