modular_arithmetic_invariant

formal source

  97    simp [finCost]
  98
  99/-- Modular realization has invariant extracted arithmetic. -/
 100noncomputable def modular_arithmetic_invariant (k : ℕ) (R : LogicRealization.{0, 0}) :
 101    (UniversalForcing.arithmeticOf (modularRealization k)).peano.carrier
 102      ≃ (UniversalForcing.arithmeticOf R).peano.carrier :=
 103  ArithmeticOf.equivOfInitial
 104    (UniversalForcing.arithmeticOf (modularRealization k))
 105    (UniversalForcing.arithmeticOf R)
 106
 107/-- The modular interpretation is periodic on the carrier. -/
 108theorem modular_interpret_periodic (k : ℕ) (n : ArithmeticFromLogic.LogicNat) :
 109    modularInterpret k
 110        (ArithmeticFromLogic.LogicNat.fromNat
 111          (ArithmeticFromLogic.LogicNat.toNat n + modulus k))
 112      = modularInterpret k n := by
 113  apply Fin.ext
 114  simp [modularInterpret, ArithmeticFromLogic.LogicNat.toNat_fromNat]
 115
 116end ModularLogicRealization
 117end Foundation
 118end IndisputableMonolith