argmin_add_const
plain-language theorem explainer
Shifting the objective J by any real constant leaves its argmin unchanged. Workers on discrete variational problems in fluid or field models cite the result to normalize reference levels without altering the minimizing state. The proof splits the biconditional and applies linear arithmetic in each direction to equate the two inequality families.
Claim. Let $J : State → ℝ$. For any real $c$ and state $x$, $x$ minimizes $J$ if and only if $x$ minimizes the shifted map $s ↦ J(s) + c$.
background
The module develops monotone-transform invariance for argmin in RRF. The predicate isArgmin J x is defined to mean that J(x) ≤ J(y) for every state y. State is supplied by upstream definitions as a discrete Galerkin truncation in 2D fluids or a finite lattice vorticity field; the theorem therefore applies directly to those concrete models. The surrounding results establish that argmin is preserved under any strictly monotone re-mapping of J, with constant addition as the elementary case.
proof idea
Constructor splits the biconditional into two implications. Each direction assumes the argmin property for one functional, instantiates it at an arbitrary y, and invokes linarith to cancel the constant and recover the inequality for the other functional.
why it matters
The lemma supplies a basic normalization tool inside the monotone-invariance package. It supports the module claim that only ordering, not absolute scale, determines the minimizing configuration, which is required for RRF strain interpretations. No downstream uses are recorded, but the result sits alongside the strict-mono and composition lemmas that close the invariance argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.