metaCost_total
plain-language theorem explainer
The theorem shows that the meta-cost between any two realizations of type LogicRealization.{0,0} always evaluates to some natural number. Researchers checking the reflexive closure of the Universal Forcing Meta-Theorem cite this as the totality clause among the three Aristotelian conditions on the meta-cost. The proof is a direct term that supplies the meta-cost value itself as the witness and closes the existential by reflexivity.
Claim. For any two realizations $R$ and $S$ in the type of LogicRealization instances at level {0,0}, there exists a natural number $c$ such that the meta-cost of $R$ and $S$ equals $c$.
background
The meta-carrier is the type of all LogicRealization.{0,0} instances and lives in Type 1. The meta-cost is the function that returns 0 when two such realizations are propositionally equal and 1 otherwise, using classical decidability to detect definitional distinctness rather than orbit non-isomorphism. This module formalizes the next step after the Universal Forcing Meta-Theorem: the meta-theorem itself is shown to possess the structural shape of a Law-of-Logic realization, including the three definitional Aristotelian conditions on its meta-cost.
proof idea
The proof is a one-line term wrapper. It constructs the existential witness directly from the value of the meta-cost on the given pair and uses reflexivity to discharge the equality.
why it matters
This result supplies the totality leg of the meta-cost in the construction of MetaRealizationCert and in the theorem that the framework is reflexively closed. The latter states that the Universal Forcing Meta-Theorem itself instantiates the Law-of-Logic structural shape, with the meta-theorem supplying the forced-arithmetic-invariance condition. It thereby closes the self-reference loop for the Recognition Science framework without invoking Gödel-style diagonalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.