PreState
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not specify how a value in [0,1] is generated by any recognition process.
- Does not assert dynamical evolution or time dependence of the state.
- Does not extend the structure to values outside the unit interval or to multiple components.
- Does not connect the cost directly to the phi-ladder or physical constants.
formal statement (Lean)
10structure PreState where
11 val : ℝ
12 in_unit_interval : 0 ≤ val ∧ val ≤ 1
13
14/-- Pre-logical cost landscape on `[0,1]`: minima occur at the boundary states. -/