`in`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.MetaphysicalRealization
domain: Foundation
line: 33 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.UniversalForcing.MetaphysicalRealization on GitHub at line 33.

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

formal source

  30    ∀ R S : LogicRealization, (arithmeticOf R).peano.carrier ≃ (arithmeticOf S).peano.carrier
  31
  32/-- The universal forcing theorem supplies a canonical metaphysical-ground
  33structure in the neutral, structural sense. -/
  34noncomputable def universalGround : MetaphysicalGround where
  35  sourceName := "Universal generator of distinguishability"
  36  identifies_arithmetic := fun R => R.orbitEquivLogicNat
  37  invariant := fun R S => ArithmeticOf.equivOfInitial (arithmeticOf R) (arithmeticOf S)
  38
  39/-- The metaphysical-ground identification is unique up to the same canonical
  40arithmetic equivalence supplied by Universal Forcing. -/
  41noncomputable def metaphysical_ground_unique (R : LogicRealization) :
  42    (arithmeticOf R).peano.carrier ≃ ArithmeticFromLogic.LogicNat :=
  43  R.orbitEquivLogicNat
  44
  45end MetaphysicalRealization
  46end UniversalForcing
  47end Foundation
  48end IndisputableMonolith

papers checked against this theorem

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