pith. machine review for the scientific record. sign in
structure definition def or abbrev high

MeasurementFalsifier

show as:
view Lean formalization →

MeasurementFalsifier is a record type that catalogs candidate experimental violations of the Recognition Science derivation of wavefunction collapse from ledger commitment. Physicists examining the Born rule or no-cloning would reference it to specify concrete counterexamples. The declaration is a plain structure definition with four string fields and no proof obligations.

claimA falsifier for the measurement postulate is a tuple consisting of a violation type, an experiment description, the outcome expected under Recognition Science, and the observed result that would contradict the ledger-commitment account.

background

The module derives the measurement postulate by equating superposition with uncommitted ledger entries and measurement with forced commitment that selects one branch. Probabilities arise from J-cost, where lower-cost branches are favored, recovering the Born rule. Upstream, LedgerFactorization calibrates J on the positive reals while PhiForcingDerived supplies the cost structure; SpectralEmergence forces the gauge content and three generations from the Q3 lattice.

proof idea

The declaration is a structure definition that introduces four string fields: violationType, experiment, expected, and observed. No tactics or lemmas are applied; the body is empty because the object is a data type rather than a theorem.

why it matters in Recognition Science

The structure supports the module's claim that collapse follows from ledger balancing rather than an added postulate. It directly serves the paper proposition on deriving the measurement postulate from Recognition Science and the J-cost mechanism. No downstream uses are recorded, leaving open whether concrete experimental protocols will be attached later.

scope and limits

formal statement (Lean)

 275structure MeasurementFalsifier where
 276  /-- Type of violation. -/
 277  violationType : String
 278  /-- Description of the experiment. -/
 279  experiment : String
 280  /-- Expected outcome from RS. -/
 281  expected : String
 282  /-- Observed outcome that falsifies. -/
 283  observed : String
 284
 285/-- No such falsifier has ever been found. -/

depends on (8)

Lean names referenced from this declaration's body.