Pith. sign in
module module high

IndisputableMonolith.Verification.GWTC3RingdownGuardedFamilyScripts

show as:
view Lean formalization →

Aggregates the three GWTC-3 ringdown damping-family scripts that the runtime family guard accepts (DS 1-mode at 10M, Kerr 220 at 0M, Kerr 220 at 10M), with smoke counts and a single certificate. Verification authors cite it when wiring guarded scripts into the shared runner. The argument is structural: acceptance lemmas for each allowed script plus rejection of a blocked representative.

claimThe guarded GWTC-3 ringdown script set consists exactly of the three family-mapped damping scripts (DS one-mode start $10M$, Kerr $220$ start $0M$, Kerr $220$ start $10M$). Each is accepted by the runtime family guard; a representative non-mapped script is rejected. Smoke tests pass with pass-count equal to test-count, and a one-statement certificate packages these facts.

background

GWTC-3 ringdown work in this stack studies quasi-normal-mode (QNM) damping statistics on controlled model families rather than ad-hoc single events. Upstream modules close three such families as structural theorems: the DS one-mode family with ringdown start at $10M$, and two Kerr $220$ families differing only by start window ($0M$ vs $10M$).

The runtime family guard (Session 131 selector) admits only those three mapped families. Anything outside that map is blocked at the script boundary. This module sits between those family theorems and the shared guarded runner: it names the accepted scripts, records smoke-test bookkeeping, and exposes a compact certificate object for downstream import.

proof idea

Definitional layer first: counts of guarded scripts and smoke tests, plus boolean aggregates (all-passed, pass-count equals test-count). Then three acceptance lemmas, one per allowed family script, each discharging the guard predicate on that script. A fourth lemma rejects a representative blocked script. Equality lemmas tie the numeric counts to the selector. The module closes with a one-statement certificate bundling the acceptance and smoke facts for the shared runner.

why it matters in Recognition Science

Feeds GWTC3RingdownSharedRunner, which refactors controlled-family damping scripts onto one guarded runner. Without this module the runner would re-import each family and restate guard acceptance inline. In the Recognition verification layer this is infrastructure, not a physics forcing step (not T0–T8): it locks the Session 131 family stratification so only the three closed damping-statistic families can execute under the shared path. The certificate is the stable import surface for that lock.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (15)