RecognitionStructure
plain-language theorem explainer
RecognitionStructure equips any type X with a binary relation recognizes that is reflexive for at least one element. Workers on the meta-principle derivation cite it when constructing ledgers or chains from the requirement that recognition cannot be empty. The declaration is a bare structure with an existence field and no proof obligations.
Claim. A recognition structure on a type $X$ consists of a binary relation $R : X → X → Prop$ together with a witness that there exists at least one $x ∈ X$ such that $R(x,x)$.
background
The module formalizes the meta-principle that nothing cannot recognize itself, so any recognition structure must contain a self-recognizing element. Upstream RecognitionStructure declarations in Chain and Recognition modules supply only a carrier type and relation without the existence axiom; the version here adds the minimal closure. Related one definitions in IntegersFromLogic and RationalsFromLogic supply the numeric scaffolding that later steps attach to this structure.
proof idea
Direct structure definition that introduces the recognizes relation and the has_self_recognition existence field with no further obligations.
why it matters
The structure supplies the carrier type for AtomicTick, Chain, and Ledger in the Chain module and appears inside the recognition_forcing_complete master theorem. It realizes the meta-principle step that precedes ledger formation and the self-similar fixed point phi in the T0-T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.