framework_is_reflexively_closed
plain-language theorem explainer
The universal forcing meta-theorem satisfies the Law-of-Logic structural shape on the type of realizations: its meta-cost vanishes on identical realizations, is symmetric, takes natural-number values, and the meta-theorem itself supplies the forced-arithmetic invariance between orbits. Researchers formalizing self-referential foundations in Recognition Science cite this to establish reflexive closure of the framework. The proof packages four meta-lemmas into a single conjunction via a direct term construction.
Claim. Let $M$ be the type of all LogicRealization instances in Type 1. The meta-cost function on $M$ obeys the three Aristotelian conditions: for all $R$ in $M$, meta-cost$(R,R)=0$; for all $R,S$ in $M$, meta-cost$(R,S)=$ meta-cost$(S,R)$; and for all $R,S$ in $M$ there exists $c$ in $N$ with meta-cost$(R,S)=c$. Moreover, the meta-theorem supplies that for all $R,S$ in $M$, Nonempty$(R.Orbit ≃ S.Orbit)$.
background
The module shows that the Universal Forcing Meta-Theorem, which asserts any two LogicRealization instances have canonically isomorphic forced arithmetic, itself fits the Law-of-Logic structural shape. The meta-carrier is the type of LogicRealization.{0,0} instances living in Type 1. The meta-cost between two realizations is zero when they are propositionally equal and one otherwise, by classical decidability; this detects definitional distinctness rather than orbit non-isomorphism. The module supplies a MetaRealizationCert recording the required structural properties without instantiating full orbit coherence axioms. Upstream, LogicAsFunctionalEquation.Identity encodes the zero self-cost law as the mathematical counterpart of A = A, while ArithmeticOf.canonical supplies the realization-independent Peano object used in the invariance step.
proof idea
The proof is a term-mode construction that directly assembles the required conjunction. It applies the lemma metaCost_self to witness the identity condition, metaCost_symm for symmetry, metaCost_total for the existence of natural-number costs, and then for the invariance clause it introduces arbitrary realizations R and S and applies metaForcedArithmeticInvariance to obtain the required Nonempty equivalence.
why it matters
This declaration confirms that the Universal Forcing Meta-Theorem itself forms a Law-of-Logic-shaped structure on the type of realizations, thereby establishing reflexive closure of the framework. It aligns with the Recognition Science forcing chain by exhibiting self-similar preservation of the comparison law under meta-application, consistent with the self-similar fixed point and eight-tick octave structure. The result closes a foundational loop without deriving specific constants such as the alpha band or phi-ladder masses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.