corePairAmplitude_pos
plain-language theorem explainer
The theorem asserts that core pair amplitude, the absolute normalized vorticity at each lattice site, is strictly positive for every CoreNSOperator. Discrete Navier-Stokes modelers in the Recognition Science setting cite it to guarantee non-vanishing pair events when constructing the full incompressible operator. The proof is a direct one-line application of the normalized vorticity positivity field already present in the operator structure.
Claim. For any natural number $n$, any CoreNSOperator $op$ on an $n$-site lattice, and any site index $i$, the core pair amplitude satisfies $0 < |op.state.omega_i| / op.omega_rms$, where $omega$ denotes the vorticity field carried by the state inside $op$.
background
The module constructs a concrete discrete incompressible Navier-Stokes operator surface on a finite three-direction lattice. CoreNSOperator supplies only the physical flow data: lattice topology, mesh size $h>0$, viscosity $nu>0$, a divergence-free velocity field, and the state containing the vorticity field omega. Pair-budget quantities are then derived rather than postulated. corePairAmplitude is defined as the site-wise normalized vorticity $|op.state.omega i| / op.omega_rms$. The upstream PrimitiveDistinction.from result supplies the seven-axiom foundation that yields the structural conditions used to build EvolutionIdentity, which CoreNSOperator extends.
proof idea
The proof is a one-line wrapper that applies the normalized_omega_pos field of the given CoreNSOperator instance at site $i$. No further tactics or reductions are required; the positivity is inherited directly from the operator data.
why it matters
corePairAmplitude_pos supplies the positivity witness required by corePairEvent, which in turn populates the pair fields inside IncompressibleNSOperator. This step completes the DerivedEstimates layer that turns raw core flow data into a fully constructed incompressible operator surface. It sits inside the Recognition Science program of deriving fluid equations from the forcing chain (T0-T8) and the Recognition Composition Law, ensuring the discrete pair events remain non-vanishing before any continuous limit is taken.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.