PerpetualComplexityCert
plain-language theorem explainer
The PerpetualComplexityCert structure packages the coprimeness of the 8-tick and 45-tick cadences together with their lcm of 360, a misalignment predicate, and the explicit negation of universal synchronization. Cosmologists working in the Recognition Science setting cite it to certify that local complexity persists at every epoch. The structure is assembled directly from the coprimeness lemma and the no-heat-death corollary without additional proof steps.
Claim. Let $C$ be the structure whose fields are: $8$ and $45$ are coprime, the least common multiple of $8$ and $45$ equals $360$, for every natural number $t$ not divisible by $360$ at least one of $t$ modulo $8$ or $t$ modulo $45$ is nonzero, and it is not the case that every natural number $t$ is divisible by both $8$ and $45$.
background
The Perpetual Complexity module combines the existence of passive vacuum-energy modes with the incommensurability of the recognition cadence (period 8) and the phase cadence (period 45). The upstream coprime_8_45 lemma records that gcd(8,45)=1. The upstream no_heat_death theorem states that it is impossible for every natural number to be divisible by both 8 and 45, proved by exhibiting the counterexample t=1. The module doc identifies this combination as the content of Theorem 10.1 in Dark_Energy_Mode_Counting.tex.
proof idea
The declaration is a structure definition. Its coprime_8_45 field is supplied by the coprime_8_45 lemma. Its sync_360 field follows from the definition of lcm. Its misalignment field is witnessed by the misalignment_exists lemma. Its no_heat_death field is taken verbatim from the no_heat_death theorem.
why it matters
This certificate is instantiated by the perpetualComplexityCert definition, which realizes the Perpetual Complexity Theorem. It supplies the arithmetic obstruction required by Theorem 10.1 of the paper, closing the argument that the eight-tick octave and the 45-tick phase never align completely and thereby guaranteeing ongoing complexity generation in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.