kernel_is_equivalence
The kernel relation of any primitive interface on a carrier is an equivalence relation. Workers building recognition lattices or observer certificates cite it to guarantee that observational indistinguishability yields a well-defined quotient. The proof is a one-line term-mode wrapper that assembles the three kernel lemmas into the Equivalence structure.
claimLet $I$ be a primitive interface on carrier $K$, consisting of a positive integer $n$ and an observation map $I.observe : K → Fin n$. The relation $x ∼ y$ defined by $I.observe(x) = I.observe(y)$ is an equivalence relation on $K$.
background
The module proves that non-trivial recognition forces a primitive interface, the minimal structure through which distinctions become events. A PrimitiveInterface on $K$ is a structure with positive $n : ℕ$ and observe : $K → Fin n$, supplying finite resolution; its kernel is the relation observe(x) = observe(y). The local setting is the pre-physical floor before ObserverFormalization upgrades the interface to ledger configurations.
proof idea
The proof is a term-mode construction that directly supplies the Equivalence record: reflexivity from kernel_refl I, symmetry from kernel_symm I, and transitivity from kernel_trans I. No tactics are used; the three sibling lemmas are packaged into the required fields.
why it matters in Recognition Science
This result supplies the iseqv field for interfaceSetoid and the kernel_equiv component of observerFromRecognitionCert and recognitionLatticeCert. It realizes the partition into observational classes required by the Recognizer structure, advancing the chain from distinctions to the primitive observer and the induced logic. The declaration closes the equivalence step in the foundation module without invoking the phi-ladder or physical constants.
scope and limits
- Does not prove or assume that the interface distinguishes at least two points.
- Does not derive the integer n from any recognition axiom.
- Does not interpret the carrier K as a physical configuration space.
- Does not connect the kernel to the phi-ladder or constants such as G or alpha.
Lean usage
def interfaceSetoid {K : Type*} (I : PrimitiveInterface K) : Setoid K where r := I.kernel; iseqv := kernel_is_equivalence Iformal statement (Lean)
69theorem kernel_is_equivalence {K : Type*} (I : PrimitiveInterface K) :
70 Equivalence (I.kernel) :=
proof body
Term-mode proof.
71 ⟨kernel_refl I,
72 fun {x y} h => kernel_symm I (x := x) (y := y) h,
73 fun {x y z} h₁ h₂ => kernel_trans I (x := x) (y := y) (z := z) h₁ h₂⟩
74
75/-! ## Non-Trivial Recognition -/
76
77/-- A carrier has non-trivial recognition when at least two configurations are
78distinguishable. At the primitive floor this is simply the existence of a
79non-equality. -/