nthPrime
plain-language theorem explainer
nthPrime supplies the canonical non-resonant scale schedule p_n for the Bet-2 self-falsification hypothesis in the RM2U non-parasitism module. It sets p_n to the nth natural number that is prime. Researchers modeling tail-flux vanishing in the Navier-Stokes radial profile would reference this schedule to obtain lower bounds along prime indices when the flux fails to vanish. The definition is a direct one-line wrapper around the standard prime enumerator.
Claim. Let $p_n$ denote the $n$-th prime number, obtained by enumerating the natural numbers that satisfy the primality predicate in strictly increasing order.
background
In the RM2U.NonParasitism module the non-parasitism condition is expressed as the vanishing of the tail-flux boundary term at infinity for the relevant ell=2 coefficient in the radial profile. The Prime predicate is the standard primality condition on natural numbers, kept as a transparent alias for the Mathlib predicate. This definition provides the scale schedule used to test self-falsification when the tail flux does not vanish, as required by the PrimeScheduleSelfFalsification structure.
proof idea
The definition is a one-line wrapper that applies the Nat.nth enumerator to the Prime predicate.
why it matters
This definition populates the canonical non-resonant schedule that feeds the PrimeScheduleSelfFalsification interface and the bet2_of_primeSchedule theorem. The latter derives the Bet2SelfFalsificationHypothesis from a lower bound on tail flux along the prime schedule. It closes the prime-based route for the single hard gate in the RM2U to RM2 pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.