unique_minimizer_principle
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not apply when the feasible set fails to be convex.
- Does not apply outside the positive reals.
- Does not construct the feasible set from any particular ledger constraint.
- Does not derive the Born rule or any probability measure.
formal statement (Lean)
60theorem unique_minimizer_principle (p : ConstrainedProblem)
61 (h_convex : Convex ℝ p.feasible)
62 (x_min : ℝ) (hx_feas : x_min ∈ p.feasible)
63 (hx_min : ∀ y ∈ p.feasible, Jcost x_min ≤ Jcost y)
64 (y_min : ℝ) (hy_feas : y_min ∈ p.feasible)
65 (hy_min : ∀ z ∈ p.feasible, Jcost y_min ≤ Jcost z) :
66 x_min = y_min := by
proof body
Tactic-mode proof.
67 by_contra h_ne
68 have hx := hx_min y_min hy_feas
69 have hy := hy_min x_min hx_feas
70 have h_eq : Jcost x_min = Jcost y_min := le_antisymm hx hy
71 -- Strict convexity: Jcost is strictly convex on (0,∞), so equal cost at two points forces equality.
72 have hJ_pos : StrictConvexOn ℝ p.feasible Jcost :=
73 StrictConvexOn.subset Jcost_strictConvexOn_pos
74 (fun z hz => Set.mem_Ioi.mpr (p.positive z hz)) h_convex
75 have h_mid_mem : (x_min + y_min) / 2 ∈ p.feasible := by
76 have hsmul := h_convex hx_feas hy_feas (by norm_num : (0 : ℝ) ≤ 1/2) (by norm_num : (0 : ℝ) ≤ 1/2)
77 (by norm_num : (1/2 : ℝ) + (1/2 : ℝ) = 1)
78 simp only [smul_eq_mul] at hsmul
79 convert hsmul using 1
80 ring
81 have h_strict : Jcost ((x_min + y_min) / 2) < (1/2) * Jcost x_min + (1/2) * Jcost y_min := by
82 have heq : (1/2 : ℝ) • x_min + (1/2 : ℝ) • y_min = (x_min + y_min) / 2 := by
83 simp only [smul_eq_mul]; ring
84 rw [← heq]
85 exact hJ_pos.2 hx_feas hy_feas h_ne (by norm_num : (0 : ℝ) < 1/2) (by norm_num : (0 : ℝ) < 1/2)
86 (by norm_num : (1/2 : ℝ) + (1/2 : ℝ) = 1)
87 -- RHS = Jcost y_min since Jcost x_min = Jcost y_min
88 rw [h_eq, show (1/2 : ℝ) * Jcost y_min + (1/2) * Jcost y_min = Jcost y_min by ring] at h_strict
89 have h_min := hx_min ((x_min + y_min) / 2) h_mid_mem
90 rw [h_eq] at h_min
91 linarith
92
93/-! ## Finite-Resolution Observers -/
94
95/-- An observer with finite resolution sees a coarse-grained state. -/