pith. sign in
module module high

IndisputableMonolith.NavierStokes.StretchingPairs

show as:
view Lean formalization →

StretchingPairs defines the J-cost change under paired stretching events on discrete vorticity amplitudes, one scaled by λ and its pair by 1/λ. Researchers tracking monotonicity in the φ-ladder cutoff for Navier-Stokes would cite these objects when assembling pair budgets. The module supplies a collection of definitions and nonnegativity facts built directly on the Recognition Composition Law imported from DiscreteVorticity.

claimFor a paired stretching event with amplitudes transforming as $x \to \lambda x$ and $x \to x/\lambda$, the net change in J-cost satisfies $\Delta J = J(\lambda x) + J(x/\lambda) - 2J(x)$ and is controlled by the Recognition Composition Law.

background

The module operates inside the discrete Navier-Stokes regularity program. It imports DiscreteVorticity, which packages finite vorticity fields on a lattice window together with total, RMS, and normalized amplitudes plus transport, viscous, and stretching contribution fields, and PhiLadderCutoff, which supplies the algebraic core showing that the φ-ladder terminates the energy cascade. The central objects are PairEvent and the associated budget functions that record J-cost increments under reciprocal scalings.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

StretchingPairs supplies the pair-budget and nonnegativity lemmas consumed by DiscreteNSOperator when it derives concrete pair-budget and viscous-absorption fields from the flow's velocity gradient, and by VortexStretching when it closes the three analytic gaps using the cited papers [P1] Thapa & Washburn, [P2] Washburn & Zlatanovic, and [P3] Pardo-Guerra et al.

scope and limits

used by (2)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (11)