RecognitionLikeStructure
plain-language theorem explainer
RecognitionLikeStructure equips an arbitrary type with a reflexive symmetric relation, serving as the target structure in the cost-to-recognition bridge. It is cited by stability_forces_recognition and recognition_forcing_complete when mapping JStableStructure instances to recognition objects. The declaration is a direct structure definition with no proof obligations or computational reduction.
Claim. A RecognitionLikeStructure consists of a type $C$ together with a binary relation $R$ on $C$ such that $R(x,x)$ holds for every $x$ in $C$ and $R(x,y)$ implies $R(y,x)$ for all $x,y$ in $C$.
background
The RecognitionForcing module shows that recognition structures arise from the cost foundation imported via LawOfExistence and LedgerForcing. RecognitionLikeStructure supplies the minimal relational signature (reflexive and symmetric) used to witness that equal-cost partitions on a JStableStructure yield a recognition-like object. Upstream carrier definitions fix concrete frequencies at $5phi$ Hz, supplying the physical scale for the abstract carrier types that appear in downstream mappings.
proof idea
Direct structure definition; the four fields are introduced by the structure keyword with no tactics or lemmas applied.
why it matters
It is the codomain of stable_to_recognition and is invoked inside stability_forces_recognition and the master theorem recognition_forcing_complete. The declaration therefore closes the forcing step from JStableStructure to RecognitionStructure, completing the module claim that recognition is forced by cost. It aligns with the Recognition Composition Law and the phi-ladder mass formula in the larger T0-T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.