JStableStructure
plain-language theorem explainer
JStableStructure defines a carrier type paired with a real-valued cost function bounded from below. Researchers citing the Recognition Forcing results use it as the interface for theorems that convert stable cost minima into recognition relations. The declaration is a direct structure definition with three fields and no proof body.
Claim. A J-stable structure consists of a type $C$ equipped with a function $cost : C → ℝ$ such that there exists $m ∈ ℝ$ with $m ≤ cost(x)$ for all $x ∈ C$.
background
The RecognitionForcing module proves that recognition is forced by the cost foundation. It builds on ObservableExtractionMechanism, a structure supplying a nonconstant extraction map from type S to reals, and RecognitionStructure, which equips S with a reflexive and symmetric recognizes relation. Upstream cost definitions appear in ObserverForcing (cost of a recognition event equals its J-cost) and MultiplicativeRecognizerL4 (derived cost of a comparator on positive ratios). The module doc states that this module proves that recognition is forced by the cost foundation.
proof idea
As a structure definition with zero proof lines, JStableStructure is introduced by declaring its three fields: carrier of type Type, cost mapping carrier to reals, and the existential lower bound on cost values.
why it matters
This structure supplies the interface for Part 3 of the module. It is used directly by stability_forces_recognition to produce a RecognitionLikeStructure with identical carrier and by recognition_forcing_complete as one conjunct in the master theorem. The construction aligns with the Recognition Science framework by linking bounded J-cost to recognition events, including the zero-cost self-recognition case at ratio 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.