metaCost_self
plain-language theorem explainer
The identity property of the meta-cost states that any logic realization compared to itself has zero cost. Researchers establishing reflexive closure of the universal forcing meta-theorem cite this result as the first Aristotelian condition. The proof is a direct unfolding of the meta-cost definition followed by simplification.
Claim. Let $R$ be a logic realization. The meta-cost of comparing $R$ to itself equals zero.
background
The meta-carrier is the type of all LogicRealization instances, placed in Type 1. The meta-cost between two realizations is defined to return 0 when they are propositionally equal and 1 otherwise, using classical decidability; the definition detects definitional distinctness rather than orbit non-isomorphism. This module shows that the universal forcing meta-theorem itself satisfies the Law-of-Logic structural shape, with a meta-carrier, meta-cost, and the three definitional Aristotelian conditions.
proof idea
The proof is a one-line wrapper that unfolds the meta-cost definition and applies simplification.
why it matters
This supplies the identity condition required by metaRealizationCert and framework_is_reflexively_closed. The latter theorem states that the framework is reflexively closed because the meta-cost satisfies identity, non-contradiction and totality while the meta-theorem supplies the comparison law. It completes the structural embedding of the meta-theorem inside the Law-of-Logic shape.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.