strainAtRung
plain-language theorem explainer
Strain at rung k is defined as phi raised to k. Astrophysicists working with Recognition Science models of binary merger signals cite this to enforce the constant phi ratio between adjacent source classes. The module sets five GW categories whose peak strains scale by successive powers of phi. The declaration is a direct power assignment with no lemmas or computation.
Claim. The gravitational wave strain at rung $k$ is defined by $s(k) := phi^k$.
background
In the module on gravitational wave amplitudes from J-cost, strains follow a phi-decay law across mass-class categories. The module document states that adjacent binary merger classes differ in peak strain by phi, with five canonical categories (NS-NS, BH-NS, BH-BH, SMBH, stochastic) matching configDim D = 5. This definition supplies the explicit functional form used to certify the phi-ratio property.
proof idea
The declaration is a direct definition that sets strainAtRung k to phi^k. No lemmas are applied and the body consists solely of the power expression.
why it matters
This definition supplies the explicit strain values required by the GravitationalWaveCert structure, which asserts both the five source categories and the universal phi ratio between adjacent rungs. It also enables the strainRatio theorem that proves the ratio equals phi for any k. The construction realizes the RS prediction that gravitational wave strains follow the phi-decay law across mass classes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.