hasIdentityStep_of_nontrivial

formal source

  69def hasIdentityStep (R : LogicRealization) : Prop :=
  70  ∃ x : R.Carrier, R.compare x R.zero ≠ 0
  71
  72theorem hasIdentityStep_of_nontrivial (R : LogicRealization) :
  73    R.hasIdentityStep :=
  74  R.nontrivial
  75
  76/-- A realization whose internal forced arithmetic embeds faithfully into its
  77ambient carrier. Periodic realizations, such as modular carriers, need not
  78satisfy this; their internal orbit is still free while the carrier
  79interpretation is periodic. -/
  80structure FaithfulArithmeticInterpretation (R : LogicRealization) : Prop where
  81  injective : Function.Injective R.interpret
  82  zero_step_noncollapse : ∀ n : R.Orbit, R.interpret R.orbitZero ≠ R.interpret (R.orbitStep n)
  83
  84/-- Fold over `LogicNat` into the positive-ratio carrier for the selected
  85non-trivial generator. -/
  86noncomputable def positiveRatioOrbitInterpret
  87    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
  88    LogicNat → {x : ℝ // 0 < x}
  89  | LogicNat.identity => ⟨1, one_pos⟩
  90  | LogicNat.step n =>
  91      let γ : ℝ := Classical.choose h.non_trivial
  92      let x := positiveRatioOrbitInterpret C h n
  93      ⟨γ * x.1, mul_pos (Classical.choose_spec h.non_trivial).1 x.2⟩
  94
  95@[simp] theorem positiveRatioOrbitInterpret_val
  96    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) (n : LogicNat) :
  97    (positiveRatioOrbitInterpret C h n).1 =
  98      ArithmeticFromLogic.embed (ArithmeticFromLogic.generatorOfLawsOfLogic h) n := by
  99  induction n with
 100  | identity =>
 101      rfl
 102  | step n ih =>