def
definition
tickStep
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.PhysicsLogicRealization on GitHub at line 38.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
35 simp [physicsCost, h, h']
36
37/-- Identity-tick successor. -/
38def tickStep (x : PhysicsState) : PhysicsState :=
39 ⟨ArithmeticFromLogic.LogicNat.succ x.tick⟩
40
41/-- Interpret the free arithmetic orbit as identity-tick states. -/
42def physicsInterpret (n : ArithmeticFromLogic.LogicNat) : PhysicsState :=
43 ⟨n⟩
44
45/-- Physics realization skeleton. -/
46def physicsRealization : LogicRealization where
47 Carrier := PhysicsState
48 Cost := Nat
49 zeroCost := inferInstance
50 compare := physicsCost
51 zero := ⟨ArithmeticFromLogic.LogicNat.zero⟩
52 step := tickStep
53 Orbit := ArithmeticFromLogic.LogicNat
54 orbitZero := ArithmeticFromLogic.LogicNat.zero
55 orbitStep := ArithmeticFromLogic.LogicNat.succ
56 interpret := physicsInterpret
57 interpret_zero := rfl
58 interpret_step := by intro n; rfl
59 orbit_no_confusion := by
60 intro n h
61 exact ArithmeticFromLogic.LogicNat.zero_ne_succ n h
62 orbit_step_injective := ArithmeticFromLogic.LogicNat.succ_injective
63 orbit_induction := by
64 intro P h0 hs n
65 exact ArithmeticFromLogic.LogicNat.induction (motive := P) h0 hs n
66 orbitEquivLogicNat := Equiv.refl ArithmeticFromLogic.LogicNat
67 orbitEquiv_zero := rfl
68 orbitEquiv_step := by intro n; rfl