framework_is_reflexively_closed
plain-language theorem explainer
The Universal Forcing Meta-Theorem satisfies the Law-of-Logic structural conditions when viewed as a comparison operator on the type of all realizations. Researchers tracing the self-referential closure of the Recognition Science foundation would cite this result. The proof is a term-mode refinement that directly assembles the three meta-cost properties from sibling lemmas and wraps the invariance statement in Nonempty.
Claim. Let $M$ be the type of all LogicRealization instances. The meta-cost function on $M$ satisfies: meta-cost$(R,R)=0$ for every $R$; meta-cost$(R,S)=$meta-cost$(S,R)$ for every pair; meta-cost$(R,S)$ equals some natural number $c$ for every pair; and for every pair $R,S$ the forced-arithmetic orbits of $R$ and $S$ are equivalent (witnessed by a nonempty type of equivalences).
background
MetaCarrier is the type of LogicRealization.{0,0} instances, placed in Type 1. Meta-cost is the function that returns 0 when two realizations are propositionally equal and 1 otherwise, by classical decidability; it registers definitional distinctness rather than orbit non-isomorphism. The three Aristotelian conditions are identity (cost of a realization with itself is zero), symmetry (cost is reciprocal), and totality (cost is natural-number valued). These are supplied by the sibling lemmas metaCost_self, metaCost_symm and metaCost_total. The fourth clause reifies the meta-theorem itself as the comparison law, wrapped in Nonempty because the equivalence lives in Type 1 while the conjunction is propositional. The module sets the local theoretical setting as structural self-reference: the meta-theorem fits the Law-of-Logic shape without attempting a full meta-level LogicRealization instance.
proof idea
The proof is a term-mode refinement. It supplies the conjunction by pairing the three meta-cost lemmas (metaCost_self, metaCost_symm, metaCost_total) with a lambda that, for any pair R S, returns the singleton containing the application of metaForcedArithmeticInvariance R S.
why it matters
This declaration records the reflexive-fixed-point property of the Universal Forcing Meta-Theorem: the act of comparing realizations is itself Law-of-Logic-shaped. It completes the self-reference step described in the module doc-comment, showing that universal_forcing is its own input under the meta-realization shape. The result sits at the end of the foundation chain that begins with the meta-theorem in UniversalForcing and the Aristotelian conditions in LogicAsFunctionalEquation; it is cited by any later argument that treats the entire framework as a single closed structure. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.