199 ⟨metaRealizationCert⟩ 200 201/-! ## The Reflexive-Closure Theorem -/ 202 203/-- **The framework is reflexively closed.** 204 205The Universal Forcing Meta-Theorem itself instantiates the Law-of-Logic 206structural shape: the meta-cost satisfies the three definitional 207Aristotelian conditions, and the meta-theorem itself supplies the 208forced-arithmetic-invariance condition. The framework that proves 209"every Law-of-Logic realization has the same forced arithmetic" is 210itself a Law-of-Logic-shaped structure on the type of realizations. 211 212The forced-arithmetic-invariance condition is wrapped in `Nonempty` 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. -/
depends on (17)
Lean names referenced from this declaration's body.