acousticsCert
plain-language theorem explainer
acousticsCert assembles the AcousticsCert record by feeding the verified count of five acoustic phenomena and the count of eight DFT modes into the two fields of the structure. Researchers modeling RS-derived sound therapy under RS_PAT_026 would cite this record to confirm that the five canonical effects match configDim D = 5 and that the mode count equals 2^3. The definition is a direct record construction that pulls the two values from prior cardinality theorems.
Claim. The acoustics certificate is the structure asserting that the cardinality of the set of acoustic phenomena equals 5 and that the number of discrete Fourier transform modes equals 8.
background
The module AcousticsFromRS encodes five canonical acoustic phenomena (reflection, refraction, diffraction, absorption, interference) as the finite type AcousticPhenomenon whose cardinality is fixed at 5, matching configDim D = 5. It further identifies the eight DFT modes with the 2^3 octave structure. The upstream theorem acousticPhenomenonCount proves the cardinality equals 5 by exhaustive decision, while dftModes_8 proves the mode count equals 8 by the same method; both results are quoted directly in the AcousticsCert structure definition.
proof idea
This is a one-line wrapper that applies acousticPhenomenonCount to the five_phenomena field and dftModes_8 to the eight_modes field of the AcousticsCert structure.
why it matters
The definition realizes the RS_PAT_026 claim that five phenomena equal configDim D = 5 and that eight DFT modes supply the phi-harmonic sound therapy framework with fundamental frequency 5φ Hz. It closes the Lean encoding of the overtone series 5φ, 10φ, 15φ, … and sits at the interface with the eight-tick octave (T7) from the forcing chain, providing a concrete bridge to acoustic applications without new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.