Cosmology Dark Energy Theta Phi Four Theta Phi Four Amplitude Pos

A positive dark-energy amplitude

In cosmology, dark energy is the name for the unknown influence that appears to accelerate the expansion of the universe. Its strength is often described by a number, an amplitude, that observations constrain but do not pin down. This page reports a specific candidate for that number, and what a machine-checked proof establishes about it.

The candidate is θ = φ⁻⁴ = 1/φ⁴, where φ is the golden ratio, approximately 1.618. So the proposed amplitude is about 1 divided by 6.854, which is roughly 0.146. The declaration thetaPhiFour_amplitude_pos proves that this number is strictly greater than zero. That is its entire content: the amplitude is positive. It does not say how large the amplitude is compared to measured values, nor does it claim that this candidate is the actual dark energy.

The proof is part of a larger framework called Recognition Science, which models physical quantities as outcomes of a discrete ledger of recognition events, where each event carries a forced cost. Within that framework, the candidate is built from the golden ratio, which itself emerges from a proved uniqueness theorem about cost functions. The specific step here takes that ratio, raises it to the fourth power, and inverts it, a choice the framework interprets as a four-dimensional dilution of a unit cost.

The declaration also relies on two supporting facts, both proven in the same module. First, φ⁴ is larger than 6, which follows from the known lower bound 1.61 < φ. Second, therefore 1/φ⁴ is less than 1/6, a sharp envelope the framework associates with sub-saturation. These two facts together ensure the candidate is a valid inhabitant of the framework's first-principles theta target, which requires the amplitude to be positive and at most one. The positivity theorem is the final piece that certifies the candidate.

What the declaration does not claim is equally important. It does not assert that φ⁻⁴ is the measured value of dark energy's amplitude; no such measurement is cited. It does not claim that the physical premise, that four-dimensional φ-dilution is the correct occupancy law, has been derived from deeper principles. That premise remains an open scientific burden. The proof only establishes algebraic facts about the number itself, not its physical reality.

/-- The candidate's dynamic amplitude is positive. -/
theorem thetaPhiFour_amplitude_pos :
    0 < attenuatedAmplitude thetaPhiFour :=
  thetaDerived_amplitude_pos thetaPhiFourFirstPrinciples

/-- `φ⁴` is larger than `6`, using the established lower bound `1.61 < φ`. -/
theorem six_lt_phi_four : (6 : ℝ) < phi ^ 4 := by
  have h : (1.61 : ℝ) < phi := phi_gt_onePointSixOne
  have hpos : (0 : ℝ) < phi := phi_pos
  nlinarith [sq_nonneg (phi - 1.61), sq_nonneg (phi ^ 2 - (1.61 : ℝ) ^ 2)]

/-- The candidate is strictly below the sharp `1/6` envelope. -/
theorem thetaPhiFour_lt_one_sixth : thetaPhiFour < (1 : ℝ) / 6 := by
  unfold thetaPhiFour
  have h6 : (6 : ℝ) < phi ^ 4 := six_lt_phi_four
  have hphi4 : (0 : ℝ) < phi ^ 4 := pow_pos phi_pos 4
  have h6pos : (0 : ℝ) < (6 : ℝ) := by norm_num
  rw [div_lt_div_iff₀ hphi4 h6pos]
  nlinarith

What this page does not claim

The declaration does not claim that 1/φ⁴ equals the measured dark energy amplitude. The declaration does not claim that four-dimensional φ-dilution is a proven physical law. The declaration does not claim that the candidate is unique among possible dark energy amplitudes.

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