Physics Acoustics From Rs Acoustic Phenomenon Count

The five canonical phenomena

Classical acoustics organizes the behavior of sound into a small set of canonical phenomena. The standard list has five entries: reflection, refraction, diffraction, absorption, and interference. Reflection sends a wave back from a surface, refraction bends it when it enters a new medium, diffraction spreads it around an obstacle, absorption removes energy from it, and interference combines two waves into a stronger or weaker result. These five are the usual working inventory of an acoustics textbook.

The Recognition Science framework models this inventory as a finite set. Its machine-checked library of formal theorems defines an inductive type named AcousticPhenomenon whose five constructors are exactly reflection, refraction, diffraction, absorption, and interference. The library then proves a counting theorem: the number of distinct phenomena in this set is 5. The proof runs by deciding the finite cases, with no unfinished proof obligations and no added axioms. The theorem establishes a clean fact: the five-item list is closed and complete within the framework's model.

The same library file links this count to a separate structure. A definition sets the number of DFT modes, the discrete frequency components in an eight-point transform, to 2³ = 8. A second theorem proves that this definition equals 8. A certificate structure bundles both facts, the five phenomena and the eight modes, into a single object. The framework's sound therapy account uses these eight modes to target frequency envelopes in the theta band, with a fundamental frequency of 5φ Hz ≈ 8.09 Hz and an overtone series at integer multiples of that base.

The count does not claim that these five phenomena are the only acoustic effects in nature. It claims that the framework's formal model has exactly five canonical entries. The theorem does not derive the physical laws of reflection or interference, does not assign numerical values to absorption coefficients, and does not prove that the eight DFT modes cause any therapeutic outcome. The eight-mode link to sound therapy is a framework-internal identification, not a measured physiological claim. What the theorem establishes is precise and narrow: within the framework's definition, the canonical acoustic list has exactly five members.

inductive AcousticPhenomenon where
  | reflection | refraction | diffraction | absorption | interference
  deriving DecidableEq, Repr, BEq, Fintype

theorem acousticPhenomenonCount : Fintype.card AcousticPhenomenon = 5 := by decide

/-- DFT-8 modes = 2^3. -/
def dftModes : ℕ := 2 ^ 3

theorem dftModes_8 : dftModes = 8 := by decide

What this page does not claim

The theorem does not prove that reflection, refraction, diffraction, absorption, and interference are the only acoustic effects in nature. The eight DFT modes are not shown to cause any physiological or therapeutic outcome. No physical law of acoustics is derived from the counting theorem.

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/Physics/AcousticsFromRS.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: