Foundation Universal Forcing Strict Categorical Logic Nat Cost

The discrete cost

In mathematics, a cost function assigns a number to a pair of objects, often measuring how far apart they are. The declaration logicNatCost defines the simplest meaningful cost on the natural numbers: it charges 0 when the two numbers are the same, and 1 when they are different. This is the discrete metric, the mathematical object that treats every distinct pair of numbers as equally distant.

The declaration appears within the Recognition Science framework as part of a strict categorical realization. It uses the canonical ledger, a discrete record of events, as its carrier. The framework proves two properties of this cost: it is symmetric, meaning the cost from a to b equals the cost from b to a, and it charges zero exactly when the two entries are identical. These are the defining features of a metric that recognizes only equality and difference, with no gradation in between.

In Recognition Science, the cost of recognition is forced, not chosen. The framework's central theorem shows that any cost function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1, a continuous function with a unique minimum at x = 1. The declaration logicNatCost serves a different role: it is the discrete, categorical hook that realizes the recognition structure on the natural numbers themselves. It does not derive the continuous cost J; it provides a separate, simpler object that the framework can use as a building block.

The machine-checked library of formal theorems proves the symmetry and self-cost properties of logicNatCost from its definition alone. These proofs are complete and axiom-clean. What the declaration does not claim is any connection to the golden ratio, the eight-tick cycle, or the forcing of three spatial dimensions. Those results flow from the continuous cost function J, not from this discrete metric. The declaration is a categorical realization hook, a piece of infrastructure, not a source of physical constants.

def logicNatCost (a b : LogicNat) : Nat :=
  if a = b then 0 else 1

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

@[simp] theorem logicNatCost_self (a : LogicNat) : logicNatCost a a = 0 := by
  simp [logicNatCost]

What this page does not claim

The declaration does not derive the continuous cost function J or any physical constants. The discrete cost does not force the golden ratio, the eight-tick cycle, or three spatial dimensions. The cost function is not claimed to be the unique cost satisfying the five conditions; that is a separate theorem about J.

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/Categorical.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: