pairwise_RCL_balance_factored
plain-language theorem explainer
The theorem equates the pairwise stretching change to the factored expression 2(J(x) + 1)J(λ) for positive reals x and λ. Discrete Navier-Stokes modelers working with vorticity stretching would cite this to obtain immediate nonnegativity and quadratic bounds on pair budgets. The proof is a direct rewrite of the base RCL balance followed by algebraic simplification via ring.
Claim. For positive reals $x > 0$ and $λ > 0$, the paired stretching change satisfies $Δ(x, λ) = 2(J(x) + 1)J(λ)$, where $J$ denotes the J-cost function induced by the Recognition Composition Law.
background
The module isolates the algebraic core of paired stretching and compression events under the Recognition Composition Law, remaining deliberately PDE-free so that discrete Navier-Stokes operators can reuse the same J-cost balances. J-cost is the derived cost of a multiplicative recognizer comparator, equivalently the cost of any recognition event, and satisfies nonnegativity by construction. Upstream results include the LedgerFactorization structure calibrating J on positive ratios and the PhiForcingDerived structure of J-cost.
proof idea
One-line wrapper that applies the base pairwise RCL balance theorem and then uses ring to factor the expression.
why it matters
This factorization is invoked by the nonnegativity theorem for pairwise stretching and by the factored bound in vortex stretching. It closes the algebraic step in the J-cost monotonicity program for discrete Navier-Stokes, consistent with the Recognition Composition Law and the phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.