PreState
plain-language theorem explainer
PreState encodes a pre-logical configuration as a real number constrained to the closed unit interval. Researchers building cost landscapes or stability predicates in the pre-logical layer cite this structure as the domain for subsequent definitions. The declaration is introduced directly as a structure with a value field and an interval-membership predicate.
Claim. A pre-logical state consists of a real number $val$ satisfying $0 ≤ val ≤ 1$.
background
The PreLogicalCost module defines pre-logical states to support a cost landscape on the unit interval whose minima lie at the endpoints. The sibling definition preCost computes the quadratic $val × (1 - val)$, which vanishes exactly at the boundaries. Upstream cost functions from MultiplicativeRecognizerL4 (derivedCost of a comparator on positive ratios) and ObserverForcing (J-cost of a recognition event) supply the broader cost semantics that this structure instantiates locally.
proof idea
The declaration is a structure definition that directly introduces the type PreState together with its two fields: a real-valued component and the proposition asserting closed-unit-interval membership. No lemmas or tactics are invoked.
why it matters
PreState supplies the domain for the downstream definitions IsStable (preCost equals zero) and preCost itself, as well as the theorem stable_iff_boundary that equates stability with the boundary values 0 and 1. This step populates the pre-logical cost landscape required by the Recognition framework before full recognition events or J-cost analysis are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.