IndisputableMonolith.Foundation.UniversalForcingSelfReference
This module defines the meta-carrier as the type of LogicRealization.{0,0} instances, which lives in Type 1. It supports the Universal Forcing program by supplying a common carrier for mappings from different Law-of-Logic settings. The module is a definition module that organizes auxiliary constructions such as metaCost and MetaRealizationCert around this carrier.
claimThe meta-carrier is the type of instances of the LogicRealization interface at levels 0 and 0, denoted $\mathrm{MetaCarrier} := \mathrm{LogicRealization}_{0,0}$, which resides in $\mathrm{Type}\,1$.
background
The module imports LogicRealization, whose doc states it creates a common object into which different Law-of-Logic settings (continuous positive ratios, discrete propositions, categorical settings) can be mapped. It also imports UniversalForcing, whose doc states: "First formal statement of the Universal Forcing theorem: any two Law-of-Logic realizations have canonically equivalent forced arithmetic objects, because those objects are initial Peano algebras." NaturalNumberObject supplies the Lawvere characterization of the forced arithmetic as a triple (N, z, s) such that for every (X, x, f) there exists a unique map.
The supplied DOC_COMMENT identifies the meta-carrier as the type of LogicRealization.{0,0} instances sitting in Type 1. The module therefore provides the self-referential carrier needed to close the forcing construction on itself.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the meta-carrier that enables the meta-level definitions (metaCost, metaForcedArithmeticInvariance, MetaRealizationCert) inside the same file. These in turn support the Universal Forcing theorem stated in the imported UniversalForcing module, whose doc describes the canonical equivalence of forced arithmetic objects across realizations.
scope and limits
- Does not contain any theorems or proofs.
- Does not specify a concrete Law-of-Logic realization.
- Does not address continuous or discrete cases directly.
- Does not prove equivalence of forced arithmetic objects.
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