RecognitionLikeStructure
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not require transitivity of the relation.
- Does not construct the relation from a cost function.
- Does not impose non-emptiness or other structure on the carrier.
- Does not reference the J function or phi constants.
formal statement (Lean)
135structure RecognitionLikeStructure where
136 carrier : Type
137 rel : carrier → carrier → Prop
138 refl : ∀ x, rel x x
139 symm : ∀ x y, rel x y → rel y x
140