arith
plain-language theorem explainer
arith supplies the forced arithmetic object for any strict logic realization by delegating through its lightweight conversion. Researchers auditing domain realizations against the canonical natural numbers cite this when confirming that native law data alone yields the Peano structure. It is a one-line wrapper that composes the lightweight conversion with the arithmetic extraction function.
Claim. For any strict logic realization $R$, the arithmetic object is defined as the arithmetic object extracted from the lightweight realization obtained by converting $R$.
background
A strict logic realization supplies only a carrier type, a cost type equipped with zero, comparison and composition operations, plus identity and non-contradiction laws; no orbit field is present. The module derives the free orbit uniformly as LogicNat, the inductive type whose constructors identity and step mirror the multiplicative orbit generated by the generator element. toLightweight maps any strict realization to the standard logic realization interface by populating the zero and orbit fields from LogicNat. arithmeticOf then extracts the Peano object together with its initiality witness from any logic realization. This construction lives in the StrictRealization module, whose setting requires that the orbit used by universal forcing is always the derived LogicNat.
proof idea
The definition is a one-line wrapper that applies arithmeticOf to the result of toLightweight R.
why it matters
This definition is called by the axiom-audit lemmas _biology_ok, _categorical_ok, _ethics_ok, _music_ok, _narrative_ok and _ordered_ok, each of which shows that the Peano carrier of arith(R) is equivalent to LogicNat for the corresponding domain realization. It closes the strict interface path for the universal forcing theorem, confirming that realizations supplying only native law data still force the same arithmetic object. It thereby supports the claim that the extracted arithmetic is independent of the presentation of the realization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.