pith. machine review for the scientific record. sign in
def definition def or abbrev high

echoAmplitude

show as:
view Lean formalization →

echoAmplitude defines the amplitude of the k-th gravitational wave echo as the reciprocal of phi to the power k. Researchers modeling black hole echo sequences in the Recognition Science framework cite it for the geometric decay law per reflection. It is supplied as a direct noncomputable definition that assigns the value without invoking lemmas or further reduction.

claimThe amplitude of the gravitational wave echo at reflection number $k$ equals $phi^{-k}$, where $phi$ is the golden ratio.

background

The GravitationalWaveEchoFromRS module treats gravitational wave echoes in strong-field regimes by adding amplitude decay to the existing delay formula. Module documentation states that each successive echo is suppressed by the factor $1/phi$, yielding five canonical parameters (delay, amplitude, frequency, phase, quality) that match configuration dimension D=5. This definition mirrors the upstream echoAmplitude from BHEchoAmplitudes, which sets the value to $phi^{-n}$ for reflection count n.

proof idea

The declaration is a direct definition that sets echoAmplitude k to the multiplicative inverse of phi raised to k. No lemmas are applied and no tactics are used; it functions as a one-line abbreviation relying on the phi constant imported from Constants.

why it matters in Recognition Science

This definition supplies the amplitude component required by BHEchoAmplitudeCert, which certifies positivity for all n, unity at n=0, the one-step ratio phi inverse, and strict decrease. It completes the echo decay law in the RS strong-field model, consistent with the phi-ladder and the five-parameter echo structure. It supports downstream cataloging of amplitudes for headline events.

scope and limits

formal statement (Lean)

  30noncomputable def echoAmplitude (k : ℕ) : ℝ := (phi ^ k)⁻¹

proof body

Definition body.

  31

used by (10)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.