recognizerInducesLogicCert
plain-language theorem explainer
A definition assembles the automatic properties of any recognizer into the RecognizerInducesLogicCert structure. Researchers working on the unification of recognition geometry with the law of logic would cite this to record that identity, non-contradiction, and totality hold definitionally from the recognizer type signature plus equality. The construction is a direct record that delegates each of its four fields to the corresponding property already present on the Recognizer type.
Claim. The recognizer-induces-logic certificate is the structure whose fields are the maps identity_auto : ∀ {𝒞 ℰ} (r : Recognizer 𝒞 ℰ) (w : ℝ), ∀ e : ℰ, r.cost w e e = 0; non_contradiction_auto : ∀ {𝒞 ℰ} (r : Recognizer 𝒞 ℰ) (w : ℝ), ∀ e₁ e₂ : ℰ, r.cost w e₁ e₂ = r.cost w e₂ e₁; totality_auto : ∀ {𝒞 ℰ} (r : Recognizer 𝒞 ℰ) (w : ℝ), ∀ e₁ e₂ : ℰ, ∃ c : ℝ, r.cost w e₁ e₂ = c; and primitive_observer_auto supplying the primitive observer induced by r.
background
A recognizer is a surjective map from configuration space 𝒞 to event space ℰ whose kernel encodes observational indistinguishability. The cost function on events is induced by equality on configurations, as developed in the PrimitiveDistinction and MagnitudeOfMismatch modules. The module documentation states that this setup forces the three definitional Aristotelian conditions (L1 identity, L2 non-contradiction, L3a totality) automatically while reducing composition consistency to an explicit hypothesis; the recognizer itself supplies the primitive observer in the sense of ObserverFromRecognition.
proof idea
The definition constructs the structure by supplying each field via a lambda expression that directly invokes the corresponding automatic property already defined on the Recognizer type: identity, non_contradiction, totality, and induces_primitive_observer.
why it matters
This definition exhibits the concrete certificate that realizes the forcing chain from recognition geometry to the law of logic. It is used by the inhabited theorem to establish that the certificate type is nonempty. In the Recognition Science framework it shows that three of the four classical conditions are definitional, leaving only the compositional axiom as substantive content and thereby reducing the Aristotelian framework to a single named hypothesis as promised by the companion paper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.