Foundation Universal Instantiation From Distinction

A minimal starting point

In mathematics, a distinction is simply the fact that two objects are not the same. This construction takes that bare idea and shows it is enough to reconstruct the natural numbers: 0, 1, 2, and so on. The construction is minimal. It does not assume a continuum, a metric, or any smooth structure. It starts with a carrier, any collection of objects, and two distinct points within it, and builds a discrete record of events from that alone.

The key move is to define a cost on the carrier: zero when two inputs are equal, one when they are distinct. This two-valued equality cost is symmetric and satisfies a triangle inequality, so it qualifies as a genuine cost in the framework's sense. The framework then defines a step map that sends every point to the second distinguished point, creating a cycle that alternates between the two. This cycle is the seed of arithmetic: the first point plays the role of zero, and every subsequent step plays the role of a successor.

The framework proves a universal instantiation theorem: any carrier with at least two distinguishable points admits a native realization of the framework's logic interface. This means the carrier itself, not some external copy, supports the structure. The theorem is constructive, in the sense that it names the two points and the step map explicitly. A further theorem states that any inhabited carrier with some distinction admits such a realization, and a certificate bundles both statements into a single package.

In Recognition Science, this result matters because it answers a skeptical objection. Earlier work assumed a canonical reality certificate existed and bundled a distinction beside it. This framework shows the distinction can stand alone: it instantiates the interface on its own carrier, without borrowing from a pre-existing structure. The forced arithmetic that follows is canonically equivalent to the natural numbers, and any two such carriers, however different, produce the same arithmetic object.

The continuous layer of spacetime is not reached here. The framework explicitly declines to assert that every carrier has a smooth real-valued cost. Instead, it proves the first universal step that is actually true: distinction implies arithmetic. The smooth layer is reached later through canonical realization-invariance, not by pretending an arbitrary carrier is the real line. This is a deliberate boundary, and it keeps the claim honest.

/-- Every inhabited carrier with some distinction admits a native
`LogicRealization`. The `DecidableEq K` instance is obtained classically. -/
theorem exists_logicRealization_of_distinction
    (K : Type u) [Nonempty K] (h : ∃ x y : K, x ≠ y) :
    Nonempty (LogicRealization.{u, 0}) := by
  classical
  rcases h with ⟨x, y, hxy⟩
  exact ⟨logicRealizationOfDistinction K x y hxy⟩

/-- The forced arithmetic of the `K`-native realization is canonically
`LogicNat`. -/
noncomputable def distinction_arithmetic_equiv_logicNat
    {K : Type u} [DecidableEq K] (x y : K) (hxy : x ≠ y) :
    (UniversalForcing.arithmeticOf
      (logicRealizationOfDistinction K x y hxy)).peano.carrier ≃ LogicNat :=
  (logicRealizationOfDistinction K x y hxy).orbitEquivLogicNat

/-- Any two non-singleton carriers, with chosen distinctions, have
canonically equivalent forced arithmetic. -/
noncomputable def distinction_realizations_have_same_arithmetic
    {K L : Type u} [DecidableEq K] [DecidableEq L]
    {x y : K} {a b : L} (hxy : x ≠ y) (hab : a ≠ b) :
    (UniversalForcing.arithmeticOf
      (logicRealizationOfDistinction K x y hxy)).peano.carrier ≃
    (UniversalForcing.arithmeticOf
      (logicRealizationOfDistinction L a b hab)).peano.carrier :=
  (logicRealizationOfDistinction K x y hxy).orbitEquivLogicNat.trans
    (logicRealizationOfDistinction L a b hab).orbitEquivLogicNat.symm

theorem universalInstantiationCert
    (K : Type u) [Nonempty K] :
    UniversalInstantiationCert K where
  instantiate := exists_logicRealization_of_distinction K
  named := exists_named_logicRealization_of_distinction K

What this page does not claim

The framework does not prove that every carrier has a smooth real-valued J-cost. The framework does not derive the fine-structure constant or any specific physical constant. The framework does not show that the two-valued equality cost satisfies the multiplicative composition law, which it provably fails.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/UniversalInstantiationFromDistinction.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: