Verification Falsifier Register Datasets

Falsifiability accounting

Verification falsifier register datasets are the accounting ledgers of the Recognition Science framework's testability program. A ledger, here, is a discrete record of events, and this particular record tracks one thing: which real-world observation would falsify which framework prediction. Each entry names an observational channel or dataset, states a numerical sensitivity scale, gives a Recognition Science target scale or band to compare against, and flags whether current data are already sensitive to that target. The module does not claim any dataset has confirmed the framework. It only makes explicit which experiment tests which prediction, and at what reported precision.

The entries cover the major frontiers of gravitational physics. The cosmological constant sector attaches Planck 2018 data with ΩΛ = 0.6889 ± 0.0056. Dark energy attaches DESI BAO, Planck CMB, and supernovae analyses with w₀ = -1.03 ± 0.03. Strong-field tests attach Cassini Shapiro delay (γ - 1 = (2.1 ± 2.3)×10⁻⁵), GRAVITY S2 precession (f_SP = 1.10 ± 0.19), and EHT M87* shadow observations. Pulsar timing attaches NANOGrav 15-year and EPTA DR2 stochastic background records. Black-hole ringdown attaches LIGO/Virgo/KAGRA GWTC-3 tests of general relativity, including the graviton-mass bound m_g ≤ 2.42×10⁻²³ eV/c². Each attachment is deliberately conservative: a row is attached only when it has a named channel, a numerical sensitivity, a target scale, and an honest sensitivity flag.

The formal content is a set of definitions and theorems in the framework's machine-checked library. A dataset attachment is a structure with six fields: sector, dataset, units, sensitivity, rsTargetScale, and currentlySensitive. Theorems prove that every attachment has positive sensitivity and positive target scale, meaning each record is a genuine, non-vacuous comparison. One aggregate theorem, falsifier_dataset_register_one_statement, packages all ten positive-sensitivity proofs together with the inhabited certificate. The certificate structure FalsifierDatasetRegisterCert and its inhabitant falsifierDatasetRegisterCert establish that the whole register is well-formed. Zero sorry (admitted proof obligations) and zero framework-specific axioms appear in the module.

The purpose is falsifiability accounting, not empirical confirmation. The register's honesty flags show the current state: Planck's ΩΛ measurement is already sensitive to the framework's target band, while most other sectors, including black-hole echoes, quasinormal modes, and the BMV phase-rate experiment, are not yet sensitive. This is the framework's own discipline: it names the experiment that could kill each prediction, and it says plainly when that experiment has not yet reached the needed precision. The module does not prove any physics. It proves that the framework has a complete, non-vacuous falsification register, which is a different and prior achievement: a theory that can say exactly what would disprove it.

theorem falsifierDatasetRegisterCert_inhabited :
    Nonempty FalsifierDatasetRegisterCert :=
  ⟨falsifierDatasetRegisterCert⟩

/-- One-statement form: all falsifier-register rows have positive
dataset sensitivities and positive RS target scales. -/
theorem falsifier_dataset_register_one_statement :
    HasPositiveSensitivity bmvAttachment ∧
    HasPositiveSensitivity hawkingTemperatureAttachment ∧
    HasPositiveSensitivity leadingLogEntropyAttachment ∧
    HasPositiveSensitivity pageCurveAttachment ∧
    HasPositiveSensitivity echoAttachment ∧
    HasPositiveSensitivity omegaLambdaAttachment ∧
    HasPositiveSensitivity darkEnergyWAttachment ∧
    HasPositiveSensitivity qnmAttachment ∧
    HasPositiveSensitivity ptaAttachment ∧
    HasPositiveSensitivity strongFieldAttachment ∧
    Nonempty FalsifierDatasetRegisterCert :=
  ⟨bmv_sensitivity_pos,
   hawking_sensitivity_pos,
   leadingLog_sensitivity_pos,
   pageCurve_sensitivity_pos,
   echo_sensitivity_pos,
   omegaLambda_sensitivity_pos,
   darkEnergyW_sensitivity_pos,
   qnm_sensitivity_pos,
   pta_sensitivity_pos,
   strongField_sensitivity_pos,
   falsifierDatasetRegisterCert_inhabited⟩

theorem falsifierDatasetRegisterCert_inhabited :
    Nonempty FalsifierDatasetRegisterCert :=
  ⟨falsifierDatasetRegisterCert⟩

theorem falsifierDatasetRegisterCert_inhabited :
    Nonempty FalsifierDatasetRegisterCert :=
  ⟨falsifierDatasetRegisterCert⟩

What this page does not claim

No dataset has confirmed any Recognition Science prediction. The module does not prove that any physics prediction is correct. The sensitivity flags do not imply current experiments can distinguish the framework from conventional physics.

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/FalsifierRegisterDatasets.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: