237theorem meta_meta_theorem (R S : MetaCarrier) : 238 metaForcedArithmeticInvariance R S = universal_forcing_via_NNO R S :=
proof body
Decided by rfl or decide.
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 247 different setup involving Gödel numbering and reflection principles. 248 249* It does not produce a full `LogicRealization.{1, 0}` instance with 250 every orbit/step coherence axiom. The orbit fields require design 251 choices that are not part of the self-reference content; in 252 particular, choosing a meaningful "step on realizations" is its own 253 programme. 254 255What this module *does* prove: 256 257* The meta-cost on `LogicRealization.{0,0}` satisfies the three 258 definitional Aristotelian conditions automatically. 259 260* The meta-theorem `universal_forcing_via_NNO` already supplies the 261 forced-arithmetic-invariance condition that the structural shape 262 requires. 263 264* The meta-realization is reflexive: comparing a realization to itself 265 yields the identity equivalence. 266 267* Therefore the framework is reflexively closed in the structural 268 sense: the act of comparing realizations is itself a 269 Law-of-Logic-shaped operation, with all definitional conditions 270 automatic and the meta-theorem itself filling the substantive role. 271-/ 272 273end UniversalForcingSelfReference 274end Foundation 275end IndisputableMonolith
depends on (29)
Lean names referenced from this declaration's body.