Cosmology Dark Energy Theta Status Implied Theta Amplitude Valid

The amplitude bound

The dark-energy amplitude in this framework is written as δw0 = θ · J(φ), where J(φ) is a fixed positive number and θ is a fraction between 0 and 1. The theorem impliedTheta_amplitude_valid proves that the θ inferred from observational data, called the implied occupancy, yields an amplitude that is strictly positive and no larger than J(φ). In plain terms, the data-envelope value of θ cannot push the amplitude to zero or above its natural ceiling.

The proof is short and direct. It combines two facts: the implied θ is positive and less than 1/6, and J(φ) itself is positive. Multiplying a positive fraction by a positive number gives a positive result, and because θ is at most 1, the product cannot exceed J(φ). The theorem is a formal statement in the machine-checked library of formal theorems, so the reasoning is verified step by step.

The declaration does not derive θ from first principles. The exact value of θ remains an open target; the framework only establishes that any future derivation that supplies a θ in the interval (0, 1] will automatically satisfy the same positivity and ceiling bounds. This separates the proven envelope from the unproven exact value, preventing a fit to data from being mistaken for a derivation.

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

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

/-- 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 derived from first principles. The amplitude equals a specific measured dark-energy density. The theorem proves the framework's dark-energy model is physically correct.

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: