Foundation Universal Instantiation From Distinction Eq Cost Ne One

The equality cost

The declaration eqCost_ne_one is a small but load-bearing theorem about a simple idea: the cost of recognizing that two things are different. In the framework's model, recognition has a price, and the most basic price is a binary one. The cost function eqCost assigns 0 when two inputs are equal and 1 when they are distinct. The theorem states that if you have a proof that two points are not equal, then the cost is exactly 1. It is a formal, machine-checked statement: given a distinction, the cost is one.

This theorem is part of a larger construction in the framework's library, a machine-checked collection of formal theorems. The construction takes any carrier, any set of points, with at least two distinguishable elements, and builds a realization of the framework's logic on that very carrier. The equality cost serves as the comparison, one point serves as the identity, and a step map sends everything to the second point. The theorem eqCost_ne_one is the hinge: it certifies that the cost function behaves correctly when a distinction is present.

What the theorem does not claim is just as important. It does not say that any carrier has a smooth, real-valued cost function of the kind the framework's main theorems use. It does not assert that the equality cost satisfies the multiplicative composition law that the framework's central cost function satisfies. In fact, the framework explicitly notes that equality cost provably fails that law. The theorem only establishes the behavior of a two-valued cost on a distinction; it does not elevate that cost to the status of the framework's primary cost function.

The payoff is universal instantiation. The construction proves that any non-singleton carrier, any set with at least two distinct points, can instantiate the framework's logic interface. This is the first universal step: it shows the framework's arithmetic object arises from any bare distinction, not just from a specially chosen carrier. The theorem is a bridge from the abstract logic to any concrete set with two points.

theorem eqCost_ne_one {K : Type u} [DecidableEq K] {a b : K} (h : a ≠ b) :
    eqCost a b = 1 := by
  simp [eqCost, h]

/-- 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 equality cost is not the framework's central cost function. The theorem does not claim that any carrier has a native smooth real-valued cost. The equality cost does not satisfy the multiplicative composition law.

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: