pairEventBudget
The definition assigns to each paired stretching event the net J-cost change from simultaneous stretch by a factor and its reciprocal compression. Discrete Navier-Stokes discretizations cite it to aggregate stretching into total pair budgets for viscosity bounds. It is implemented as a direct application of the pairwise stretching change function.
claimFor a paired stretching event with amplitude $a > 0$ and stretch factor $λ > 0$, the J-cost budget is $J(aλ) + J(a/λ) - 2J(a)$, where $J$ is the J-cost function.
background
The module isolates the algebraic core of the J-cost monotonicity program using paired stretching and compression events together with the exact Recognition Composition Law balance. A PairEvent records a positive real amplitude and positive stretch factor. The J-cost function J satisfies the RCL identity that makes the pairwise cost change well-defined and non-negative under the positivity hypotheses. This definition operates in a PDE-free discrete setting so that Navier-Stokes operators can reuse the pair budgets without abstraction cycles. The upstream pairwiseStretchingChange supplies the concrete expression Jcost(x * lam) + Jcost(x / lam) - 2 * Jcost x.
proof idea
The definition is a one-line wrapper that applies pairwiseStretchingChange to the amplitude and stretchFactor components of the PairEvent.
why it matters in Recognition Science
This supplies the per-event J-cost contribution that builds indexedPairBudget and totalPairBudget. It is invoked in the absorption results core_pair_budget_absorbed and core_stretching_absorbed, which show that the derived pair budget is absorbed by viscosity. The construction fills the RCL pair event step in the discrete Navier-Stokes stretching analysis, supporting monotonicity arguments that connect to the broader Recognition Science forcing chain.
scope and limits
- Does not prove that the budget is non-negative.
- Does not address continuous-space limits or infinite lattices.
- Does not include viscous dissipation or external forcing terms.
- Does not establish the absorption inequality; that appears in downstream theorems.
Lean usage
simp only [pairEventBudget]formal statement (Lean)
66def pairEventBudget (ev : PairEvent) : ℝ :=
proof body
Definition body.
67 pairwiseStretchingChange ev.amplitude ev.stretchFactor
68