framework_is_reflexively_closed

formal source

 213because the equivalence is `Type 1`-valued, while the conjunction here
 214is propositional. The Nonempty wrapper is harmless: the equivalence
 215exists for every pair, so its `Nonempty` is trivially inhabited. -/
 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
 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. -/
 237theorem meta_meta_theorem (R S : MetaCarrier) :
 238    metaForcedArithmeticInvariance R S = universal_forcing_via_NNO R S :=
 239  rfl
 240
 241/-! ## Honest acknowledgements
 242
 243What this module *does not* prove:
 244
 245* It does not prove `universal_forcing` proves itself in the
 246  metalogical sense. Gödel-style self-reference would require a