LogCriticalMomentFinite
LogCriticalMomentFinite encodes the integrability condition A(r)/r ∈ L¹((1,∞), dr) for the radial coefficient in the RM2U tail obstruction. Navier-Stokes analysts working on the simplified 1D radial model would cite it when checking closure under coercive bounds. The definition is a direct abbreviation that invokes Mathlib's IntegrableOn predicate on the half-line with Lebesgue volume.
claimA radial function $A : ℝ → ℝ$ has finite log-critical moment when $A(r)/r$ is integrable over the interval $(1, ∞)$ with respect to Lebesgue measure, i.e., $∫_{(1,∞)} |A(r)/r| dr < ∞$.
background
The RM2U.Core module supplies the Lean specification for the RM2U tail/tightness gate, reducing the problem to a 1D radial coefficient A(r) for r ≥ 1 at fixed time and direction parameter b. The manuscript expresses the obstruction via the boundary/tail-flux term (-A(r)) · (A'(r) · r²) as r → ∞. This definition isolates the log-critical shell moment as the concrete integrability requirement A(r)/r ∈ L¹((1,∞), dr). Upstream results supply auxiliary A symbols (active edge count, actualization operator, volume) that appear in the broader framework but are not invoked inside this definition.
proof idea
The declaration is a one-line definition that directly applies the IntegrableOn predicate to the function fun r => A r / r over Set.Ioi 1 with respect to volume measure.
why it matters in Recognition Science
It supplies the base predicate for RM2Closed in the RM2Closure sibling module, which encodes the manuscript's one-line Cauchy-Schwarz argument that L² control on A implies the log-critical moment is finite. The definition therefore closes the simplified radial model of the RM2 obstruction and feeds the coerciveL2Bound implication theorem. It sits inside the Navier-Stokes reduction that reuses SkewHarmGate identities from the parent EnergyIdentity layer.
scope and limits
- Does not prove integrability for any concrete A.
- Does not encode the full 3D vector field or time evolution.
- Does not incorporate the direction parameter b or the flux term explicitly.
- Does not address higher moments or Sobolev embeddings beyond L¹ of A/r.
Lean usage
def RM2Closed (A : ℝ → ℝ) : Prop := LogCriticalMomentFinite Aformal statement (Lean)
67def LogCriticalMomentFinite (A : ℝ → ℝ) : Prop :=
proof body
Definition body.
68 IntegrableOn (fun r : ℝ => A r / r) (Set.Ioi (1 : ℝ)) volume
69
70end RM2U
71end NavierStokes
72end IndisputableMonolith