Foundation Universal Forcing Strict Modular Zmod Cost

The modular cost

In mathematics, a modular arithmetic system is like a clock: after reaching the modulus n, the numbers wrap around. The declaration zmodCost defines a cost function on such a system. For any two elements a and b, the cost is 0 if they are the same, and 1 if they are different. It is the simplest possible way to measure whether two positions on a clock face agree.

Two properties of this cost function are proved as theorems. First, the cost of comparing an element with itself is always 0. Second, the cost is symmetric: the cost of comparing a to b equals the cost of comparing b to a. These are the only two theorems stated for zmodCost in the source file. The definition itself is a model, a chosen way to represent recognition within the framework, not a derived result.

The cost function is used to build a strictModularRealization, a structure that connects this modular system to the framework's broader logical machinery. The carrier interpretation is periodic, meaning the system treats numbers that differ by the modulus as equivalent. But the forced arithmetic, the operations that the framework derives, remains the free orbit, not the modular one. The modular cost governs only the recognition of sameness or difference.

What zmodCost does not claim is important. It does not claim to be the unique cost function forced by the framework's axioms. It does not derive the golden ratio, the eight-tick cycle, or any of the framework's larger constants. It is a local, definitional choice for a specific modular setting, with two elementary theorems about its behavior. The declaration establishes a small, precise fact: on a clock face, sameness costs nothing and difference costs one.

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

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

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

/-- Strict modular realization for moduli `n > 1`. -/
def strictModularRealization (n : ℕ) [Fact (1 < n)] : StrictLogicRealization where
  Carrier := ZMod n
  Cost := Nat
  zeroCost := inferInstance
  compare := zmodCost
  compose := fun a b => a + b
  one := 0
  generator := 1
  identity_law := zmodCost_self
  non_contradiction_law := zmodCost_symm
  excluded_middle_law := True
  composition_law := True
  invariance_law := True
  nontrivial_law := by
    have hne : (1 : ZMod n) ≠ 0 := by
      intro h
      have hval := congrArg ZMod.val h
      rw [ZMod.val_one n, ZMod.val_zero] at hval
      norm_num at hval
    simp [zmodCost, hne]

What this page does not claim

This answer does not claim zmodCost is the unique cost function forced by the framework. This answer does not claim the modular cost derives the golden ratio or any other framework constant. This answer does not claim the modular cost function is a theorem rather than a definitional choice.

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: