IndisputableMonolith.RRF.Theorems.MonotoneArgmin
The MonotoneArgmin module defines the predicate isArgmin for a real-valued cost function J and establishes monotonicity preservation under strictly increasing compositions, constant shifts, and positive scaling. It supplies pure order-theoretic facts for the RRF theorem collection. Researchers deriving uniqueness or stability of minimizers in Recognition Science structures would cite these lemmas. Proofs consist of direct unfoldings of the argmin definition combined with standard monotonicity axioms from Mathlib.
claimA point $x$ satisfies isArgmin$(J,x)$ when $J(x)leq J(y)$ for all $y$. If $f$ is strictly monotone then argmin$(fcirc J)=$ argmin$(J)$. Similar preservation holds for argmin$(J+c)$ and argmin$(aJ)$ when $a>0$.
background
The module works with real-valued functions equipped with the standard order. It introduces isArgmin as the predicate identifying global minimizers of $J$. Imports supply basic facts on monotone maps and order relations from Mathlib.Order. The local setting is the pure-logic layer of RRF theorems, as stated in the parent module: 'These are proven mathematical facts about RRF structures. No physical hypotheses here—just pure logic.'
proof idea
The module organizes a collection of small lemmas. Each result unfolds the isArgmin definition, applies the relevant monotonicity or order-preservation property, and closes by rewriting the inequality. Examples include argmin_comp_strictMono reducing to preservation of strict increase and argmin_add_const following from translation invariance of the order. All steps use elementary tactics on assumptions.
why it matters in Recognition Science
This module feeds the umbrella IndisputableMonolith.RRF.Theorems collection, supplying the order-theoretic facts required for later RRF derivations that rely on minimizer uniqueness or invariance. It fills the pure-mathematics slot in the Recognition Science chain before any physical constants or forcing steps appear. The parent doc-comment underscores that these lemmas remain free of physical content.
scope and limits
- Does not prove existence of an argmin for arbitrary J.
- Does not treat non-real codomains or infinite-dimensional domains.
- Does not incorporate Recognition Science constants or the forcing chain.
- Does not address uniqueness beyond the listed monotonicity claims.