FermiFalsifier
plain-language theorem explainer
The FermiFalsifier structure records four classes of observations that would refute the Recognition Science derivation of the Fermi-Dirac distribution from the odd-phase 8-tick ledger constraint. Quantum statisticians and integrated-information researchers would cite it when testing whether J-cost minimization and antisymmetry together force the standard occupation number. It is introduced as a plain record pairing a descriptive label with a verification status string.
Claim. A record type consisting of a string field naming a potential counterexample to the emergence of $f(E) = [e^{(E - μ)/kT} + 1]^{-1}$ from the odd-phase ledger and a second string field reporting its experimental status.
background
The FermiDirac module derives the Fermi-Dirac distribution from the odd-phase ledger constraint inside Recognition Science's 8-tick structure. Fermions are assigned odd 8-tick phases (exp(iπ) = -1), which together with the antisymmetry requirement and minimum-J-cost thermal equilibrium produce the standard occupation number. The derivation begins from Pauli exclusion (0 or 1 fermion per state), fixed average energy, and fixed particle number, then maximizes entropy subject to those constraints.
proof idea
This declaration is a structure definition that directly encodes the four falsification conditions listed in the module documentation. No lemmas or tactics are applied; the fields are populated by string literals that downstream code uses to build the experimentalStatus list.
why it matters
The structure supplies the concrete falsifiers referenced by the experimentalStatus definition in the same module, which lists verification limits for Pauli exclusion, Fermi-Dirac measurements in metals, the Chandrasekhar limit, and linear-T specific heat. It thereby closes the empirical loop on the THERMO-009 target of deriving quantum statistics from ledger structure. It touches the open question whether integration always reduces J-cost in new populations, as stated in the doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.