Cosmology Dark Energy Theta Status Implied Theta Attenuation

The amplitude residue

The dark-energy amplitude is the size of the effect that accelerates cosmic expansion. In the Recognition Science framework, this amplitude is written as θ times a base factor J(φ), where J is a cost function and φ is the golden ratio. The declaration impliedThetaAttenuation packages the current best estimate of θ, called the implied occupancy, into a form the framework's library can reason about. It is a definition, not a discovery: it takes a number that comes from fitting observational data and labels it as an admissible attenuation fraction.

What the theorem does prove is a sharp bound. The machine-checked theorem impliedTheta_band shows that the implied occupancy lies strictly between 0 and 1/6. That means the dark-energy amplitude is positive but less than one-sixth of its ceiling value J(φ). The proof is short: the bound follows from two earlier lemmas, one showing positivity and one showing the upper limit. A second theorem, impliedTheta_amplitude_valid, confirms that this amplitude is both positive and below the ceiling, so the framework's existing envelope theorems apply to it.

The declaration also sets up what a future derivation must supply. The structure ThetaFromFirstPrinciples defines the exact shape of a first-principles derivation: a real number θ with 0 < θ ≤ 1. Two theorems show that any such θ immediately gives a positive amplitude below the ceiling. This is the honest status: the framework proves the envelope and the bound, but it does not derive the exact value of θ from first principles. The exact θ remains an open target, not a proved result.

In plain terms, the declaration says three things. First, the current data-implied value of θ is small, below one-sixth, and therefore the amplitude is safely inside its allowed band. Second, if anyone later derives θ from the framework's axioms, the amplitude obligations are already settled by theorem. Third, the current θ is an envelope value from data, not a derivation, and the framework says so explicitly in its status certificate. The consequence for a reader is clear: the framework's contribution here is a rigorous bound and a clean target, not a prediction of the exact dark-energy amplitude.

/-- The current sharp implied theta lies in the admissible positive sub-saturation band. -/
theorem impliedTheta_band :
    0 < impliedOccupancy ∧ impliedOccupancy < (1 : ℝ) / 6 :=
  ⟨impliedOccupancy_pos, impliedOccupancy_lt_one_sixth⟩

/-- The implied amplitude is positive and below the ceiling. -/
theorem impliedTheta_amplitude_valid :
    0 < attenuatedAmplitude impliedOccupancy ∧
      attenuatedAmplitude impliedOccupancy ≤ Cost.Jcost phi :=
  ⟨by
      unfold attenuatedAmplitude
      exact mul_pos impliedOccupancy_pos Constants.Jcost_phi_pos,
    attenuatedAmplitude_le_ceiling impliedThetaAttenuation⟩

/-- Any first-principles theta derivation gives a positive amplitude. -/
theorem thetaDerived_amplitude_pos (T : ThetaFromFirstPrinciples) :
    0 < attenuatedAmplitude T.theta := by
  unfold attenuatedAmplitude
  exact mul_pos T.theta_pos Constants.Jcost_phi_pos

/-- Any first-principles theta derivation keeps the amplitude below the `J(φ)` ceiling. -/
theorem thetaDerived_amplitude_le_ceiling (T : ThetaFromFirstPrinciples) :
    attenuatedAmplitude T.theta ≤ Cost.Jcost phi :=
  attenuatedAmplitude_le_ceiling T.toAmplitudeAttenuation

What this page does not claim

The exact value of θ is not derived from first principles. The implied occupancy is not a prediction from the framework's axioms. The declaration does not explain what physical process sets the dark-energy amplitude.

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