structure ISAR.ObservationalIsomorphism (D1 D2 : Dialect) : Type

An observational isomorphism between two dialects D1 and D2. It establishes that their observation spaces are isomorphic (via f and g), and that they commute with decoding from the invariant substrate quotient.

• f : D1.Obs → D2.Obs
• g : D2.Obs → D1.Obs
• f_congr (o1 o2 : D1.Obs) : D1.ObsEq o1 o2 → D2.ObsEq (self.f o1) (self.f o2)
• g_congr (o1 o2 : D2.Obs) : D2.ObsEq o1 o2 → D1.ObsEq (self.g o1) (self.g o2)
• f_g_inverse (o : D2.Obs) : D2.ObsEq (self.f (self.g o)) o
• g_f_inverse (o : D1.Obs) : D1.ObsEq (self.g (self.f o)) o
• commute (q : InvariantLayer) : D2.ObsEq (self.f (D1.decode q)) (D2.decode q)

theorem ISAR.no_preferred_syntax (D1 D2 : Dialect) (iso : ObservationalIsomorphism D1 D2) (q : InvariantLayer) : D2.ObsEq (iso.f (D1.decode q)) (D2.decode q)

No Preferred Syntax Theorem: If two dialects are observationally isomorphic, then for any state in the invariant substrate q, their decoded observations are isomorphic. Thus, neither syntax is ontologically privileged; they are just different representations of the same underlying substrate state.

def ISAR.ObservationalIsomorphism.refl (D : Dialect) : ObservationalIsomorphism D D

Observational isomorphism is reflexive.

Equations

• ISAR.ObservationalIsomorphism.refl D = { f := id, g := id, f_congr := ⋯, g_congr := ⋯, f_g_inverse := ⋯, g_f_inverse := ⋯, commute := ⋯ }

def ISAR.ObservationalIsomorphism.symm {D1 D2 : Dialect} (iso : ObservationalIsomorphism D1 D2) : ObservationalIsomorphism D2 D1

Observational isomorphism is symmetric.

Equations

• iso.symm = { f := iso.g, g := iso.f, f_congr := ⋯, g_congr := ⋯, f_g_inverse := ⋯, g_f_inverse := ⋯, commute := ⋯ }

def ISAR.ObservationalIsomorphism.trans {D1 D2 D3 : Dialect} (iso1 : ObservationalIsomorphism D1 D2) (iso2 : ObservationalIsomorphism D2 D3) : ObservationalIsomorphism D1 D3

Observational isomorphism is transitive.

Equations

• iso1.trans iso2 = { f := iso2.f ∘ iso1.f, g := iso1.g ∘ iso2.g, f_congr := ⋯, g_congr := ⋯, f_g_inverse := ⋯, g_f_inverse := ⋯, commute := ⋯ }