`physics_faithful`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.PhysicsLogicRealization on GitHub at line 79.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  76    simp [physicsCost]
  77
  78/-- Physics tick interpretation is faithful. -/
  79theorem physics_faithful :
  80    LogicRealization.FaithfulArithmeticInterpretation physicsRealization where
  81  injective := by
  82    intro a b h
  83    cases h
  84    rfl
  85  zero_step_noncollapse := by
  86    intro n h
  87    have htick := congrArg PhysicsState.tick h
  88    exact ArithmeticFromLogic.LogicNat.zero_ne_succ n htick
  89
  90/-- Physics realization has invariant extracted arithmetic. -/
  91noncomputable def physics_arithmetic_invariant (R : LogicRealization.{0, 0}) :
  92    (UniversalForcing.arithmeticOf physicsRealization).peano.carrier
  93      ≃ (UniversalForcing.arithmeticOf R).peano.carrier :=
  94  ArithmeticOf.equivOfInitial
  95    (UniversalForcing.arithmeticOf physicsRealization)
  96    (UniversalForcing.arithmeticOf R)
  97
  98end PhysicsLogicRealization
  99end Foundation
 100end IndisputableMonolith

papers checked against this theorem

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