structure
definition
MetaRealizationCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.UniversalForcingSelfReference on GitHub at line 164.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
carrier -
carrier -
of -
Identity -
LogicRealization -
cost -
cost -
identity -
is -
of -
as -
is -
of -
MetaCarrier -
metaCost -
is -
of -
is -
total -
and -
total -
S -
identity -
comparison
used by
formal source
161orbit/step coherence axioms; instead, we record that every structural
162property the heavy structure would require has been independently
163proved. -/
164structure MetaRealizationCert where
165 /-- Meta-carrier exists at universe 1. -/
166 carrier_type : Type 1
167 carrier_eq_realization_type : carrier_type = LogicRealization.{0, 0}
168 /-- Meta-cost is well-defined and total. -/
169 cost_total : ∀ R S : MetaCarrier, ∃ c : ℕ, metaCost R S = c
170 /-- (L1) Identity on the meta-cost. -/
171 identity : ∀ R : MetaCarrier, metaCost R R = 0
172 /-- (L2) Non-contradiction on the meta-cost. -/
173 non_contradiction : ∀ R S : MetaCarrier, metaCost R S = metaCost S R
174 /-- (L3a) Totality on the meta-cost. -/
175 totality : ∀ R S : MetaCarrier, ∃ c : ℕ, metaCost R S = c
176 /-- The meta-cost equals zero iff the realizations are equal. -/
177 cost_zero_iff_eq : ∀ R S : MetaCarrier, metaCost R S = 0 ↔ R = S
178 /-- Forced-arithmetic invariance: the meta-theorem reified as the
179 comparison law of the meta-realization. -/
180 forced_arithmetic_invariance :
181 ∀ R S : MetaCarrier, R.Orbit ≃ S.Orbit
182 /-- Reflexivity of the forced-arithmetic invariance. -/
183 arithmetic_invariance_self :
184 ∀ R : MetaCarrier,
185 forced_arithmetic_invariance R R = Equiv.refl R.Orbit
186
187noncomputable def metaRealizationCert : MetaRealizationCert where
188 carrier_type := LogicRealization.{0, 0}
189 carrier_eq_realization_type := rfl
190 cost_total := metaCost_total
191 identity := metaCost_self
192 non_contradiction := metaCost_symm
193 totality := metaCost_total
194 cost_zero_iff_eq := metaCost_eq_zero_iff