MetaCarrier
plain-language theorem explainer
MetaCarrier denotes the type of LogicRealization instances at base universe level. It supplies the domain for meta-cost comparisons that establish reflexive closure of the Universal Forcing meta-theorem. The abbreviation performs a direct universe lift to place the type in Type 1.
Claim. Let LogicRealization be the structure with Carrier : Type u, Cost : Type v, zeroCost, compare : Carrier → Carrier → Cost, and zero : Carrier. Then MetaCarrier := LogicRealization at levels u=0, v=0, which lies in Type 1.
background
The module formalizes self-reference for Universal Forcing: the meta-theorem itself must fit the Law-of-Logic shape with a meta-carrier, meta-cost, and three Aristotelian conditions. LogicRealization supplies a carrier, cost type, zeroCost, compare function, and zero element; its fields encode the structural laws needed by the forcing program. The meta-carrier sits one universe above the realizations it compares, matching the convention already fixed in NaturalNumberObject.
proof idea
The declaration is a one-line abbreviation that aliases LogicRealization.{0,0} directly to MetaCarrier.
why it matters
MetaCarrier is the domain for metaCost, metaCost_self, metaCost_symm, metaCost_total, and framework_is_reflexively_closed. It supplies the carrier required to show that the meta-theorem itself satisfies the Law-of-Logic structural shape, thereby closing the framework reflexively. The construction touches the self-reference step after the Universal Forcing meta-theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.