MeasurementFalsifier
plain-language theorem explainer
MeasurementFalsifier records the violation category, experiment, Recognition Science prediction, and contradictory observation that would refute the ledger-commitment derivation of wavefunction collapse. Experimental groups testing the Born rule or no-cloning theorem would cite the structure when designing null-result protocols. The declaration is a bare structure definition carrying four String fields together with the note that no instance has been observed.
Claim. A falsifier consists of a string for violation type, a string for the experiment performed, a string for the outcome predicted by the ledger model, and a string for the observed result that contradicts the prediction.
background
The module derives the measurement postulate from Recognition Science ledger structure: superposition corresponds to an uncommitted ledger entry with multiple branches coexisting, while measurement forces commitment to one branch with the others cancelled. Probabilities follow from J-cost, yielding the Born rule as relative recognition weight. The supplied upstream structures supply supporting pieces: LedgerFactorization calibrates J on the positive reals, PhiForcingDerived encodes the J-cost functional, and SpectralEmergence fixes the gauge and generation content that the ledger must accommodate.
proof idea
The declaration is a structure definition that introduces the record type with four fields; no lemmas or tactics are applied.
why it matters
The structure enumerates the concrete experimental signatures (Born-rule violation, reversible measurement, cloning, persistent interference after which-path information) that would falsify the ledger-based account of collapse. It thereby anchors the module's claim that the measurement postulate is derivable rather than postulated. The definition sits downstream of the eight-tick octave and J-uniqueness steps in the forcing chain and upstream of any quantitative test of the derived Born rule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.