window_insufficient
plain-language theorem explainer
No positive integer window shorter than 360 can be a common multiple of both 8 and 45. Researchers modeling finite-horizon decision procedures under the Gap-45 barrier cite this result to establish the minimal resolution length. The statement follows from the coprimality of the two periods, which forces their least common multiple to be exactly 360. The proof is a direct one-line application of the no_smaller_multiple_8_45 lemma.
Claim. For every natural number $w$ with $0 < w < 360$, it is not the case that $8$ divides $w$ and $45$ divides $w$.
background
The Gap-45 Recognition Barrier module formalizes the consequences of gcd(8,45)=1. No proper divisor of 360 can be a common multiple of both periods, so any finite window of length w < 360 encounters configurations where the 8-tick cycle and the 45-fold phase structure impose incompatible constraints. The module treats this non-alignment as the mathematical core of the barrier; the link to experiential navigation remains a separate hypothesis.
proof idea
The proof is a one-line wrapper that applies the lemma no_smaller_multiple_8_45 from IndisputableMonolith.Gap45.Beat, forwarding the positivity and strict upper-bound hypotheses directly.
why it matters
The result supplies the window_min field inside the BarrierCert definition, which is then used by the phase_mismatch theorem to show that t mod 8 and t mod 45 cannot vanish simultaneously for t < 360. It closes the finite-horizon non-alignment step in the Gap-45 barrier, directly instantiating the eight-tick octave (T7) together with the incommensurable 45-fold structure. The parent BarrierCert aggregates this fact with coprimality and beat-primality results to certify the full recognition obstruction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.