metaCost_total

formal source

  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⟩
  97
  98/-- The meta-cost is zero iff the realizations are definitionally
  99equal. -/
 100theorem metaCost_eq_zero_iff (R S : MetaCarrier) :
 101    metaCost R S = 0 ↔ R = S := by
 102  unfold metaCost
 103  by_cases h : R = S
 104  · simp [h]
 105  · simp [h]
 106
 107/-! ## Forced-Arithmetic Invariance: The Meta-Theorem -/
 108
 109/-- **The meta-theorem reified.** For any two realizations, the canonical
 110equivalence between their forced arithmetic objects exists. This is
 111exactly `universal_forcing_via_NNO`, packaged as the comparison law of
 112the meta-realization. -/
 113noncomputable def metaForcedArithmeticInvariance (R S : MetaCarrier) :
 114    R.Orbit ≃ S.Orbit :=
 115  universal_forcing_via_NNO R S
 116
 117/-- The meta-theorem is reflexive: comparing a realization to itself
 118yields the identity equivalence on its orbit. -/
 119theorem metaForcedArithmeticInvariance_self (R : MetaCarrier) :
 120    metaForcedArithmeticInvariance R R = Equiv.refl R.Orbit := by
 121  -- Both sides are the canonical NNO equivalence from R to itself,
 122  -- which by uniqueness is the identity.
 123  apply Equiv.ext
 124  intro n
 125  -- The NNO equivalence applied at n satisfies the universal property