rung_ordering
plain-language theorem explainer
The rung ordering theorem asserts that the predicted recognition rungs for four LIGO events satisfy GW170817 at rung 1 less than GW230529 at rung 2 less than GW150914 at rung 8 less than GW190521 at rung 10. Gravitational-wave analysts and Recognition Science modelers cite it to confirm mass-scaled assignments in the black-hole echo catalog. The proof is a one-line wrapper that splits the conjunction via refine and discharges each inequality by decide.
Claim. Let $r$ map each headline event to its predicted recognition rung via logarithmic mass scaling. Then $r$(GW170817) $<$ $r$(GW230529) $∧$ $r$(GW230529) $<$ $r$(GW150914) $∧$ $r$(GW150914) $<$ $r$(GW190521).
background
The module records per-event black-hole echo predictions for four canonical LIGO/Virgo events, giving source mass, recognition rung $N$, echo delay $Δt(N)$, and frequency $f_{echo}(N) = 1/Δt(N)$ in RS-native units. The rung function is defined by concrete values obtained from log-mass scaling: rung $N ≈ ⌊log_φ(M/M_{ref})⌋$, producing rung 1 for GW170817, rung 2 for GW230529, rung 8 for GW150914, and rung 10 for GW190521. This setting extends the generic bounce-radius and echo-delay scaling supplied by the structural BH-echo certificate in the sibling BHEchoesLIGOCatalog module.
proof idea
The proof is a one-line wrapper. It applies refine to split the three-way conjunction into separate goals, then discharges each goal by decide on the explicit numerical comparisons supplied by the predictedRung definition.
why it matters
The theorem supplies the rung ordering required by bhEchoCatalogCert, which in turn populates the master certificates in AnimalZComplexityBound and MasteryThresholdFromGap45. It completes the per-event ladder in the gravity catalog, allowing falsification by any high-SNR event whose echo signature fails to appear at the predicted rung. The ordering follows the same strict monotonicity pattern used for z-rungs and mastery thresholds, consistent with the phi-ladder and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.