Verification Cassini Strong Field Likelihood

The Cassini check

The Cassini spacecraft's 2002 radio experiment measured how much the Sun's gravity delays a signal passing near it, a test of the parameter γ that describes how strongly mass bends spacetime. The result, reported by Bertotti, Iess, and Tortora, was γ − 1 = (2.1 ± 2.3) × 10⁻⁵. In general relativity, γ equals 1 exactly, so the measurement is consistent with Einstein's theory, and it remains the best solar-system constraint on this particular deviation.

Recognition Science (RS) derives a specific prediction for this same deviation from its foundational forcing chain, not from a fit to data. The framework's structural target is φ⁻⁴⁴, approximately 6.376 × 10⁻¹⁰, where φ is the golden ratio. The question is whether the Cassini result supports or refutes that target.

The framework's machine-checked library of formal theorems now contains a certificate that answers this question exactly. The certificate proves two facts. First, the Cassini central value lies within one standard deviation of the RS target: the absolute difference between 2.1 × 10⁻⁵ and 6.376 × 10⁻¹⁰ is less than the reported uncertainty of 2.3 × 10⁻⁵. Second, and more important, Cassini is not currently sensitive to the target scale: the target is roughly 36,000 times smaller than the experiment's one-sigma precision. The measurement simply cannot see a deviation that small.

In plain language, this is a consistency check, not a confirmation. The certificate, named CassiniStrongFieldLikelihoodCert, packages these facts as a formal object: the residual is within one sigma, the target is below the noise floor, and the dataset is explicitly marked as not currently sensitive. A companion theorem states the whole result in one line. The proof uses no axioms beyond the standard logical kernel, and it contains no unproven assumptions.

What this changes is the status of the strong-field falsifier row in the RS verification register. It moves from a mere dataset attachment to a dataset-specific, machine-checked likelihood statement. The honest verdict is that the RS prediction survives the Cassini test, but the test is too weak to say anything more. The next step is not a better analysis of old data; it is a measurement with precision near the target scale, which no current experiment approaches.

/-- Cassini central value is within 1σ of the RS structural target scale. -/
theorem cassini_residual_lt_one_sigma :
    cassiniStrongFieldResidual < cassiniGammaSigma := by
  unfold cassiniStrongFieldResidual cassiniGammaMinusOneCentral
    cassiniRSTargetScale cassiniGammaSigma strongFieldAttachment
  norm_num

/-- Cassini is not currently sensitive to the φ⁻⁴⁴ target:
the one-sigma uncertainty is larger than the target scale. -/
theorem cassini_sigma_gt_rs_target :
    cassiniRSTargetScale < cassiniGammaSigma := by
  unfold cassiniRSTargetScale cassiniGammaSigma strongFieldAttachment
  norm_num

structure CassiniStrongFieldLikelihoodCert where
  sigma_pos : 0 < cassiniGammaSigma
  target_pos : 0 < cassiniRSTargetScale
  residual_lt_one_sigma :
    cassiniStrongFieldResidual < cassiniGammaSigma
  not_currently_sensitive :
    cassiniRSTargetScale < cassiniGammaSigma
  dataset_status :
    HasPositiveSensitivity strongFieldAttachment ∧
    HasPositiveTargetScale strongFieldAttachment ∧
    strongFieldAttachment.currentlySensitive = false

/-- One-statement Cassini likelihood attachment theorem. -/
theorem cassini_strong_field_likelihood_one_statement :
    (cassiniStrongFieldResidual < cassiniGammaSigma) ∧
    (cassiniRSTargetScale < cassiniGammaSigma) ∧
    (strongFieldAttachment.currentlySensitive = false) ∧
    Nonempty CassiniStrongFieldLikelihoodCert :=
  ⟨cassini_residual_lt_one_sigma,
   cassini_sigma_gt_rs_target,
   rfl,
   cassiniStrongFieldLikelihoodCert_inhabited⟩

What this page does not claim

This module does not claim empirical confirmation of the RS target, only statistical compatibility. This module does not claim that Cassini's measurement is wrong or that its uncertainty is misreported. This module does not claim that the RS target is the only value compatible with the Cassini data.

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