metaRealizationCert
plain-language theorem explainer
The meta-realization certificate assembles a Law-of-Logic structure whose carrier is the type of logic realizations at universe level (0,0), with meta-cost obeying identity, symmetry, totality, and zero-cost equivalence to equality, plus forced arithmetic invariance. Researchers tracing reflexive closure of forcing theorems cite this construction. The definition is a direct structure literal that wires each field to an existing meta-cost lemma or invariance result.
Claim. Let $M$ be the type of logic realizations at universe level $(0,0)$. The meta-realization certificate is the structure on $M$ whose meta-cost function $c$ satisfies $c(R,R)=0$, $c(R,S)=c(S,R)$, $c(R,S)=0$ if and only if $R=S$, and the forced-arithmetic-invariance law that any two realizations induce canonically isomorphic arithmetic.
background
LogicRealization is the structure that packages a carrier type, a cost type equipped with zero, a comparison map, and a distinguished zero element; these data extract an arithmetic object invariant under the universal forcing comparison. MetaRealizationCert records the structural properties that the meta-level comparison of such realizations must satisfy: a meta-carrier at universe 1, a meta-cost that is total, zero on identical realizations, symmetric, and zero precisely when the realizations coincide, together with the invariance of forced arithmetic under that comparison. The module works in the setting where the universal forcing meta-theorem already supplies the arithmetic invariance; the certificate simply reifies that theorem as one of the required fields.
proof idea
The definition is a one-line structure literal. It sets the carrier type to LogicRealization.{0,0} by reflexivity and populates the remaining fields by direct reference to the meta-cost lemmas: identity from metaCost_self, non-contradiction from metaCost_symm, totality from metaCost_total, zero-cost equivalence from metaCost_eq_zero_iff, and the two invariance statements from metaForcedArithmeticInvariance and metaForcedArithmeticInvariance_self.
why it matters
This definition supplies the reflexive-closure step of the framework: the universal forcing meta-theorem is shown to instantiate the Law-of-Logic shape at the meta level, with the meta-carrier one universe above the realizations it compares. It is the immediate premise of the inhabitedness theorem that asserts a nonempty MetaRealizationCert exists. The construction uses only the meta-cost properties already proved in the same module and the invariance result imported from UniversalForcing, thereby closing the self-reference loop at the structural level without diagonalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.