arith_universal_initial'
plain-language theorem explainer
Any Law-of-Logic realization forces an arithmetic structure whose Peano carrier is canonically equivalent to the reference LogicNat object. Researchers working on universal forcing or cross-realization invariance would cite this equivalence when establishing that arithmetic is independent of the concrete carrier. The definition is a direct one-line alias to the orbit equivalence field already present in the realization.
Claim. For any Law-of-Logic realization $R$, the Peano carrier extracted from the arithmetic of $R$ is equivalent to the natural numbers forced by the Law of Logic: $(arithmeticOf R).peano.carrier ≃ LogicNat$.
background
LogicRealization supplies a carrier type, a comparison cost type with zero-cost element, an identity element, and a step generator together with the structural laws required by the Universal Forcing program. The target of the program is never the ambient carrier but the arithmetic object extracted from the identity and step data. LogicNat is the inductive type whose constructors identity and step mirror the orbit {1, γ, γ², …} as the smallest subset of positive reals closed under multiplication by the generator γ and containing the multiplicative identity.
proof idea
One-line wrapper that returns the orbitEquivLogicNat field of the supplied realization R.
why it matters
This definition supplies the initial arithmetic equivalence required by the Universal Forcing Meta-Theorem stated in the module. It guarantees that every Law-of-Logic realization produces a Peano structure canonically equivalent to the reference LogicNat, thereby feeding the invariance results universal_forcing and universal_peano_surface. The construction directly implements the claim that forced arithmetic is realization-independent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.