Foundation Universal Forcing Categorical Realization Categorical Realization

The categorical realization

In mathematics, a categorical realization is a way of showing that a formal system has essentially only one model: any two structures satisfying the same axioms are isomorphic, meaning they are the same up to renaming. The Recognition Science framework uses this idea to connect its own abstract machinery to the familiar numbers we count with. Its library of machine-checked theorems defines a specific object, called categoricalRealization, which packages the framework's universal arithmetic into a single structure.

The declaration itself is a definition, not a theorem. It re-exports a canonical construction already present in the framework, and it names it under the UniversalForcing module tree. The construction uses a Peano object, which is the category-theoretic way of describing the natural numbers: a starting point (zero) and a successor operation that builds each next number. The definition simply says: take the canonical categorical realization and call it categoricalRealization.

What the definition establishes, through a companion equivalence, is that the arithmetic carried by this realization is exactly the arithmetic of the natural numbers. The library proves a bijection between the carrier of the realization's arithmetic and the standard LogicNat type. In plain language: the numbers that the framework's forced arithmetic talks about are the same numbers we use for counting, no more and no less. This is a structural identity result, not a claim about physics or measurement.

In Recognition Science, this matters because the framework derives physical constants and dimensions from a forcing chain that begins with a cost function. The categorical realization anchors that chain: the arithmetic that appears inside the framework is not some exotic alternative arithmetic, but the standard one. It does not, however, claim that the framework derives the natural numbers from nothing, nor that it proves the consistency of arithmetic, nor that it explains why counting works in the physical world. It only identifies the arithmetic structure that the framework uses.

/-- Canonical categorical realization via the `LogicNat` Peano object. -/
def categoricalRealization : LogicRealization :=
  canonicalCategoricalRealization

/-- Categorical realization carries the universal forced arithmetic. -/
noncomputable def categorical_arith_equiv_logicNat :
    (arithmeticOf categoricalRealization).peano.carrier
      ≃ ArithmeticFromLogic.LogicNat :=
  categoricalRealization.orbitEquivLogicNat

What this page does not claim

The definition does not prove that the natural numbers exist or are consistent. It does not claim that Recognition Science derives arithmetic from physical principles. It does not say anything about the physical world or measurements.

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