 186    _ = (realizationLift R B).toFun n := rfl
 187
 188/-- The extracted realization orbit is initial. -/
 189def realization_initial (R : LogicRealization) :
 190    PeanoObject.IsInitial (realizationPeano R) where
 191  lift := realizationLift R
 192  uniq := by
 193    intro B f g
 194    rw [realizationLift_unique_fun R B f, realizationLift_unique_fun R B g]
 195
 196/-- Arithmetic extracted from the realization's own identity-step orbit. -/
 197def extracted (R : LogicRealization) : ArithmeticOf R where
 198  peano := realizationPeano R
 199  initial := realization_initial R
 200
 201/-- Peano surface for the extracted arithmetic of any realization. -/
 202theorem extracted_peanoSurface (R : LogicRealization) :
 203    PeanoSurface (extracted R) where
 204  zero_ne_step := R.orbit_no_confusion
 205  step_injective := R.orbit_step_injective
 206  induction := R.orbit_induction
 207
 208/-- The natural equivalence between two initial Peano objects. -/
 209noncomputable def equivOfInitial {R S : LogicRealization}
 210    (A : ArithmeticOf R) (B : ArithmeticOf S) : A.peano.carrier ≃ B.peano.carrier where
 211  toFun := (A.initial.lift B.peano).toFun
 212  invFun := (B.initial.lift A.peano).toFun
 213  left_inv := by
 214    intro x
 215    have hcomp :
 216        (PeanoObject.Hom.comp (B.initial.lift A.peano) (A.initial.lift B.peano)).toFun =
 217          (PeanoObject.Hom.id A.peano).toFun :=
 218      A.initial.uniq A.peano
 219        (PeanoObject.Hom.comp (B.initial.lift A.peano) (A.initial.lift B.peano))

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.