`for`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcingSelfReference
domain: Foundation
line: 38 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.UniversalForcingSelfReference on GitHub at line 38.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  35the meta-realization to `Type 1` and make the universe lift explicit.
  36
  37We do not attempt to instantiate the full heavy `LogicRealization`
  38structure for the meta-realization (the orbit/step coherence axioms
  39require additional design choices that are not part of the
  40self-reference content). Instead, we give a `MetaRealizationCert`
  41recording all the structural properties that *would* be required of
  42such an instance, and prove that the meta-theorem already supplies
  43each one.
  44
  45## What this earns
  46
  47The framework is reflexively closed: the meta-theorem is itself a
  48Law-of-Logic-shaped operation comparing realizations, with the three
  49definitional Aristotelian conditions automatic and the meta-theorem's
  50canonical equivalence supplying the forced-arithmetic invariance for
  51free.
  52-/
  53
  54namespace IndisputableMonolith
  55namespace Foundation
  56namespace UniversalForcingSelfReference
  57
  58open Classical
  59open UniversalForcing
  60
  61/-! ## The Meta-Carrier and Meta-Cost -/
  62
  63/-- The **meta-carrier**: the type of `LogicRealization.{0,0}` instances.
  64This sits in `Type 1` because `LogicRealization.{0,0}` is itself in
  65`Type 1`. -/
  66abbrev MetaCarrier : Type 1 := LogicRealization.{0, 0}
  67
  68/-- The **meta-cost** between two realizations. By Classical decidability,

papers checked against this theorem

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