Cosmology Dark Energy Phi Dilution Law

The dilution law

Dark energy is the name cosmologists give to the observed acceleration of the universe's expansion. In the standard picture it is a property of empty space itself, often modeled by a cosmological constant, a fixed energy density that does not dilute as the universe grows. The Recognition Science framework approaches the same phenomenon from a different direction: it treats the cosmos as a system that keeps a discrete record of events, and it derives constants from that record rather than fitting them to data.

Within that framework, the dark-energy phi-dilution law is a proposed rule for how a certain quantity, the occupancy fraction of a phantom-Carnot unit, weakens as it passes through the dimensions of the carrier field. The rule states that each carrier dimension attenuates the signal by one factor of the golden ratio, φ, which is approximately 1.618. For a carrier of dimension n, the occupancy fraction becomes φ⁻ⁿ, or 1 divided by φ raised to the n-th power. This is a definitional choice, a model of how the attenuation works, not a derived result on its own.

The framework's library, a machine-checked collection of formal theorems, then proves what follows if that rule is accepted. A separate theorem in the library establishes that the dark-energy carrier field has dimension 4. Combining that theorem with the dilution rule forces the occupancy fraction to be φ⁻⁴, which is about 0.1459. The library proves this value is positive, less than one-sixth, and consistent with the framework's cost ceiling. These are formal results, conditional on the named dilution law being the correct admissibility rule.

The same module derives a present-day amplitude from this forced occupancy fraction. The closed form is (φ - 3/2) / (3φ + 2), which evaluates to a number between 0.015 and 0.018. The library proves this amplitude sits above a strong falsifier threshold and below a sharp DESI threshold, meaning the prediction is not trivially excluded by existing cosmological bounds. This is a theorem about the framework's own model, not a measurement of the real universe.

The practical consequence is that the framework does not need to fit the dark-energy amplitude. Once the dilution rule and the four-dimensional carrier are accepted, the amplitude follows by proof. What remains open is whether the dilution rule itself is physically correct, and whether the framework's model of dark energy matches the full range of cosmological observations.

/-- Dimension-uniform φ attenuation through a carrier dimension `n`: one factor of `φ⁻¹`
per dimension. -/
def phiDilution (n : ℕ) : ℝ := 1 / phi ^ n

/-- 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 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 predicted-amplitude certificate is inhabited. -/
def predictedAmplitudeCert : PredictedAmplitudeCert where
  closed_form := predictedPresentAmplitude_closed
  band := predictedPresentAmplitude_band
  positive := predictedPresentAmplitude_pos
  below_ceiling := predictedPresentAmplitude_lt_ceiling
  far_below_ceiling := predictedPresentAmplitude_lt_ceiling_div_six
  above_strong_falsifier := predictedPresentAmplitude_above_strong_falsifier
  below_sharp_desi := predictedPresentAmplitude_below_sharp_desi

What this page does not claim

The dilution rule itself is not proved; it is a named model assumption. The predicted amplitude is not a measurement of the real universe's dark energy density. The framework does not claim to replace the standard cosmological model without further empirical checks.

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: