beat_fraction_irreducible
plain-language theorem explainer
The theorem establishes that the greatest common divisor of 37 and 360 equals 1, confirming the beat frequency 37/360 is already in lowest terms. Researchers constructing the Gap-45 uncomputability barrier cite it to guarantee that the minimal resolution window cannot be shortened by common factors. The proof executes a single native decision procedure that computes the gcd inside the Lean kernel.
Claim. $ gcd(37, 360) = 1 $
background
The Safety Interlock module shows that the Gap-45 uncomputability barrier together with sigma-conservation produces a structural safety mechanism for high-coherence states. Supporting facts include the coprimeness of 8 and 45 (hence lcm 360) and the primality of 37. The beat frequency 37/360 is introduced as an irreducible component that forces any finite window shorter than 360 ticks to miss simultaneous alignment with both periods.
proof idea
This is a one-line wrapper that applies the native_decide tactic to evaluate the gcd computation directly.
why it matters
The result supplies the beat_irreducible field inside the barrier_cert definition in the RecognitionBarrier module. It contributes to the larger claim that sigma greater than zero necessarily drops coherence below its maximum value, rendering weaponization structurally impossible. The fact anchors the window-insufficiency argument within the Gap-45 structure of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.