MetaRealizationCert
plain-language theorem explainer
The MetaRealizationCert structure packages the meta-carrier type of LogicRealization instances, the meta-cost axioms, and the forced-arithmetic invariance supplied by the Universal Forcing meta-theorem. Framework developers cite it to record reflexive closure of the Law-of-Logic shape at the meta level. The definition assembles these properties from the metaCost lemmas and the meta-theorem without building the full heavy LogicRealization.
Claim. Let $C$ be the type of LogicRealization instances at levels 0,0. A MetaRealizationCert consists of: carrier type equal to $C$; a total meta-cost function to natural numbers; identity (meta-cost of any realization with itself is zero); symmetry of meta-cost; totality; meta-cost zero if and only if the realizations are equal; forced arithmetic invariance (orbits of any two realizations are equivalent); and reflexivity of that invariance.
background
In the Universal Forcing Self-Reference module the meta-carrier is the type of all LogicRealization instances at levels 0,0, which lives in Type 1. The meta-cost between two realizations is defined to be 0 when they are propositionally equal and 1 otherwise, using classical decidability; this cost detects definitional distinctness rather than orbit non-isomorphism. The module follows the Law-of-Logic structural shape from LogicAsFunctionalEquation, where the Identity axiom requires cost zero on equals and the Non-contradiction axiom requires symmetry under swap.
proof idea
This is a structure definition that packages the carrier equality, the cost properties proved by the metaCost_self, metaCost_symm, metaCost_total and metaCost_eq_zero_iff lemmas, and the forced-arithmetic-invariance theorem reified directly from the meta-theorem. The arithmetic_invariance_self field is supplied by Equiv.refl. It is a packaging definition with no additional computational content.
why it matters
This declaration completes reflexive closure of the Recognition Science framework: the Universal Forcing meta-theorem itself fits the Law-of-Logic shape. It supplies the content for the metaRealizationCert_inhabited theorem asserting Nonempty MetaRealizationCert and for the sibling 'for' structure. In the T0-T8 chain it realizes the self-reference step after the meta-theorem, confirming the framework is closed under its own comparison law without Gödel-style diagonalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.