distinction_arithmetic_equiv_logicNat
plain-language theorem explainer
Any non-singleton carrier K equipped with a chosen distinction x ≠ y yields a LogicRealization whose extracted arithmetic object has Peano carrier canonically equivalent to LogicNat. Researchers applying universal forcing to arbitrary distinguishable carriers cite this to obtain the same arithmetic structure as the canonical realization without assuming extra structure on K. The definition is a one-line wrapper that directly invokes the orbit equivalence supplied by the distinction realization construction.
Claim. For any type $K$ with decidable equality and distinct elements $x,y$ in $K$, the Peano carrier of the arithmetic object extracted from the logic realization built from the distinction $(x,y)$ is equivalent to LogicNat.
background
The module constructs a LogicRealization directly from any carrier $K$ that admits at least one distinction. The realization uses the two-valued equality cost as comparison, takes $x$ as identity point, and maps every element to $y$ under the step operation; its internal orbit is the free LogicNat orbit. LogicNat is the inductive type generated by an identity element (zero-cost) and a successor step, mirroring the orbit of repeated multiplication by the generator in the positive reals. The function arithmeticOf extracts the full ArithmeticOf record from any such realization, exposing its Peano carrier among other data.
proof idea
The definition is a one-line wrapper that applies the orbitEquivLogicNat field of the logicRealizationOfDistinction term.
why it matters
This definition supplies the canonical equivalence between the forced arithmetic of an arbitrary distinction-based realization and the standard LogicNat, thereby completing the module's first universal step: every non-singleton carrier instantiates the Law-of-Logic interface and therefore inherits the same arithmetic object under Universal Forcing. It supports the subsequent claim that realization-invariance, rather than native J-cost on $K$, reaches the continuous layer. The construction touches the transition from bare distinction to forced arithmetic without presupposing a smooth real-valued cost function on the carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.