MetaCarrier

formal source

  63/-- The **meta-carrier**: the type of `LogicRealization.{0,0}` instances.
  64This sits in `Type 1` because `LogicRealization.{0,0}` is itself in
  65`Type 1`. -/
  66abbrev MetaCarrier : Type 1 := LogicRealization.{0, 0}
  67
  68/-- The **meta-cost** between two realizations. By Classical decidability,
  69this is `0` if the realizations are propositionally equal and `1`
  70otherwise. The choice is structural: the cost detects definitional
  71distinctness, not orbit non-isomorphism (which by the meta-theorem is
  72always trivial). -/
  73noncomputable def metaCost (R S : MetaCarrier) : ℕ :=
  74  if R = S then 0 else 1
  75
  76/-! ## The Three Definitional Aristotelian Conditions on Meta-Cost -/
  77
  78/-- **(L1) Identity** for the meta-cost: comparing a realization with
  79itself has zero cost. -/
  80theorem metaCost_self (R : MetaCarrier) : metaCost R R = 0 := by
  81  unfold metaCost
  82  simp
  83
  84/-- **(L2) Non-Contradiction** for the meta-cost: the comparison is
  85symmetric in its arguments. -/
  86theorem metaCost_symm (R S : MetaCarrier) : metaCost R S = metaCost S R := by
  87  unfold metaCost
  88  by_cases h : R = S
  89  · subst h; rfl
  90  · have hSR : ¬ S = R := fun h' => h h'.symm
  91    simp [h, hSR]
  92
  93/-- **(L3a) Totality** for the meta-cost: defined on every pair of
  94realizations, returns a value (the function type signature). -/
  95theorem metaCost_total (R S : MetaCarrier) : ∃ c : ℕ, metaCost R S = c :=
  96  ⟨metaCost R S, rfl⟩