arith
plain-language theorem explainer
arith supplies the forced arithmetic object for any strict Law-of-Logic realization by delegating to the existing extraction after conversion to the lightweight interface. Domain modelers in biology, ethics, or categorical structures cite it to obtain the Peano object without supplying an orbit field. The definition is a one-line wrapper that applies the arithmetic extraction to the converted realization.
Claim. For a strict realization $R$ (native comparison, composition, identity, and non-contradiction data only), the arithmetic object is the one extracted from the lightweight conversion of $R$, where the orbit is derived uniformly as the inductive type generated by the identity element and the generator step.
background
StrictLogicRealization is the structure that supplies only native law data: a carrier type, a cost type with zero, a compare function, a compose function, a one element, a generator, plus the identity and non-contradiction laws. The module derives the free orbit uniformly as LogicNat, the inductive type with constructors identity (zero-cost element) and step (iteration of the generator). toLightweight converts a strict realization to the earlier LogicRealization interface by setting the zero field to the one element and leaving the orbit fields to be derived. arithmeticOf then extracts the ArithmeticOf structure, which packages a PeanoObject together with its initiality property.
proof idea
One-line wrapper that applies arithmeticOf to the result of toLightweight R.
why it matters
The definition completes the strict path of Universal Forcing so that domain realizations (biology, ethics, music, narrative, ordered, categorical) can be audited for equivalence of their extracted Peano carrier to LogicNat. It is referenced by the _ok audit lemmas that invoke orbitEquivLogicNat on the lightweight conversion. The construction therefore lets the framework treat strict realizations uniformly without re-proving arithmetic extraction for each domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.