Foundation Universal Forcing Strict Ordered Int Cost

The integer cost function

The declaration intCost defines a cost function on pairs of integers. It charges 0 when the two integers are equal and 1 when they differ. This is the simplest possible discrete cost: either two things are the same, or they are not. The function maps any pair of integers to a natural number, so the cost is always a nonnegative whole number.

Two properties of this function are proved as theorems. First, the cost of comparing an integer with itself is always 0. Second, the cost is symmetric: the cost of comparing a to b equals the cost of comparing b to a. Both follow directly from the definition and the equality relation on integers. The symmetry property is the recognition-theoretic requirement that cost does not depend on the order in which two items are presented.

In Recognition Science, this integer cost function is a concrete instance of a ledger, a discrete record of events with a forced cost of recognition. The framework builds a strictOrderedRealization on top of this cost, and proves that this realization's arithmetic is equivalent to the standard natural numbers. The integer cost function is therefore not an isolated curiosity; it is the seed of a full arithmetic structure.

What intCost does not claim is important. It does not claim to be the unique cost function satisfying the framework's five conditions; that uniqueness belongs to the continuous function J(x) = (x + 1/x)/2 - 1. The integer cost is a different object: a discrete, non-continuous cost that satisfies symmetry and self-cost zero but does not satisfy the continuous composition law. It is a separate realization, not a competitor to J.

The practical consequence is that the framework admits multiple legitimate cost structures. The integer cost gives a discrete, computable ledger on the integers, while the continuous cost gives the unique smooth structure. Both are proved internally consistent, and both feed into the framework's arithmetic constructions. A reader should see intCost as one working example of a recognition cost, not as the definition of what recognition cost must be.

@[simp] theorem intCost_self (a : ℤ) : intCost a a = 0 := by
  simp [intCost]

theorem intCost_symm (a b : ℤ) : intCost a b = intCost b a := by
  by_cases h : a = b
  · subst h
    simp [intCost]
  · have h' : b ≠ a := by intro hb; exact h hb.symm
    simp [intCost, h, h']

/-- Strict ordered integer realization. -/
def strictOrderedRealization : StrictLogicRealization where
  Carrier := ℤ
  Cost := Nat
  zeroCost := inferInstance
  compare := intCost
  compose := fun a b => a + b
  one := 0
  generator := 1
  identity_law := intCost_self
  non_contradiction_law := intCost_symm
  excluded_middle_law := True
  composition_law := True
  invariance_law := True
  nontrivial_law := by
    simp [intCost]

What this page does not claim

The integer cost function is not the unique cost satisfying the framework's five conditions. The integer cost does not satisfy the continuous composition law that forces J. The equivalence between the strict ordered realization and natural numbers is not proved in this pack.

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/UniversalForcing/Strict/Ordered.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: