stretching_absorbed_by_viscosity
plain-language theorem explainer
The theorem shows that for any incompressible Navier-Stokes operator on a finite lattice the summed stretching contributions are bounded above by the negative of the summed viscous contributions. Researchers deriving J-cost monotonicity for discrete fluid models cite this absorption step to close the derivative bound. The proof is a one-line wrapper applying order transitivity to the operator-pair budget bound on stretching followed by the viscosity absorption of that budget.
Claim. For any natural number $N$ and incompressible Navier-Stokes operator $ns$ on $N$ sites, the total stretching satisfies totalStretching$(ns.contributions) ≤ -$totalViscous$(ns.contributions)$, where the totals are formed by summing the sitewise contributions of the operator.
background
J-cost is the cost function induced by a multiplicative recognizer via the Recognition Composition Law, defined as the derived cost of its comparator on positive ratios; the same quantity appears as the cost of any recognition event. The module establishes J-cost monotonicity for the concrete lattice NS operator by deriving transport cancellation from conservative incompressible flux, bounding the stretching term by the operator's own RCL pair budget, and verifying that viscosity absorbs the resulting budget. This theorem supplies the absorption step after the sitewise RCL pair bounds have been summed. Upstream results include the transitivity of the order relation on LogicNat and the cost definitions from observer forcing and multiplicative recognizers.
proof idea
The proof is a one-line wrapper that applies the transitivity lemma le_trans to the two inequalities totalStretching_le_operatorPairBudget ns and operatorPairBudget_absorbed_by_viscosity ns.
why it matters
This result is invoked directly by dJcost_dt_nonpos_of_operator to conclude that the total J-cost derivative is nonpositive once transport cancellation and absorption are established. It completes the bookkeeping portion of the monotonicity program for the discrete incompressible Navier-Stokes operator described in the module documentation. In the Recognition Science setting it supports the claim that J-cost is nonincreasing under lattice evolution, consistent with the forcing-chain landmarks from T5 (J-uniqueness) through T8 (D = 3).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.