GravitationalWaveCert
plain-language theorem explainer
GravitationalWaveCert is a structure that certifies exactly five gravitational wave source categories and a constant strain ratio of phi between adjacent rungs on the phi-ladder. Astrophysicists applying Recognition Science to binary merger signals would cite it when mapping mass classes to observable amplitudes. The declaration is a bare structure definition with no proof body or lemmas.
Claim. A structure asserting that the set of gravitational wave source categories has cardinality five and that the strain amplitude $s$ at consecutive rungs satisfies $s(k+1)/s(k) = phi$ for all natural numbers $k$, where $s(k) = phi^k$.
background
The module treats gravitational wave strain for binary mergers in Recognition Science terms, with amplitude following a phi-decay law across mass classes. GWSourceCategory is the inductive enumeration of five types: NS-NS, BH-NS, BH-BH, SMBH, and stochastic background. The upstream strainAtRung definition sets the value at rung $k$ to $phi^k$, so the ratio between adjacent rungs is constantly $phi$. This local setting follows from the J-cost function and the self-similar fixed point.
proof idea
The declaration is a structure definition that directly records the two certification fields. No lemmas are applied and no tactics are used; the cardinality statement and the universal ratio statement stand as the packaged properties.
why it matters
The structure is instantiated by the downstream gravitationalWaveCert to supply the phi-ladder prediction for GW strains. It connects the T5 J-uniqueness and T6 phi fixed point to astrophysical observables, realizing the module claim that adjacent source classes differ in peak strain by phi and that the source classification has dimension 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.