Strict Monotone Objective Argmax Alignment

Abstract

Strictly increasing objective factorization preserves every feasible argmax set.

Theorem 1.1 (Strictly increasing factorization preserves feasible maximizers).

$$\begin{gathered} \forall Z:Type,S:\mathrm{Set}\left(Z\right),O_A,O_P:Z\to \mathbb{R},g:\mathbb{R}\to \mathbb{R}, \\ \mathrm{StrictMono}\left(g\right)\wedge O_P=g\circ O_A \\ \Rightarrow \{z\mid z\in S\wedge \forall w\in S,O_A(w)\le O_A(z)\}=\{z\mid z\in S\wedge \forall w\in S,O_P(w)\le O_P(z)\}. \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DecisionValueScale/StrictMonotoneObjectiveArgmaxAlignment.strict_monotone_factorization_preserves_argmax (✓ std3). ∎

Source. Repository-derived.

Commentary.

The agent and principal objectives are real-valued functions on the same state-action carrier and are optimized over the same feasible set.

A strictly increasing transform preserves and reflects every weak order comparison, so each feasible candidate is maximal for one objective exactly when it is maximal for the other.

References

• Truth anchor: D5/S3/ConceptDynamics/DecisionValueScale/StrictMonotoneObjectiveArgmaxAlignment.strict_monotone_factorization_preserves_argmax