pith. machine review for the scientific record. sign in
def definition def or abbrev high

gap45

show as:
view Lean formalization →

The definition instantiates the gap-45 frustration structure by supplying the coprimality witness for the periods 8 and 45. Cosmologists studying perpetual complexity cite this to establish incommensurability of recognition and phase cadences. The construction is a direct record that sets the coprime field from the upstream theorem and the synchronization period to 360.

claimLet $G$ be the structure with recognition period $8$, phase period $45$, the coprimality condition that their gcd equals 1, and synchronization period equal to their least common multiple. The definition supplies the instance of $G$ in which coprimality is witnessed by the theorem establishing gcd of 8 and 45 equals 1 and the synchronization period is set to 360.

background

Gap45Frustration is the structure that encodes the coprimality of the eight-tick recognition period and the 45-unit phase period. Its doc-comment states that this coprimality prevents global phase synchronization. The module PerpetualComplexity combines this with the positive vacuum energy result to conclude that the universe cannot reach heat death, as stated in the module doc-comment referencing Dark_Energy_Mode_Counting.tex §10 Theorem 10.1.

proof idea

The definition constructs the frustration structure by assigning the coprimality witness from the theorem establishing gcd of 8 and 45 equals 1, and sets the synchronization period to 360 as noted in the attached comment referencing the proof in SyncMinimization.

why it matters in Recognition Science

This supplies the coprimality component of the perpetual complexity theorem, which combines it with the positive cosmological constant result to show that heat death is impossible. It realizes the eight-tick octave from the forcing chain and prevents synchronization as required by the paper theorem 10.1. The result is used by the no-heat-death declaration in the same module.

scope and limits

formal statement (Lean)

  40def gap45 : Gap45Frustration where
  41  coprime := coprime_3

proof body

Definition body.

  42  sync_period := 360
  43
  44/-- The sync period is 360 (proved in SyncMinimization). -/

depends on (9)

Lean names referenced from this declaration's body.