Foundation Universal Forcing Modular Realization Zmod Cost Symm

The cyclic cost

In mathematics, a cyclic group is like a clock face: after the highest number you wrap back to zero. The declaration zmodCost_symm concerns a very simple way of assigning a cost to any two positions on such a clock. The rule is: if the two positions are the same, the cost is zero; if they differ, the cost is one. This is the cost, a plain number attached to a pair of events, which Recognition Science uses as a primitive measure of how much recognition work a transition requires.

The theorem zmodCost_symm states that this cost is symmetric: the cost of going from position a to position b equals the cost of going from b to a. On a clock face, this is the unremarkable fact that the distance between two numbers does not depend on which direction you measure it. The proof is a short case split: if the positions are equal, both costs are zero; if they differ, both costs are one. The declaration also records the companion fact that the cost of any position with itself is zero.

This symmetry is one of the five plain conditions that, in the framework's central theorem, force the specific cost function J(x) = (x + 1/x)/2 - 1. The cyclic version is a deliberately simplified model: it uses a finite clock face instead of the continuous positive numbers where the main theorem lives. What the lemma establishes is that this finite model satisfies the symmetry requirement. It does not establish that the cyclic cost equals J, nor that the finite model obeys the other four conditions, such as the composition law that ties costs of combined steps together.

The framework's library also shows that this cyclic model carries the same universal arithmetic as any other realization of its logical structure. That is a separate, more substantial claim about the model's role in the forcing chain. The symmetry lemma itself is a small but necessary brick: it certifies that the simplest finite example meets one of the axioms that, in the continuous case, lead to the golden ratio and the eight-tick cycle. What a reader should take away is that symmetry is cheap to satisfy; the hard content of the framework lies in the other conditions.

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 cyclic cost equals the function J(x) = (x + 1/x)/2 - 1. The cyclic model satisfies the composition law or any condition beyond symmetry and self-cost zero. The symmetry lemma alone forces the golden ratio or the eight-tick cycle.

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: