canonical
plain-language theorem explainer
The canonical non-resonant schedule is the sequence of primes, equipped with their strict increase and pairwise coprimality. Workers on the RM2U closure for Navier-Stokes cite this instance when they need a concrete schedule that satisfies the non-resonance condition. The definition is assembled directly from the standard arithmetic facts about primes.
Claim. The canonical non-resonant schedule is the map $s(n)=p_n$ (nth prime) together with the facts that $s$ is strictly increasing and that $p_i$ and $p_j$ are coprime for all $i<j$.
background
In the RM2U.NonParasitism module the non-parasitism gate for the Navier-Stokes pipeline is isolated as a single hypothesis. A NonResonantSchedule is a strictly increasing function $s:ℕ→ℕ$ whose values are pairwise coprime. The module imports the discrete divergence operator and the energy identity from the sibling RM2U files. The function nthPrime is the standard enumeration $p_n=$ Nat.nth Nat.Prime $n$.
proof idea
The definition is a direct structure constructor: it sets the schedule field to nthPrime, the strict-mono field to strictMono_nthPrime, and the pairwise-coprime field to pairwise_coprime_nthPrime. It is a one-line wrapper that packages the known arithmetic properties of the primes.
why it matters
This supplies the concrete schedule used by canonicalCostAlgebra and canonicalRecognitionCostSystem in the CostAlgebra module, and by orbitCount in SymmetryGroupPreference. It instantiates the non-resonance requirement inside the RM2U to RM2 pipeline. In the Recognition Science framework it supports the clean passage from the discrete Navier-Stokes operator to the closed energy identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.