Cosmology Dark Energy Amplitude Derivation Implied Occupancy Lt One Sixth

The attenuation bound

In cosmology, dark energy is the unknown agent that accelerates the expansion of the universe. One way to study it is to ask how strong its effect is: what amplitude, or size, should the physical quantity driving that acceleration have? In the Recognition Science framework, that question gets a precise answer with a surprising twist: the framework does not compute a single number for the amplitude. It proves a ceiling, then shows that the value implied by cosmological data sits far below that ceiling.

The ceiling comes from a function called the cost function, which the framework derives from first principles. That cost function, evaluated at the golden ratio, gives a maximum possible amplitude. The framework's recognition model, a discrete record of events that reality keeps, forces this ceiling through a chain of theorems. The physical amplitude, however, is not that ceiling by default. It is an attenuation fraction: a number between zero and one multiplied by the ceiling. A fraction of one would mean the amplitude saturates at its maximum; a fraction of zero would mean no dark energy at all.

The declaration impliedOccupancy_lt_one_sixth establishes that the attenuation fraction implied by current cosmological data is strictly below one sixth. In plain terms, the data-implied amplitude is less than one sixth of the maximum allowed by the framework. The proof is a theorem in the framework's machine-checked library of formal theorems, with zero unproved assumptions. This is a sharp bound: it excludes the possibility that dark energy saturates its ceiling, and it also excludes any value at or above one sixth of that ceiling.

What this does not claim is just as important. The declaration does not derive the attenuation fraction itself. It proves the envelope, the range within which the amplitude must lie, and it shows that the data-implied value falls in the lower part of that range. The remaining problem, deriving the exact fraction from more basic principles, remains open. The framework has narrowed the question to a single scalar, but it has not yet answered that question.

/-- The data-implied attenuation fraction is strictly below `1/6`. This is the precise
sub-saturation statement: the full `J(φ)` ceiling is at least six times too large to be the
gap-implied dynamic amplitude. -/
theorem impliedOccupancy_lt_one_sixth : impliedOccupancy < (1 : ℝ) / 6 := by
  unfold impliedOccupancy
  rw [div_lt_iff₀ Constants.Jcost_phi_pos]
  nlinarith [CosmicAgingAmplitudeSharp.jPhi_dominates_implied]

/-- An admissible amplitude attenuation fraction. -/
structure AmplitudeAttenuation where
  theta : ℝ
  theta_nonneg : 0 ≤ theta
  theta_le_one : theta ≤ 1

/-- The amplitude envelope certificate is inhabited. -/
def dynamicAmplitudeEnvelopeCert : DynamicAmplitudeEnvelopeCert where
  ceiling_pos := Constants.Jcost_phi_pos
  admissible_nonneg := attenuatedAmplitude_nonneg
  admissible_below_ceiling := attenuatedAmplitude_le_ceiling
  saturation_is_ceiling := attenuatedAmplitude_saturation
  implied_theta_pos := impliedOccupancy_pos
  implied_theta_lt_one_sixth := impliedOccupancy_lt_one_sixth
  implied_factorization := implied_amplitude_factorization

What this page does not claim

The attenuation fraction itself is not derived, only its upper bound. The framework does not claim that dark energy saturates its ceiling or that the data-implied value is the true amplitude. The bound does not give a prediction for the exact dark energy amplitude, only a range.

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