forcedArith
plain-language theorem explainer
For any Law-of-Logic realization R, the forced arithmetic is the Peano object extracted from R, with all ArithmeticOf universes pinned to R's carrier universe. Downstream CanonicalIso lemmas cite it as the uniform source of zero and step for every realization. The body is a one-line abbreviation of the existing arithmetic-extraction map.
Claim. Given a Law-of-Logic realization $R$, write $\mathrm{forcedArith}(R)$ for the arithmetic object forced by $R$, namely the Peano object (carrier, zero, step) extracted from $R$'s identity/step data, with every universe parameter of that arithmetic object fixed to the carrier universe of $R$.
background
A Law-of-Logic realization supplies a carrier, a comparison cost, an identity element, and a step/generator action, together with the structural laws the Universal Forcing program needs. The invariant target is not the ambient carrier; it is the arithmetic object extracted from the identity/step data.
That extracted object is an ArithmeticOf structure: a Peano object (carrier with zero and successor) together with an initiality witness. The Universal Forcing spine already produces a bare carrier bijection between the forced arithmetics of any two realizations. This module upgrades that bijection to a unique structure-preserving Peano isomorphism.
The present abbreviation is the uniform handle used throughout CanonicalIso: every later statement about zero-preservation, step-commutation, uniqueness, and the isomorphism certificate is quantified over forcedArith R rather than the raw extraction map, with universes monomorphized to the realization's own carrier level.
proof idea
One-line abbreviation: forcedArith R is definitionally arithmeticOf R, with the ArithmeticOf universe parameters pinned to {u, v, u, u, u} so the Peano carrier lives in the same universe as R.Carrier. No proof obligations; pure universe-specialized alias.
why it matters
This alias is the spine of CanonicalIso. Every parent result in the module is stated in terms of it: equivOfInitial_map_zero and equivOfInitial_map_step show the universal forcing bijection sends forced zero to forced zero and commutes with step; toHom, universalForcingPeanoEquiv, and peanoEquiv_unique package that map as the unique Peano-algebra isomorphism; hom_eq_universalForcing says any Peano homomorphism equals that map; UniversalForcingIsoCert quantifies the package over all {0,0} realizations.
In the Recognition framework this is Part II of Universal Forcing: arithmetic extraction. It does not yet touch the forcing chain T0–T8, the J-cost, or physical constants; it only locks the Peano layer so later work can lift the unique iso to ordered-semiring structure. The module doc is explicit that ring operations and order are the remaining crown toward full Part II.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.