HeatCapacityFalsifier
plain-language theorem explainer
The HeatCapacityFalsifier structure encodes the three propositions whose joint truth would refute the Recognition Science derivation of heat capacity from eight-tick mode counting. A researcher comparing the framework to measured deviations from classical equipartition or the Debye T³ law would cite this definition to mark the model's empirical boundary conditions. It is introduced as a plain structure definition that packages the failure modes and asserts their logical inconsistency.
Claim. A structure $F$ whose fields are the propositions $P_1$ (equipartition fails at high temperature), $P_2$ (Debye $T^3$ law fails), $P_3$ (eight-tick counting is irrelevant to mode energies), together with the implication $P_1 ∧ P_2 → ⊥$.
background
The module derives heat capacity by counting quadratic modes that arise from the eight-tick periodicity imposed by the Recognition forcing chain. Classical equipartition assigns $kT/2$ to each such mode; quantum corrections follow from the discrete spectrum of the eight-tick octave. The structure isolates the three empirical conditions that would break this counting argument: failure of equipartition at high temperature, absence of the Debye $T^3$ law at low temperature, and irrelevance of the eight-tick structure to the mode spectrum.
proof idea
The declaration is a structure definition that directly encodes the three failure propositions together with the logical requirement that the first two cannot hold simultaneously. No lemmas are applied; the construction is purely definitional.
why it matters
This definition supplies the explicit falsification criteria for the heat-capacity derivation in the Recognition Science framework. It directly implements the third clause of the module target that the derivation would be falsified if eight-tick counting proves irrelevant to modes. The structure therefore closes the empirical loop around the eight-tick octave (T7) and the mode-counting step that follows from it. No downstream theorems currently depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.