`strictUniversalGround`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcing.Strict.Metaphysical
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.Strict.Metaphysical 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

depends on

formal source

  30        ≃ (StrictLogicRealization.arith S).peano.carrier
  31
  32/-- Canonical strict metaphysical ground supplied by strict universal forcing. -/
  33noncomputable def strictUniversalGround : StrictMetaphysicalGround where
  34  sourceName := "Strict universal generator of distinguishability"
  35  identifies_arithmetic := fun R =>
  36    (StrictLogicRealization.toLightweight R).orbitEquivLogicNat
  37  invariant := fun R S =>
  38    ArithmeticOf.equivOfInitial (StrictLogicRealization.arith R)
  39      (StrictLogicRealization.arith S)
  40
  41/-- Structural identification of the metaphysical ground with the universal
  42forced arithmetic object. -/
  43noncomputable def strict_metaphysical_ground_unique (R : StrictLogicRealization) :
  44    (StrictLogicRealization.arith R).peano.carrier ≃ ArithmeticFromLogic.LogicNat :=
  45  (StrictLogicRealization.toLightweight R).orbitEquivLogicNat
  46
  47end Metaphysical
  48end Strict
  49end UniversalForcing
  50end Foundation
  51end IndisputableMonolith

papers checked against this theorem

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