Pith. sign in
module module high

IndisputableMonolith.Foundation.DistinctionToArithmetic

show as:
view Lean formalization →

From one distinction on a carrier K (points x ≠ y), the module extracts the forced ArithmeticOf object via the K-native Law-of-Logic realization. Anyone who needs the named map from bare distinction data to Peano arithmetic cites this packaging. Construction composes Universal Instantiation from Distinction with ArithmeticOf initiality; uniqueness follows from Universal Forcing. The reals are recorded as not forced.

claimGiven a carrier $K$ and distinguishable points $x \neq y$ in $K$, there is a forced arithmetic object obtained from the $K$-native Law-of-Logic realization: the initial Peano algebra generated by that realization's identity and step data, unique up to unique isomorphism. A forcing map from distinction data to this object exists and is unique in the universal-forcing sense. The real line is not among the objects forced by a bare distinction.

background

Recognition Science extracts arithmetic from Law-of-Logic realizations rather than postulating Peano axioms. ArithmeticOf takes any such realization and returns the initial Peano algebra generated by its identity and step data. Initial objects are unique up to unique isomorphism; that is the mechanism behind Universal Forcing (any two realizations have canonically equivalent forced arithmetic objects).

Universal Instantiation from Distinction answers the skeptical objection that a bare distinction should not sit beside a prebuilt reality certificate. Given carrier $K$ with $x \neq y$, it builds a $K$-native Law-of-Logic realization on that carrier alone. This module feeds that realization into ArithmeticOf and names the resulting forced object, the forcing map, and related surface facts (Peano structure, countability, equivalence to logic-native naturals).

RealLineNonNativity supports the negative claim: the continuum is not forced from a single distinction, so the forced object stays discrete and countable.

proof idea

Definition-and-packaging module, not one deep proof. arithmeticOfDistinction is the composite of Universal Instantiation from Distinction with the ArithmeticOf extractor. Peano surface structure, carrier equivalence to logic-native naturals, and countability are corollaries of initiality of the forced Peano algebra. distinction_forces_arithmeticOf, the forcing map, and map uniqueness are instances of Universal Forcing (canonical equivalence of initial Peano algebras). real_not_forced_from_distinction applies real-line non-nativity. DistinctionArithmeticCert bundles the positive forcing facts for downstream certificates.

why it matters in Recognition Science

Supplies the named map from distinction data to ArithmeticOf that the program register asks for: the bridge from "one distinction exists" to "Peano arithmetic is forced." It sits on Universal Instantiation from Distinction, ArithmeticOf initiality, and Universal Forcing, and records that the reals are outside the forced package. No used_by edges are listed yet; the natural consumers are foundation certificates and any later step that needs arithmetic as already forced from bare distinguishability. In the broader RS chain this is substrate for later landmarks (phi, eight-tick octave, D = 3), which presuppose discrete arithmetic rather than a continuum forced at the first step.

scope and limits

depends on (6)

Lean names referenced from this declaration's body.

declarations in this module (11)