Pith. sign in
module module moderate

IndisputableMonolith.Verification.GWTC3RingdownSharedRunner

show as:
view Lean formalization →

Certification module for the GWTC-3 ringdown shared-runner refactor: family-statistic scripts now route through one common runner after the guarded-family wiring. Verification auditors cite it to confirm runner presence, mapping counts, and post-refactor smoke passes in a single certificate. The argument is structural bookkeeping: Nat equalities and Boolean smoke flags assembled into one inhabited cert record.

claimThere is a shared-runner certificate for the GWTC-3 ringdown family scripts: the shared runner is present, the refactored family-script count equals the guarded-family count, the supported-mapping count is positive, and every post-refactor smoke test passes. These facts are packaged as one inhabited certificate object.

background

This module sits in the Verification domain of the Recognition Science mirror. Upstream, GWTC3RingdownGuardedFamilyScripts records Session 133: the runtime family guard is wired into the mapped family-statistic scripts as a structural theorem (zero sorry, zero RS-internal axioms).

The shared-runner layer is the next housekeeping step. After the guard wiring, the family scripts are refactored so they invoke one common runner rather than duplicated entry points. Sibling definitions track four observables: whether that runner is present, how many family scripts were refactored, how many supported mappings exist, and whether the post-refactor smoke suite still passes.

The local theoretical setting is empirical-pipeline integrity for GWTC-3 ringdown statistics, not a new physical law. The module only asserts that the refactor preserved the guarded-script surface and that the smoke suite remains green.

proof idea

Structural certificate assembly, not a deep derivation. Boolean and Nat witnesses (sharedRunnerPresent, refactoredFamilyScriptCount, supportedMappingCount, smokeTestsAfterRefactor / smokePassesAfterRefactor) are checked by short equalities and positivity lemmas: runner present, refactored count matches the guarded count, supported mapping count is positive, and all smoke tests pass after the refactor. Those facts are bundled into GWTC3RingdownSharedRunnerCert and discharged by an inhabitedness instance (gwtc3RingdownSharedRunnerCert_inhabited). One-statement surface theorem exposes the cert to downstream importers.

why it matters in Recognition Science

Feeds Track6FalsifierSensitivity, the Fork F integration endpoint for Track 6 of the Quantum Gravity Discovery Master Plan. That downstream module is itself a structural theorem with no placeholder proofs and no new RS-internal assumptions; it needs a clean shared-runner surface so falsifier-sensitivity checks run against one runner rather than a scatter of pre-refactor scripts.

In the broader verification chain, this closes the Session-133 refactor loop: guarded family scripts plus shared runner plus green smoke equals a single cert that Track 6 can import without re-auditing entry points. It does not advance the T0–T8 forcing chain or the mass ladder; it hardens the GWTC-3 ringdown empirical track so later sensitivity claims rest on a stable runner contract.

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)