structure ISAR.AdmissibleDialect : Type 1

A Dialect is Admissible if it satisfies the coherence conditions necessary to be presented as an admissible semantic Kernel.

• D : Dialect
• view_of : ISKSubtype → self.D.Object
• view_eq : self.D.Object → self.D.Object → 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_view (t : ISKSubtype) : OperEq (self.D.encode (self.view_of t)) t
• view_eq_decode (obj : self.D.Object) : self.view_eq (self.view_of (self.D.encode obj)) obj
• decode_eq (o1 o2 : self.D.Object) : self.view_eq o1 o2 → OperEq (self.D.encode o1) (self.D.encode o2)

def ISAR.AdmissibleDialect.toKernel (AD : AdmissibleDialect) : Kernel

Canonical translation of any Admissible Dialect into a category-theoretic Kernel.

Equations

• AD.toKernel = { Carrier := AD.D.Object, view_of := AD.view_of, view_eq := AD.view_eq, is_equiv := ⋯, sound := ⋯, decode := AD.D.encode, decode_view := ⋯, view_eq_decode := ⋯, decode_eq := ⋯ }

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

An isomorphism between two category-theoretic Kernels.

• hom1 : KernelHom K1 K2
• hom2 : KernelHom K2 K1
• inverse1 (c : K1.Carrier) : K1.view_eq (self.hom2.hom (self.hom1.hom c)) c
• inverse2 (c : K2.Carrier) : K2.view_eq (self.hom1.hom (self.hom2.hom c)) c

def ISAR.dialect_canonical_hom (AD1 AD2 : AdmissibleDialect) : KernelHom AD1.toKernel AD2.toKernel

Canonical morphism translation from AD1 to AD2 using the substrate as the medium.

Equations

• ISAR.dialect_canonical_hom AD1 AD2 = { hom := fun (obj : AD1.toKernel.Carrier) => AD2.view_of (AD1.D.encode obj), hom_view := ⋯, hom_congr := ⋯ }

def ISAR.isomorphism_unification (AD1 AD2 : AdmissibleDialect) (_iso : ObservationalIsomorphism AD1.D AD2.D) : KernelIsomorphism AD1.toKernel AD2.toKernel

Unification Theorem: Any observational isomorphism between two admissible dialects D1 and D2 induces a category-theoretic KernelIsomorphism between their corresponding Kernels. The translation morphisms are constructed canonicaly using the substrate as the universal medium.

Equations

• ISAR.isomorphism_unification AD1 AD2 _iso = { hom1 := ISAR.dialect_canonical_hom AD1 AD2, hom2 := ISAR.dialect_canonical_hom AD2 AD1, inverse1 := ⋯, inverse2 := ⋯ }

def ISAR.TRS_AdmissibleDialect : AdmissibleDialect

Equations

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

def ISAR.Bytecode_AdmissibleDialect : AdmissibleDialect

Equations

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

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

Universal Factorization Theorem: Every admissible dialect kernel factors uniquely through ISAR_Kernel. We state this for the five concrete semantic views:

1. ZFC / HF Set theory (HF_Kernel)
2. Structural Quantity Calculus (QuantityKernel)
3. Pure SKI Term Rewriting (TRS_AdmissibleDialect.toKernel)
4. Stack VM Bytecode (Bytecode_AdmissibleDialect.toKernel)

def ISAR.OperEq_D {Object : Type} (step : Object → Object → Prop) (o1 o2 : Object) : Prop

Operational equivalence (joinability) on a transition system.

Equations

• ISAR.OperEq_D step o1 o2 = ∃ (o3 : Object), Relation.ReflTransGen step o1 o3 ∧ Relation.ReflTransGen step o2 o3

theorem ISAR.OperEq_D_refl {Object : Type} (step : Object → Object → Prop) (o : Object) : OperEq_D step o o

theorem ISAR.OperEq_D_symm {Object : Type} (step : Object → Object → Prop) {o1 o2 : Object} (h : OperEq_D step o1 o2) : OperEq_D step o2 o1

theorem ISAR.OperEq_D_trans {Object : Type} (step : Object → Object → Prop) (confluent : ∀ (s s1 s2 : Object), Relation.ReflTransGen step s s1 → Relation.ReflTransGen step s s2 → ∃ (s3 : Object), Relation.ReflTransGen step s1 s3 ∧ Relation.ReflTransGen step s2 s3) {o1 o2 o3 : Object} (h1 : OperEq_D step o1 o2) (h2 : OperEq_D step o2 o3) : OperEq_D step o1 o3

noncomputable def ISAR.encode_from_sig (sig : Fin 4 → Fin 4 → ℤ) : ISKSubtype

The encoding function mapping a 4x4 observed causal signature to an ISKSubtype term. Constructively defined using the expressive completeness of the ISK monoid.

Equations

• ISAR.encode_from_sig sig = if h : ISAR.ISKAlgebra (ISAR.toMatrix4 sig) then Classical.choose ⋯ else ⟨ISAR.ITerm.norm, ISAR.ISKTerm.norm⟩

structure ISAR.ConfluentSNSystem : Type 1

A transition system that is confluent, strongly normalizing, and semantically representable via a faithful causal signature into the 4x4 ISAR basis.

