Cosmology Dark Energy Phi Dilution Law Predicted Present Amplitude Lt Ceiling Di

The predicted dark-energy amplitude

Dark energy is the name astronomers give to the unknown influence that makes the expansion of the universe accelerate. In the Recognition Science framework, that influence has a ledger, a discrete record of recognition events, and the framework's central cost function J(x) = (x + 1/x)/2 - 1 sets a ceiling on how large the dark-energy amplitude can be. The declaration predictedPresentAmplitude_lt_ceiling_div_six is a proved theorem in the framework's machine-checked library of formal theorems. It states that the present-day dark-energy amplitude, a number the framework derives from first principles, is strictly less than one sixth of that ceiling.

The amplitude in question is not a free parameter. The framework derives it from a chain of forced steps. A unit of dark-energy occupancy, modeled as a phantom-Carnot cycle, is attenuated by one factor of the golden ratio φ per dimension as it passes through the carrier of Einstein's field equations. That carrier is already proved to have dimension four in the framework, so the occupancy fraction becomes φ⁻⁴ = 1/φ⁴. The amplitude is then the cost function evaluated at that fraction, divided by a denominator that emerges from the algebra. The closed form is (φ - 3/2) / (3φ + 2), which evaluates to a number between 0.015 and 0.018. The theorem in question proves this number is below J(φ)/6, and since J(φ) = φ - 3/2 ≈ 0.118, the bound is about 0.0197. The amplitude is therefore pinned to a narrow band, roughly 0.015 to 0.018, which is less than one sixth of the ceiling.

This matters because the band is falsifiable. The same library proves the amplitude sits above a strong falsifier threshold and below a sharp threshold derived from DESI, the Dark Energy Spectroscopic Instrument. If future measurements place the dark-energy amplitude outside the band, the framework's premise of dimension-uniform φ dilution would be ruled out. The theorem does not, however, claim that the amplitude has been measured. It is a prediction, not an observation. It also does not claim that the φ-dilution law itself is derived from the forcing chain; the law is a named premise, a definitional choice, and the theorem is conditional on it. The framework proves that if the law holds, then the amplitude must lie in this band.

The practical consequence is a target for observation. The framework has produced a sharp, testable number for the present dark-energy amplitude, and it has done so without fitting any parameter. Whether that number matches the sky is an empirical question, and the theorem's role is to make the prediction precise enough that the question can be answered.

/-- `δw(0)` is more than six times below the ceiling, confirming `J(φ)` is a ceiling and not
the value (occupancy `θ = φ⁻⁴ < 1/6`). -/
theorem predictedPresentAmplitude_lt_ceiling_div_six :
    predictedPresentAmplitude < Cost.Jcost phi / 6 := by
  have hb := predictedPresentAmplitude_band.2
  have hlo : (1.61 : ℝ) < phi := phi_gt_onePointSixOne
  rw [jcost_phi_closed]
  have hnum : (0.11 : ℝ) < phi - 3/2 := by linarith
  linarith

/-- 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

/-- 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]

/-- The dimension-uniform dilution law forces `θ=φ⁻⁴` because the EFE carrier dimension is
`4`. -/
theorem darkEnergyThetaFromDimension_eq_phiFour :
    darkEnergyThetaFromDimension = DarkEnergyThetaPhiFour.thetaPhiFour := by
  unfold darkEnergyThetaFromDimension phiDilution DarkEnergyThetaPhiFour.thetaPhiFour
  rw [darkEnergyCarrierDimension_eq_four]

/-- The dark-energy EFE carrier is four-dimensional. -/
theorem darkEnergyCarrierDimension_eq_four : darkEnergyCarrierDimension = 4 := by
  unfold darkEnergyCarrierDimension
  exact Gravity.FullEFEWithDarkEnergy.lambda_efe_dimension 1

/-- The predicted amplitude lies strictly above the BIT strong-test falsifier `0.005`: the
dynamic signature is large enough to be a real DESI/Roman/Euclid target. -/
theorem predictedPresentAmplitude_above_strong_falsifier :
    CosmicAgingAmplitudeSharp.bit_strong_falsifier < predictedPresentAmplitude := by
  have h := predictedPresentAmplitude_band.1
  unfold CosmicAgingAmplitudeSharp.bit_strong_falsifier
  linarith

/-- 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

What this page does not claim

The dark-energy amplitude has been measured; it is a prediction, not an observation. The φ-dilution law is derived from the forcing chain; it is a named premise, and the theorem is conditional on it. The framework derives the fine-structure constant α; that remains open.

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: