RecognitionStructure
plain-language theorem explainer
RecognitionStructure axiomatizes a reflexive symmetric relation on an arbitrary type S. It supplies the minimal interface for recognition relations inside the cost-to-recognition forcing. Researchers constructing chains, ledgers or atomic ticks cite this definition when they need a uniform recognition carrier. The entry is a pure structure definition carrying no proof obligations.
Claim. Let $S$ be a type. A recognition structure on $S$ is a binary relation $R : S → S → Prop$ satisfying reflexivity ($∀ s, R(s,s)$) and symmetry ($∀ s_1 s_2, R(s_1,s_2) → R(s_2,s_1)$).
background
The module RecognitionForcing derives recognition structures from the cost foundation (J-cost, ledger events). Upstream RecognitionStructure stubs appear in Chain (minimal U and R) and in RRF.Core.Recognition and MetaPrinciple (existential self-recognition). The present version strengthens self-recognition to a universal axiom and adds symmetry. The module doc states that the entire module proves recognition is forced by the cost foundation.
proof idea
The declaration is a structure definition that directly introduces the recognizes field together with the two required axioms; no tactics or lemmas are applied.
why it matters
RecognitionStructure is the target type for the master theorem recognition_forcing_complete and is instantiated by cost_to_recognition_bridge. It is used to define Chain, Ledger and AtomicTick. The structure supplies the recognition interface required by the T5–T8 forcing steps that convert cost minima into observable recognition events.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.