arithmeticOf
plain-language theorem explainer
The definition extracts the forced arithmetic object from any Law-of-Logic realization by pulling its internal identity-step orbit into a Peano algebra. Researchers working on universal forcing or logic realizations would cite this to establish the invariant arithmetic across different models. It is implemented as a one-line wrapper delegating to the extracted constructor in ArithmeticOf.
Claim. For any realization $R$ of the Law of Logic, the forced arithmetic object $A(R)$ is the Peano algebra extracted from $R$'s orbit together with its initiality witness.
background
The UniversalForcing module states the first formal version of the Universal Forcing theorem: any two Law-of-Logic realizations have canonically equivalent forced arithmetic objects because those objects are initial Peano algebras. Key upstream definitions include ArithmeticOf, the structure pairing a PeanoObject with a proof of its initiality, and LogicNat, the inductive type whose identity and step constructors generate the multiplicative orbit {1, γ, γ², …} as the smallest subset of positive reals closed under the generator and containing the zero-cost element. The extraction step uses the realization's own internal orbit rather than an external reference object.
proof idea
This is a one-line wrapper that applies ArithmeticOf.extracted to the input realization, constructing the structure with peano set to realizationPeano R and initial set to realization_initial R.
why it matters
This definition supplies the central object referenced by every downstream invariant, including categorical_arithmetic_invariant, bool_arithmetic_invariant, modular_arithmetic_invariant, ordered_arithmetic_invariant, and physics_arithmetic_invariant, each of which invokes equivOfInitial to obtain the canonical equivalence between initial Peano algebras. It realizes the first theorem form of Universal Forcing and supplies the arithmetic spine used in later physics and engineering modules. In the Recognition framework it marks the transition from logic realizations to the invariant arithmetic that supports the phi-ladder and forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.