pairwiseStretchingChange
plain-language theorem explainer
The definition computes the net J-cost change for a paired stretching event that stretches one copy of amplitude x by factor lam while compressing the other by 1/lam. Discrete Navier-Stokes constructions cite this quantity to bound local stretching contributions by available pair budgets. It is introduced as the direct expression J(x lam) + J(x/lam) - 2 J(x) using the canonical cost function satisfying the Recognition Composition Law.
Claim. The net change in J-cost under a paired stretching event of amplitude $x$ and stretch factor $lambda$ is given by $J(x lambda) + J(x / lambda) - 2 J(x)$, where $J$ is the cost function obeying the Recognition Composition Law $J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y)$.
background
The J-cost function is the canonical cost derived from the multiplicative recognizer and satisfying the Composition axiom of the Recognition Composition Law. This module extracts the algebraic identity for paired stretching and compression events to support the J-cost monotonicity program in discrete Navier-Stokes settings. The module remains deliberately PDE-free so that lattice operators can reuse the definitions without creating abstraction cycles. Upstream results include the Composition class from CostAxioms, which encodes the d'Alembert functional equation in multiplicative form, and the cost definitions from ObserverForcing and MultiplicativeRecognizerL4 that realize J as the derived cost on positive ratios.
proof idea
The declaration is a direct definition that expands to the algebraic expression Jcost(x * lam) + Jcost(x / lam) - 2 * Jcost x. Subsequent results apply the Composition axiom to rewrite it as 2 * Jcost x * Jcost lam + 2 * Jcost lam or the factored form 2 * (Jcost x + 1) * Jcost lam.
why it matters
This definition provides the precise cost increment for each paired stretching event and is referenced by the CoreNSOperator and the core_stretching_le_pair_budget theorem in the DiscreteNSOperator module. It realizes the Recognition Composition Law balance for stretching pairs in the Navier-Stokes context, connecting to the phi-ladder and eight-tick octave structures of the broader framework. It supports the program of deriving monotonicity bounds that may bear on the regularity question for the Navier-Stokes equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.