Encyclopedia Verification Verification Track6 Falsifier Sensitivity

ARTICLE 2 claims 2 theorems

Verification Track6 Falsifier Sensitivity

A machine-checked certificate that quantum gravity rivals have named, testable differences, without claiming any of them is confirmed.

Falsifier sensitivity

Falsifier sensitivity is the practice of spelling out, in advance, what evidence would count against a theory. In Recognition Science (RS), this takes a concrete form: a falsifier register, a discrete list of rival quantum gravity approaches and the observable signatures that could distinguish each from RS. The register is not a wish list. Each row names a rival theory and attaches a specific dataset or measurement channel that could, in principle, separate that rival from RS predictions.

The certificate that packages this work, Track6FalsifierSensitivity, is a structural certificate rather than a new observational claim. It proves, in the framework's machine-checked library of formal theorems, that Track 6 of the quantum gravity discovery plan has a single, coherent sensitivity package. The certificate counts what exists: three theorem-grade discriminator sectors (leading-log entropy, echo damping, and rung phase), four rival rows covered by the discriminator matrix (LQG, string, CDT/causal sets, and Bohmian/Diosi-Penrose), all ten falsifier-register rows with named dataset attachments, and six rows upgraded to likelihood or status records.

The certificate also guards the reproducibility surface for gravitational wave ringdown analysis. The GWTC-3 ringdown shared runner prevents mixed-family posterior aggregation in the QNM/echo damping path, accepting three ringdown families and two supported observable mappings. This is a methodological guard: it stops an analysis from accidentally combining signals from different theoretical families, which would blur the very distinctions the falsifier register is meant to keep sharp.

In plain language, the certificate establishes that RS has a working, auditable infrastructure for saying what would falsify it, and that this infrastructure covers the main rival approaches with named data channels. It does not establish that any rival is falsified, nor that any RS prediction is empirically confirmed. The certificate is deliberately conservative: it proves the package exists and is internally consistent, not that the physics inside it is right.

THEOREM track6_falsifier_sensitivity_one_statement · IndisputableMonolith/Verification/Track6FalsifierSensitivity.lean
track6_falsifier_sensitivity_one_statement · IndisputableMonolith/Verification/Track6FalsifierSensitivity.lean:165
/-- **Fork F handoff theorem.**

Track 6 has a single integration endpoint: three theorem-grade
discriminator sectors, four rival rows covered by the discriminator matrix,
all ten falsifier-register rows dataset-attached, six rows upgraded to
likelihood/status records, and a guarded GWTC-3 ringdown runner with two
supported observable mappings. -/
theorem track6_falsifier_sensitivity_one_statement :
    (theoremGradeDiscriminatorSectors = 3) ∧
    (rivalRowsCovered = 4) ∧
    (falsifierRowsWithDatasetAttachments = 10) ∧
    (rowsWithLikelihoodOrStatusRecords = 6) ∧
    (guardedRingdownFamilies = 3) ∧
    (guardedRingdownMappings = 2) ∧
    Nonempty Track6FalsifierSensitivityCert :=
  ⟨theorem_grade_discriminator_sector_count,
   rival_rows_covered_count,
   dataset_attachment_row_count,
   likelihood_or_status_row_count,
   guarded_ringdown_family_count,
   guarded_ringdown_mapping_count,
   track6FalsifierSensitivityCert_inhabited⟩
THEOREM guarded_ringdown_family_count · IndisputableMonolith/Verification/Track6FalsifierSensitivity.lean
theorem guarded_ringdown_family_count :
    guardedRingdownFamilies = 3 := rfl

What this page does not claim

No empirical confirmation of any RS prediction is claimed. No rival theory is claimed to be falsified. The certificate does not upgrade the PTA, strong-field, or ringdown physics into a final discovery statement.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Verification/Track6FalsifierSensitivity.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND