def
definition
metaCost
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.UniversalForcingSelfReference on GitHub at line 73.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
70otherwise. The choice is structural: the cost detects definitional
71distinctness, not orbit non-isomorphism (which by the meta-theorem is
72always trivial). -/
73noncomputable def metaCost (R S : MetaCarrier) : ℕ :=
74 if R = S then 0 else 1
75
76/-! ## The Three Definitional Aristotelian Conditions on Meta-Cost -/
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