phase_mismatch
plain-language theorem explainer
phase_mismatch shows that no natural number t with 0 < t < 360 is divisible by both 8 and 45. Researchers analyzing incommensurable periodic constraints in finite-horizon decision procedures cite the result to bound alignment windows. The argument converts the modular conditions to divisibility statements and applies the window_insufficient lemma.
Claim. For any natural number $t$ satisfying $0 < t < 360$, it is not the case that $8$ divides $t$ and $45$ divides $t$.
background
The Gap-45 module formalizes the mathematical core of the recognition barrier arising from coprimality of 8 and 45. The 8-tick phase corresponds to the eight-tick octave (period $2^3$) while the 45-fold phase encodes an additional periodic constraint; their least common multiple is 360. The upstream window_insufficient theorem states: 'No window of length w < 360 can simultaneously be a multiple of 8 and 45. Any finite-horizon procedure with horizon < 360 ticks will encounter a tick where it cannot verify alignment of both periods.'
proof idea
One-line wrapper that applies window_insufficient. The intro tactic extracts the two divisibility assumptions from the negated conjunction, Nat.dvd_of_mod_eq_zero converts each mod-zero hypothesis into a divides statement, and the exact tactic discharges the goal by invoking window_insufficient on the original bounds and the new divisibility pair.
why it matters
The result supplies the non-alignment fact required by DomainInstance in RecognitionCategory, where each domain algebra is obtained by applying a functor to the canonical Recognition Algebra. It fills the coprimality and window-insufficiency step in the Gap-45 barrier (MODULE_DOC), separating the proved mathematical core from the separate hypothesis that the barrier forces experiential navigation. The eight-tick octave and the 360-tick minimal resolution window are the relevant framework landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.