FaithfulArithmeticInterpretation

formal source

  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 =>
 103      simp [positiveRatioOrbitInterpret, ArithmeticFromLogic.embed, ih,
 104        ArithmeticFromLogic.generatorOfLawsOfLogic]
 105
 106/-- Continuous positive-ratio Law-of-Logic realizations embed into the
 107setting-independent interface. -/
 108noncomputable def ofPositiveRatioComparison
 109    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
 110    LogicRealization where