gap45_lcm
plain-language theorem explainer
The theorem establishes that the least common multiple of 8 and 45 equals 360. Researchers analyzing the Gap-45 barrier within the superhuman safety interlock cite this identity when deriving cycle lengths for coherence constraints. The proof proceeds as a direct native decision that evaluates the LCM equality without additional lemmas.
Claim. $lcm(8,45)=360$
background
The SafetyInterlock module proves that the Gap-45 uncomputability barrier and σ-conservation together create a fundamental safety interlock for high-coherence operation. It enumerates several proved results including the coprimeness of 8 and 45, this LCM value, the primality of 37, and the optimality of σ=0 under the J-cost. The local setting centers on structural constraints that limit high-coherence states and prevent weaponization.
proof idea
The proof is a one-line wrapper that applies native_decide to compute the LCM directly in the natural numbers.
why it matters
This arithmetic identity supports the key proved results listed in the SafetyInterlock module, including downstream claims on power ethics and the structural impossibility of weaponization. It incorporates the factor 8 that aligns with the eight-tick octave in the Recognition framework. No open questions are resolved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.