unification
plain-language theorem explainer
Any recognizer from configurations to events automatically induces the three definitional Aristotelian conditions (identity, symmetry, totality) on its induced cost together with a primitive observer separating distinct events when recognition is nontrivial. Researchers deriving logic from recognition geometry cite this to reduce the Aristotelian framework to one compositional axiom. The proof is a direct term-mode wrapper applying five lemmas on the recognizer structure.
Claim. Let $r$ be a surjective map from configuration space $𝒞$ to event space $ℰ$. For any real weight $w$, if $r$ has nontrivial recognition then the induced cost satisfies $cost(w,e,e)=0$ for all $e$, $cost(w,e_1,e_2)=cost(w,e_2,e_1)$, totality (a real value exists for every pair), single-valuedness on unordered pairs, and there exists a primitive observer separating some distinct pair of events.
background
A recognizer is a surjective map from configurations to events whose many-to-one character generates the indistinguishability quotient. The cost is the J-cost of the recognition event. The module shows that equality-induced costs on the event space automatically satisfy the definitional Aristotelian conditions while the recognizer itself supplies the primitive observer. MODULE_DOC states: 'A recognizer automatically supplies the three definitional Aristotelian conditions on its event space: (L1) Identity, (L2) Non-Contradiction, (L3a) Totality. These are forced by the equality-induced cost on ℰ together with the type signature of the recognizer.' SingleValuedOnUnorderedPair from MagnitudeOfMismatch supplies the symmetry step.
proof idea
The proof is a one-line wrapper that applies the five lemmas Recognizer.identity, Recognizer.non_contradiction, Recognizer.totality, Recognizer.singleValued, and Recognizer.induces_primitive_observer to the respective conjuncts of the goal via refine.
why it matters
This theorem supplies the definitional half of the forcing chain from Recognition Geometry to the Law of Logic in the companion paper, leaving only the RecognizerComposition hypothesis for the substantive content. It is used by prelogical_boolean_fragment to obtain Boolean-style operations on stable states and by GUTUnification and weinberg_angle_in_range to constrain couplings. It touches the open question whether composition consistency follows from deeper recognition axioms or must remain an independent hypothesis. Relevant to T5 J-uniqueness and the eight-tick octave in the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.