forced_arithmetic_surfaces_equivalent
plain-language theorem explainer
Any two Law-of-Logic realizations force isomorphic Peano carriers: the extracted arithmetic surfaces are equivalent as types. Cite this when arguing that the Universal Forcing arithmetic object does not depend on the ambient realization. The proof is a short term construction: both orbits are identified with the same LogicNat type, hence with each other by transitivity and symmetry.
Claim. For any two Law-of-Logic realizations $R$ and $S$, the Peano carriers of their forced arithmetic objects are equivalent: there exists a type equivalence $(\mathrm{arithmeticOf}\, R).\mathrm{peano}.\mathrm{carrier} \simeq (\mathrm{arithmeticOf}\, S).\mathrm{peano}.\mathrm{carrier}$.
background
UniversalForcing states the first formal Universal Forcing theorem: any two Law-of-Logic realizations have canonically equivalent forced arithmetic objects, because those objects are initial Peano algebras.
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 forcing program needs. The invariant target is not the ambient carrier; it is the arithmetic object extracted from the identity/step data. The map arithmeticOf packages that extraction: the forced arithmetic object of a realization.
The Peano surface of that object is the discrete arithmetic skeleton (carrier plus successor structure) pulled out of the realization's orbit under the generator. Equivalence of those carriers is the precise sense in which two realizations "force the same arithmetic."
proof idea
Term-mode proof that builds a witness of Nonempty of an equivalence. After unpacking, the goal is rewritten to an equivalence of orbits $R.\mathrm{Orbit} \simeq S.\mathrm{Orbit}$. Each realization supplies orbitEquivLogicNat, an equivalence from its orbit to the common LogicNat type. Compose $R$'s equivalence with the inverse of $S$'s; the composite is the required orbit equivalence, hence the Peano-carrier equivalence.
why it matters
This is the concrete equivalence form of Universal Forcing inside Foundation: arithmetic surfaces forced by distinct Law-of-Logic realizations are the same up to type equivalence. The module doc frames the parent claim as "any two Law-of-Logic realizations have canonically equivalent forced arithmetic objects, because those objects are initial Peano algebras." The declaration closes that uniqueness statement for the Peano carriers themselves.
No downstream consumers are wired yet in the graph; siblings such as universal_forcing, arith_universal_initial, and arithmetic_invariant sit beside it as the rest of the forcing package. In the broader RS chain this supports the claim that the discrete arithmetic layer (and thus the eight-tick / octave counting structure built on it) is forced independently of which realization one starts from.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.