pith. machine review for the scientific record. sign in
def definition def or abbrev

physicsRealization

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  46def physicsRealization : LogicRealization where
  47  Carrier := PhysicsState

proof body

Definition body.

  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
  69  identity := physicsCost_self
  70  nonContradiction := physicsCost_symm
  71  excludedMiddle := True
  72  composition := True
  73  actionInvariant := True
  74  nontrivial := by
  75    refine ⟨⟨ArithmeticFromLogic.LogicNat.succ ArithmeticFromLogic.LogicNat.zero⟩, ?_⟩
  76    simp [physicsCost]
  77
  78/-- Physics tick interpretation is faithful. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (26)

Lean names referenced from this declaration's body.