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
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.