PartitionFunctionFalsifier
plain-language theorem explainer
PartitionFunctionFalsifier packages three concrete failure modes for the ledger-derived partition function in Recognition Science. A researcher testing the statistical mechanics extraction from J-cost sums would cite it to mark the exact boundaries of the THERMO-002 claim. The declaration is a plain structure definition whose content is exhausted by the three propositions and their disjunctive implication to falsehood.
Claim. A structure whose fields are the propositions $P_1$ (thermodynamic quantities fail to follow from the partition function $Z$), $P_2$ (J-cost does not map to energy), $P_3$ (the eight-tick octave does not produce quantum statistics), together with the implication $P_1lor P_2lor P_3to bot$.
background
The module derives the partition function as a sum over ledger configurations weighted by J-cost, recovering $Z=sum_i exp(-beta E_i)$ and the standard thermodynamic relations for free energy, average energy, entropy and heat capacity. J-cost is the recognition cost function imported from the Cost module; energy is identified with it via the sibling energyFromJCost. The eight-tick octave is the period-$2^3$ structure forced by the upstream UnifiedForcingChain. The local setting is THERMO-002, whose core insight is that $Z$ encodes all thermodynamic information once the ledger sum is in place.
proof idea
This is a direct definition of a structure with three propositional fields and one implication field. No lemmas or tactics are invoked; the declaration simply records the three falsification conditions listed in the module documentation.
why it matters
The structure sharpens the THERMO-002 derivation by naming the precise ways the ledger-to-$Z$ step could break, thereby bounding the claim that thermodynamic quantities follow from the partition function. It directly references the eight-tick octave (T7) for quantum statistics and the J-cost to energy map. No downstream theorems are recorded, leaving open whether any of the three failure modes can be realized inside the full Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.