BornRuleFalsifier
plain-language theorem explainer
Packages the three concrete observations that would defeat the RS derivation of the Born rule P = |ψ|² on DFT-8 sectors: wrong sector probabilities on a normalised state, phase dependence of J-cost, or failure of the two-branch exp(−C) calibration. Anyone auditing QF-002 or the BornRuleForcing chain cites this as the explicit falsifier interface. It is a pure structure (definition), not a proved theorem.
Claim. A falsifier of the Born-rule derivation consists of three propositions: (i) some normalised ledger state has sector probabilities unequal to $\|\psi_k\|^2$; (ii) the $J$-cost depends on phase; (iii) the two-branch Born identities fail. The structure also records that (i) is already contradictory (implies $\mathrm{False}$).
background
Module QF-002 derives the Born rule as the unique probability measure on 8-mode sectors that is normalised, phase-invariant, additive over disjoint mode-sets, and consistent with the two-branch $\exp(-C)$ Gibbs model. The DFT-8 decomposition splits any ledger state $\psi$ into eight orthogonal modes; Parseval then transfers the measure to the frequency basis.
$J$-cost is the unique cost functional forced by the Recognition Composition Law (T5: $J(x)=(x+x^{-1})/2-1$). Its phase invariance is already proved in-module, so probabilities can depend only on moduli $|\psi_k|$. The two-branch identities $P_{\cos}$ and $P_{\sin}$ calibrate the singleton weight to $r\mapsto r^2$ (TwoOutcomeBornCert / BornRuleForcing).
This structure does not re-prove those facts; it names the three observations that would overturn them.
proof idea
No proof body: the declaration is a structure (definition). It exposes three bare Prop fields for the falsifying observations and one implication field asserting that wrong sector probabilities already yield False. Downstream code can inhabit or refute those fields; nothing is discharged here.
why it matters
Gives QF-002 an explicit, referee-checkable defeat condition rather than an open-ended claim. Ties directly to the module result that $P=|\psi|^2$ is forced by phase-invariant $J$-cost, Finset additivity, and the two-branch $\exp(-C)$ calibration on the eight-tick (T7) DFT-8 sectors. No downstream consumers are wired yet (used_by empty); the structure stands as the audit hook for the BornRuleForcing chain and sibling lemmas (born_rule_from_jcost, normalization_from_jcost, gleason_from_rs, born_rule_phase_independent).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.