JStableStructure
plain-language theorem explainer
JStableStructure defines a carrier type equipped with a real-valued cost function that is bounded from below. Researchers tracing the cost-to-recognition forcing path cite it when moving from bounded costs to recognition-like relations. The declaration is a bare structure definition with three fields and no proof obligations.
Claim. A J-stable structure consists of a type $X$ together with a map $c : X → ℝ$ such that there exists $m ∈ ℝ$ with $m ≤ c(x)$ for all $x ∈ X$.
background
The module proves that recognition is forced by the cost foundation. ObservableExtractionMechanism is a structure carrying an extraction map $S → ℝ$ that is non-constant. RecognitionStructure equips a type with a reflexive and symmetric recognition relation. Configuration packages a positive real value for modeling recognition events via LedgerForcing.RecognitionEvent.
proof idea
This is a structure definition introducing the three fields directly. No lemmas or tactics are invoked.
why it matters
It supplies the input type for stability_forces_recognition and stable_to_recognition, which construct RecognitionLikeStructure by equating equal-cost elements. These feed the master theorem recognition_forcing_complete. The structure closes the stability-to-recognition step in the cost foundation argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.