PrimeScheduleSelfFalsification
plain-language theorem explainer
The structure encodes the prime-schedule interface for Bet-2 self-falsification on an RM2URadialProfile. If tail flux fails to vanish then its absolute value is bounded below by a positive constant along the primes, while the series of those absolute values remains summable. Workers closing the RM2U non-parasitism gate cite this when reducing the full hypothesis to a schedule-specific statement. The content is introduced directly as a structure definition with no derivation steps.
Claim. Let $P$ be an RM2URadialProfile. The property holds if, whenever the tail flux of $P$ does not vanish, there exists $ε>0$ such that $ε≤|$tail flux of $P$ at the $n$-th prime$|$ for every natural $n$, and the series of absolute tail fluxes evaluated at the primes is summable.
background
In the RM2U.NonParasitism module non-parasitism is the statement that the tail flux (boundary term at infinity) vanishes for the ℓ=2 coefficient of the radial profile. The prime schedule is the strictly increasing sequence of primes given by nthPrime. Upstream structures supply supporting objects: NucleosynthesisTiers.of places nuclear densities on φ-tiers, LedgerFactorization.of calibrates the J-cost, IntegrationGap.A fixes the active-edge count at 1, and PhiForcingDerived.of records the J-cost minimization property.
proof idea
This is a structure definition that directly packages the lower-bound and summability fields along the prime schedule. No lemmas are invoked and no tactics are applied; the two properties are introduced by fiat as the required interface.
why it matters
The structure is consumed by bet2_of_primeSchedule to obtain the standard Bet2SelfFalsificationHypothesis. It therefore supplies the schedule-specific bridge inside the single hard non-parasitism gate that isolates the RM2U to RM2 pipeline. The construction touches the open question whether the tail flux vanishes or produces a concrete falsifying lower bound along primes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.