minimal_resolution_window
plain-language theorem explainer
The theorem establishes that 8 divides 360 and 45 divides 360, confirming 360 as the minimal integer that resolves both the 8-tick cycle and the 45-fold phase structure. Researchers formalizing the Gap-45 barrier in Recognition Science cite this when showing that shorter windows leave the coprime constraints unaligned. The proof is a direct term construction supplying explicit divisor witnesses verified by norm_num.
Claim. The minimal window resolving both the 8-tick and 45-fold periodicities satisfies $8 | 360$ and $45 | 360$.
background
The Gap-45 Recognition Barrier module starts from the coprimality gcd(8,45)=1. This prevents any proper sub-period of the 8-tick cycle from aligning with the 45-fold phase structure. The module documentation states that no proper divisor of 360 divides both numbers simultaneously and that the beat frequency 37/360 behaves as irreducible because 37 is prime.
proof idea
The term proof applies the pair constructor to supply the two witnesses directly: 45 for the first divisibility and 8 for the second. Each witness is confirmed by a norm_num call that computes the exact quotient.
why it matters
This result supplies the full_resolution component inside the BarrierCert definition, which bundles coprimality, beat primality, and window insufficiency. It completes the mathematical core of the Gap-45 barrier and connects to the eight-tick octave (T7) in the forcing chain by exhibiting the smallest period that encompasses both periodicities. The link from this barrier to experiential navigation remains a hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.