PairEvent
plain-language theorem explainer
PairEvent supplies a structure for a single paired stretching event consisting of a positive real amplitude and positive real stretch factor. Discrete Navier-Stokes modelers cite it when building finite J-cost budgets for stretching pairs under the Recognition Composition Law. The declaration is a direct structure definition whose four fields enforce positivity to guarantee non-negative contributions to pairwise RCL balance.
Claim. A paired stretching event consists of positive real numbers $a > 0$ (amplitude) and $s > 0$ (stretch factor) together with proofs of these inequalities.
background
The module isolates the algebraic core behind J-cost monotonicity for discrete stretching and compression events. It supplies the exact Recognition Composition Law balance for such pairs and finite pair budgets indexed by lists or lattice sites, remaining PDE-free so that concrete discrete Navier-Stokes operators can reuse the same definitions without abstraction cycles. Upstream, the cost of a recognition event is defined as its J-cost via the derived cost of a multiplicative recognizer comparator, and the unit elements in logic integers and rationals are supplied as base cases.
proof idea
Introduced directly as a structure definition with four fields: amplitude and stretchFactor as reals, plus explicit positivity proofs. No lemmas or tactics are invoked; the structure simply packages the data and constraints for downstream budget functions.
why it matters
This definition feeds corePairEvent and pairEventAt in DiscreteNSOperator, as well as indexedPairBudget, pairEventBudget, and their non-negativity theorems that sum J-cost contributions over lattice sites. It supplies the algebraic core for the RCL balance program in the Navier-Stokes module, aligning with J-uniqueness (T5) and the Recognition Composition Law in the forcing chain. No open scaffolding questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.