metaCost
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not detect orbit non-isomorphism between realizations.
- Does not instantiate the full orbit/step coherence axioms for a meta-realization.
- Does not prove any Gödel-style self-reference statement.
- Does not lift the cost to real numbers or J-cost.
formal statement (Lean)
73noncomputable def metaCost (R S : MetaCarrier) : ℕ :=
proof body
Definition body.
74 if R = S then 0 else 1
75
76/-! ## The Three Definitional Aristotelian Conditions on Meta-Cost -/
77
78/-- **(L1) Identity** for the meta-cost: comparing a realization with
79itself has zero cost. -/