IndisputableMonolith.Foundation.UniversalForcing.Invariance.TwoCases

   1import IndisputableMonolith.Foundation.UniversalForcing.ContinuousRealization
   2import IndisputableMonolith.Foundation.UniversalForcing.DiscreteRealization
   3
   4/-!
   5  TwoCases.lean
   6
   7  First non-trivial invariance kernel: continuous positive-ratio realizations
   8  and the discrete Boolean realization have canonically equivalent forced
   9  arithmetic.
  10-/
  11
  12namespace IndisputableMonolith
  13namespace Foundation
  14namespace UniversalForcing
  15namespace Invariance
  16namespace TwoCases
  17
  18open LogicAsFunctionalEquation
  19open ContinuousRealization
  20open DiscreteRealization
  21
  22/-- Continuous positive-ratio arithmetic is canonically equivalent to discrete
  23Boolean arithmetic. -/
  24noncomputable def arith_continuous_equiv_arith_discrete
  25    (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
  26    (arithmeticOf (continuousRealization C h)).peano.carrier
  27      ≃ (arithmeticOf discreteRealization).peano.carrier :=
  28  ArithmeticOf.equivOfInitial (arithmeticOf (continuousRealization C h))
  29    (arithmeticOf discreteRealization)
  30
  31end TwoCases
  32end Invariance
  33end UniversalForcing
  34end Foundation
  35end IndisputableMonolith
  36