RecognizerInducesLogicCert
plain-language theorem explainer
RecognizerInducesLogicCert packages the automatic consequences of any recognizer: its induced cost obeys identity, symmetry, and totality while nontrivial recognition forces a primitive observer on the event space. A physicist or logician tracing the Recognition Science unification to the Law of Logic would cite this certificate to separate definitional Aristotelian conditions from the remaining compositional axiom. The structure is a pure record whose four fields are each justified by prior lemmas on recognizers and observers.
Claim. Let $r$ be a recognizer (surjective map from configuration space to event space). The structure asserts that the induced cost satisfies $cost(w,e,e)=0$, $cost(w,e_1,e_2)=cost(w,e_2,e_1)$, and totality (existence of a real value for every pair), and that nontrivial recognition yields a primitive observer $O$ together with distinct events separated by $O$.
background
A recognizer is a surjective map from configurations to events whose kernel encodes observational indistinguishability. The cost on events is the derived J-cost or multiplicative comparator supplied by upstream definitions in MultiplicativeRecognizerL4 and ObserverForcing. A primitive observer is the interface structure (PrimitiveInterface) that separates distinct outcomes, as defined in ObserverFromRecognition and PreTemporalForcingOrder.
proof idea
The declaration is a pure structure definition. Each field is later instantiated by the downstream construction recognizerInducesLogicCert, which applies Recognizer.identity, Recognizer.non_contradiction, Recognizer.totality, and Recognizer.induces_primitive_observer respectively.
why it matters
The certificate completes the single forcing chain from Recognition Geometry to the Law of Logic described in the companion paper RS_Recognition_Geometry_Logic_Unification.tex. It supplies the three definitional Aristotelian conditions and the primitive observer for free, reducing the remaining content to the RecognizerComposition hypothesis. It directly feeds the inhabited theorem recognizerInducesLogicCert_inhabited and isolates the open question whether composition consistency can be derived from deeper recognition principles.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.