monotone_preserves_argmin
plain-language theorem explainer
Strictly monotone real functions preserve argmin locations for maps from finite nonempty sets. Recognition Science invokes this to establish that distinct domains share identical structural minima under rescaled costs. The term proof is a direct one-line application of the monotonicity implied by StrictMono to the supplied minimality inequality.
Claim. If $g : ℝ → ℝ$ is strictly monotone and $x_0$ minimizes $f : α → ℝ$ over a finite nonempty set $α$, then $x_0$ also minimizes the composition $g ∘ f$.
background
The RecognitionCategory module constructs a category whose objects are recognition algebras equipped with J-costs and whose morphisms are structure-preserving maps. It imports CostAlgebra for the J-automorphisms (id and comp) and CostAxioms for the Composition class that encodes the Recognition Composition Law: $F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)$. Upstream ArithmeticOf supplies the canonical initial Peano object used to anchor the initial algebra.
proof idea
One-line term proof: introduce the arbitrary element x and apply the fact that StrictMono g yields a monotone map, then substitute the given inequality hmin x.
why it matters
The declaration supplies the monotone invariance principle required for the categorical certificate in the module summary, which states that RS is the initial algebra, domains are functorial images, and representation independence follows from monotone invariance. It closes the loop from the Composition axiom to domain-independent minima without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.