pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Gap45

show as:
view Lean formalization →

The Gap45 module supplies the integer-arithmetic lemmas establishing gcd(8,45)=1, lcm(8,45)=360, and the supporting coprimality of 9 and 5. Researchers constructing safety interlocks or recognition barriers in high-coherence systems cite these facts to demonstrate incommensurability between the 8-tick octave and 45-fold phase structure. Proofs consist of short direct applications of Mathlib gcd and lcm properties.

claim$gcd(8,45)=1$, $lcm(8,45)=360$, $gcd(9,5)=1$, together with the divisibility facts $9|45$, $5|45$, and the absence of smaller common multiples.

background

In the Recognition Science framework the eight-tick octave (T7) supplies a periodic constraint on tick sequences. The Gap45 module isolates the auxiliary number theory required to show that this period shares no common divisor with a 45-fold phase structure, preventing alignment inside any finite window.

proof idea

The module consists of a sequence of elementary lemmas. Each applies the universal properties of gcd and lcm to the concrete integers 8, 45, 9, and 5. The coprimality of 8 and 45 follows from the coprimality of 9 and 5 together with the factorization 45=9*5.

why it matters in Recognition Science

These lemmas supply the gap45_coprime and gap45_lcm facts invoked by the SafetyInterlock theorem to combine the Gap-45 uncomputability barrier with σ-conservation. They also underpin the RecognitionBarrier argument that any finite-horizon decision procedure encounters incompatible 8-tick and 45-fold demands.

scope and limits

used by (2)

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

declarations in this module (21)