Foundation Universal Forcing Strict Modular

Strict modular realization

Modular arithmetic is the mathematics of clocks and calendars: after 12 comes 1, after December comes January. The integers mod n, written ZMod n, keep only the remainders when you divide by n, so for n = 12 the numbers 13 and 1 are the same position. The modulus n is the number of distinct positions on the cycle.

In Recognition Science, recognition means telling two states apart, and cost is the price the framework assigns to that act. The strict modular realization defines the simplest possible cost on ZMod n: cost 0 when the two positions are identical, cost 1 when they differ. The framework proves this cost is symmetric, meaning the price of telling a from b equals the price of telling b from a, and that comparing a position with itself costs nothing. This is the discrete ledger of recognition events: a record where every distinction is equally expensive, and no distinction costs more than one unit.

The central result is that this finite, periodic carrier still produces the same forced arithmetic as the infinite natural numbers. The framework constructs a strict modular realization, a model of its logic where the underlying states are the residues mod n, and then proves that the arithmetic derived from this model is equivalent to the standard natural numbers. In plain terms: a clock face with n hours can simulate the full number line for the purposes of the framework's forced arithmetic, as long as n is greater than 1.

This matters because it shows the framework's arithmetic is stable: it does not secretly depend on having an infinite set of states. The same laws that force the cost function J(x) = (x + 1/x)/2 - 1 and its consequences hold when the carrier is a finite cycle. The equivalence is a proved theorem in the machine-checked library of formal theorems, not a heuristic or a numerical accident.

def zmodCost {n : ℕ} (a b : ZMod n) : Nat :=
  if a = b then 0 else 1

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

def strictModular_arith_equiv_logicNat (n : ℕ) [Fact (1 < n)] :
    (StrictLogicRealization.arith (strictModularRealization n)).peano.carrier
      ≃ ArithmeticFromLogic.LogicNat :=
  (StrictLogicRealization.toLightweight (strictModularRealization n)).orbitEquivLogicNat

What this page does not claim

The strict modular realization does not prove that modular arithmetic is the only possible carrier. This module does not derive the cost function J(x) or any of the framework's physical constants. The equivalence to natural numbers does not mean the framework's arithmetic is classical; it means the derived arithmetic matches the natural numbers.

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