acousticPhenomenonCount
plain-language theorem explainer
The theorem fixes the cardinality of the acoustic phenomena type at five, matching the configuration dimension in the RS acoustics derivation. Researchers deriving wave phenomena from the Recognition Science forcing chain cite it to anchor the five-element phenomenon space. The proof is a direct decision on the Fintype instance generated by the five-constructor inductive definition.
Claim. The set of acoustic phenomena has cardinality five: $|$ {reflection, refraction, diffraction, absorption, interference} $| = 5$.
background
The AcousticsFromRS module identifies five canonical acoustic phenomena with configuration dimension D equal to five, as part of the RS_PAT_026 claim on precision sound therapy via DFT-8 modes. The inductive type AcousticPhenomenon enumerates exactly those five cases and derives the required Fintype, DecidableEq, and Repr instances. Upstream, the modes definition supplies the finite set of truncated 2D Galerkin modes whose count is 2^3.
proof idea
One-line wrapper that applies the decide tactic. The tactic evaluates Fintype.card on the inductive type whose five constructors yield an automatic Fintype instance, confirming the equality by exhaustive enumeration.
why it matters
The result supplies the five_phenomena field inside the acousticsCert definition, closing the module's certification of the acoustics framework. It realizes the claim that five phenomena equal configDim D = 5 and aligns with the eight-tick octave (T7) and the DFT-8 envelope for phi-harmonic sound therapy. The proof is complete with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.