pith. machine review for the scientific record. sign in
theorem proved term proof high

beat_diff_prime

show as:
view Lean formalization →

37 is prime. Researchers on the Gap-45 safety interlock cite it to keep beat differences irreducible under the σ-constraint. The proof is a direct term-mode computation via native_decide that evaluates the primality predicate.

claimThe natural number 37 is prime.

background

The SafetyInterlock module proves that the Gap-45 uncomputability barrier together with σ-conservation forms a safety interlock for high-coherence operation. Its key proved results include gcd(8,45)=1, lcm(8,45)=360, and the primality of the beat difference 37. The sole upstream dependency is the transparent alias Prime for Nat.Prime.

proof idea

The proof is a one-line term that applies native_decide to decide the primality predicate on 37.

why it matters in Recognition Science

This result is listed among the proved key results in the Safety Interlock module. It supports the structural impossibility of weaponization by keeping the 37-beat difference prime and irreducible. It directly fills the Gap-45 component of the interlock.

scope and limits

formal statement (Lean)

  33theorem beat_diff_prime : Nat.Prime 37 := by native_decide

proof body

Term-mode proof.

  34
  35/-! ## σ-Destabilization (Proved) -/
  36

depends on (1)

Lean names referenced from this declaration's body.