master_absorption
plain-language theorem explainer
The master absorption result shows that the time derivative of the J-cost is non-positive whenever the transport term vanishes and the stretching contribution is bounded above by the negative of the viscous term. Researchers working on Navier-Stokes regularity in the Recognition Science framework would cite this to close energy estimates. The proof is a one-line algebraic reduction that rewrites the split and applies zero addition followed by linear arithmetic.
Claim. Suppose real numbers satisfy $dJ/dt = T + V + S$, $T = 0$, and $S ≤ -V$, where $T$, $V$, and $S$ are the transport, viscous, and stretching contributions. Then $dJ/dt ≤ 0$.
background
The Vortex-Stretching module supplies estimates that close three analytic gaps for the Navier-Stokes equations, drawing on published results including Thapa & Washburn (2026) on finite-volume rigidity. The J-cost is the recognition cost function obeying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), with its time derivative decomposed into transport, viscous, and stretching totals. The upstream zero_add lemma from ArithmeticFromLogic states that zero plus any LogicNat equals the number itself and is invoked here to cancel the transport term in the real setting.
proof idea
This is a one-line term proof. It rewrites the split equality together with the transport-zero hypothesis and the zero_add identity, then applies linarith to extract the non-positivity conclusion from the absorption hypothesis.
why it matters
The result supports closure of the analytic gaps listed in the module documentation and directly precedes the exponential vorticity decay statement in the same file. It supplies the non-positivity control on the J-cost derivative needed for vortex-stretching bounds, consistent with the framework's derivation of spatial dimension D=3 and the phi-ladder mass formula from the forcing chain T0-T8. No open scaffolding questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.