ConstrainedProblem
plain-language theorem explainer
ConstrainedProblem packages a nonempty feasible set of positive reals as the domain for J-cost minimization. Researchers on ledger dynamics in Recognition Science cite it to encode the input conditions for uniqueness results. The definition supplies exactly the set properties required by the convexity argument that follows.
Claim. A constrained problem consists of a nonempty set $S$ of feasible states with every element of $S$ strictly positive.
background
The determinism module formalizes F-007 by showing that J-cost minimization over positive reals is deterministic. J-cost is the non-negative cost of a recognition event, obtained from the derived cost of a multiplicative recognizer comparator and from the ledger factorization on positive ratios. Upstream results establish that this cost is strictly convex on $(0,∞)$, with structures such as PhiForcingDerived supplying the explicit form of J-cost and NucleosynthesisTiers locating physical quantities on the phi-ladder.
proof idea
The declaration is a structure definition that directly assembles the three required fields: the feasible set, a proof of nonemptiness, and a proof that every element is positive. No lemmas are applied beyond the standard Set.Nonempty predicate and the membership predicate on reals.
why it matters
This structure is the sole hypothesis type for the unique_minimizer_principle theorem, which concludes that the next ledger state is uniquely fixed by the current state and the constraint. It thereby supplies the formal core of F-007, confirming deterministic dynamics once J-cost convexity is granted. The construction sits inside the T5 J-uniqueness step of the forcing chain and supplies the domain on which the eight-tick octave and D=3 spatial structure act.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.