RecognitionStructure
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.