Cosmology Cosmic Aging Amplitude Sharp Desi Sharp Threshold Pos

The sharp threshold

In cosmology, the parameter w describes how the pressure of dark energy relates to its density. A value of exactly -1 means dark energy behaves like a constant energy density, the cosmological constant. Some models allow w to vary slightly over time, written as w(z) = -1 + δw · Z(z)/Z_today, where δw is a small number measuring the deviation from -1.

The Recognition Science framework has a model for cosmic aging, the gradual change in the universe's expansion rate. This model predicts a central value for the dark energy density parameter ΩΛ of 0.6845. The Planck 2018 satellite measurement gives a central value of 0.6889. The gap between these two numbers is about 0.0044, a small but real difference that the framework's model must explain.

Within the framework, this gap translates into a required deviation δw from -1. Using a linear approximation, the implied δw falls between roughly 0.0088 and 0.0147, with a midpoint around 0.011. The declaration desi_sharp_threshold_pos proves a simple but important fact: this sharp threshold, defined as twice the maximum implied δw, is a positive number. The machine-checked proof confirms it lies between 0.026 and 0.034.

This sharp threshold matters because it is far tighter than the older, looser bound. The looser bound allowed δw to be as large as about 0.118, the saturation ceiling from the framework's cost function. The new threshold is about eight times smaller. This makes it a much more powerful test for the Dark Energy Spectroscopic Instrument (DESI) and future surveys like Roman and Euclid.

In Recognition Science, this sharp threshold is a falsifier. If DESI measures a δw that is clearly below this threshold, it would contradict the framework's explanation of the Planck-RS gap. A null result at 0.005, for instance, would directly challenge the model. The declaration desi_sharp_threshold_pos itself only establishes positivity, but it is part of a chain of results that define this sharper, operationally meaningful test.

This does not claim that the framework's model is correct, nor that the linear approximation used to translate the ΩΛ gap into δw is exact. The full nonlinear treatment remains a target. The sharp threshold is a prediction, not a measurement, and its utility depends on the accuracy of the linear kernel assumption.

/-- The sharpened threshold is positive. -/
theorem desi_sharp_threshold_pos : 0 < desi_sharp_threshold := by
  unfold desi_sharp_threshold
  have : 0 < delta_w_implied_max := by
    unfold delta_w_implied_max
    apply div_pos gap_observed_pos
    unfold z_norm_late_lower; norm_num
  linarith

/-- The sharpened threshold is in `(0.026, 0.034)`. -/
theorem desi_sharp_threshold_band :
    0.026 < desi_sharp_threshold ∧ desi_sharp_threshold < 0.034 := by
  unfold desi_sharp_threshold
  have h1 : 0.013 < delta_w_implied_max := delta_w_implied_max_gt
  have h2 : delta_w_implied_max < 0.017 := delta_w_implied_max_lt
  refine ⟨?_, ?_⟩ <;> linarith

/-- The slack factor: J(φ) is **at least 6x larger** than the
implied δw. -/
theorem jPhi_dominates_implied :
    delta_w_implied_max * 6 < Cost.Jcost phi := by
  have := delta_w_implied_max_lt_jPhi_over_6
  linarith [Cost.Jcost_unit0]

/-- The strong falsifier is below the smallest implied `δw_min`. -/
theorem strong_falsifier_below_implied_min :
    bit_strong_falsifier < delta_w_implied_min := by
  unfold bit_strong_falsifier
  exact lt_trans (by norm_num : (0.005 : ℝ) < 0.008) delta_w_implied_min_gt

What this page does not claim

The sharp threshold is a measured quantity, not a predicted one. The linear approximation translating the ΩΛ gap into δw is exact. The framework's model of cosmic aging is confirmed by this threshold.

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/Cosmology/CosmicAgingAmplitudeSharp.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: