AcousticPhenomenon
plain-language theorem explainer
AcousticPhenomenon enumerates the five canonical wave phenomena as an inductive type. Researchers deriving acoustics from the Recognition Science forcing chain cite this enumeration when establishing configDim D = 5 or certifying DFT-8 structures. The definition is a direct inductive construction that automatically derives finite cardinality, decidable equality, and related instances.
Claim. Let $A$ be the inductive type whose constructors are the five elements reflection, refraction, diffraction, absorption, and interference, equipped with decidable equality and finite type structure.
background
The Acoustics from RS module (B10 / RS_PAT_026) identifies the five canonical acoustic phenomena with configuration dimension D = 5. This matches the eight DFT modes generated by the 2^3 octave structure, yielding a phi-harmonic sound therapy framework whose fundamental frequency is 5φ Hz in the theta band and whose overtones follow the series 5φ, 10φ, 15φ, … . The module states that Lean encodes these facts with zero sorry or axiom.
proof idea
The declaration is a direct inductive definition listing the five constructors, followed by automatic derivation of DecidableEq, Repr, BEq, and Fintype instances. No manual tactics or lemmas are invoked.
why it matters
This inductive type supplies the five phenomena required by the downstream cardinality theorem acousticPhenomenonCount and the certification structure AcousticsCert. It realizes the RS_PAT_026 claim that five phenomena equal configDim D = 5, connecting to the eight-tick octave (T7) and the spatial dimension D = 3 (T8) of the UnifiedForcingChain. The construction anchors the phi-ladder frequency assignments used in precision sound therapy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.