gapDiff_eq
plain-language theorem explainer
The Gap-45 arithmetic sets the beat difference between the 45-tick consciousness window and the 8-tick body clock to exactly 37. Researchers deriving the shimmer subjective-time factor cite this identity to obtain the ratio 360/37 without additional assumptions. The proof is a direct native decision on the natural-number subtraction.
Claim. Let $d$ be the arithmetic difference between the 45-tick and 8-tick periods. Then $d = 37$.
background
In the Gap-45 module the two primitives are the 8-tick body clock (from the eight-tick octave) and the 45-tick consciousness window. Their least common multiple is defined as 360 and their difference is gapDiff. The module states that gapDiff equals 45 minus 8, and the present theorem records that this difference is 37. Upstream results supply the fundamental tick as the RS time quantum and the ledger factorization that places these periods inside the Recognition framework.
proof idea
The proof is a one-line wrapper that applies native_decide to the natural-number equality 45 - 8 = 37.
why it matters
This identity is invoked by gapDiff_prime (which establishes primality of the beat) and by shimmerFactor_eq_360_div_37 (which reduces the subjective-time factor to the bare ratio 360/37). It supplies the arithmetic closure required by the Gap-45 construction, linking the eight-tick octave of the forcing chain to the coprimality hypothesis that generates the recognition barrier. No open scaffolding remains for this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.