distinction_realizations_have_same_arithmetic
plain-language theorem explainer
Any two non-singleton carriers, each equipped with a chosen distinction, induce LogicRealizations whose extracted arithmetic objects have canonically isomorphic Peano carriers. Researchers building the Recognition Science foundation layer would invoke this result to confirm that forced arithmetic is universal across carriers. The definition composes the orbit equivalences to the canonical LogicNat from each realization.
Claim. Let $K$ and $L$ be types with decidable equality. For distinct $x,y$ in $K$ and distinct $a,b$ in $L$, the carrier of the Peano arithmetic extracted from the logic realization built on the distinction in $K$ is isomorphic to the corresponding carrier built on the distinction in $L$.
background
The module Universal Instantiation from One Distinction shows how any carrier with two distinguishable points instantiates the Law-of-Logic interface on that carrier itself. The construction logicRealizationOfDistinction takes a type $K$ with $x≠y$ and produces a LogicRealization whose Carrier is exactly $K$, whose Cost is Nat, and whose internal orbit is the free LogicNat orbit. Upstream, arithmeticOf extracts the forced arithmetic object from any such realization; its doc-comment states that for any two Law-of-Logic realizations the arithmetic objects extracted are equivalent.
proof idea
This is a one-line wrapper that composes the orbit equivalence to LogicNat supplied by the first distinction realization with the symmetric equivalence supplied by the second. It relies directly on the orbitEquivLogicNat field of each LogicRealization produced by logicRealizationOfDistinction.
why it matters
This declaration shows that the forced arithmetic object is independent of the underlying carrier once a distinction is present, thereby completing the first universal step asserted in the module: every non-singleton carrier yields the same arithmetic as the canonical recognition realization. It advances the Recognition framework from a bare distinction to carrier-invariant arithmetic before the continuous J/spacetime layer is reached via realization-invariance. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.