arithmeticOf
plain-language theorem explainer
Assigns to each Law-of-Logic realization its forced arithmetic object, the initial Peano algebra extracted from the realization's own identity-step orbit. Researchers proving arithmetic invariance across realizations or stating the universal forcing theorem cite it as the base extractor. The definition is a one-line wrapper delegating to the extracted constructor.
Claim. Let $R$ be a realization of the Law of Logic. Then arithmeticOf$(R)$ is the arithmetic object whose Peano algebra is generated by the identity-step orbit of $R$ and which is initial among all such algebras.
background
The 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. A LogicRealization supplies a carrier together with an identity element and a generator step whose orbit is the smallest subset of positive reals closed under multiplication by the generator and containing the identity. The structure ArithmeticOf $R$ packages a PeanoObject with a proof that the object is initial. Upstream, the extracted definition constructs this object by taking the Peano algebra realized by the orbit of $R$ together with the initiality witness for that algebra.
proof idea
One-line wrapper that applies ArithmeticOf.extracted to the input realization.
why it matters
This definition supplies the common arithmetic object referenced by every invariance statement, including categorical_arithmetic_invariant, bool_arithmetic_invariant, modular_arithmetic_invariant, ordered_arithmetic_invariant and physics_arithmetic_invariant. It fills the first formal spine of the universal forcing theorem by making the extracted arithmetic the reference point for all realizations. It touches the open question of how later modules enrich the interpretation map from each carrier into this invariant arithmetic object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.