Foundation Universal Forcing Strict Categorical

The strict categorical realization

In mathematics, a natural numbers object (NNO) is a universal way to count: it is a set with a distinguished starting element and a successor operation that, given any other set with a starting point and a next-step map, uniquely determines a function. This is the categorical definition of the natural numbers, and it underlies arithmetic, recursion, and most of computation. The framework's ledger, a discrete record of events with a forced cost structure, needs a concrete carrier to be realized in formal logic.

The module Strict/Categorical.lean provides exactly that carrier. It defines a cost function on the natural numbers: the cost is 0 if two numbers are equal, and 1 otherwise. This is the simplest possible discrete metric, and the module proves it is symmetric, meaning the cost from a to b equals the cost from b to a. It then constructs a strict categorical realization, a formal object that satisfies the framework's requirements for a discrete recognition ledger, using this natural-number carrier.

The key result is an equivalence: the arithmetic structure of this realization is the same as the natural numbers themselves. In plain language, the framework's ledger can be built from the ordinary counting numbers, with no extra assumptions. This is a machine-checked theorem in the framework's library of formal theorems, meaning the proof is verified by a computer and does not rely on any unstated axioms.

What this establishes is that the framework's foundational structure is not exotic: it sits on the same natural numbers that schoolchildren count with. The cost function, the symmetry, and the realization all reduce to familiar arithmetic. This is a sanity check and a bridge: it shows the framework's abstract requirements have at least one concrete, standard model.

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']

/-- Strict categorical realization via the canonical `LogicNat` Peano/NNO hook. -/
def strictCategoricalRealization : StrictLogicRealization where
  Carrier := LogicNat
  Cost := Nat
  zeroCost := inferInstance
  compare := logicNatCost
  compose := fun a b => a + b
  one := LogicNat.zero
  generator := LogicNat.succ LogicNat.zero
  identity_law := logicNatCost_self
  non_contradiction_law := logicNatCost_symm
  excluded_middle_law := True
  composition_law := True
  invariance_law := True
  nontrivial_law := by
    simp [logicNatCost, LogicNat.zero_ne_succ]

def strictCategorical_arith_equiv_logicNat :
    (StrictLogicRealization.arith strictCategoricalRealization).peano.carrier
      ≃ LogicNat :=
  (StrictLogicRealization.toLightweight strictCategoricalRealization).orbitEquivLogicNat

What this page does not claim

This module does not prove the uniqueness of the cost function J(x); it only provides one concrete model. This module does not derive any physical constants or empirical predictions. The natural-number carrier is a definitional choice, not a forced consequence of the framework's axioms.

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: