ObserverFromRecognitionCert
ObserverFromRecognitionCert packages the assertion that any carrier type admitting at least one non-trivial distinction possesses a primitive interface separating that pair, together with the requirement that the interface kernel forms an equivalence. A foundation researcher cites it when passing from raw distinguishable configurations to the minimal separating structure that later modules upgrade to physical observers. The declaration is a structure whose two fields are supplied directly by the forcing lemma and the kernel-equivalence lemma.
claimLet $K$ be any type. If $K$ admits non-trivial recognition (i.e., there exist $x,y$ satisfying the equality distinction), then there exists a primitive interface $O$ on $K$ together with $x,y$ such that the distinction holds and $O$ separates them (distinct observed outcomes). Moreover, for every primitive interface $O$ the induced kernel relation is an equivalence.
background
NontrivialRecognition on a carrier $K$ is the existence of at least one pair of configurations that satisfy the equality distinction predicate. PrimitiveObserver is an alias for PrimitiveInterface, the minimal finite-valued recognizer that maps each configuration to an observed outcome. Separates asserts that the two points land in distinct outcomes under the interface map. The module supplies the pre-physical floor: once a carrier carries even one non-trivial distinction, recognition forces a separating interface whose kernel is reflexive, symmetric and transitive.
proof idea
The declaration is a structure definition. Its first field is populated by the lemma that non-trivial recognition forces a separating primitive interface; its second field is populated by the lemma that every such interface kernel is an equivalence relation. No further tactics or reductions are required inside the structure itself.
why it matters in Recognition Science
The certificate closes the step from raw non-trivial recognition to the primitive observer interface required for the pre-temporal forcing order. It is instantiated to produce the inhabited certificate type used by downstream observer formalization. In the Recognition framework it realizes the claim that an interface is forced by recognition, supplying the minimal event structure before constants, the phi-ladder or spatial dimensions are introduced.
scope and limits
- Does not construct an explicit interface for any concrete carrier.
- Does not address continuous, infinite or physical carriers.
- Does not incorporate measurement, time or the forcing chain T0-T8.
- Does not derive numerical constants such as phi or K.
Lean usage
def observerFromRecognitionCert : ObserverFromRecognitionCert where forced := nontrivial_recognition_forces_observer kernel_equiv := kernel_is_equivalenceformal statement (Lean)
146structure ObserverFromRecognitionCert where
147 forced :
148 ∀ K : Type*, NontrivialRecognition K →
149 ∃ (O : PrimitiveObserver K) (x y : K),
150 equalityDistinction K x y ∧ Separates O x y
151 kernel_equiv :
152 ∀ {K : Type*} (O : PrimitiveObserver K), Equivalence (O.kernel)
153
154/-- Certificate: the primitive observer is forced by non-trivial recognition. -/