bmvFalsifierStatus
plain-language theorem explainer
Canonical status record for the BMV falsifier-band package: all four honesty flags are true by definition. Panel and audit code cite it to confirm the package is ledgered as a certified witness band, a named falsifier, amplitude-channel theorems cited, and permanently off the pillar-3 discriminator. Construction is a structure inhabitant; projection lemmas are pure rfl.
Claim. The canonical BMV falsifier status record sets every flag true: the witness band is certified, the amplitude-channel uniqueness theorems are cited with exact premises, the falsifier is named (band-robust and model-point forms), 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. Any quantum mediator that yields the same four weak-field branch phases produces the same amplitude matrix and the same nonzero-determinant witness, so the package cannot separate Recognition Science from GR+QFT or other quantum-mediator models.
The status structure is an explicit documentation record with four Boolean flags: certified witness band (the entangling invariant in $[1/2, 7/10]$), citation of amplitude-channel forcing theorems, a named falsifier (det \neq 0 non-product criterion, plus clean-null refutation), and permanent exclusion from pillar-3. Mathematics lives in the theorems those flags name; the flags themselves carry no proof content.
Honest tier: algebra and numeric bands in the file are theorems (kernel-checked rationals). The premise that the RS channel actually produces Newtonian weak-field phases at this geometry and magnitude remains MODEL/OPEN.
proof idea
Pure definitional inhabitant of the status structure. Each field is set to the Boolean literal true. No tactics, no lemmas, no obligations. Downstream projection theorems are one-line rfl wrappers that only restate these field equalities.
why it matters
Gives the module a single named ledger entry that audit and panel code can query. Downstream, the four single-flag theorems and the conjunction theorem only confirm this definition by reflexivity. The same-branch-phases congruence explains why excluded_from_pillar3 must stay true: identical phases imply identical BMV witness, so the package cannot discriminate RS from other quantum mediators.
In the Recognition framing this is the falsifier floor for gravitational entanglement under the weak-field phase model plus named geometry. A clean null at that geometry contradicts the package (model-point and band-robust forms). Framework-level refutation still needs the unformalized magnitude premise that RS produces those phases; that half is MODEL/OPEN, not theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.