gapDiff_prime
The declaration proves that the Gap-45 beat difference equals 37 and is therefore prime. A researcher formalizing the Recognition Barrier would cite it to establish that the 37-tick frequency shares no common factors with the 360-tick window. The proof reduces the claim to the already-decided primality of 37 via a single rewrite.
claimLet $d := 45 - 8$. Then $d$ is a prime number.
background
In the Gap-45 module the two primitives are the 8-tick body period and the 45-tick consciousness window. Their least common multiple is 360 and their difference is defined as gapDiff := gapPeriod - bodyPeriod. The upstream result beat_is_prime states that 37 is prime, and gapDiff_eq shows that gapDiff equals 37. This local arithmetic sits inside the larger claim that the shimmer factor 360/37 arises purely from these two periods without external calibration.
proof idea
The proof is a one-line wrapper. It rewrites gapDiff using the equality gapDiff = 37 and then applies the theorem that 37 is prime.
why it matters in Recognition Science
This result supplies the primality needed for the coprimality hypothesis in the Recognition Barrier. The module doc-comment notes that the beat is prime and therefore coprime with every proper divisor of the 360-tick window. It closes the arithmetic foundation for the subjective-time factor 360/37 before any physical interpretation is attached.
scope and limits
- Does not prove any physical interpretation of the shimmer factor.
- Does not address whether 37 remains prime in other number bases or rings.
- Does not connect the primality to the forcing chain T0-T8.
formal statement (Lean)
80theorem gapDiff_prime : Nat.Prime gapDiff := by
proof body
Term-mode proof.
81 rw [gapDiff_eq]; exact beat_is_prime
82
83/-- The two Gap-45 primitives are coprime, which is the hypothesis
84 that generates the whole barrier. -/