bmvFalsifierStatus_all
plain-language theorem explainer
All four status flags of the BMV falsifier package hold simultaneously: witness band certified, amplitude-channel theorem cited, falsifier named, and exclusion from pillar 3. Anyone documenting the BMV entanglement witness as a falsifier floor (not a discriminator) cites this. The proof is four reflexivity checks against the status definition.
Claim. The BMV falsifier status record has every flag true: the entanglement witness band is certified, the amplitude-channel uniqueness theorem is cited, the falsifier is named, and the package is excluded from the pillar-3 discriminator slot.
background
This module treats Bose–Marletto–Vedral (BMV) gravitational entanglement as a falsifier floor, not a discriminator. BMV entanglement is predicted by any quantum mediator, so the package is permanently excluded from the pillar-3 slot that would separate Recognition Science from GR+QFT or other quantum-mediator models sharing the same four branch phases.
What a clean null formally refutes is narrow: under the Newtonian weak-field phase model plus the named geometry, the joint two-qubit branch state is non-product (nonzero amplitude-matrix determinant), with the certified invariant in $[1/2, 7/10]$, bounded away from $0 \bmod 2\pi$. A measured product state at that geometry contradicts that package alone.
The upstream definition bmvFalsifierStatus is a documentation record whose four Boolean fields are set true by construction. It is not a proof obligation; it packages the honest tier of the module (algebra and certified numeric bands are theorems; the magnitude of RS branch phases remains MODEL/OPEN).
proof idea
Term-mode one-liner. The goal is a four-way conjunction of equalities to true. Each conjunct is discharged by rfl against the corresponding field of the canonical status inhabitant, whose definition hard-codes every flag as true. No lemmas are applied beyond definitional equality.
why it matters
The declaration is the single-shot certificate that the BMV package carries its full honesty labels: certified witness band, cited amplitude-channel theorem, named falsifier, and explicit pillar-3 exclusion. Module framing is binding: BMV cannot distinguish RS from any quantum-mediator model with the same branch phases; a clean null only refutes the weak-field-plus-geometry package, and framework-level falsification remains MODEL/OPEN until the unformalized magnitude premise is closed.
No downstream theorems currently depend on it (used_by is empty). Its role is archival and panel-facing: anyone reading the QuantumChannel gravity stack can point here to confirm that the four status claims are definitionally locked, not aspirational. It sits beside the algebraic entanglement theorems (bmv_band_entanglement, clean_null_refutes_rs) without claiming more than those theorems deliver.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.