corePairAmplitude
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not define stretch factors or viscous absorption terms.
- Does not prove positivity of the amplitude; that is a separate theorem.
- Applies only inside the CoreNSOperator; does not extend to the full derived operator.
- Does not encode any time-step or forcing data beyond the carried state.
Lean usage
def useAmplitude {N : ℕ} (op : CoreNSOperator N) (i : Fin N) : ℝ := corePairAmplitude op iformal statement (Lean)
142def corePairAmplitude {siteCount : ℕ} (op : CoreNSOperator siteCount)
143 (i : Fin siteCount) : ℝ :=
proof body
Definition body.
144 |op.state.omega i| / op.omega_rms
145