aliasing_ratio_lt_one
plain-language theorem explainer
The declaration establishes that the rational 37/45 lies strictly below 1. Researchers modeling the Gap-45 recognition barrier cite it to confirm the beat frequency remains sub-unity, so that discrete 8-tick cycles alias into apparent continuity within each 45-fold period. The proof reduces to a direct numerical check of the inequality.
Claim. The aliasing ratio satisfies $37/45 < 1$.
background
The Gap-45 Recognition Barrier module formalizes the mathematical obstruction arising from coprimality of the 8-tick octave and the 45-fold phase structure. Because gcd(8,45)=1, no proper divisor of 360 simultaneously divides both periods, so any bounded observation window encounters incompatible constraints. The beat frequency 37 ticks per 45-fold cycle is therefore less than one full cycle, producing aliasing that the module interprets as subjective time running slower than ledger time by the factor 360/37.
proof idea
The proof is a one-line wrapper that applies norm_num to evaluate the rational comparison directly.
why it matters
This supplies the aliasing-ratio component inside the BarrierCert definition that aggregates the core theorems of the module. It anchors the claim that finite windows cannot resolve the coprime periodicities, consistent with the eight-tick octave (T7) and the forcing of three spatial dimensions (T8) in the broader Recognition Science chain. The link from this mathematical barrier to experiential navigation remains an explicit hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.