metaCost
plain-language theorem explainer
metaCost assigns 0 to equal LogicRealization instances and 1 otherwise on the meta-carrier type. Researchers citing the reflexive closure of the Universal Forcing Meta-Theorem use it as the structural cost detecting definitional distinctness. The definition is a direct case split on propositional equality via classical decidability.
Claim. For realizations $R,S$ in the meta-carrier (type of LogicRealization instances at level 0,0), the meta-cost is $0$ if $R=S$ and $1$ otherwise.
background
The module shows the Universal Forcing Meta-Theorem itself obeys the Law-of-Logic shape. MetaCarrier is defined as the type of LogicRealization.{0,0} instances and lives in Type 1. The meta-cost is the comparison operator on this carrier that returns zero precisely on propositional equality. Upstream, Identity from LogicAsFunctionalEquation encodes the zero self-cost pattern that this definition instantiates at the meta level; ObserverForcing.cost and MultiplicativeRecognizerL4.cost supply the lower-level J-cost precedents.
proof idea
One-line definition by case distinction: if the two realizations are propositionally equal then return 0, else return 1.
why it matters
metaCost supplies the cost function required by framework_is_reflexively_closed, the theorem asserting that the meta-theorem itself satisfies the three Aristotelian conditions plus forced-arithmetic invariance. It thereby closes the self-reference loop inside the Recognition framework without invoking Gödel-style diagonalization. The construction stays within the structural (not semantic) reading of self-reference given in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.