IndisputableMonolith.Foundation.UniversalForcingSelfReference
The UniversalForcingSelfReference module defines the meta-carrier as the type of LogicRealization.{0,0} instances in Type 1, together with meta-cost functions and realization certificates for self-referential forcing. Researchers on categorical logic and initial algebras would cite it when assembling meta-level structures atop the Universal Forcing imports. This is a definition module that assembles components from LogicRealization and NaturalNumberObject without proofs.
claimThe meta-carrier is the type of LogicRealization instances at levels (0,0), denoted MetaCarrier and residing in Type 1. It is equipped with meta-cost functions satisfying self-reference, symmetry and totality, plus MetaRealizationCert objects witnessing forced arithmetic invariance.
background
The module imports LogicRealization, which supplies a setting-independent interface for the Universal Forcing program by creating a common object into which different Law-of-Logic settings map. UniversalForcing states that any two realizations have canonically equivalent forced arithmetic objects because they are initial Peano algebras. NaturalNumberObject makes precise the Lawvere characterization: a triple (N, z, s) is a natural-number object if for every (X, x, f) there exists a unique map. DiscreteRealization re-exports the Boolean case. The local theoretical setting is the meta-layer needed for self-reference within these forcing constructions.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
This module supplies the meta-carrier, metaCost and MetaRealizationCert structures that enable self-referential arguments inside the Universal Forcing program. It feeds the invariance and certification steps required by the parent UniversalForcing theorem on equivalent initial Peano algebras and by the Lawvere natural-number object characterization.
scope and limits
- Does not prove any theorem about forced arithmetic equivalence.
- Does not instantiate concrete LogicRealization objects.
- Does not derive physical constants or the forcing chain T0-T8.
- Does not address continuous-ratio or other non-discrete settings.
depends on (4)
declarations in this module (14)
-
structure
for -
abbrev
MetaCarrier -
def
metaCost -
theorem
metaCost_self -
theorem
metaCost_symm -
theorem
metaCost_total -
theorem
metaCost_eq_zero_iff -
def
metaForcedArithmeticInvariance -
theorem
metaForcedArithmeticInvariance_self -
structure
MetaRealizationCert -
def
metaRealizationCert -
theorem
metaRealizationCert_inhabited -
theorem
framework_is_reflexively_closed -
theorem
meta_meta_theorem