order_arithmetic_invariant
The definition establishes that the Peano carrier extracted from the order-theoretic realization on the integers is equivalent to the Peano carrier from any other Law-of-Logic realization. Researchers tracing the universal forcing chain would cite it to confirm invariance of the arithmetic structure. The proof is a direct one-line application of the general equivalence between initial Peano objects.
claimLet $R$ be any Law-of-Logic realization. The Peano carrier of the arithmetic object forced by the ordered realization on the integers is equivalent to the Peano carrier of the arithmetic object forced by $R$.
background
The module defines an order-theoretic realization on the integers equipped with equality cost and unit step. This lightweight realization carries the forced arithmetic via a certified internal orbit while interpreting the carrier as the standard embedding of LogicNat into integers. A Law-of-Logic realization consists of a carrier type, a cost type with zero, a comparison map, a zero element, and the structural propositions required by the forcing program. The arithmetic object associated to any such realization is a Peano object together with a proof that the object is initial. The upstream equivalence result constructs the natural isomorphism between two initial Peano objects by lifting each through the other.
proof idea
This is a one-line wrapper that applies the equivalence of initial Peano objects to the arithmetic objects of the ordered realization and the given realization.
why it matters in Recognition Science
The declaration confirms that the ordered realization carries the universal forced arithmetic, directly supporting the first theorem form of Universal Forcing that any two Law-of-Logic realizations yield equivalent arithmetic objects. It anchors the order-theoretic choice inside the forcing chain without altering the extracted Peano structure. No open questions are closed here; the result simply records the invariance for this particular realization.
scope and limits
- Does not compute explicit maps between carriers.
- Does not address realizations outside the Law-of-Logic class.
- Does not establish uniqueness of the ordered realization.
formal statement (Lean)
74noncomputable def order_arithmetic_invariant (R : LogicRealization.{0, 0}) :
75 (arithmeticOf orderRealization).peano.carrier ≃ (arithmeticOf R).peano.carrier :=
proof body
Definition body.
76 ArithmeticOf.equivOfInitial (arithmeticOf orderRealization) (arithmeticOf R)
77
78end OrderRealization
79end UniversalForcing
80end Foundation
81end IndisputableMonolith