BoseFalsifier
plain-language theorem explainer
The falsifier structure records candidate observations that would contradict the Bose-Einstein distribution derived from Recognition Science's even-phase ledger constraint. Experimental physicists checking consistency between ledger-based quantum statistics and laboratory BEC data would cite this record. The definition is a direct record type with two string fields carrying no computational content.
Claim. A record type consisting of a string field for a potential falsification description and a string field for its verification status.
background
The BoseEinstein module derives the distribution from the even-phase ledger constraint in which integer-spin particles satisfy exp(2πi) = +1, allowing multiple occupancy of a single state. Entropy is maximized subject to fixed average energy and particle number, yielding the standard Bose-Einstein form. Upstream results include the convexity of J-cost minimization established in PhysicsComplexityStructure and the discrete φ-tiers of physical quantities from RSNativeUnits.
proof idea
Defines a record type directly with two string fields; no lemmas or tactics are applied.
why it matters
The structure supplies the element type for the experimentalStatus list that enumerates verified outcomes including the distribution itself, the BEC transition, and the critical-temperature formula. It therefore closes the falsification interface for the THERMO-010 derivation that rests on the eight-tick octave and even-phase symmetry. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.