• Object : Type
• nonempty : Nonempty self.Object
• step : self.Object → self.Object → Prop
• confluent (s s1 s2 : self.Object) : Relation.ReflTransGen self.step s s1 → Relation.ReflTransGen self.step s s2 → ∃ (s3 : self.Object), Relation.ReflTransGen self.step s1 s3 ∧ Relation.ReflTransGen self.step s2 s3
• sn : WellFounded fun (x y : self.Object) => self.step y x
• causal_signature : self.Object → Fin 4 → Fin 4 → ℤ
• sig_faithful (o1 o2 : self.Object) : self.causal_signature o1 = self.causal_signature o2 → OperEq_D self.step o1 o2
• sig_in_ISK (o : self.Object) : ISKAlgebra (toMatrix4 (self.causal_signature o))
• sig_step (o1 o2 : self.Object) : self.step o1 o2 → self.causal_signature o1 = self.causal_signature o2
• sig_faithful_opereq (o1 o2 : self.Object) : OperEq (encode_from_sig (self.causal_signature o1)) (encode_from_sig (self.causal_signature o2)) → OperEq_D self.step o1 o2
• sig_surjective (t : ISKSubtype) : ∃ (o : self.Object), OperEq (encode_from_sig (self.causal_signature o)) t

noncomputable def ISAR.eval_to_nf (D : ConfluentSNSystem) (o : D.Object) : D.Object

The evaluation function reducing any transition system object to its normal form.

Equations

• ISAR.eval_to_nf D o = ⋯.fix (fun (x : D.Object) (ih : (y : D.Object) → D.step x y → D.Object) => if h : ∃ (y : D.Object), D.step x y then ih (Classical.choose h) ⋯ else x) o

theorem ISAR.eval_to_nf_step (D : ConfluentSNSystem) (o : D.Object) (h : ∃ (y : D.Object), D.step o y) : eval_to_nf D o = eval_to_nf D (Classical.choose h)

theorem ISAR.reflTransGen_head_cases {α : Type} {r : α → α → Prop} {x z : α} (h : Relation.ReflTransGen r x z) : x = z ∨ ∃ (y : α), r x y ∧ Relation.ReflTransGen r y z

theorem ISAR.eval_to_nf_eq_of_reflTransGen (D : ConfluentSNSystem) (o1 o2 : D.Object) (hr : Relation.ReflTransGen D.step o1 o2) : eval_to_nf D o1 = eval_to_nf D o2

theorem ISAR.eval_to_nf_is_nf (D : ConfluentSNSystem) (o : D.Object) : ¬∃ (y : D.Object), D.step (eval_to_nf D o) y

theorem ISAR.reflTransGen_eval_to_nf (D : ConfluentSNSystem) (o : D.Object) : Relation.ReflTransGen D.step o (eval_to_nf D o)

theorem ISAR.causal_signature_eq_of_reflTransGen (D : ConfluentSNSystem) (o1 o2 : D.Object) (hr : Relation.ReflTransGen D.step o1 o2) : D.causal_signature o1 = D.causal_signature o2

theorem ISAR.eval_to_nf_eq_of_OperEq_D (D : ConfluentSNSystem) (o1 o2 : D.Object) (h : OperEq_D D.step o1 o2) : eval_to_nf D o1 = eval_to_nf D o2

theorem ISAR.OperEq_D_of_eval_to_nf_eq (D : ConfluentSNSystem) (o1 o2 : D.Object) (h : eval_to_nf D o1 = eval_to_nf D o2) : OperEq_D D.step o1 o2

theorem ISAR.OperEq_D_iff_eval_to_nf_eq (D : ConfluentSNSystem) (o1 o2 : D.Object) : OperEq_D D.step o1 o2 ↔ eval_to_nf D o1 = eval_to_nf D o2

noncomputable def ISAR.system_view_of (D : ConfluentSNSystem) (t : ISKSubtype) : D.Object

The decoding/projection function mapping substrate terms back to system objects, constructively defined by finding the matching object signature and evaluating to normal form.

Equations

• ISAR.system_view_of D t = if h : ∃ (o : D.Object), ISAR.OperEq (ISAR.encode_from_sig (D.causal_signature o)) t then ISAR.eval_to_nf D (Classical.choose h) else Classical.choice ⋯

theorem ISAR.system_sound (D : ConfluentSNSystem) (t u : ISKSubtype) (h : OperEq t u) : OperEq_D D.step (system_view_of D t) (system_view_of D u)

Soundness of the view mapping: operational equivalence in the substrate implies joinability (OperEq_D) in the system.

theorem ISAR.system_view_of_eq (D : ConfluentSNSystem) (o : D.Object) (t : ISKSubtype) (h : OperEq (encode_from_sig (D.causal_signature o)) t) : system_view_of D t = eval_to_nf D o

Completeness: encoding the view of a term is operationally equivalent to the term itself.

theorem ISAR.system_decode_view (D : ConfluentSNSystem) (t : ISKSubtype) : OperEq (encode_from_sig (D.causal_signature (system_view_of D t))) t

theorem ISAR.system_view_eq_decode (D : ConfluentSNSystem) (obj : D.Object) : OperEq_D D.step (system_view_of D (encode_from_sig (D.causal_signature obj))) obj

Inverse Coherence: viewing the encoding of an object is joinable to the object itself.

theorem ISAR.system_decode_eq (D : ConfluentSNSystem) (o1 o2 : D.Object) (h : OperEq_D D.step o1 o2) : OperEq (encode_from_sig (D.causal_signature o1)) (encode_from_sig (D.causal_signature o2))

Congruence: joinability of objects implies operational equivalence of their encodings.

theorem ISAR.OperEq_D_equiv (D : ConfluentSNSystem) : Equivalence (OperEq_D D.step)

noncomputable def ISAR.confluence_SN_gives_AdmissibleDialect (D : ConfluentSNSystem) : AdmissibleDialect

The Fundamental Theorem of Dialect Realizability (Proven Constructively): Any confluent and strongly normalizing system D with a faithful causal signature into the ISAR basis automatically yields an AdmissibleDialect structure, where the compilation/encoding is constructed semantically from the causal signature rather than being provided by hand.

Equations

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