pith. machine review for the scientific record. sign in
structure definition def or abbrev high

RecognitionStructure

show as:
view Lean formalization →

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.

claimA 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  91structure RecognitionStructure (S : Type) where
  92  recognizes : S → S → Prop
  93  self_recognition : ∀ s, recognizes s s
  94  symmetric : ∀ s₁ s₂, recognizes s₁ s₂ → recognizes s₂ s₁
  95

used by (29)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.