`physicsRealization`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.PhysicsLogicRealization
domain: Foundation
line: 46 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.PhysicsLogicRealization on GitHub at line 46.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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
  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]

papers checked against this theorem

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