recognizer_induces_logic
plain-language theorem explainer
A non-trivial recognizer on an event space automatically supplies the three Aristotelian conditions (identity, non-contradiction, totality) and a primitive observer. Anyone citing the T0/T4 claim that classical logic is induced by recognition, not postulated, points here. The declaration is a one-line public alias of the foundation Unification Theorem.
Claim. Let $r$ be a recognizer from configurations $\mathcal{C}$ to events $\mathcal{E}$, with real weight $w$. If $r$ has non-trivial recognition, then on $\mathcal{E}$: cost vanishes on the diagonal ($r.cost(w,e,e)=0$), cost is symmetric, and the remaining definitional Aristotelian totality condition holds; moreover $r$ itself is the primitive observer. Composition consistency is not part of the claim.
background
RecognitionCore is the public aggregator at the T0/T4 layer of the forcing chain: recognizer, indistinguishability quotient, full recognition signature, and completeness. The module's stance is that a single Boolean observable is atomic, not complete; physical content sits in the admitted recognizer family. Every export here is sorry-free and axiom-free inside the project.
A recognizer pairs a configuration type with an event space and a cost functional. Non-trivial recognition means the event space is populated enough that recognition actually occurs. The three definitional Aristotelian conditions on that space are: identity (self-cost zero), a non-contradiction form (symmetry of cost), and totality. The primitive observer is not an extra structure: it is the recognizer itself.
Upstream, the Unification Theorem states exactly this package under the non-triviality hypothesis, and notes that the fourth condition (composition consistency, the multiplicative d'Alembert / Recognition Composition Law) is not automatic.
proof idea
One-line public abbrev: the declaration is definitionally equal to the foundation Unification Theorem (Foundation.RecognizerInducesLogic.unification). No local proof work; all content is inherited from that theorem's argument under the non-trivial recognition hypothesis.
why it matters
This is a named public citation target in RecognitionCore: the formal claim that a recognizer induces classical logical structure (three Aristotelian conditions plus observer) for free on its event space. It sits at the T0/T4 recognizer/signature layer of the forcing chain, answering how logic appears once recognition is admitted rather than being bolted on as an axiom.
Composition consistency (the d'Alembert form of the Recognition Composition Law) is deliberately excluded; that is the sibling export on the multiplicative event space. Downstream use inside this aggregator is empty so far; the value is the stable citation surface for papers and later modules that need "logic from recognition" without re-opening the foundation file.
Together with recognizer-forces-observer and the quotient/signature completeness exports, it closes the story that observer and logic are recognition-induced, while completeness and RCL remain separate, sharper claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.