total_conservativeTransportField_zero
The theorem shows that the sum over lattice sites of flux(i) minus flux(perm(i)) vanishes for arbitrary real-valued flux and any permutation of the finite site set. Discrete Navier-Stokes modelers cite it to confirm global cancellation of conservative transport contributions. The tactic proof unfolds the sum and difference definitions, distributes the summation, invokes permutation invariance of the finite sum, and cancels by ring arithmetic.
claimLet $n$ be a natural number, let $f : [n] → ℝ$, and let $σ$ be any permutation of $[n]$. Then $∑_{i=0}^{n-1} (f(i) - f(σ(i))) = 0$.
background
A ScalarField on a lattice of siteCount sites is a map from Fin siteCount to the reals. The conservativeTransportField is the pointwise difference between a given flux and the same flux evaluated after a permutation, which encodes a conservative redistribution of the scalar quantity across sites. The total operator is the sum of field values over the finite set of sites. The module constructs concrete discrete differential operators on a finite three-direction lattice to realize an incompressible Navier-Stokes surface whose pair-budget fields are derived from the core flow data.
proof idea
The proof is a short tactic sequence. It unfolds total and conservativeTransportField, rewrites the sum of differences via Finset.sum_sub_distrib, replaces the permuted sum by the original sum using Equiv.sum_comp, and finishes with ring simplification.
why it matters in Recognition Science
This lemma supplies the cancellation step for core_transport_zero and operator_transport_zero, which assert that totalTransport vanishes for both the CoreNSOperator and the full IncompressibleNSOperator. It thereby closes the structural conservation property for the derived pair-budget and viscous-absorption fields. Within the Recognition framework the result instantiates the global cancellation required by the forcing chain when transport is realized on a finite lattice.
scope and limits
- Does not address convergence to the continuous Navier-Stokes equations.
- Does not restrict the choice of flux or permutation beyond being defined on the finite site set.
- Does not supply bounds on the size of individual transport terms.
Lean usage
exact total_conservativeTransportField_zero flux permformal statement (Lean)
73theorem total_conservativeTransportField_zero {siteCount : ℕ}
74 (flux : ScalarField siteCount) (perm : Equiv.Perm (Fin siteCount)) :
75 total (conservativeTransportField flux perm) = 0 := by
proof body
Tactic-mode proof.
76 unfold total conservativeTransportField
77 rw [Finset.sum_sub_distrib]
78 have hperm : (∑ i : Fin siteCount, flux (perm i)) = ∑ i : Fin siteCount, flux i := by
79 simpa using (Equiv.sum_comp perm flux)
80 rw [hperm]
81 ring
82
83/-! ## Velocity Gradient Magnitude -/
84
85/-- Maximum absolute forward difference across all component/direction pairs. -/