216theorem framework_is_reflexively_closed : 217 -- Identity, non-contradiction, totality of meta-cost are automatic: 218 (∀ R : MetaCarrier, metaCost R R = 0) ∧ 219 (∀ R S : MetaCarrier, metaCost R S = metaCost S R) ∧ 220 (∀ R S : MetaCarrier, ∃ c : ℕ, metaCost R S = c) ∧ 221 -- The meta-theorem supplies the comparison law: 222 (∀ R S : MetaCarrier, Nonempty (R.Orbit ≃ S.Orbit)) := by
proof body
Term-mode proof.
223 refine ⟨metaCost_self, metaCost_symm, metaCost_total, ?_⟩ 224 intro R S 225 exact ⟨metaForcedArithmeticInvariance R S⟩ 226 227/-! ## The Meta-Meta-Theorem -/ 228 229/-- **Meta-meta-theorem.** Applying the meta-theorem inside the 230meta-realization yields the meta-theorem again. The structure of the 231meta-theorem is preserved under self-application: comparing two 232realizations through the meta-realization gives the same canonical 233equivalence as comparing them directly through `universal_forcing`. 234 235This is the reflexive-fixed-point property: `universal_forcing` is its 236own input under the meta-realization shape. -/
depends on (30)
Lean names referenced from this declaration's body.