gravitationalWaveCert
plain-language theorem explainer
The declaration constructs a concrete GravitationalWaveCert by populating its two fields with pre-established results on source cardinality and strain ratios. Astrophysicists modeling binary merger signals under the Recognition Science phi-ladder would cite this to fix the amplitude decay across mass classes. The definition succeeds by direct record construction that substitutes the decidable count theorem and the algebraic ratio identity.
Claim. Let GWSourceCategory be the set of five canonical gravitational wave source types. The certificate asserts that its cardinality equals 5 and that strainAtRung(k+1) / strainAtRung(k) = phi for every natural number k.
background
The module treats gravitational wave strain in binary mergers as following a phi-decay law across mass-class rungs, with five source categories (NS-NS, BH-NS, BH-BH, SMBH, stochastic) matching configDim = 5. StrainAtRung encodes the peak amplitude scaling with mass rung, and the ratio between adjacent rungs is required to equal the golden ratio phi. The GravitationalWaveCert structure packages exactly these two properties as a record whose fields must be supplied by theorems.
proof idea
The definition builds the GravitationalWaveCert record by direct field assignment: five_categories receives the theorem gwSourceCount and phi_ratio receives the theorem strainRatio. No additional tactics or reductions occur beyond these substitutions.
why it matters
This supplies the explicit phi-ladder data for gravitational wave amplitudes, anchoring the RS prediction that adjacent source classes differ in peak strain by phi. It closes the interface between the J-cost framework and astrophysical observables, though no downstream theorems yet consume the certificate. The construction aligns with the five-category count already proved by enumeration in the sibling gwSourceCount.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.