RecognitionStructure
plain-language theorem explainer
RecognitionStructure equips a type S with a reflexive and symmetric binary relation recognizes. Chain, ledger, and atomic tick constructions cite this to instantiate minimal recognition on observables or extraction mechanisms. The declaration is a bare structure with three fields and no proof obligations.
Claim. A recognition structure on a type $S$ consists of a relation $R : S → S → Prop$ such that $R(s,s)$ holds for every $s$ and $R(s_1,s_2)$ implies $R(s_2,s_1)$.
background
The RecognitionForcing module shows that recognition structures are forced by the cost ledger. Upstream, the Chain module supplies a minimal stub with carrier U and relation R. The RRF.Core and MetaPrinciple modules re-export analogous structures; MetaPrinciple requires only an existential self-recognition clause. This local version strengthens the stub by mandating explicit reflexivity and symmetry on the recognizes field.
proof idea
Direct structure definition. The three fields are introduced verbatim: the relation, the universal self-recognition axiom, and the symmetry implication. No tactics or lemmas are applied.
why it matters
This structure is the target of recognition_forcing_complete and cost_to_recognition_bridge. It is instantiated by AtomicTick, Chain, and Ledger in the Chain module. Within the Recognition Science framework it supplies the minimal relational axioms that connect the J-cost foundation to the eight-tick octave and the derivation of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.