`metaCost_self`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.UniversalForcingSelfReference on GitHub at line 80.

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

  77
  78/-- **(L1) Identity** for the meta-cost: comparing a realization with
  79itself has zero cost. -/
  80theorem metaCost_self (R : MetaCarrier) : metaCost R R = 0 := by
  81  unfold metaCost
  82  simp
  83
  84/-- **(L2) Non-Contradiction** for the meta-cost: the comparison is
  85symmetric in its arguments. -/
  86theorem metaCost_symm (R S : MetaCarrier) : metaCost R S = metaCost S R := by
  87  unfold metaCost
  88  by_cases h : R = S
  89  · subst h; rfl
  90  · have hSR : ¬ S = R := fun h' => h h'.symm
  91    simp [h, hSR]
  92
  93/-- **(L3a) Totality** for the meta-cost: defined on every pair of
  94realizations, returns a value (the function type signature). -/
  95theorem metaCost_total (R S : MetaCarrier) : ∃ c : ℕ, metaCost R S = c :=
  96  ⟨metaCost R S, rfl⟩
  97
  98/-- The meta-cost is zero iff the realizations are definitionally
  99equal. -/
 100theorem metaCost_eq_zero_iff (R S : MetaCarrier) :
 101    metaCost R S = 0 ↔ R = S := by
 102  unfold metaCost
 103  by_cases h : R = S
 104  · simp [h]
 105  · simp [h]
 106
 107/-! ## Forced-Arithmetic Invariance: The Meta-Theorem -/
 108
 109/-- **The meta-theorem reified.** For any two realizations, the canonical
 110equivalence between their forced arithmetic objects exists. This is

papers checked against this theorem

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