RecognitionLikeStructure
plain-language theorem explainer
RecognitionLikeStructure equips an arbitrary type with a reflexive symmetric binary relation, serving as the formal target for cost-derived recognition in the forcing theorems. Researchers deriving recognition from ledger costs cite this structure when showing that J-stable configurations induce a recognition object. The declaration is a bare structure definition whose fields are populated by construction in downstream applications.
Claim. A RecognitionLikeStructure on a type $C$ consists of a binary relation $R : C → C → Prop$ together with proofs that $R$ is reflexive ($∀ x : C, R(x,x)$) and symmetric ($∀ x y : C, R(x,y) → R(y,x)$).
background
The RecognitionForcing module proves that recognition is forced by the cost foundation. RecognitionLikeStructure supplies the minimal interface for a reflexive symmetric relation on a carrier, which is instantiated by setting the relation to cost equality on a JStableStructure. Upstream engineering modules provide concrete carriers, such as the 5φ Hz frequency defined in CorticalNeuromodulationDevice.carrier and PhantomCoupledGWAntennaSensitivity.carrier.
proof idea
This is a direct structure definition. No lemmas or tactics are applied; the four fields are declared explicitly and the reflexive and symmetric properties are supplied by construction when the structure is built downstream.
why it matters
RecognitionLikeStructure is the target type in stability_forces_recognition and is used in the master theorem recognition_forcing_complete to assert that every JStableStructure yields a RecognitionLikeStructure. It completes the step from cost stability to a recognition structure, supporting the module claim that recognition is forced by the cost foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.