bet2_of_primeSchedule
plain-language theorem explainer
Any RM2U radial profile obeying the prime-schedule self-falsification conditions also satisfies the Bet-2 self-falsification hypothesis. Workers on the RM2U non-parasitism gate cite the result to connect a prime-based lower bound on absolute tail flux directly to a contradiction. The term proof extracts the lower bound from the hypothesis, invokes the uniform non-summability lemma on the tail-flux sequence, and obtains an immediate contradiction with the summability premise.
Claim. Let $P$ be an RM2U radial profile. Suppose that failure of tail-flux vanishing implies the existence of $ε>0$ such that $ε≤|tailFlux(P.A,P.A',p_n)|$ for every prime $p_n$, and that the series of absolute tail fluxes along the primes is summable. Then failure of tail-flux vanishing yields a contradiction.
background
The RM2U.NonParasitism module isolates non-parasitism as the vanishing of the tail flux for the ℓ=2 coefficient at infinity. The prime-schedule structure encodes two properties: a positive lower bound on absolute tail flux along the prime sequence whenever vanishing fails, and summability of those absolute values. The target hypothesis is the direct statement that non-vanishing produces falsehood. Upstream results supply the uniform non-summability lemma that converts a positive lower bound into non-summability of the series.
proof idea
The proof is a term-mode wrapper. It assumes the negation of tail-flux vanishing, applies the lower-bound field of the hypothesis to obtain ε and the uniform lower bound, invokes the uniform non-summability lemma on the tail-flux sequence along primes, and obtains a direct contradiction with the summability field.
why it matters
This declaration closes the prime-schedule route to the Bet-2 self-falsification hypothesis inside the non-parasitism gate of RM2U. It supplies the standard interface that downstream RM2 closure arguments can use without reference to the specific prime schedule. The result sits at the interface between the abstract non-parasitism hypothesis and concrete scale-disjointness arguments that exploit the prime sequence for non-resonance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.