core_transport_zero
plain-language theorem explainer
The core_transport_zero theorem establishes that the summed transport contributions over all lattice sites vanish for any CoreNSOperator. Researchers deriving dissipation bounds or J-cost monotonicity in discrete incompressible flow would cite it to confirm structural conservation. The proof is a direct term reduction that unfolds totalTransport, rewrites via the operator's transport definition, and applies the zero-sum lemma for conservative flux fields on finite sets.
Claim. Let $N$ be a natural number and let $op$ be a CoreNSOperator on an $N$-site lattice with divergence-free velocity and transport flux. Then the total transport field satisfies $T = 0$, where $T$ is the sum over all sites of the transport component of the contribution fields.
background
The module builds a concrete discrete incompressible Navier-Stokes operator on a finite three-direction lattice. CoreNSOperator supplies the minimal physical data: topology, spacing $h>0$, viscosity $ν>0$, divergence-free velocity, and a scalar transport flux; pair-budget and absorption fields are derived later. totalTransport aggregates the transport, stretching, and absorption pieces of the ContributionFields structure. The result rests on the upstream lemma total_conservativeTransportField_zero, which states that the sum of conservativeTransportField flux perm over Fin siteCount equals zero by Finset.sum_sub_distrib and permutation invariance of the flux sum.
proof idea
Term-mode proof: unfold totalTransport to expose the transport sum, rewrite the transport component via op.transport_def (which equates it to conservativeTransportField of the flux under the lattice permutation), then apply total_conservativeTransportField_zero directly.
why it matters
The cancellation supplies the transport hypothesis for core_dJdt_nonpos, which concludes op.dJdt ≤ 0 from the core operator alone. It therefore closes the transport leg of J-cost monotonicity in the discrete Navier-Stokes layer, allowing dissipation to be read off without assuming external pair-budget fields. This step aligns with the Recognition Science program of deriving continuum conservation from finite-lattice structural identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.