MetaCarrier
MetaCarrier is the type of all LogicRealization instances at base universe levels 0,0, lifted to Type 1. Researchers closing the self-reference loop in the Universal Forcing meta-theorem cite it as the domain for meta-cost comparisons between realizations. The declaration is a direct one-line abbreviation that supplies the carrier for the three Aristotelian conditions and the forced-arithmetic invariance law.
claimLet $M$ denote the type of all Law-of-Logic realizations at universe levels $0,0$, which resides in Type 1.
background
LogicRealization is the structure that equips a carrier with a comparison cost, zero element, and step action together with the propositions required by the Universal Forcing program. The module UniversalForcingSelfReference shows that the meta-theorem itself obeys the same Law-of-Logic shape: a meta-carrier, a meta-cost that is zero precisely on propositional equality, and the three definitional conditions on that cost. The module doc states that self-reference here is structural, not Gödel-style, and that the meta-carrier sits one universe above the realizations it compares.
proof idea
One-line abbreviation that directly aliases MetaCarrier to LogicRealization.{0,0}.
why it matters in Recognition Science
MetaCarrier supplies the domain for metaCost and for the theorem framework_is_reflexively_closed, which asserts that the Universal Forcing Meta-Theorem itself satisfies the Law-of-Logic structural shape. It thereby closes the reflexive loop: the statement that every realization has the same forced arithmetic is reified as a comparison law on the type of realizations. The module doc notes that the full heavy LogicRealization axioms are not instantiated at the meta-level; only the structural properties supplied by the meta-theorem are recorded.
scope and limits
- Does not instantiate the full LogicRealization structure at the meta-level.
- Does not prove Gödel-style self-reference of the meta-theorem.
- Does not address orbit non-isomorphism beyond the meta-theorem's triviality claim.
- Does not extend the carrier to higher universe levels.
Lean usage
def metaCostExample (R S : MetaCarrier) : ℕ := if R = S then 0 else 1formal statement (Lean)
66abbrev MetaCarrier : Type 1 := LogicRealization.{0, 0}
proof body
Definition body.
67
68/-- The **meta-cost** between two realizations. By Classical decidability,
69this is `0` if the realizations are propositionally equal and `1`
70otherwise. The choice is structural: the cost detects definitional
71distinctness, not orbit non-isomorphism (which by the meta-theorem is
72always trivial). -/