`physics_arithmetic_invariant`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.PhysicsLogicRealization
domain: Foundation
line: 91 · 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 91.

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

formal source

  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.