corePairAmplitude
plain-language theorem explainer
corePairAmplitude supplies the normalized absolute vorticity at each lattice site from a CoreNSOperator. Discrete Navier-Stokes researchers in the Recognition framework cite it when building derived pair events and budgets from raw flow data. The definition is a direct one-line normalization of |omega_i| by the root-mean-square vorticity of the carried state.
Claim. Let $op$ be a CoreNSOperator on a lattice with $N$ sites. For each site $i$, the core pair amplitude is $|omega_i| / omega_{rms}$, where $omega$ is the vorticity field from the state carried by $op$.
background
CoreNSOperator is the structure holding physical data of a discrete incompressible lattice Navier-Stokes flow: lattice topology, spacing $h$, viscosity $nu$, a State containing the vorticity field omega, a divergence-free velocity field, and transport flux. No pair-budget or absorption fields are present; those are derived later in the module. The module constructs a concrete IncompressibleNSOperator surface whose pair-amplitude and stretch fields are now computed from the core rather than postulated.
proof idea
This is a one-line definition that returns the absolute value of the vorticity component at site i divided by the root-mean-square vorticity stored in op.state.
why it matters
corePairAmplitude is the base quantity used to define corePairEvent and to prove corePairAmplitude_pos, core_stretching_le_pair_budget, and core_pair_budget_absorbed. It supplies the amplitude field required by the DerivedEstimates layer that turns a CoreNSOperator into the full IncompressibleNSOperator, closing the construction path described in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.