Pith. sign in
module module high

IndisputableMonolith.Verification.GWTC3RingdownGuardedFamilyScripts

show as:
view Lean formalization →

Bundles the three accepted GWTC-3 ringdown controlled-family damping scripts under the Session-131 runtime family guard, with smoke-test counts and a one-statement certificate. Downstream shared runners import it to run only DS_1mode_10M, Kerr_220_0M, and Kerr_220_10M. Argument is structural: accept the three mapped families, reject a representative blocked script, and check smoke counts.

claimUnder the GWTC-3 ringdown runtime family guard, the three mapped controlled families (DS$_1$mode at $10M$, Kerr $220$ at $0M$, Kerr $220$ at $10M$) are accepted as guarded scripts; a representative non-mapped script is rejected; smoke-test pass count equals test count (all pass). A single certificate packages these facts.

background

GWTC-3 ringdown verification in this stack tracks quasi-normal-mode (QNM) damping statistics on controlled event families, not free-form model shopping. Upstream modules close three concrete families: the first controlled-family scaling of the Session-123 one-member QNM damping statistic (DS$_1$mode, start window $10M$), and two Kerr-$220$ scalings that keep the same mode while switching the ringdown start-time window between $0M$ and $10M$.

The runtime family guard (Session 131) is the selector that accepts only those three mapped model families. This module sits above the three family modules and the guard: it does not re-derive the damping statistics; it records which scripts the guard admits and that a smoke suite over those scripts is clean.

Local setting is verification infrastructure: guarded script counts, smoke pass/fail tallies, and a compact certificate object for downstream runners.

proof idea

Definition-and-certificate module, not a deep analytic proof. It wires the three family modules through the family-guard predicate, exposes count constants (guarded scripts, smoke tests, smoke passes), and proves elementary equalities: guarded count matches the selector, smoke pass count equals test count, and smokeAllPassed. Separate lemmas assert acceptance of each of the three mapped scripts and rejection of a representative blocked script. The top certificate is a one-statement packaging of those facts for import by the shared runner.

why it matters in Recognition Science

Feeds GWTC3RingdownSharedRunner, which "records the refactor that moved controlled-family damping scripts onto a shared guarded runner." Without this bundle, the runner would re-import the three families and the guard ad hoc. In the Recognition verification layer this is the gate that keeps ringdown damping claims inside the Session-131 stratified selector: only DS$_1$mode@$10M$ and the two Kerr-$220$ windows run as guarded scripts. It closes a structural checkpoint (0 sorry, 0 RS-internal axiom per upstream status lines) so later shared-runner theorems can cite a single certificate rather than three separate family modules.

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)