predictedRung
plain-language theorem explainer
predictedRung maps each of the four headline LIGO events to an integer recognition rung chosen to match observed source mass via log-base-phi scaling on the phi-ladder. Gravitational-wave researchers checking black-hole echo signatures would cite these assignments when comparing predicted delays against catalog data. The definition is realized by exhaustive pattern matching on the HeadlineEvent inductive type.
Claim. The function mapping headline events to recognition rungs is defined by cases: GW150914 maps to 8, GW170817 maps to 1, GW190521 maps to 10, and GW230529 maps to 2.
background
The BHEchoPerEventCatalog module records per-event black-hole echo predictions for four canonical LIGO/Virgo events inside the Recognition Science framework. HeadlineEvent is the inductive type whose constructors are exactly GW150914, GW170817, GW190521, and GW230529, each tied to an approximate source mass in solar units. Rung numbers are selected so the mass formula (yardstick times phi to the power rung minus 8 plus gap) reproduces the observed masses, as listed in the module table with GW150914 at rung 8 for mass near 65 solar masses and similarly for the remaining events.
proof idea
The definition is implemented by direct pattern matching on the four constructors of HeadlineEvent, returning the pre-assigned natural number in each case. No lemmas or tactics are applied beyond the built-in case distinction.
why it matters
It supplies the rung values required by predictedBounceRadius and predictedEchoDelay, which populate the BHEchoCatalogCert structure that certifies positivity of delays and frequencies together with rung ordering. The assignments realize the per-event table in the module documentation and connect LIGO masses to the phi-ladder used in Recognition Science mass formulas. Downstream rung_ordering confirms the size hierarchy among the four events using exactly these values. It supports tests of phi-ladder scaling central to the T6 fixed-point step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.