EchoParameter
plain-language theorem explainer
The echo parameter enumeration fixes five labels for gravitational wave echoes in the Recognition Science setting: delay, amplitude, frequency, phase, and quality. Modelers of black-hole echoes or RS strong-field signals cite this to set the configuration dimension to 5. The declaration is a plain inductive type that derives Fintype, enabling immediate cardinality results.
Claim. The set of gravitational wave echo parameters consists of the five elements delay, amplitude, frequency, phase, and quality.
background
The Gravitational Wave Echo from RS module treats echoes as characterized by five parameters whose count equals the configuration dimension D = 5. It extends the delay formula Δt = 2 r_min log(φ) by adding amplitude decay of 1/φ per successive echo. Upstream results supply the eight-tick phase kπ/4, the unimodular phase e^{i w}, S-matrix transition amplitudes, and double-slit path amplitudes.
proof idea
The declaration is an inductive definition introducing five constructors and deriving Fintype, DecidableEq, Repr, and BEq. No tactics or lemmas are applied; the Fintype instance is generated automatically by the deriving clause.
why it matters
This enumeration supplies the five parameters required by GWEchoCert for the amplitude decay relation echoAmplitude (k + 1) / echoAmplitude k = phi^{-1} and positive delay. It realizes the configDim D = 5 stated in the module documentation and connects to the eight-tick octave and phi-ladder. The downstream cardinality theorem echoParameterCount follows directly from the Fintype derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.