experimentalStatus
plain-language theorem explainer
experimentalStatus enumerates four experimental checks confirming the Fermi-Dirac distribution derived from Recognition Science's odd-phase ledger constraint. Quantum statisticians and condensed-matter physicists cite the list when validating the 8-tick antisymmetry requirement against data. The body is a direct list construction of FermiFalsifier pairs with no reduction steps.
Claim. The experimental status is the list of pairs (``Pauli violation search'', ``Limit: < 10^{-29} per interaction''), (``Fermi-Dirac measurement'', ``Verified in metals, semiconductors''), (``White dwarf mass limit'', ``Chandrasekhar limit confirmed''), (``Low-T specific heat'', ``Linear T confirmed in all metals'').
background
FermiFalsifier is the structure pairing a falsification type string with a status string. The module derives the Fermi-Dirac distribution f(E) = 1 / (exp((E - μ)/kT) + 1) from the odd 8-tick phase where fermions satisfy exp(iπ) = -1, enforcing antisymmetry and minimum J-cost equilibrium. Upstream results supply discrete enumerations such as the seven plot families, the eight kinship systems, and the seven Greek modes that establish the Recognition Science pattern of finite lists over continuous parameters.
proof idea
The definition is a direct list construction of four FermiFalsifier records. No lemmas or tactics are invoked beyond the structure definition itself.
why it matters
The definition closes the verification step for the module's derivation of quantum statistics from ledger structure, aligning with the eight-tick octave of the forcing chain. It records that all listed predictions hold, supporting the claim that the odd-phase constraint reproduces observed fermion behavior. No downstream declarations depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.