Pith. sign in
module module high

IndisputableMonolith.Verification.Track6FalsifierSensitivity

show as:
view Lean formalization →

Inventory module for Track 6 falsifier sensitivity in the quantum-gravity master plan. It lists theorem-grade discriminator sectors (leading-log entropy, echo damping, rung phase), covered rival rows, falsifier rows with dataset and likelihood attachments, and guarded GWTC-3 ringdown families/mappings, plus cardinality theorems. Gravity Track 7 handoff integration imports it as the sensitivity ledger. Argument shape is named lists over imported Track 6.C/6.D and falsifier-register modules, with trivial count proofs.

claimThe module fixes the theorem-grade discriminator sector set $S=\{\text{leading-log entropy},\ \text{echo damping},\ \text{rung phase}\}$, the covered rival rows of the $4\times 3$ discriminator matrix, the falsifier-register rows carrying dataset attachments and likelihood/status records, and the guarded GWTC-3 ringdown family and mapping collections, and records each collection's cardinality.

background

Track 6 of the quantum-gravity master plan is the observational discriminator lane: strong-field structural tests (6.C) and a $4$ rivals $\times$ $3$ sectors discriminator matrix (6.D). The three theorem-grade sectors named here are leading-log entropy, echo damping, and rung phase. Upstream, DiscriminatorMatrix and StrongFieldStructural close those structural theorems with zero sorry and no RS-internal axioms.

Separately, the §7 falsifier register attaches concrete datasets and numerical sensitivity records (FalsifierRegisterDatasets) and a likelihood/status layer over Sessions 107--115 (FalsifierLikelihoodRegister). GWTC-3 ringdown work is factored through a shared guarded-family runner so controlled damping scripts share one interface.

This module sits in Verification: it does not re-prove discriminators or likelihoods; it aggregates which rows and families are theorem-grade, dataset-backed, likelihood-tagged, or ringdown-guarded, and exposes the counts.

proof idea

Definition-and-count module, not a deep derivation. Named lists (theorem-grade sectors, rival rows covered, falsifier rows with dataset attachments, rows with likelihood/status records, guarded ringdown families and mappings) are assembled by reference to the imported Track 6.C/6.D and falsifier-register modules. Companion theorems assert the cardinalities of those lists; proofs are list-length evaluations over the fixed enumerations. No analytic estimates or new physics identities appear here.

why it matters in Recognition Science

Gives Track 7 a single importable sensitivity ledger: which discriminator sectors are theorem-grade, how many rival rows are covered, how many falsifier rows carry datasets or likelihood/status records, and how many GWTC-3 ringdown families/mappings are on the guarded runner. Downstream, MasterTheoremHandoffIntegration (Gravity Track 7 fork handoff) imports this module among the parallel fork receipts (Tracks 1.B, 1.B-PHY/1.C, 2.C, 3.C). In the master-plan chain it is the verification-side closure stamp for Track 6.C/6.D plus §7 register attachments, so handoff can cite coverage counts without reopening structural proofs. It does not itself decide any rival theory; it only certifies what is already theorem-grade and instrumented.

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)