theorem
proved
physicsCost_self
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.PhysicsLogicRealization on GitHub at line 27.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
24def physicsCost (x y : PhysicsState) : Nat :=
25 if x = y then 0 else 1
26
27@[simp] theorem physicsCost_self (x : PhysicsState) : physicsCost x x = 0 := by
28 simp [physicsCost]
29
30theorem physicsCost_symm (x y : PhysicsState) : physicsCost x y = physicsCost y x := by
31 by_cases h : x = y
32 · subst h
33 simp [physicsCost]
34 · have h' : y ≠ x := by intro hyx; exact h hyx.symm
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