operator_transport_zero
plain-language theorem explainer
The theorem proves that the total transport contribution of any IncompressibleNSOperator vanishes identically on the finite lattice. Researchers modeling discrete incompressible fluids or establishing J-cost monotonicity cite it to confirm cancellation of conservative transport terms. The term-mode proof is a direct reduction that unfolds totalTransport, rewrites via the operator's transport definition, and invokes the zero-sum result on conservative transport fields.
Claim. Let $N$ be a natural number and let $ns$ be an incompressible Navier-Stokes operator on the $N$-site lattice equipped with its transport flux. Then the sum of the transport contributions equals zero: $totalTransport(ns.contributions) = 0$.
background
The module constructs the IncompressibleNSOperator as a structure extending EvolutionIdentity on a finite three-direction lattice topology. It carries spacing $h$, viscosity $ν$, a divergence-free velocity field, and a transportFlux derived from the core velocity gradient and Laplacian, with pair-budget fields now built from the flow data rather than postulated. The definition totalTransport sums the transport components of ContributionFields. Upstream, total_conservativeTransportField_zero shows that the lattice sum of any conservativeTransportField is zero by rewriting the sum as a difference and using permutation invariance of the flux total.
proof idea
The proof is a one-line wrapper. It unfolds the definition of totalTransport, rewrites the contributions field using the transport_def of the IncompressibleNSOperator, and applies the theorem total_conservativeTransportField_zero to conclude the sum vanishes.
why it matters
This supplies the transport cancellation needed for J-cost monotonicity under discrete NS evolution. It is invoked in dJcost_dt_nonpos_of_operator to combine with stretching absorption and obtain $dJdt ≤ 0$. Within the Recognition framework the result supports dissipation consistent with the J-functional and phi-ladder on a discrete fluid model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.