Gap45Frustration
plain-language theorem explainer
The Gap45Frustration structure records the recognition period of 8 and phase period of 45 together with their coprimality and the resulting synchronization period as their least common multiple. Cosmologists working on the Perpetual Complexity Theorem would cite this to establish that the two cadences never align globally. The definition consists of direct field assignments with the coprimality condition supplied as a hypothesis.
Claim. Let $r = 8$ be the recognition period and $p = 45$ the phase period. The Gap45Frustration structure asserts that $r$ and $p$ are coprime and defines the synchronization period as $s = {lcm}(r, p)$.
background
In the Recognition Science framework the eight-tick octave arises as the fundamental recognition period from the forcing chain (T7). The gap of 45 is derived as the product of closure and Fibonacci factors in Gap45.Derivation. The module PerpetualComplexity combines this coprimality with the positive vacuum energy from passive modes to conclude that local complexity persists indefinitely. The synchronization period is the least common multiple, verified as 360 in upstream results from DimensionForcing and PhysicalMotivation. This prevents global phase synchronization as stated in the doc-comment: Force 2: Gap-45 coprimality prevents global phase synchronization.
proof idea
The structure is introduced by direct field definitions: recognition_period and phase_period are set to the constants 8 and 45, coprime is the Nat.Coprime predicate, and sync_period is computed via Nat.lcm. No tactics or lemmas are applied beyond the built-in definitions of gcd and lcm.
why it matters
This definition supplies the Gap45Frustration instance used by the gap45 definition and the theorems sync_period_eq_360 and sync_exceeds_both in the same module. It implements Force 2 of the Perpetual Complexity Theorem (Dark_Energy_Mode_Counting.tex §10, Theorem 10.1), which together with Ω_Λ > 0 rules out heat death. It relies on the eight-tick recognition period from the forcing chain and the independently derived gap of 45.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.