metaForcedArithmeticInvariance

formal source

 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
 131    IsNaturalNumberObject.equiv
 132  simp only [Equiv.refl_apply, Equiv.coe_fn_mk]
 133  -- Use the recursor uniqueness: the recursor with target (R.orbitZero, R.orbitStep)
 134  -- is the identity.
 135  have h_id_zero : (id : R.Orbit → R.Orbit) R.orbitZero = R.orbitZero := rfl
 136  have h_id_step : ∀ k, (id : R.Orbit → R.Orbit) (R.orbitStep k) =
 137      R.orbitStep ((id : R.Orbit → R.Orbit) k) := fun _ => rfl
 138  have huniq := (realizationOrbit_isNNO R).recursor_unique
 139    R.orbitZero R.orbitStep
 140    (id : R.Orbit → R.Orbit) h_id_zero h_id_step n
 141  -- huniq : id n = (realizationOrbit_isNNO R).recursor R.orbitZero R.orbitStep n
 142  -- Goal : (realizationOrbit_isNNO R).recursor R.orbitZero R.orbitStep n = n
 143  -- `id n` reduces to `n`.