HTheoremForce
plain-language theorem explainer
HTheoremForce is the structure that encodes the first driver in the perpetual complexity argument: the proposition that free energy decreases. Cosmologists working on heat-death bounds cite it when pairing the H-theorem with the coprimality of the 8-tick and 45-tick cadences. The declaration is a bare structure definition whose single field is the Prop free_energy_decreasing.
Claim. The H-theorem force is the proposition that free energy decreases: free_energy_decreasing : Prop.
background
The module PerpetualComplexity combines two results to show that thermal death is impossible. The first is that passive modes carry permanent vacuum energy (Ω_Λ > 0). The second is that the recognition cadence (8 ticks) and the phase cadence (45 ticks) are coprime, so global synchronization never occurs. Upstream, the 8-tick phase is defined as (k : ℝ) * π / 4 for k in Fin 8 and is periodic with period 2π; the complex phase is the unimodular number e^{i w}.
proof idea
This is a structure definition that simply introduces the field free_energy_decreasing : Prop. No lemmas are applied; the declaration is a direct wrapper around the named proposition.
why it matters
The structure supplies the H-theorem half of the Perpetual Complexity Theorem (Dark_Energy_Mode_Counting.tex §10, Theorem 10.1). It pairs with the Gap-45 frustration result to guarantee that local complexity is generated at every epoch. In the Recognition framework it rests on the eight-tick octave (T7) and the coprimality that prevents phase locking.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.