Foundation Modular Logic Realization Modular Interpret Periodic

Periodic carriers

In mathematics, a periodic function repeats its values at regular intervals, like the hours on a clock face. The declaration modular_interpret_periodic establishes a precise, machine-checked statement about a particular way of building such a repeating structure inside Recognition Science. It shows that the framework's universal forcing construction can be realized on a finite, cyclic carrier, one that wraps around like a clock, without losing the arithmetic that lives underneath.

The construction works by taking the free, unbounded natural numbers and mapping them onto a finite set of size k + 2, using the remainder after division. This is the familiar idea of modular arithmetic, where 0, 1, 2, 3, 4, 5, 0, 1, 2, 3 repeats forever. The theorem states that this mapping is periodic: adding the modulus (the size of the finite set) to any natural number leaves its image unchanged. The successor operation on the natural numbers becomes a simple step around the finite cycle, and the whole structure satisfies the same laws as the unbounded one.

In Recognition Science, the framework models reality as maintaining a discrete record of recognition events, and its universal forcing chain derives structures from a single cost function. This declaration shows that the framework's logic does not demand that every realization faithfully embed arithmetic into its carrier. The carrier can be finite and periodic, while the internal orbit of logic remains free and unbounded. The theorem modular_arithmetic_invariant makes this precise: the arithmetic extracted from the modular realization is equivalent to that of any other realization, so the periodic carrier does not change what arithmetic the framework sees.

What the declaration does not claim is more limited than what it does. It does not claim that the finite carrier itself is the natural numbers, only that it interprets them periodically. It does not claim that the periodic interpretation is the only possible realization, nor that it is preferred over others. It establishes a possibility result: the framework can run on a finite clock face, and the arithmetic it extracts remains invariant. The consequence is that Recognition Science does not tie its logic to the size or structure of the carrier it uses; the logic is what it is, regardless of how it is realized.

/-- The modular interpretation is periodic on the carrier. -/
theorem modular_interpret_periodic (k : ℕ) (n : ArithmeticFromLogic.LogicNat) :
    modularInterpret k
        (ArithmeticFromLogic.LogicNat.fromNat
          (ArithmeticFromLogic.LogicNat.toNat n + modulus k))
      = modularInterpret k n := by
  apply Fin.ext
  simp [modularInterpret, ArithmeticFromLogic.LogicNat.toNat_fromNat]

/-- Modular realization has invariant extracted arithmetic. -/
noncomputable def modular_arithmetic_invariant (k : ℕ) (R : LogicRealization.{0, 0}) :
    (UniversalForcing.arithmeticOf (modularRealization k)).peano.carrier
      ≃ (UniversalForcing.arithmeticOf R).peano.carrier :=
  ArithmeticOf.equivOfInitial
    (UniversalForcing.arithmeticOf (modularRealization k))
    (UniversalForcing.arithmeticOf R)

What this page does not claim

The finite carrier is not the natural numbers themselves, only an interpretation of them. The periodic realization is not claimed to be unique or preferred over other realizations. The declaration does not establish that Recognition Science requires finite carriers, only that it permits them.

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