unique_minimizer_principle
plain-language theorem explainer
The unique minimizer principle states that J-cost minimization over any convex feasible set of positive reals admits exactly one solution. Researchers modeling deterministic ledger updates in Recognition Science cite it to conclude that each constrained step has no branching choice. The argument proceeds by contradiction: equal costs at two distinct points plus strict convexity yield a strictly lower cost at their midpoint, violating the minimality assumption.
Claim. Let $F$ be a nonempty convex subset of $(0,∞)$ and let $J$ be the J-cost function. If $x,y∈F$ both satisfy $J(x)≤J(z)$ and $J(y)≤J(z)$ for every $z∈F$, then $x=y$.
background
ConstrainedProblem is the structure whose feasible field is a nonempty set of positive reals; the positive predicate enforces that every element lies in $(0,∞)$. Jcost is the cost function induced by the multiplicative recognizer (or equivalently by any RecognitionEvent), whose strict convexity on $(0,∞)$ is recorded in the upstream theorem Jcost_strictConvexOn_pos. The local setting is the F-007 determinism argument: J-cost minimization supplies the unique next ledger state once a convex constraint (for example log-sum = constant) is imposed.
proof idea
Assume two distinct minimizers x_min and y_min. Apply le_antisymm to the two minimality inequalities to obtain Jcost x_min = Jcost y_min. Form the StrictConvexOn instance on the feasible set by restricting Jcost_strictConvexOn_pos via subset. Convexity of the feasible set places the midpoint inside it. The strict-convexity inequality then gives Jcost(midpoint) < Jcost x_min, contradicting minimality of x_min; linarith closes the contradiction.
why it matters
This theorem supplies the deterministic core of F-007: because the J-cost landscape is strictly convex, every constrained ledger update is forced to a single successor state. It therefore grounds the claim that apparent randomness is an artifact of finite-resolution projection rather than intrinsic nondeterminism. The result sits immediately downstream of the strict-convexity fact in Cost.Convexity and feeds the observer-forcing and projection-lossy constructions that follow in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.