core_stretching_le_pair_budget
plain-language theorem explainer
The theorem shows that the stretching contribution at each lattice site in a discrete Navier-Stokes flow is bounded by the pairwise stretching change evaluated at the derived amplitude and stretch factor. Discrete fluid modelers and Recognition Science derivations of Navier-Stokes cite this when constructing the full incompressible operator from core flow data. The proof is a direct term-mode reduction that unfolds the amplitude and factor definitions then invokes the core operator's built-in stretching bound.
Claim. Let op be a CoreNSOperator on a lattice with siteCount sites. For each site i the stretching contribution satisfies stretching_i ≤ J(x λ) + J(x/λ) - 2 J(x), where x = |ω_i| / ω_rms is the normalized vorticity amplitude and λ = 1 + Δt · |∇u|_i is the local stretch factor.
background
CoreNSOperator encodes the physical lattice data for a discrete incompressible flow: topology, spacing h, viscosity ν, velocity field, and the divergence-free condition. Pair amplitudes are defined as normalized vorticity |ω_i| / ω_rms; stretch factors are 1 + dt · velocityGradientMag. The pairwiseStretchingChange function returns the net J-cost change for a paired stretching event x → λx together with x → x/λ, using the Recognition Composition Law identity J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y).
proof idea
The proof is a one-line term-mode wrapper. It unfolds pairwiseStretchingChange, corePairAmplitude, and corePairStretchFactor, then applies the stretching_bound field carried inside the CoreNSOperator structure.
why it matters
This bound feeds directly into core_stretching_absorbed (which shows total stretching ≤ -total viscous absorption) and into the construction of the IncompressibleNSOperator structure. It closes the derivation of the six previously free pair-budget fields from the core flow data, consistent with the Recognition Science program of building Navier-Stokes operators from lattice primitives rather than postulating budgets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.