NonResonantSchedule
plain-language theorem explainer
NonResonantSchedule encodes a strictly increasing map from naturals to naturals whose values are pairwise coprime. Workers on the RM2U non-parasitism gate for the Navier-Stokes reduction cite the structure to guarantee a resonance-free integer schedule for boundary-term analysis. The definition is a plain structure whose two predicate fields directly enforce the monotonicity and coprimality conditions.
Claim. A non-resonant schedule is a function $s : {N} {to} {N}$ that is strictly increasing and satisfies $gcd(s(i),s(j))=1$ for all distinct $i,j$.
background
The RM2U.NonParasitism module isolates the single hard gate of the RM2U to RM2 pipeline: the requirement that the tail-flux boundary term at infinity vanishes for the ell=2 coefficient. NonResonantSchedule supplies the integer schedule that prevents parasitic resonances in that analysis. It rests on the canonical arithmetic object, which supplies realization-independent Peano arithmetic, and on the canonical synchronization object from the Gap45.Beat module.
proof idea
The declaration is a structure definition with an empty proof body. Its canonical instance is obtained by supplying the nthPrime function together with the already-proved lemmas strictMono_nthPrime and pairwise_coprime_nthPrime.
why it matters
The structure populates the canonical non-resonant schedule that feeds the non-parasitism hypothesis for the RM2U closure. It thereby discharges the only genuinely hard statement identified in the module documentation, where non-parasitism is phrased as vanishing of the tail-flux boundary term. The prime-based construction guarantees the coprimality needed for the frequency schedule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.