structure ISAR.Kernel : Type 1

An admissible semantic kernel (view) over the invariant quotient. It consists of:

1. A carrier type.
2. A view mapping fragment terms to the carrier.
3. An equivalence relation representing observational equivalence in the view.
4. Soundness: operational equivalence in the fragment implies equivalence in the view.
5. A decoding/reconstruction mapping back to the fragment.
6. Coherence axioms:
   • decode (view M) ≈ M
   • view (decode c) ≈ c
   • c1 ≈ c2 implies decode c1 ≈ decode c2

• Carrier : Type
• view_of : ISKSubtype → self.Carrier
• view_eq : self.Carrier → self.Carrier → Prop
• is_equiv : Equivalence self.view_eq
• sound (t u : ISKSubtype) : OperEq t u → self.view_eq (self.view_of t) (self.view_of u)
• decode : self.Carrier → ISKSubtype
• decode_view (t : ISKSubtype) : OperEq (self.decode (self.view_of t)) t
• view_eq_decode (c : self.Carrier) : self.view_eq (self.view_of (self.decode c)) c
• decode_eq (c1 c2 : self.Carrier) : self.view_eq c1 c2 → OperEq (self.decode c1) (self.decode c2)

def ISAR.Kernel.setoid (K : Kernel) : Setoid K.Carrier

Observational equivalence setoid on the carrier of a Kernel.

Equations

• K.setoid = { r := K.view_eq, iseqv := ⋯ }

@[reducible, inline]

abbrev ISAR.ISAR_Kernel : Kernel

The canonical ISAR quotient presentation itself as a Kernel.

Equations

• ISAR.ISAR_Kernel = { Carrier := ISAR.ISKSubtype, view_of := id, view_eq := ISAR.OperEq, is_equiv := ⋯, sound := ⋯, decode := id, decode_view := ⋯, view_eq_decode := ⋯, decode_eq := ⋯ }

def ISAR.ComputableISAR_Kernel (fuel : ℕ) : Kernel

The computable ISAR kernel parametrized by normalization fuel.

Equations

• One or more equations did not get rendered due to their size.

def ISAR.ComputableISAR_Kernel_Optimal (t : ISKSubtype) (_ht : LinearIKTerm ↑t) : Kernel

The optimal computable ISAR kernel for linearly-typed terms.

Equations

• ISAR.ComputableISAR_Kernel_Optimal t _ht = ISAR.ComputableISAR_Kernel (ISAR.sufficient_fuel t)

structure ISAR.KernelHom (K1 K2 : Kernel) : Type

A structure-preserving morphism between semantic kernels. Must preserve the view mapping and map equivalent carrier elements to equivalent elements.

• hom : K1.Carrier → K2.Carrier
• hom_view (t : ISKSubtype) : K2.view_eq (self.hom (K1.view_of t)) (K2.view_of t)
• hom_congr (c1 c2 : K1.Carrier) : K1.view_eq c1 c2 → K2.view_eq (self.hom c1) (self.hom c2)

def ISAR.canonical_hom (K : Kernel) : KernelHom K ISAR_Kernel

The canonical structure-preserving morphism from any Kernel K into ISAR_Kernel.

Equations

• ISAR.canonical_hom K = { hom := K.decode, hom_view := ⋯, hom_congr := ⋯ }

theorem ISAR.morphism_uniqueness (K : Kernel) (f : KernelHom K ISAR_Kernel) (c : K.Carrier) : OperEq (f.hom c) (K.decode c)

Uniqueness (Terminality) Theorem: Every structure-preserving morphism f : K → ISAR_Kernel from any admissible semantic kernel K into the canonical ISAR presentation is observationally equivalent to the canonical decoding morphism.

def ISAR.HomEquiv (K : Kernel) (f g : KernelHom K ISAR_Kernel) : Prop

Observational equivalence between morphisms K → ISAR_Kernel.

Equations

• ISAR.HomEquiv K f g = ∀ (c : K.Carrier), ISAR.OperEq (f.hom c) (g.hom c)

@[implicit_reducible]

instance ISAR.homSetoid (K : Kernel) : Setoid (KernelHom K ISAR_Kernel)

Setoid instance for quotienting morphism space modulo observational equivalence.

Equations

• ISAR.homSetoid K = { r := ISAR.HomEquiv K, iseqv := ⋯ }

theorem ISAR.ISAR_Kernel_terminal (K : Kernel) : ∃! _f_class : Quotient (homSetoid K), True

ISAR Kernel Terminality.

The quotient of the morphism space KernelHom K ISAR_Kernel modulo observational equivalence is a singleton (unique existence holds).

Proof: Existence follows constructively from canonical_hom K. Uniqueness follows by applying morphism_uniqueness to show that any structure-preserving morphism is observationally equivalent to canonical_hom K (the canonical decoding).

False-variant: junk on the carrier, not a disproof of terminality

view_eq := True cannot inhabit Kernel: decode_eq + decode_view would force all terms OperEq-related, contradicting distinct atom NFs.

DegenerateKernel still inhabits Kernel by ignoring a Bool tag in view_eq. Terminality holds; observations do not see the tag. This is a regression that the interface does not force view_eq to be equality on Carrier. It is not a disproof of ISAR_Kernel_terminal.

theorem ISAR.NormalI_norm_atom : NormalI ITerm.norm

theorem ISAR.NormalI_konst_atom : NormalI ITerm.konst

theorem ISAR.not_OperEq_norm_konst : ¬OperEq ⟨ITerm.norm, ISKTerm.norm⟩ ⟨ITerm.konst, ISKTerm.konst⟩

theorem ISAR.no_indiscrete_Kernel (K : Kernel) (h : ∀ (c1 c2 : K.Carrier), K.view_eq c1 c2) : False

An indiscrete view_eq would collapse OperEq; hence no such Kernel.

def ISAR.DegenerateKernel : Kernel

Carrier is ISKSubtype × Bool; view_eq ignores the tag.

Equations

• One or more equations did not get rendered due to their size.

theorem ISAR.DegenerateKernel_view_eq_ignores_tag (t : ISKSubtype) : DegenerateKernel.view_eq (t, false) (t, true)

theorem ISAR.DegenerateKernel_carriers_not_eq (t : ISKSubtype) : (t, false) ≠ (t, true)

theorem ISAR.DegenerateKernel_terminal : ∃! _f_class : Quotient (homSetoid DegenerateKernel), True