strictOrder_comp_strictMono
plain-language theorem explainer
Strictly monotone g preserves the strict J-cost ordering on states: if J(x) < J(y) then g(J(x)) < g(J(y)). Researchers establishing argmin invariance under rescalings cite this basic fact. The proof is a direct one-line application of the StrictMono hypothesis to the input inequality.
Claim. Let $g : ℝ → ℝ$ be strictly monotone. For states $x, y$, if $J(x) < J(y)$ then $g(J(x)) < g(J(y))$.
background
The RRF theorems module shows that argmin of the J-cost is invariant under strictly monotone rescalings because only ordering matters, not absolute values. State denotes either the discrete 2D Galerkin state at truncation level N or a finite discrete vorticity field on a lattice window. J is the cost functional whose ordering determines minimization. The result rests on the standard definition of StrictMono from Mathlib.Order.Monotone.Basic.
proof idea
Term-mode proof consisting of a single direct application of the StrictMono hypothesis hg to the given strict inequality hxy.
why it matters
This lemma is the strict-order half of the monotone invariance argument that yields argmin (g ∘ J) = argmin J. It is fundamental to RRF because the physical interpretation of strain is carried by the ordering of J, which survives any monotone rescaling. The module positions it as a prerequisite for the main argmin_comp_strictMono result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.