def
definition
modularInterpret
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.ModularLogicRealization on GitHub at line 47.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
44 ⟨(x.val + 1) % modulus k, Nat.mod_lt _ (modulus_pos k)⟩
45
46/-- Interpret the free orbit periodically in a finite cyclic carrier. -/
47def modularInterpret (k : ℕ) (n : ArithmeticFromLogic.LogicNat) : Fin (modulus k) :=
48 ⟨ArithmeticFromLogic.LogicNat.toNat n % modulus k, Nat.mod_lt _ (modulus_pos k)⟩
49
50@[simp] theorem modularInterpret_zero (k : ℕ) :
51 modularInterpret k ArithmeticFromLogic.LogicNat.zero = ⟨0, modulus_pos k⟩ := by
52 apply Fin.ext
53 change 0 % modulus k = 0
54 exact Nat.zero_mod (modulus k)
55
56theorem modularInterpret_step (k : ℕ) (n : ArithmeticFromLogic.LogicNat) :
57 modularInterpret k (ArithmeticFromLogic.LogicNat.succ n)
58 = cycStep k (modularInterpret k n) := by
59 apply Fin.ext
60 change ArithmeticFromLogic.LogicNat.toNat (ArithmeticFromLogic.LogicNat.succ n) % modulus k =
61 (ArithmeticFromLogic.LogicNat.toNat n % modulus k + 1) % modulus k
62 rw [ArithmeticFromLogic.LogicNat.toNat_succ, Nat.succ_eq_add_one]
63 have h := (Nat.add_mod (ArithmeticFromLogic.LogicNat.toNat n) 1 (modulus k)).symm
64 simpa [Nat.mod_eq_of_lt (one_lt_modulus k)] using h
65
66/-- Finite cyclic Law-of-Logic realization with periodic interpretation. -/
67def modularRealization (k : ℕ) : LogicRealization where
68 Carrier := Fin (modulus k)
69 Cost := Nat
70 zeroCost := inferInstance
71 compare := finCost
72 zero := ⟨0, modulus_pos k⟩
73 step := cycStep k
74 Orbit := ArithmeticFromLogic.LogicNat
75 orbitZero := ArithmeticFromLogic.LogicNat.zero
76 orbitStep := ArithmeticFromLogic.LogicNat.succ
77 interpret := modularInterpret k