argmin_comp_strictMono
plain-language theorem explainer
Strictly monotone functions preserve the argmin of the cost J over states. Recognition Science workers cite this when rescaling strain costs while retaining the same minimizing configuration. The term proof applies monotonicity of g directly to the argmin inequality in a single step.
Claim. Suppose $g : ℝ → ℝ$ is strictly monotone. If $x$ minimizes the cost $J$, then $x$ minimizes $g ∘ J$.
background
The module treats monotone transform invariance for argmin sets in the RRF setting. State is the discrete 2D Galerkin state type, and $J$ is the cost function whose minimizing states are characterized by the predicate isArgmin. StrictMono $g$ asserts that $g(a) < g(b)$ whenever $a < b$, which implies ordinary monotonicity. Upstream structures supply the J-cost definition and the State type used in the signature.
proof idea
The term proof is a one-line wrapper. It introduces an arbitrary competitor $y$ and applies the monotonicity of $g$ to the inequality $J x ≤ J y$ supplied by the argmin hypothesis.
why it matters
This supplies the forward direction of the equivalence argmin_equiv_strictMono in the same module. The result anchors invariance of argmin sets under strictly monotone maps, a property required for RRF consistency with the Recognition Composition Law and the ordering preserved across the phi-ladder. It leaves open which concrete monotone maps correspond to physical observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.