weakOrder_comp_mono
plain-language theorem explainer
Monotone maps preserve the weak ordering induced by the J-cost on discrete states. Researchers on recognition rate functions cite this to establish that rescaling the cost leaves state orderings unchanged. The proof is a direct one-line application of the monotonicity hypothesis to the input inequality.
Claim. Let $g : ℝ → ℝ$ be monotone. For discrete states $x, y$ satisfying $J(x) ≤ J(y)$, it holds that $(g ∘ J)(x) ≤ (g ∘ J)(y)$.
background
In the RRF module, J is the cost functional whose ordering determines argmin sets on states. The local setting states that if g is strictly monotone then argmin(g ∘ J) equals argmin J, so the meaning of strain is preserved under any monotone rescaling. Upstream, State from CPM2D is the discrete 2D Galerkin state type at truncation level N, while State from DiscreteVorticity is a finite discrete vorticity field on a lattice window of siteCount sites.
proof idea
The proof is the one-line term that applies the monotonicity hypothesis hg directly to the given inequality hxy.
why it matters
This weak-order result supports the module's main theorems on argmin invariance under strictly monotone transforms. It supplies the ordering preservation needed for the strict-mono cases that establish equivalence of argmin sets. In the Recognition framework it ensures J-cost orderings remain stable under monotone rescalings, consistent with the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.