`arith`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.StrictRealization
domain: Foundation
line: 95 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.StrictRealization on GitHub at line 95.

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

  92
  93/-- Strict forced arithmetic is the arithmetic extracted from the derived
  94lightweight realization. -/
  95def arith (R : StrictLogicRealization) : ArithmeticOf (toLightweight R) :=
  96  arithmeticOf (toLightweight R)
  97
  98/-- Every strict realization has forced arithmetic canonically equivalent to
  99`LogicNat`. -/
 100def arith_equiv_logicNat (R : StrictLogicRealization) :
 101    (arith R).peano.carrier ≃ LogicNat :=
 102  (toLightweight R).orbitEquivLogicNat
 103
 104/-- Universal forcing for strict realizations. -/
 105noncomputable def universal_forcing (R S : StrictLogicRealization) :
 106    (arith R).peano.carrier ≃ (arith S).peano.carrier :=
 107  ArithmeticOf.equivOfInitial (arith R) (arith S)
 108
 109/-- The Peano surface is inherited from the derived free orbit. -/
 110theorem peano_surface (R : StrictLogicRealization) :
 111    ArithmeticOf.PeanoSurface (arith R) :=
 112  UniversalForcing.peano_surface (toLightweight R)
 113
 114end StrictLogicRealization
 115
 116end Strict
 117end UniversalForcing
 118end Foundation
 119end IndisputableMonolith

papers checked against this theorem

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