event_count
plain-language theorem explainer
The theorem establishes that the finite set of headline LIGO/Virgo events used for black-hole echo predictions contains exactly four members. Gravitational-wave analysts would cite the result to confirm catalog completeness before applying rung-based delay and frequency formulas. The proof is a one-line decision procedure that evaluates the Fintype cardinality directly from the inductive enumeration of the four events.
Claim. $|S|=4$ where $S=$$${GW150914, GW170817, GW190521, GW230529}$$$ is the set of canonical headline events.
background
The module records per-event black-hole echo predictions for the four headline LIGO/Virgo events, supplying bounce-radius and echo-delay scalings in Recognition Science native units. HeadlineEvent is the inductive type that enumerates precisely these four events, each carrying an assigned recognition rung obtained from log-mass scaling. The Fintype instance derived from the inductive definition supplies the cardinality. The local setting fixes the catalog size before the positivity and ordering properties of the predictions are certified.
proof idea
The proof is a term-mode application of the decide tactic to the goal Fintype.card HeadlineEvent = 4. The tactic reduces the statement using the Fintype instance that is automatically generated for the four-constructor inductive type HeadlineEvent.
why it matters
The result supplies the event_count field of the BHEchoCatalogCert structure that certifies the complete per-event echo catalog. It anchors the set of test cases against which rung ordering and positivity of delays and frequencies are verified. In the Recognition framework the fixed count of four events supports the gravity-sector predictions that employ the phi-ladder and adjacent-rung frequency ratios of 1/phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.