metaForcedArithmeticInvariance
plain-language theorem explainer
The definition reifies the universal forcing meta-theorem as the canonical orbit equivalence between any two LogicRealization instances inside the meta-carrier. Researchers establishing reflexive closure of the Recognition framework cite it as the comparison law of the meta-realization. It is a one-line wrapper that directly invokes the NNO equivalence.
Claim. For any two instances $R,S$ of LogicRealization$_{(0,0)}$, there exists a canonical equivalence $R.Orbit ≃ S.Orbit$ supplied by the natural-number-object property.
background
MetaCarrier is the type of LogicRealization.{0,0} instances and lives in Type 1. The module shows that the meta-theorem itself fits the Law-of-Logic structural shape on this carrier, with a meta-cost and the forced-arithmetic-invariance condition. The upstream result universal_forcing_via_NNO states that any two realizations have iteration orbits satisfying the natural-number-object property, hence are canonically equivalent.
proof idea
One-line wrapper that applies universal_forcing_via_NNO to the pair of realizations.
why it matters
It supplies the forced-arithmetic-invariance condition required by framework_is_reflexively_closed, which proves the framework is reflexively closed. The declaration completes the meta-realization certificate and is invoked by meta_meta_theorem to establish the reflexive-fixed-point property. It directly instantiates the meta-theorem reified as the comparison law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.