Cosmology Dark Energy Theta Status

The theta status

In the Recognition Science framework, the dynamic dark-energy amplitude is written as δw0 = θ · J(φ). The symbol J(φ) is a fixed number derived from the framework's cost function, and θ is a fraction that attenuates, or reduces, that amplitude. The question is what θ is.

The framework's machine-checked library of formal theorems does not yet prove an exact value for θ. That remains an open target. What the library does prove is a sharp bound on the value implied by observational data: 0 < θ_implied < 1/6. This is a data-envelope result, not a first-principles derivation. The library states this distinction explicitly.

To prevent the common mistake of replacing the missing derivation with a fitted value, the module defines the exact theorem-shaped input a future derivation must supply. It is a structure called ThetaFromFirstPrinciples, requiring a real number θ with 0 < θ ≤ 1. The library proves that once such a θ is supplied, all amplitude obligations reduce to already proved envelope theorems: the attenuated amplitude is positive and stays below the J(φ) ceiling.

In plain language, the module separates what is known from what is not. It proves that any admissible θ yields a valid amplitude, and it proves the current implied θ lies in the admissible band. The exact value of θ remains open, but the framework has defined the target precisely and made the remaining algebra fully theorem-checked.

/-- The theorem-shaped output required from a future first-principles derivation of the
dynamic occupancy/coupling fraction. -/
structure ThetaFromFirstPrinciples where
  theta : ℝ
  theta_pos : 0 < theta
  theta_le_one : theta ≤ 1

/-- 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 θ has been derived from first principles. The implied θ value is a derivation rather than a data-envelope constraint. The framework predicts a specific numerical value for 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: