`metaCost_symm`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.UniversalForcingSelfReference
domain: Foundation
line: 86 · 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 86.

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

  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
 111exactly `universal_forcing_via_NNO`, packaged as the comparison law of
 112the meta-realization. -/
 113noncomputable def metaForcedArithmeticInvariance (R S : MetaCarrier) :
 114    R.Orbit ≃ S.Orbit :=
 115  universal_forcing_via_NNO R S
 116

papers checked against this theorem

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