echoParameterCount
plain-language theorem explainer
The finite type of echo parameters in the RS gravitational wave model has cardinality exactly five. A researcher constructing the echo certification would cite this to fix the dimension of the parameter space at configDim D = 5. The proof is a one-line wrapper that applies the decide tactic to the Fintype.card computation on the inductive type.
Claim. Let $E$ be the finite type whose elements are the five labels delay, amplitude, frequency, phase, and quality. Then $|E| = 5$.
background
The module defines the gravitational wave echo model with delay $2 r_{min} log phi$ and amplitude decay $phi^{-k}$ per echo. EchoParameter is the inductive type with constructors delay, amplitude, frequency, phase, quality, each deriving Fintype so that its cardinality is computable. The local setting states that these five parameters equal configDim D = 5.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the equality Fintype.card EchoParameter = 5.
why it matters
This supplies the five_params field inside the gwEchoCert definition, confirming that the echo parameter space has dimension 5. It fills the enumeration step required by the RS strong-field depth construction for gravitational wave echoes. The result anchors the claim that five parameters match configDim D = 5 before amplitude decay and delay positivity are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.