metaCost_eq_zero_iff
plain-language theorem explainer
The equivalence asserts that the meta-cost between any two realizations vanishes precisely when they are identical. Workers on the self-referential closure of the forcing framework cite this to establish that the meta-level comparison satisfies the zero-cost condition for equality. The proof is a direct case split on propositional equality after unfolding the meta-cost definition, followed by simplification in each branch.
Claim. Let $R, S$ be elements of the meta-carrier (the type of $LogicRealization.{0,0}$ instances). Then the meta-cost satisfies $metaCost(R,S) = 0$ if and only if $R = S$.
background
The module UniversalForcingSelfReference formalizes the reflexive closure of the universal forcing meta-theorem. The meta-carrier is the type of LogicRealization.{0,0} instances, which lives in Type 1. The meta-cost between two such realizations is zero when they are propositionally equal and one otherwise, by classical decidability. This supplies the structural ingredients for a meta-realization: carrier, cost obeying identity/non-contradiction/totality, and forced-arithmetic invariance. Upstream results include the canonical arithmetic object for any realization (ArithmeticOf.canonical) and J-cost structures from PhiForcingDerived.of.
proof idea
The proof unfolds the definition of metaCost and performs case analysis on whether R equals S. In the affirmative case simplification yields the forward implication; in the negative case it yields the converse. No external lemmas beyond the definitional unfolding and the decidability implicit in by_cases are required.
why it matters
This result supplies the identity axiom for the meta-realization certificate metaRealizationCert. It closes the loop on the meta-theorem by showing that the comparison law itself fits the Law-of-Logic shape. In the Recognition framework this contributes to the reflexive closure at the level of the universal forcing meta-theorem, confirming that the eight-tick octave and phi-ladder structures remain invariant under meta-level comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.