Encyclopedia Cosmology Cosmology Dark Energy Phi Dilution Law Predicted Present Amplitude Below Sharp D

ARTICLE 4 claims 4 theorems

Cosmology Dark Energy Phi Dilution Law Predicted Present Amplitude Below Sharp D

A machine-checked library of formal theorems derives a narrow range for the present dark energy amplitude, and proves that range sits below a sharp observational threshold.

The predicted amplitude band

Dark energy is the name cosmologists give to the observed acceleration of cosmic expansion. In the Recognition Science framework, that acceleration is modeled as a discrete record of recognition events, and the framework's machine-checked library of formal theorems derives a specific number for the present amplitude of dark energy. The number is not fitted to cosmological data; it follows from the framework's forcing chain, which starts from a proved cost function and ends in a predicted amplitude.

The derived amplitude has a closed form: (phi - 3/2) / (3 * phi + 2), where phi is the golden ratio, approximately 1.618. Numerically, the framework proves the amplitude lies strictly between 0.015 and 0.018. This is a narrow band, about 17 percent wide, and it is the framework's prediction for the present value of the dark energy amplitude in its own units.

The declaration predictedPresentAmplitude_below_sharp_desi proves one additional fact: this predicted band sits strictly below a threshold called desi_sharp_threshold, which comes from the Dark Energy Spectroscopic Instrument (DESI) survey. The framework does not claim that DESI has measured the amplitude at this precision, nor that the threshold is a direct measurement of the framework's amplitude. The theorem establishes an ordering: the framework's prediction is less than the sharp DESI threshold, whatever the threshold's exact empirical status.

In Recognition Science, the derivation works by a dilution law. A unit of phantom-Carnot occupancy, a quantity from the framework's thermodynamics, is attenuated by one factor of phi^-1 for each dimension of the carrier. The dark energy carrier is proved to be four-dimensional, so the occupancy fraction becomes phi^-4, which equals 1/(3*phi + 2). The amplitude then follows from the framework's cost function J evaluated at phi, and the band 0.015 to 0.018 is proved using only the fact that phi lies between 1.61 and 1.62.

What the declaration does not claim is just as important. It does not claim that DESI has confirmed the framework's prediction. It does not claim that the framework's amplitude is the same quantity cosmologists measure as the dark energy density parameter. And it does not claim that the framework derives the fine-structure constant or any other coupling. The theorem is a conditional statement: if the framework's premises hold, then the predicted amplitude falls in this band, and that band is below the sharp DESI threshold.

THEOREM predictedPresentAmplitude_closed · IndisputableMonolith/Cosmology/DarkEnergyPhiDilutionLaw.lean
predictedPresentAmplitude_closed · IndisputableMonolith/Cosmology/DarkEnergyPhiDilutionLaw.lean:157
/-- Closed form: `δw(0) = (φ − 3/2)/(3φ + 2)`. -/
theorem predictedPresentAmplitude_closed :
    predictedPresentAmplitude = (phi - 3/2) / (3 * phi + 2) := by
  unfold predictedPresentAmplitude DarkEnergyAmplitudeDerivation.attenuatedAmplitude
  rw [darkEnergyThetaFromDimension_eq_phiFour]
  unfold DarkEnergyThetaPhiFour.thetaPhiFour
  rw [jcost_phi_closed, phi_pow_four_eq]
  ring
THEOREM predictedPresentAmplitude_band · IndisputableMonolith/Cosmology/DarkEnergyPhiDilutionLaw.lean
/-- Numeric band: `0.015 < δw(0) < 0.018`, robust to the `(1.61, 1.62)` φ enclosure. -/
theorem predictedPresentAmplitude_band :
    0.015 < predictedPresentAmplitude ∧ predictedPresentAmplitude < 0.018 := by
  rw [predictedPresentAmplitude_closed]
  have hlo : (1.61 : ℝ) < phi := phi_gt_onePointSixOne
  have hhi : phi < (1.62 : ℝ) := phi_lt_onePointSixTwo
  have hden : (0 : ℝ) < 3 * phi + 2 := three_phi_plus_two_pos
  constructor
  · rw [lt_div_iff₀ hden]; nlinarith [hlo]
  · rw [div_lt_iff₀ hden]; nlinarith [hhi]
THEOREM predictedPresentAmplitude_below_sharp_desi · IndisputableMonolith/Cosmology/DarkEnergyPhiDilutionLaw.lean
predictedPresentAmplitude_below_sharp_desi · IndisputableMonolith/Cosmology/DarkEnergyPhiDilutionLaw.lean:211
/-- The predicted amplitude lies strictly below the sharpened DESI threshold, i.e. inside the
"consistent with the BIT explanation of the Ω_Λ gap" regime, not the diagnostic-large
regime. -/
theorem predictedPresentAmplitude_below_sharp_desi :
    predictedPresentAmplitude < CosmicAgingAmplitudeSharp.desi_sharp_threshold := by
  have hb := predictedPresentAmplitude_band.2
  have hd := (CosmicAgingAmplitudeSharp.desi_sharp_threshold_band).1
  linarith
THEOREM darkEnergyCarrierDimension_eq_four · IndisputableMonolith/Cosmology/DarkEnergyPhiDilutionLaw.lean
darkEnergyCarrierDimension_eq_four · IndisputableMonolith/Cosmology/DarkEnergyPhiDilutionLaw.lean:48
/-- The dark-energy EFE carrier is four-dimensional. -/
theorem darkEnergyCarrierDimension_eq_four : darkEnergyCarrierDimension = 4 := by
  unfold darkEnergyCarrierDimension
  exact Gravity.FullEFEWithDarkEnergy.lambda_efe_dimension 1

What this page does not claim

The framework does not claim DESI has measured the amplitude at this precision. The framework does not claim its amplitude is the same quantity as the measured dark energy density parameter. The framework does not claim to derive the fine-structure constant or any other coupling constant.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND