metaCost_symm
plain-language theorem explainer
The meta-cost on pairs of logic realizations is symmetric. Researchers formalizing reflexive closure of forcing meta-theorems cite this as the non-contradiction clause for the meta-level comparator. The proof is a one-line wrapper that unfolds the definition and splits on propositional equality of the two realizations, using reflexivity for the equal case and classical negation for the unequal case.
Claim. Let $R$ and $S$ be any two instances of the meta-carrier (the type of $LogicRealization.{0,0}$). Then the meta-cost satisfies $metaCost(R,S)=metaCost(S,R)$.
background
MetaCarrier is the type of all $LogicRealization.{0,0}$ instances, placed in Type 1. The meta-cost between two such realizations is defined to be 0 when they are propositionally equal and 1 otherwise, by classical decidability on equality. This module shows that the Universal Forcing Meta-Theorem itself obeys the Law-of-Logic structural shape on the meta-carrier: identity, non-contradiction, totality, and forced-arithmetic invariance. The present theorem supplies the non-contradiction clause.
proof idea
Unfold the meta-cost definition. Apply case analysis on whether $R$ equals $S$. In the equal case substitute and close by reflexivity. In the unequal case obtain the symmetric negation and finish by simplification.
why it matters
This theorem is invoked directly in the construction of MetaRealizationCert (non_contradiction field) and in the statement of framework_is_reflexively_closed. It completes the Aristotelian triple for the meta-cost, allowing the Universal Forcing Meta-Theorem to be reified as a Law-of-Logic structure on the type of realizations. The result therefore closes the reflexive loop required by the self-reference section of the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.