pith. sign in
module module high

IndisputableMonolith.NavierStokes.StretchingPairs

show as:
view Lean formalization →

StretchingPairs defines the J-cost change for paired stretching events on discrete vorticity amplitudes, where one scales by lambda and its counterpart by 1/lambda. Researchers tracking energy cascades in the Recognition Science Navier-Stokes regularity program cite these pair budgets when establishing monotonicity. The module supplies algebraic identities, non-negativity facts, and budget lemmas built directly from the Recognition Composition Law and upstream phi-ladder cutoff.

claimFor a paired stretching event with amplitude $x$ transforming as $xmapsto lambda x$ and $x mapsto x/lambda$, the cost change is $Delta J(x,lambda)=J(lambda x)+J(x/lambda)-2J(x)$, where $J$ denotes the J-cost function; the module proves $Delta J geq 0$ together with associated pair-event budgets and RCL balance identities.

background

The module sits inside the discrete Navier-Stokes regularity argument of Recognition Science. It imports finite vorticity bookkeeping from DiscreteVorticity, which packages lattice-window vorticity fields, total/RMS amplitudes, and transport/viscous/stretching contribution fields for the J-cost monotonicity program. It also imports the algebraic core of the phi-ladder ultraviolet cutoff from PhiLadderCutoff. Local objects include PairEvent, pairEventBudget, totalPairBudget, and indexedPairBudget, all expressed in terms of the J-cost and the Recognition Composition Law.

proof idea

This is a definition module whose lemmas are established by direct algebraic expansion using the Recognition Composition Law together with non-negativity of the J-cost defect. Key steps factor pairwise_RCL_balance, verify pairwiseStretching_nonneg by sign analysis of the resulting quadratic form, and confirm budget non-negativity for pairEventBudget and totalPairBudget by summation over lattice sites.

why it matters in Recognition Science

StretchingPairs supplies the pair-budget primitives consumed by DiscreteNSOperator when deriving concrete pair-budget and viscous-absorption fields from velocity gradients and Laplacians. These objects in turn feed VortexStretching, which closes the three analytic gaps for the Navier-Stokes regularity theorem by invoking published results on finite-volume rigidity and uniqueness of the canonical reciprocal cost.

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)