metaCost
plain-language theorem explainer
The meta-cost on the meta-carrier returns 0 when two LogicRealization instances are propositionally equal and 1 otherwise. Researchers establishing reflexive closure of the Universal Forcing Meta-Theorem cite this definition to supply the comparison operator for the meta-level Aristotelian conditions. The definition is a direct case distinction on equality that exploits classical decidability.
Claim. For realizations $R,S$ in the meta-carrier (the type of LogicRealization instances at level 0,0), define the meta-cost by $0$ if $R=S$ and $1$ otherwise.
background
The module UniversalForcingSelfReference shows that the Universal Forcing Meta-Theorem itself fits the Law-of-Logic structural shape. The meta-carrier is the type of LogicRealization.{0,0} instances and lives in Type 1. The meta-cost is the comparison operator on this carrier; its doc-comment states that the choice is structural and detects definitional distinctness rather than orbit non-isomorphism.
proof idea
The definition is a direct conditional expression that returns 0 on propositional equality and 1 otherwise, using the decidability of equality on the meta-carrier.
why it matters
This definition supplies the cost function required by the downstream theorem framework_is_reflexively_closed, which states that the meta-theorem instantiates the Law-of-Logic shape at the meta level. It completes the three definitional Aristotelian conditions (identity, non-contradiction, totality) while the meta-theorem itself supplies the forced-arithmetic-invariance condition. The construction closes the self-reference loop without invoking Gödel-style diagonalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.