Foundation Universal Instantiation From Distinction Logic Realization Of Distinc

The distinction step

In mathematics, a distinction, a choice of two different points in a set, is often the first move toward structure. The Recognition Science framework makes that move precise. Its machine-checked library of formal theorems shows that any set with at least two distinguishable points can carry a recognition structure, a discrete record of how points compare and move. The key step is a map that sends every point to the same distinguished second point. This constant map is the action of the structure, and the theorem logicRealizationOfDistinction_actionInvariant proves that this action is invariant: no matter which two points you start with, the map sends them both to the same place.

The theorem is a small but load-bearing result. It shows that the action does not depend on the input point at all. If the structure's step map is the constant map onto the marked second point, then applying it to any two points yields the same output. This invariance is what makes the structure coherent: the step is a single, well-defined move, not a scattered collection of unrelated transitions. The proof is immediate from the definition, since the map ignores its input entirely, but the statement is what the framework needs to build further structure.

In Recognition Science, this result is part of a larger argument. The framework models reality as a ledger, a discrete record of recognition events, and it derives physical laws from the cost of those recognitions. The theorem here is a preliminary step: it shows that a bare distinction, the minimal possible content, already instantiates the framework's logical interface. This is the first universal step that is actually true. It does not claim that every set has a smooth, real-valued cost function. It does not claim that the constant map is the only possible action. It claims only that the constant map is a valid, invariant action for any set with a distinction, and that this is enough to apply the framework's forcing machinery.

The theorem also carries a deliberate limitation. The two-valued equality cost, which assigns zero to equal inputs and one to distinct inputs, satisfies the additive composition law, the triangle inequality, but it provably cannot satisfy the multiplicative composition law that the full cost function requires. The framework is explicit about this: the minimal distinction realization carries only the laws that hold for it, and it declines the one law it cannot satisfy. This is not a failure but a precise boundary. The theorem establishes what a single distinction can do, and it names what it cannot.

What this means for a reader is that the framework's foundation is not built on an arbitrary assumption. It is built on a minimal, provable claim: any two distinct points are enough to start. From there, the framework's forcing chain can proceed, but this theorem itself does not reach the continuous, smooth layer of physics. That layer is reached through a separate canonical realization, not by pretending an arbitrary set is the real line. The distinction step is the first rung, and it is a solid one.

/-- The distinction step action is invariant across inputs: it is the constant
map onto the marked second point. -/
theorem logicRealizationOfDistinction_actionInvariant
    {K : Type u} [DecidableEq K] (x y : K) (hxy : x ≠ y) :
    (logicRealizationOfDistinction K x y hxy).actionInvariant := by
  show ∀ a b : K, distinctionStep x y a = distinctionStep x y b
  intro _ _; rfl

/-- 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 minimal distinction realization satisfies the *additive* composition law
(the triangle inequality) of its two-valued equality cost. This is NOT the
multiplicative composition consistency (L4), which equality cost provably fails
(`PrimitiveDistinction.equality_cost_insufficient_for_recognition`); the slot
deliberately carries only the additive law that does hold. -/
theorem logicRealizationOfDistinction_composition
    {K : Type u} [DecidableEq K] (x y : K) (hxy : x ≠ y) :
    (logicRealizationOfDistinction K x y hxy).composition := by
  show ∀ a b c : K, eqCost a c ≤ eqCost a b + eqCost b c
  intro a b c
  by_cases hac : a = c
  · have h0 : eqCost a c = 0 := by simp [eqCost, hac]
    rw [h0]; exact Nat.zero_le _
  · have hac1 : eqCost a c = 1 := eqCost_ne_one hac
    have hsplit : a ≠ b ∨ b ≠ c := by
      by_contra hcon
      push_neg at hcon
      exact hac (hcon.1.trans hcon.2)
    rw [hac1]
    rcases hsplit with hab | hbc
    · have h1 : eqCost a b = 1 := eqCost_ne_one hab
      have h2 : 0 ≤ eqCost b c := Nat.zero_le _
      omega
    · have h1 : eqCost b c = 1 := eqCost_ne_one hbc
      have h2 : 0 ≤ eqCost a b := Nat.zero_le _
      omega

What this page does not claim

The action invariant theorem does not claim that the constant map is the only possible action for a distinction. The theorem does not claim that the distinction realization reaches the smooth spacetime layer on its own. The theorem does not claim that every carrier has a native smooth real-valued J-cost.

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: