metaForcedArithmeticInvariance
Any two realizations under the meta-carrier have canonically equivalent forced arithmetic orbits. A researcher proving reflexive closure of the Recognition Science framework would cite this reification of the universal forcing meta-theorem. The definition is a one-line wrapper that directly invokes the natural-number-object equivalence from the upstream Lawvere statement.
claimFor any two meta-carriers $R$ and $S$ (instances of LogicRealization), the forced arithmetic orbits are canonically equivalent: $R.Orbit ≃ S.Orbit$.
background
The meta-carrier is the type of LogicRealization.{0,0} instances, living in Type 1. This module shows that the universal forcing meta-theorem itself fits the Law-of-Logic structural shape on the meta-carrier, with a meta-cost that is zero on propositional equality and the meta-theorem supplying the comparison law. The local setting is the self-reference formalization where structural self-application closes the framework without Gödel-style diagonalization.
proof idea
This is a one-line wrapper that applies universal_forcing_via_NNO to the pair R and S. The upstream lemma states that any two realizations have iteration orbits satisfying the natural-number-object property, hence are canonically equivalent via IsNaturalNumberObject.equiv.
why it matters in Recognition Science
This supplies the forced-arithmetic-invariance condition required by framework_is_reflexively_closed, which states that the meta-theorem instantiates the Law-of-Logic shape on the type of realizations. It also feeds meta_meta_theorem (showing preservation under self-application) and metaRealizationCert. The module doc notes that this earns reflexive closure: the act of comparing realizations is itself Law-of-Logic-shaped.
scope and limits
- Does not instantiate the full LogicRealization structure for the meta-carrier.
- Does not prove Gödel-style self-reference or diagonal lemmas.
- Does not address universe lifts beyond the explicit Type 1 convention.
- Does not compute explicit orbit elements or numerical values.
Lean usage
metaForcedArithmeticInvariance R Sformal statement (Lean)
113noncomputable def metaForcedArithmeticInvariance (R S : MetaCarrier) :
114 R.Orbit ≃ S.Orbit :=
proof body
Definition body.
115 universal_forcing_via_NNO R S
116
117/-- The meta-theorem is reflexive: comparing a realization to itself
118yields the identity equivalence on its orbit. -/