stability_forces_recognition
plain-language theorem explainer
Any J-stable structure (a type with a real-valued cost function bounded below) forces existence of a recognition-like structure on the identical carrier. Researchers assembling the recognition forcing chain cite this lemma when building the master theorem. The proof is a one-line wrapper that invokes the stable_to_recognition construction and closes by reflexivity on carriers.
Claim. Let $S$ be a J-stable structure: a type equipped with a cost function $c$ to the reals that is bounded from below. Then there exists a recognition-like structure $R$ (a type with a reflexive symmetric relation) such that the carrier of $R$ equals the carrier of $S$.
background
The RecognitionForcing module proves that recognition structures arise necessarily from cost foundations. JStableStructure packages a carrier type with a cost map to reals together with the assertion that the cost admits a finite lower bound. RecognitionLikeStructure packages the same carrier with a reflexive and symmetric binary relation. The upstream construction stable_to_recognition turns any JStableStructure into a RecognitionLikeStructure by declaring two elements related precisely when their costs coincide.
proof idea
One-line wrapper that applies stable_to_recognition to the input JStableStructure and uses reflexivity to witness the carrier equality.
why it matters
The theorem is invoked by cost_to_recognition_bridge and by the master theorem recognition_forcing_complete. It supplies the direct step from bounded-cost structures to recognition-like structures, consistent with the Recognition Science claim that cost minima coincide with recognition events. No open scaffolding questions are closed by this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.