recognizerInducesLogicCert_inhabited
plain-language theorem explainer
The theorem proves that RecognizerInducesLogicCert is inhabited by exhibiting an explicit term. Researchers formalizing the unification of recognition geometry with the law of logic would cite it to confirm that any recognizer automatically yields the three definitional Aristotelian conditions plus a primitive observer. The proof is a one-line term that directly supplies the preceding definition of the certificate.
Claim. There exists a certificate $C$ such that for every recognizer $r : 𝒞 → ℰ$ and weight $w ∈ ℝ$, the induced cost satisfies $r.cost(w, e, e) = 0$, $r.cost(w, e₁, e₂) = r.cost(w, e₂, e₁)$, and for all $e₁, e₂$ there exists $c ∈ ℝ$ with $r.cost(w, e₁, e₂) = c$, together with automatic induction of a primitive observer on the event space.
background
This module unifies Recognition Geometry with the Law of Logic by showing that any recognizer $r : 𝒞 → ℰ$ automatically generates three of the four classical Aristotelian conditions on its event space ℰ. The certificate structure RecognizerInducesLogicCert collects these automatic properties: identity_auto and non_contradiction_auto follow from the equality-induced cost, while totality_auto follows from single-valuedness of the cost function. The upstream definition recognizerInducesLogicCert constructs the certificate by delegating to the Recognizer typeclass lemmas identity, non_contradiction, totality, and induces_primitive_observer. The module doc states that a recognizer supplies the three definitional conditions (L1) Identity, (L2) Non-Contradiction, (L3a) Totality for free, plus a primitive observer, reducing the remaining content to the named compositional hypothesis RecognizerComposition.
proof idea
The proof is a term-mode construction that directly supplies the inhabitant recognizerInducesLogicCert. This preceding definition assembles the certificate by applying the four Recognizer lemmas: identity for the zero self-cost, non_contradiction for symmetry, totality for existence of the cost value, and induces_primitive_observer for the automatic observer.
why it matters
This theorem confirms that RecognizerInducesLogicCert is non-empty, thereby establishing the single forcing chain from Recognition Geometry to the Law of Logic promised in the companion paper. It feeds the unification by showing that three of the four classical conditions arise automatically from the recognizer type signature and equality-induced cost, leaving only the compositional axiom RecognizerComposition as substantive content. The result connects the upstream modules PrimitiveDistinction (definitional facts from equality), MagnitudeOfMismatch (symmetry from single-valuedness), and ObserverFromRecognition (primitive observer from non-trivial recognition).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.