Verification Falsifier Likelihood Register

The falsifier register

The verification falsifier likelihood register is a bookkeeping device inside Recognition Science. It keeps a discrete record of the ten specific predictions, called falsifiers, that the framework's master plan says could prove it wrong. For each prediction, the register records whether scientists have attached a named dataset to it, and whether that dataset has been upgraded into a likelihood, a statistical model that says how probable the data would be under the theory, or a status record that tracks a measurement's current state.

The register's arithmetic is simple and exact. Of the ten falsifier rows, six have been upgraded beyond just having a dataset: they now carry likelihood or status artifacts. These include the Planck dark-energy density, Cassini and GRAVITY S2 strong-field tests, the Event Horizon Telescope's M87* image, pulsar timing arrays, and gravitational-wave ringdown. The remaining four rows, for example the Page curve of black-hole entropy, are still dataset-only or future work. Eight individual likelihood or status artifacts exist in total, because some rows carry more than one.

What the module actually proves is that these counts add up. A machine-checked library of formal theorems verifies that six upgraded rows plus four dataset-only rows equals ten total rows, and that the number of individual artifacts is positive. It also assembles a certificate, a single structured object that bundles all eight likelihood and status proofs together with the coverage arithmetic. The certificate's existence is itself a theorem, checked line by line with no gaps and no special axioms added.

This is coverage accounting, not empirical confirmation. The register does not claim that any prediction has been verified or that the framework is true. It claims that the framework has a named, checkable plan for how it could be falsified, and that a defined portion of that plan now has real data attached to it. The honest headline is that six of ten testable predictions have moved from untested to testable, and the remaining four are explicitly tracked as open targets.

For a reader, the register answers a simple question: what would it take to break this theory, and how far along is that process? The answer is a scoreboard, not a verdict.

/-- Rows upgraded beyond dataset-only to likelihood/status records. -/
def rowsWithLikelihoodOrStatus : ℕ := 6

/-- One-statement coverage theorem for the §7 likelihood/status layer. -/
theorem falsifier_likelihood_register_one_statement :
    (individualLikelihoodArtifacts = 8) ∧
    (rowsWithLikelihoodOrStatus = 6) ∧
    (datasetOnlyRows = 4) ∧
    (totalFalsifierRows = 10) ∧
    (rowsWithLikelihoodOrStatus + datasetOnlyRows = totalFalsifierRows) ∧
    Nonempty FalsifierLikelihoodRegisterCert :=
  ⟨rfl, rfl, rfl, rfl, row_coverage_arithmetic,
   falsifierLikelihoodRegisterCert_inhabited⟩

/-- Rows still dataset-only/future. -/
def datasetOnlyRows : ℕ := 4

/-- One-statement coverage theorem for the §7 likelihood/status layer. -/
theorem falsifier_likelihood_register_one_statement :
    (individualLikelihoodArtifacts = 8) ∧
    (rowsWithLikelihoodOrStatus = 6) ∧
    (datasetOnlyRows = 4) ∧
    (totalFalsifierRows = 10) ∧
    (rowsWithLikelihoodOrStatus + datasetOnlyRows = totalFalsifierRows) ∧
    Nonempty FalsifierLikelihoodRegisterCert :=
  ⟨rfl, rfl, rfl, rfl, row_coverage_arithmetic,
   falsifierLikelihoodRegisterCert_inhabited⟩

theorem row_coverage_arithmetic :
    rowsWithLikelihoodOrStatus + datasetOnlyRows = totalFalsifierRows := by
  unfold rowsWithLikelihoodOrStatus datasetOnlyRows totalFalsifierRows
  decide

theorem individual_artifact_count_pos :
    0 < individualLikelihoodArtifacts := by
  unfold individualLikelihoodArtifacts
  decide

def falsifierLikelihoodRegisterCert : FalsifierLikelihoodRegisterCert where
  omegaLambda := OmegaLambdaPlanckLikelihood.omegaLambdaPlanckLikelihoodCert_inhabited
  cassini := CassiniStrongFieldLikelihood.cassiniStrongFieldLikelihoodCert_inhabited
  gravityS2 := GravityS2StrongFieldLikelihood.gravityS2StrongFieldLikelihoodCert_inhabited
  ehtM87 := EHTM87StrongFieldLikelihood.ehtM87StrongFieldLikelihoodCert_inhabited
  nanograv := NANOGravPTALikelihood.nanogravPTALikelihoodCert_inhabited
  epta := EPTAPTALikelihood.eptaPTALikelihoodCert_inhabited
  darkEnergyW := DarkEnergyWPlanckLikelihood.darkEnergyWPlanckLikelihoodCert_inhabited
  gwtc3 := GWTC3RingdownStatus.gwtc3RingdownStatusCert_inhabited
  row_coverage := row_coverage_arithmetic
  individual_artifacts_positive := individual_artifact_count_pos

theorem falsifierLikelihoodRegisterCert_inhabited :
    Nonempty FalsifierLikelihoodRegisterCert :=
  ⟨falsifierLikelihoodRegisterCert⟩

What this page does not claim

The register does not claim any empirical confirmation of the framework. The register does not claim that all ten falsifiers are equally strong or equally tested. The register does not claim that the four dataset-only rows are less important than the six upgraded ones.

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