Foundation Universal Forcing Strict Music

A musical ledger

Music, at its most basic, is organized sound. The organization often comes from frequency ratios: the octave is a ratio of 2:1, a perfect fifth is 3:2, a perfect fourth is 4:3. These ratios are not arbitrary; they have been the backbone of tuning systems for centuries, from Pythagorean tuning to just intonation. In the Recognition Science framework, these ratios become the atoms of a particular kind of ledger.

A ledger, in this framework, is a discrete record of events. The events here are notes, and each note is identified by its positive frequency ratio. The framework then asks a stark question: what does it cost to recognize one note as the same as another? The answer in this strict pass is brutally simple: the cost is 0 if the ratios are identical, and 1 if they are not. This is an equality-cost, a binary test of sameness. It is the most austere possible measure, ignoring all psychoacoustic nuance about consonance or dissonance. The module defines this cost function and proves it is symmetric: the cost of comparing A to B is always the same as comparing B to A.

With this cost in place, the module constructs a full musical realization. It designates the octave as the canonical generator, the basic step from which other intervals can be stacked. The perfect fifth and perfect fourth are defined as specific ratios. This realization is not a vague analogy; it is a formal structure that plugs into the framework's larger logical machinery. The module proves that this musical structure is a sub-realization of the positive ratio space, meaning it is a consistent slice of a larger formal system.

The most consequential step is the final one. The module shows that the arithmetic of this musical ledger is equivalent to the arithmetic of the natural numbers. In plain terms, the structure of counting notes by octave stacking is, in a precise formal sense, the same as the structure of counting 1, 2, 3, and so on. This is a bridge from the world of sound to the world of number, built on nothing more than a binary cost and a choice of generator. It demonstrates that a musical scale, under this strict lens, is not just a cultural artifact but a carrier of fundamental arithmetic structure.

noncomputable def ratioCost (a b : FrequencyRatio) : Nat :=
  if a = b then 0 else 1

theorem ratioCost_symm (a b : FrequencyRatio) : ratioCost a b = ratioCost b a := by
  by_cases h : a = b
  · subst h
    simp [ratioCost]
  · have h' : b ≠ a := by intro hb; exact h hb.symm
    simp [ratioCost, h, h']

noncomputable def music_arith_equiv_logicNat :
    (StrictLogicRealization.arith strictMusicRealization).peano.carrier
      ≃ ArithmeticFromLogic.LogicNat :=
  (StrictLogicRealization.toLightweight strictMusicRealization).orbitEquivLogicNat

What this page does not claim

This module does not model consonance, dissonance, or any psychoacoustic preference. The equivalence to natural number arithmetic does not claim that music is 'just' counting. No claim is made here about the origin of musical scales in human culture or biology.

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