RecognitionStructure
plain-language theorem explainer
RecognitionStructure is re-exported as the basic carrier type for recognition relations inside the RRF namespace. Chain, Ledger, and AtomicTick constructions cite this alias when they need a universe U equipped with a binary relation R. The abbreviation is a direct one-line alias with no added axioms or structure.
Claim. A recognition structure consists of a type $U$ together with a binary relation $R : U → U → Prop$.
background
In the RRF re-export layer, RecognitionStructure supplies the minimal data needed for any recognition-based construction. It is defined as a pair consisting of a carrier type U and a relation R that records when one element recognizes another. The module doc states that this re-export bridges the base Recognition module to the RRF framework so that downstream objects such as Chain and Ledger can be built without direct imports.
proof idea
This is a one-line abbreviation that directly aliases the Recognition.RecognitionStructure definition from the imported module.
why it matters
The alias is required by the Chain structure, the Ledger bookkeeping structure, and the AtomicTick class. It is used inside the recognition_forcing_complete master theorem that links observable extraction mechanisms to the existence of recognition structures. In the overall framework it supplies the recognition relation that later steps instantiate with J-cost and phi-ladder data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.