Bet2SelfFalsificationHypothesis
plain-language theorem explainer
The Bet2SelfFalsificationHypothesis encodes the assumption that non-vanishing tail flux for an RM2URadialProfile immediately yields a contradiction. Researchers closing the RM2U pipeline for Galerkin ancient elements cite it as the clean interface separating the non-parasitism gate from any specific contradiction mechanism. The declaration is a bare structure that packages the implication without derivation steps.
Claim. Let $P$ be an RM2URadialProfile. The hypothesis asserts that if the tail flux does not vanish, i.e., if $¬$TailFluxVanish$(P.A, P.A')$, then falsehood follows.
background
The module isolates non-parasitism as the single hard gate for the RM2U to RM2 pipeline. Non-parasitism requires the tail-flux boundary term at infinity to vanish for the relevant ℓ=2 coefficient; in the notation this is expressed by TailFluxVanish on the pair of radial functions A and A'. An RM2URadialProfile supplies the ℓ=2 radial coefficient together with the associated energy and coercivity data. Upstream results supply the arithmetic and scale machinery (canonical arithmetic objects, φ-powered scales, integration-gap counts) that later instantiate the prime schedule used in sibling theorems.
proof idea
This is a structure definition with no proof body. It directly records the single field selfFalsify as the implication from non-vanishing tail flux to falsehood.
why it matters
The hypothesis supplies the Bet2 route inside BetInstantiationCert, which certifies that the RM2U pipeline closes for any Galerkin ancient element. It is instantiated by bet2_of_primeSchedule (using the canonical strictly increasing pairwise-coprime prime schedule) and by bet2SelfFalsification_of_u4 (via the U4 export bridge). Downstream it feeds nonParasitism_of_bet2 and rm2Closed_of_bet2, thereby discharging the non-parasitism gate required for RM2 closure. In the Recognition framework it supports the single hard statement that keeps the Navier-Stokes RM2U pipeline checkable while leaving the concrete contradiction mechanism open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.