JStableStructure
JStableStructure equips an arbitrary type with a real-valued cost map that is bounded from below. Workers on the Recognition Forcing chain cite it when passing from cost minima to induced recognition relations. The declaration is a plain structure with three fields and no computational content.
claimA $J$-stable structure consists of a type $C$ together with a function $c:C→ℝ$ such that there exists $m∈ℝ$ with $m≤c(x)$ for every $x∈C$.
background
The RecognitionForcing module shows that recognition structures are forced by the existence of bounded cost functions on carriers. The cost field is the same J-cost appearing in ObserverForcing.cost (the J-cost of a recognition event) and in MultiplicativeRecognizerL4.cost (derivedCost of a comparator). The module setting is the passage from cost minima to RecognitionStructure via the Recognition Composition Law and the uniqueness of J.
proof idea
Direct structure definition. The three fields are introduced verbatim; no lemmas or tactics are invoked.
why it matters in Recognition Science
JStableStructure supplies the input type for stable_to_recognition and stability_forces_recognition, which in turn feed recognition_forcing_complete (the master theorem asserting that every observable extraction mechanism yields a RecognitionStructure). It therefore occupies the stability-to-recognition step that closes the T5 J-uniqueness forcing chain.
scope and limits
- Does not prescribe any explicit functional form for the cost map.
- Does not require the cost map to attain its lower bound.
- Does not assume the carrier is equipped with any algebraic operations.
- Does not invoke the Recognition Composition Law inside the structure itself.
formal statement (Lean)
130structure JStableStructure where
131 carrier : Type
132 cost : carrier → ℝ
133 cost_bounded : ∃ m : ℝ, ∀ x, m ≤ cost x
134