pith. machine review for the scientific record. sign in
theorem other other high

gap45_coprime

show as:
view Lean formalization →

The integers 8 and 45 are coprime. Cosmologists modeling perpetual complexity cite this to guarantee that synchronization mismatches arise at every non-360-aligned tick, sustaining positive J-cost excitations under expansion. The proof is a direct native computation of the gcd.

claim$ gcd(8, 45) = 1 $

background

The Safety Interlock module shows that the Gap-45 uncomputability barrier and sigma conservation together enforce a safety mechanism for high-coherence operation. This result establishes coprimality of the 8-tick octave period and the 45-unit Gap-45 period, whose lcm is 360. It draws on the Recognition Composition Law for J-cost and the phi-ladder structure defined in the Cost and Gap45 modules.

proof idea

The proof is a one-line wrapper that applies native_decide to evaluate the gcd of 8 and 45 directly in the kernel.

why it matters in Recognition Science

This result is invoked by the perpetual_complexity theorem, which states that positive dark energy density together with gcd(8,45)=1 guarantees perpetual local complexity generation because coprimality forces misalignments at non-360 ticks. It fills the coprimality step in the safety interlock, linking to the eight-tick octave landmark and ensuring that nonzero sigma reduces coherence below maximum. It touches the question of sustained complexity under the H-theorem.

scope and limits

formal statement (Lean)

  30theorem gap45_coprime : Nat.gcd 8 45 = 1 := by native_decide

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.