Pith. sign in
module module high

IndisputableMonolith.Verification.Track6FalsifierSensitivity

show as:
view Lean formalization →

Inventory module for Track 6 falsifier sensitivity: theorem-grade discriminator sectors (leading-log entropy, echo damping, rung phase), rival-row coverage, dataset attachments, likelihood/status records, and guarded GWTC-3 ringdown families. Gravity and verification authors cite the counts when auditing how much of the §7 falsifier register is instrumented. Structure is definitional lists plus cardinality lemmas over imported Track 6.C/6.D and register modules.

claimThe module records the theorem-grade discriminator sectors $\{$leading-log entropy, echo damping, rung phase$\}$, the covered rival rows of the $4\times 3$ discriminator matrix, falsifier-register rows with named dataset attachments and likelihood/status records, and the guarded GWTC-3 ringdown controlled families together with their mappings, each with an explicit finite cardinality.

background

Track 6 of the quantum-gravity master plan splits strong-field and discriminator work from the §7 falsifier register. Upstream, DiscriminatorMatrix closes Track 6.D as a structural $4$ rivals $\times$ $3$ sectors matrix (status: structural theorem, zero sorry). StrongFieldStructural closes the structural form of Track 6.C. FalsifierRegisterDatasets attaches concrete named datasets and numerical sensitivity records to every §7 register row; FalsifierLikelihoodRegister aggregates the dataset-specific likelihood/status layer (Sessions 107--115). GWTC3RingdownSharedRunner records the refactor of controlled-family damping scripts onto a shared guarded runner.

This module does not re-prove those closures. It names the live theorem-grade sector list (leading-log entropy, echo damping, rung phase) and exposes countable views: which rival rows are covered, which falsifier rows carry dataset attachments or likelihood/status records, and which ringdown families/mappings sit behind the guarded runner. The local setting is verification bookkeeping for sensitivity coverage, not a new dynamical law.

proof idea

Definitional spine plus count lemmas. Sectors, covered rival rows, dataset-attached rows, likelihood/status rows, and guarded ringdown families/mappings are introduced as explicit finite collections (lists or sets) drawn from the imported Track 6.C/6.D and register modules. Companion theorems assert the cardinalities of those collections by direct evaluation or list-length reasoning. No analytic estimates or new physics identities appear; the argument is structural inventory over already-closed upstream modules.

why it matters in Recognition Science

Supplies the Track 6 sensitivity census that MasterTheoremHandoffIntegration imports as part of the Gravity Track 7 fork-handoff receipt. Downstream that integration lane ties parallel forks (1.B stationarity, physical residual/Bianchi, many-body amplitude lift, discrete Page-capacity transfer) to a single handoff surface; without an explicit sector and register-coverage list, Track 6 would not report how much of the discriminator matrix and §7 falsifier register is theorem-grade versus merely named. Lands next to the closed structural theorems of Tracks 6.C and 6.D and the dataset/likelihood register layers, so auditors can quote finite counts rather than prose claims about coverage. Does not itself discharge a master-plan physics proposition; it is the verification ledger those handoffs read.

scope and limits

used by (1)

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

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (17)