operatorPairBudget_absorbed_by_viscosity
plain-language theorem explainer
The inequality shows that the total RCL pair budget generated by a discrete incompressible Navier-Stokes operator is bounded above by the negative of its summed viscous dissipation. Researchers discretizing fluid equations on lattices within Recognition Science would cite this to close local energy balances before summing to global monotonicity. The proof is a one-line wrapper that invokes the absorption property already stored as a field inside the IncompressibleNSOperator structure.
Claim. Let $N$ be a natural number and let $ns$ be an incompressible Navier-Stokes operator on a lattice with $N$ sites. Then the total pair-event budget of $ns$ satisfies $operatorPairBudget(ns) ≤ -totalViscous(ns.contributions)$.
background
The module supplies a concrete finite-lattice realization of the incompressible Navier-Stokes operator. An IncompressibleNSOperator extends EvolutionIdentity and carries a LatticeTopology, positive lattice spacing $h$, positive viscosity $ν$, a divergence-free velocity field, and a transport flux; from these it derives pair amplitudes and stretch factors that define sitewise RCL pair events. The operatorPairBudget is obtained by summing indexedPairBudget over the pairEventAt map, while totalViscous sums the viscous component of the contribution fields.
proof idea
The proof is a one-line wrapper that applies the pair_budget_absorbed_by_viscosity field of the IncompressibleNSOperator structure. The simpa tactic unfolds operatorPairBudget and pairEventAt to match the stored inequality directly.
why it matters
This theorem is invoked by stretching_absorbed_by_viscosity in the JcostMonotonicity module, where it combines with totalStretching_le_operatorPairBudget to yield totalStretching ≤ -totalViscous. It thereby closes the viscous absorption step for the discrete operator, supporting the Recognition Science derivation of fluid dynamics from the Recognition Composition Law on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.