Gravity Sparcfalsifier Sparc Falsifier Cert

The falsification certificate

The Recognition Science framework, which derives physical structure from a forced cost of recognition, makes a specific prediction for how fast stars should orbit the centers of their galaxies. The declaration sparc_falsifier_cert is a machine-checked certificate that this prediction is genuinely testable. It bundles together the rules of the test: the model's parameters are locked to the golden ratio phi, no per-galaxy adjustments are allowed, and the pass or fail criterion is a simple numerical comparison. The certificate proves these rules are consistent, not that the prediction is true.

The test itself is a statistical comparison against the SPARC galaxy sample. The framework predicts a median chi-squared per degree of freedom of 2.75 across the sample. The certificate defines a generous threshold of 5.0, above which the model is considered falsified, and a tighter threshold of 3.0, which tests the specific prediction more strictly. It also records that a comparison model, MOND, has a mean chi-squared of 4.65, while the ILG model's mean is 4.23, a difference the certificate proves is real. These numbers are definitions and measurements, not derived theorems.

The certificate includes control conditions: if shuffling galaxy velocities, rotating the data by 180 degrees, or swapping gas and star contributions inflates the chi-squared value, that signals the model is capturing real structure rather than noise. The certificate proves the falsification criterion is decidable, meaning for any possible median value, the model is either falsified or it passes. It also proves the global-only policy: all parameters come from phi, and the per-galaxy free parameter count is exactly zero.

What the certificate does not do is run the test. It does not compute the actual SPARC data, and it does not assert that the ILG model passes. The certificate is a formal guarantee that the test is well-defined and that the model's parameters are fixed in advance. The actual comparison against real galaxy data remains an empirical check, not a proved result.

/-- The falsification criterion is decidable (for any real number). -/
theorem falsification_decidable (x : ℝ) :
    ILG_falsified x ∨ ILG_passes x := by
  unfold ILG_falsified ILG_passes generous_threshold
  exact le_or_gt x 5.0 |>.elim (Or.inr) (Or.inl)

theorem global_only_policy : GlobalOnlyPolicy where
  alpha_from_phi := parameters_from_phi.1
  upsilon_from_phi := parameters_from_phi.2.1
  clag_from_phi := parameters_from_phi.2.2
  per_galaxy_params := zero_free_params

/-- ILG has higher median but LOWER mean than MOND — it handles
    outliers better due to the global-only constraint. -/
theorem ilg_better_mean_than_mond :
    paper2_mean_chi2 < mond_mean_chi2 := by
  unfold paper2_mean_chi2 mond_mean_chi2; norm_num

What this page does not claim

The certificate does not assert that the ILG model actually passes the falsification test. The certificate does not prove that the ILG prediction matches any measured galaxy rotation curve. The certificate does not establish that the SPARC sample is the correct or complete dataset for testing the model.

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/Gravity/SPARCFalsifier.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: