46structure ConstrainedProblem where 47 /-- The constraint set (e.g., log-sum = constant) -/ 48 feasible : Set ℝ 49 /-- Feasible set is nonempty -/ 50 nonempty : feasible.Nonempty 51 /-- All feasible points are positive -/ 52 positive : ∀ x ∈ feasible, 0 < x 53 54/-- **Theorem (Determinism core)**: For any constrained minimization of J-cost 55 over a convex set of positive reals, the minimizer is unique. 56 57 This means the next ledger state is uniquely determined by the current 58 state plus the constraint. There is no "choice" — the dynamics are 59 deterministic. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.