recognizerInducesLogicCert
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not establish composition consistency without the RecognizerComposition hypothesis.
- Does not derive quantitative constants such as the fine-structure constant or the phi-ladder mass formula.
- Does not address non-primitive observers or higher-order recognition structures.
formal statement (Lean)
246def recognizerInducesLogicCert : RecognizerInducesLogicCert where
247 identity_auto := fun r w => Recognizer.identity r w
proof body
Definition body.
248 non_contradiction_auto := fun r w => Recognizer.non_contradiction r w
249 totality_auto := fun r w => Recognizer.totality r w
250 primitive_observer_auto := fun r h => Recognizer.induces_primitive_observer r h
251