GalerkinAncientElement
plain-language theorem explainer
GalerkinAncientElement packages an ancient Navier-Stokes Galerkin truncation at level N together with its RM2U radial profile, weighted L2 moment, coercive bound from the energy inequality, and operator pairing integrability. Researchers closing the RM2U pipeline for Navier-Stokes regularity in the Recognition Science setting cite this structure when discharging the Bet1 integrability route. The definition is realized by a constructor that derives the coercive and pairing fields directly from an ancient energy decay hypothesis via two upstream
Claim. A structure consisting of a truncation level $N$, an RM2U radial profile $A(r)$, a proof that the weighted $L^2$ moment satisfies $∫_1^∞ A(r)^2 r^2 dr < ∞$, a coercive $L^2$ bound extracted from the Galerkin energy inequality at level $N$, and integrability of the operator pairing rm2uOp·A·r² in $L^1(1,∞)$.
background
The RM2U Bet Instantiation module connects the weighted L2 moment hypothesis to the full RM2U closure pipeline for ancient Navier-Stokes elements. Key local definitions are the RM2URadialProfile (the ℓ=2 radial coefficient), WeightedL2Moment (finite energy from ∫|u|² < ∞), CoerciveL2Bound (from the Galerkin energy inequality), and OperatorPairingIntegrable (Hölder plus AM-GM control of the three rm2uOp terms). The module imports Core, EnergyIdentity, NonParasitism, RM2Closure, and TailFluxInstantiation to support the Bet1 path: weighted moment plus coercive bound yields Bet1BoundaryIntegrableHypothesis, which yields NonParasitismHypothesis and finally RM2Closed.
proof idea
The structure is introduced with five fields. The ofDecay constructor assigns N and profile directly from the inputs, sets finite_energy to the supplied WeightedL2Moment, obtains coercive by applying ancientDecay_implies_coercive to the decay hypothesis, and obtains operator_pairing by applying operatorPairing_of_decayFull to the full decay datum.
why it matters
This structure supplies the concrete data that lets bet1_for_galerkin, bet1_original_for_galerkin, nonParasitism_for_galerkin, and bet2_for_galerkin discharge the Bet1 and Bet2 interfaces for any Galerkin ancient element. It feeds directly into BetInstantiationCert, which certifies that the RM2U pipeline is closed. The construction fills the energy-inequality step in the Recognition Science treatment of Navier-Stokes regularity and touches the open question of whether the full closure implies global regularity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.