Foundation Universal Instantiation From Distinction Universal Instantiation Cert

The universal certificate

In ordinary mathematics, the statement "there exist two distinct points" is a weak starting point. From it, the Recognition Science framework's certificate (a machine-checked record of a proven property) shows that any collection of objects with at least two distinguishable members can support a complete structure of logical arithmetic. The theorem named universalInstantiationCert proves this in the framework's machine-checked library of formal theorems.

The construction is minimal. Given any carrier set K with two distinct points x and y, the framework defines a cost function that assigns 0 when two inputs are equal and 1 when they differ. It then builds a step map that sends every element to y, and interprets the natural numbers so that zero maps to x and every successor maps to y. This creates an internal orbit that behaves exactly like the counting numbers, with the two-point distinction as its seed.

The certificate itself packages two claims. The first says that whenever a nonempty carrier has two distinct points, a logical realization exists on that very carrier. The second, more precise version retains the chosen points and the proof of their distinctness. Both are proved in the framework's library, and the certificate bundles them into a single statement.

What the certificate deliberately does not claim is just as important. It does not assert that every carrier carries a smooth real-valued cost of the kind that leads to the framework's continuous spacetime layer. The two-valued equality cost satisfies only an additive composition law, the triangle inequality, and it provably fails the multiplicative composition law that the full recognition cost requires. The certificate proves the first universal step that is actually true: every non-singleton carrier instantiates the logical interface, and therefore the same forced arithmetic object as the canonical realization. The continuous layer is reached later through canonical realization-invariance, not by pretending an arbitrary set is the positive real line.

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

/-- 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 certificate does not claim that every carrier has a native smooth real-valued J-cost. The certificate does not prove that the two-valued equality cost satisfies the multiplicative composition law. The certificate does not establish the continuous spacetime layer directly from a bare distinction.

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: