  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
  58  interpret_step := by intro n; rfl
  59  orbit_no_confusion := by
  60    intro n h

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.