coprime_8_45
plain-language theorem explainer
The lemma establishes that 8 and 45 share no common prime factors. Cosmologists in the Recognition Science framework cite it when constructing certificates for perpetual complexity in voxel cadences. The proof is a direct decision procedure that evaluates the gcd to one.
Claim. $8$ and $45$ are coprime, i.e., $gcd(8,45)=1$.
background
The Gap45 module assembles basic divisibility facts for the integers 8 and 45, including their coprimeness, the equality of their lcm to 360, and related statements such as the coprimeness of 9 and 5. Coprimeness is the standard arithmetic predicate that the greatest common divisor equals one. These facts sit inside the larger Recognition Science development that encodes eight-tick periodicity and 360-tick synchronization cycles.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. The tactic reduces the coprimeness goal to a decidable computation of the gcd and returns the affirmative result.
why it matters
This lemma supplies the coprime_8_45 field of the PerpetualComplexityCert structure. That structure yields the no_heat_death theorem asserting that the two cadences cannot vanish simultaneously for every tick. The result therefore closes the argument that gcd(8,45)=1 forces misalignment in 359 out of every 360 ticks, supporting the eight-tick octave within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.