isArgmin
plain-language theorem explainer
A state x minimizes a cost function J over the discrete state space precisely when J(x) is no larger than J(y) for every other state y. Researchers establishing invariance of minimizers under rescaling in Recognition Science cite this definition to anchor the RRF monotone-transform results. The definition is a direct universal quantification with no lemmas or reductions required.
Claim. Let $J : State → ℝ$. A state $x$ is an argmin of $J$ when $J(x) ≤ J(y)$ for every state $y$.
background
In the RRF module, State is the discrete 2D Galerkin state type at truncation level N. J is a cost function whose ordering properties are calibrated by the J-cost structure from PhiForcingDerived. The module proves that argmin sets are invariant under strictly monotone maps g, because only the ordering of values matters for strain measures, not their absolute magnitudes. This matches the Recognition Science emphasis on ordering relations preserved by the forcing chain.
proof idea
The declaration is a direct definition that encodes the argmin property via universal quantification over the state space. No lemmas are invoked and no tactics are applied beyond the built-in meaning of the Prop.
why it matters
This definition supplies the base predicate for the entire suite of monotone-invariance theorems in the module, including argmin_comp_strictMono and argmin_equiv_strictMono. It realizes the claim that the meaning of strain is preserved under any monotone rescaling of J, a direct consequence of the Recognition Science principle that physical outcomes depend only on ordering (T5 J-uniqueness). The definition therefore interfaces abstract cost functions with ledger factorizations and nucleosynthesis tiers that calibrate J in physical units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.