bmvFalsifierStatus_falsifier_named
plain-language theorem explainer
The canonical BMV falsifier status record marks the falsifier as named (flag true). Reviewers auditing the Gravity.QuantumChannel package cite this to confirm the documentation contract is fully populated. The proof is definitional reflexivity on the status inhabitant.
Claim. In the canonical BMV falsifier status record, the flag recording that the falsifier has been named equals $\mathrm{true}$.
background
This module treats the Bose–Marletto–Vedral (BMV) entanglement witness as a falsifier floor, not a pillar-3 discriminator. Any quantum mediator predicts the same four branch phases, so a clean null only refutes the named package (Newtonian weak-field phase model plus fixed geometry), not RS versus GR+QFT in general.
The status type is a four-flag documentation record: witness band certified, amplitude-channel theorem cited, falsifier named, and excluded from pillar 3. The canonical inhabitant sets every flag to true by definition; it is not a proof obligation.
Upstream, that inhabitant is defined with falsifier_named := true among the other flags. The present declaration simply exposes that one field as a named equality.
proof idea
One-line wrapper: reflexivity (rfl) against the definitional equation in the canonical status inhabitant, where the falsifier-named field is set to true. No lemmas or tactics beyond definitional equality.
why it matters
Inside the BMV falsifier-band package, this flag documents that the falsifier itself has been named: a measured product state at the stated geometry contradicts the package (model-point and band-robust forms in the module framing). The module is permanently excluded from the pillar-3 discriminator slot; the status record records that exclusion alongside the named-falsifier bit.
No downstream theorems currently depend on this equality. It closes the documentation contract for auditors rather than advancing the forcing chain (T0–T8) or the Recognition Composition Law. The framework-level reading “clean null refutes RS” remains MODEL/OPEN: magnitude of the branch phases is not forced by the amplitude-channel uniqueness theorems cited elsewhere in the package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.