pith. machine review for the scientific record. sign in
def definition def or abbrev high

RM2Closed

show as:
view Lean formalization →

RM2Closed defines the closure property for a radial coefficient A by requiring finiteness of its log-critical moment in the simplified Navier-Stokes model. Researchers on Galerkin ancient solutions cite it when showing that coercive L2 bounds close the RM2U pipeline to BetInstantiationCert. The definition is a direct alias to LogCriticalMomentFinite, packaging the manuscript's one-line Cauchy-Schwarz step that L2 control on A implies L1 control on A/r.

claimFor a radial function $A : (1,∞) → ℝ$, the predicate RM2Closed($A$) holds if and only if the log-critical shell moment $∫_1^∞ |A(r)|/r dr$ is finite.

background

In the RM2U.RM2Closure module the predicate RM2Closed acts as an interface hypothesis that encodes the classical closure step from coercive ℓ=2 control to boundedness of the affine obstruction. The log-critical shell moment is the integral ∫ |A(r)|/r dr over (1,∞), whose finiteness is the concrete content of RM2 in this model. The module doc states that the file hosts the coercive ℓ=2 ⇒ RM2 steps from navier-dec-12-rewrite.tex and keeps the final RM2 statement abstract to avoid scattering assumptions.

proof idea

This is a one-line definition that directly aliases RM2Closed A to LogCriticalMomentFinite A. No lemmas or tactics are invoked; the alias packages the equivalence for downstream use in rm2Closed_of_coerciveL2Bound and the Bet instantiation theorems.

why it matters in Recognition Science

RM2Closed supplies the target property for the RM2 closure inside the Navier-Stokes RM2U pipeline. It is invoked by rm2_closed_for_galerkin, BetInstantiationCert and rm2u_pipeline_complete to certify that coercive L2 bounds on any Galerkin ancient element imply a finite log-critical moment. The definition fills the interface role described in the module doc, connecting the manuscript's Cauchy-Schwarz argument to the Recognition framework's classical fluid bridge at D=3.

scope and limits

Lean usage

theorem rm2_closed_for_galerkin (G : GalerkinAncientElement) : RM2Closed G.profile.A := rm2Closed_of_coerciveL2Bound G.profile G.coercive

formal statement (Lean)

  31def RM2Closed (A : ℝ → ℝ) : Prop :=

proof body

Definition body.

  32  LogCriticalMomentFinite A
  33
  34/-- **Coercive \(\ell=2\) control ⇒ log-critical moment finiteness (RM2 in this simplified model).**
  35
  36This is the Lean translation of the manuscript’s one-line Cauchy–Schwarz argument:
  37
  38If `A ∈ L²((1,∞),dr)`, then `A/r ∈ L¹((1,∞),dr)` since `1/r ∈ L²((1,∞),dr)`.
  39
  40We package it in a way that is robust to later refactors of what “RM2 closed” means:
  41at minimum, coercive control implies the log-critical shell moment is absolutely convergent.
  42-/

used by (15)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (22)

Lean names referenced from this declaration's body.