Foundation Universal Forcing Modular Realization

Modular realization

Modular arithmetic is the mathematics of clocks and calendars: after 12 comes 1 again, and 23:59 is one minute before 00:00. In Recognition Science, the framework studies what happens when a ledger, a discrete record of events, is forced to close on itself. The modular realization is the simplest such closed carrier: take the finite set of residues ZMod n, and define the cost of recognizing two elements as 0 when they are equal and 1 otherwise. This equality cost is symmetric, and it costs nothing to recognize an element as itself, two properties the framework's theorems verify.

The framework's machine-checked library of formal theorems proves that this finite modular structure carries the same arithmetic as the natural numbers. The key construction interprets each counting number by its residue modulo n, then builds a realization of the framework's logical arithmetic on this finite carrier. A theorem named modular_arithmetic_invariant shows that the arithmetic forced by this modular realization is isomorphic to the arithmetic of any other realization. In plain terms, the forced arithmetic is universal: whether the carrier is infinite or finite, the same arithmetic structure emerges, and the finite clock face does not lose any of the forced content.

This matters because it shows the forcing chain does not depend on having an infinite set of objects. The framework's central results, including the uniqueness of the cost function J(x) = (x + 1/x)/2 - 1, are about what any cost function satisfying five plain conditions must be. The modular realization demonstrates that the universal iteration object, the arithmetic that any such ledger must support, can be realized on a finite cyclic carrier. The theorem is a MODEL-level definitional choice: the framework chooses to model the carrier as ZMod n with equality cost, then proves the invariance result about that choice.

One consequence is that the framework's arithmetic is stable across carriers of different sizes. A reader might worry that the forced arithmetic depends on having infinitely many objects to count. The modular realization closes that worry: even a finite clock face, with its wrap-around behavior, supports the same forced arithmetic as the full counting numbers. The framework's library certifies this invariance, so the universality claim holds across carriers of any size.

theorem zmodCost_symm {n : ℕ} (a b : ZMod n) : zmodCost a b = zmodCost b a := by
  by_cases h : a = b
  · subst h; simp [zmodCost]
  · have h' : b ≠ a := by intro hb; exact h hb.symm
    simp [zmodCost, h, h']

@[simp] theorem zmodCost_self {n : ℕ} (a : ZMod n) : zmodCost a a = 0 := by
  simp [zmodCost]

/-- Modular realization carries the universal forced arithmetic. -/
noncomputable def modular_arithmetic_invariant (n : ℕ) [Fact (1 < n)]
    (R : LogicRealization.{0, 0}) :
    (arithmeticOf (modularRealization n)).peano.carrier
      ≃ (arithmeticOf R).peano.carrier :=
  ArithmeticOf.equivOfInitial (arithmeticOf (modularRealization n)) (arithmeticOf R)

What this page does not claim

The modular realization does not prove the uniqueness of the cost function J; that is a separate theorem. The finite carrier does not replace the infinite natural numbers in any derivation; it only shows the arithmetic is invariant. The modular realization does not claim that physical recognition events actually occur on a finite clock face.

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