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. It supplies the named map from distinction data to that arithmetic, uniqueness of the forcing map, countability and Peano surface of the carrier, and a certificate that the reals are not forced. Anyone bridging bare distinction to Peano arithmetic cites this package. The argument wires Universal Instantiation from Distinction into ArithmeticOf initiality.

claimGiven a carrier $K$ and distinguishable points $x \neq y$ in $K$, there is a forced arithmetic object extracted from the $K$-native Law-of-Logic realization. The forcing map from distinction data is unique; the arithmetic carrier is countable and equivalent (as a Peano algebra) to the logic naturals; and the real line is not forced by a single distinction.

background

Foundation setting: start from a bare distinction and obtain arithmetic without smuggling in a pre-built number system. ArithmeticOf extracts arithmetic from an abstract Law-of-Logic realization: once identity and step data are supplied, the forced object is the initial Peano algebra on that data. Initial objects are unique up to unique isomorphism; that is the mechanism behind Universal Forcing.

Universal Instantiation from Distinction repairs the skeptical gap in Reality-from-Distinction: a carrier $K$ with $x \neq y$ must first instantiate the Law-of-Logic interface on its own carrier, not sit beside an already-certified reality object. Universal Forcing then says any two such realizations have canonically equivalent forced arithmetic objects.

Real-line non-nativity supplies the negative control: continuum structure is not native to, and is not forced by, a single distinction in this calculus.

proof idea

Definition-and-packaging module, not a single deep proof. It imports Universal Instantiation from Distinction to obtain a $K$-native Law-of-Logic realization from $(K,x,y)$, then applies ArithmeticOf to that realization to name arithmeticOfDistinction. Downstream siblings record the Peano surface, the carrier equivalence with the logic naturals, countability, the forcing map and its uniqueness, a universal-objective certificate, and the negative result that the reals are not forced. Uniqueness and canonicity ride on initiality of the Peano algebra (Universal Forcing / Canonical Forcing), not on ad-hoc constructions.

why it matters in Recognition Science

This is the named Lean map the program register asks for: distinction data to ArithmeticOf. It closes the core objection that a bare distinction was only bundled next to a pre-existing certificate rather than instantiating logic and arithmetic on its own carrier. Upstream, it depends on Arithmetic from Logic, ArithmeticOf initiality, Universal Forcing (canonically equivalent forced arithmetic for any two Law-of-Logic realizations), Canonical Forcing, Universal Instantiation from Distinction, and Real-Line Non-Nativity. No downstream edges are recorded yet; the module is an export surface for the distinction-to-arithmetic bridge inside Foundation, prior to physics forcing (T0–T8, RCL, phi ladder).

scope and limits

depends on (6)

Lean names referenced from this declaration's body.

declarations in this module (11)