Pith. sign in
module module moderate

IndisputableMonolith.Verification.GWTC3RingdownSharedRunner

show as:
view Lean formalization →

Certifies a single shared runner for the GWTC-3 ringdown guarded family scripts after refactor: presence, mapping counts, and post-refactor smoke tests all pass. Verification and Track-6 auditors cite it as the one-statement structural seal on the shared-runner layout. The argument is a thin certificate packing boolean and count equalities already proved in the guarded-family scripts module.

claimThere is a shared GWTC-3 ringdown runner such that the refactored family-script count equals the guarded-family count, the supported mapping count is positive, and every post-refactor smoke test passes. The module packages these facts as one inhabited certificate.

background

GWTC-3 ringdown verification in this codebase is organized as a family of statistic scripts under a runtime family guard. The upstream module GWTC3RingdownGuardedFamilyScripts records Session 133: that guard is wired into the mapped family-statistic scripts, with structural status (zero sorry, zero RS-internal axiom).

This module sits one layer above that wiring. It does not re-derive the guard; it records that the scripts now share a single runner, that the refactored script count matches the guarded count, that supported mappings are nonempty, and that a fixed smoke suite still passes after the refactor.

The local setting is pure verification bookkeeping inside the Recognition Science monolith: no new physics constants, no mass-ladder or J-cost claims. The objects are presence flags, natural-number counts, and a certificate type inhabiting those equalities.

proof idea

Definition-and-certificate module, not a deep proof development. Boolean and count witnesses (sharedRunnerPresent, refactoredFamilyScriptCount, supportedMappingCount, smoke pass flags) are stated, then closed by short theorems equating the refactored count to the guarded count, asserting positivity of the mapping count, and asserting that all post-refactor smoke tests passed. Those facts are bundled into GWTC3RingdownSharedRunnerCert with an inhabitation lemma. No tactic-heavy reasoning; the work is structural packaging of upstream Session-133 results.

why it matters in Recognition Science

Gives Track 6 a single importable seal that the GWTC-3 ringdown family runs through one shared runner after the guarded-script refactor. Downstream, Track6FalsifierSensitivity imports this module as part of the Fork F integration endpoint for Track 6 of the Quantum Gravity Discovery Master Plan (structural theorem, no placeholders, no new RS-internal assumptions).

Without this certificate, falsifier-sensitivity claims would have to re-open the runner layout and smoke suite. With it, sensitivity analysis can treat the shared-runner configuration as closed infrastructure. It does not itself compute ringdown residuals or RS mass predictions; it only locks the execution path those checks ride on.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (13)