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

RecognitionStructure

show as:
view Lean formalization →

RecognitionStructure supplies a minimal carrier type U equipped with binary relation R for use in chain constructions. Standalone Lean compilations cite it to isolate the interface before loading full recognition axioms from Foundation modules. The declaration is a bare structure with no attached proofs or constraints.

claimA structure consisting of a carrier type $U$ and a binary relation $R : U → U → Prop$.

background

This definition sits in the Chain module as a compilation stub. The sibling Chain structure requires sequences on U where consecutive elements satisfy R. Upstream, RSNativeUnits.U fixes the gauge with tau0 equal to one tick and ell0 one voxel while c equals 1. The Foundation.RecognitionForcing.RecognitionStructure adds self-recognition and symmetry, and UniversalForcingSelfReference records meta-realization properties for the forcing chain.

proof idea

Direct structure definition with no proof body or tactics.

why it matters in Recognition Science

It supplies the base type for AtomicTick, Ledger, and Chain inside the module. Downstream it instantiates the RecognitionStructure argument in recognition_forcing_complete and recognition_from_extraction. The stub closes a standalone-compilation gap while the richer axioms in Foundation.RecognitionForcing align with T5 J-uniqueness and the Recognition Composition Law.

scope and limits

formal statement (Lean)

   6structure RecognitionStructure where
   7  U : Type
   8  R : U → U → Prop
   9
  10/-- Chain structure with minimal axioms for standalone compilation -/

used by (29)

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

depends on (10)

Lean names referenced from this declaration's body.