metaCost_eq_zero_iff

formal source

  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
 126  -- of the recursor: it is the unique map R.Orbit → R.Orbit sending
 127  -- orbitZero to orbitZero and intertwining orbitStep. The identity
 128  -- is one such map. By uniqueness, the canonical equivalence equals
 129  -- the identity.
 130  unfold metaForcedArithmeticInvariance universal_forcing_via_NNO