Encyclopedia Cosmology Cosmology Dark Energy Phi Dilution Derivation Inv Phi Self Similar

ARTICLE 4 claims 4 theorems

Cosmology Dark Energy Phi Dilution Derivation Inv Phi Self Similar

A single equation, phi to the minus one equals one over one plus phi to the minus one, is the engine behind a derived value for dark energy's share of the universe.

The self-similar step

The golden ratio, usually written φ, is the number that solves x² = x + 1, roughly 1.618. Its reciprocal, 1/φ, is about 0.618. The theorem named inv_phi_self_similar in the Recognition Science library states a compact identity: 1/φ = 1 / (1 + 1/φ). This is not a new discovery about the golden ratio; it is a restatement of the defining equation. If you substitute 1/φ for x in the original relation, the identity follows immediately. The declaration's role is to make that substitution explicit inside a formal, machine-checked library of theorems, so that later arguments can rely on it without re-deriving it.

The identity matters because it describes a process of attenuation, a reduction in strength or occupancy. The equation says that a single step of reduction, by the factor 1/φ, leaves you in the same relationship to the next step: the reduced value is exactly what you get by applying the reduction again. In plain terms, each step shrinks the remaining amount by the same proportion, and that proportion is forced to be 1/φ by the equation itself. The library proves that any positive number satisfying this self-similarity condition must equal 1/φ. There is no other positive solution.

In Recognition Science, this single-step result becomes the foundation for a larger claim about cosmology. The framework models the universe as a ledger, a discrete record of recognition events, and defines an occupancy value that decreases as you account for more independent dimensions. The derivation assumes two things: occupancy across independent dimensions multiplies, and a single dimension attenuates by the self-similar step above. From those premises alone, the library proves that occupancy after n dimensions equals (1/φ)ⁿ. At the framework's forced spacetime dimension of four, this gives a dark-energy share of φ⁻⁴, roughly 0.146. The value is derived, not assumed.

The declaration itself does not claim anything about the physical universe. It establishes a mathematical identity about the golden ratio. The cosmological application comes from additional premises about how occupancy composes across dimensions and what the spacetime dimension is. Those premises are part of the framework, not part of the identity. The identity would hold regardless of whether dark energy exists. The framework's claim is that its model, built on this identity, produces a specific number for dark energy's share, and that this number matches the measured value within observational uncertainty. The match is an empirical check, not a consequence of the identity alone.

THEOREM inv_phi_self_similar · IndisputableMonolith/Cosmology/DarkEnergyPhiDilutionDerivation.lean
/-- The canonical attenuation `φ⁻¹` itself solves the reciprocal self-similarity equation.
Proof: apply `t ↦ 1/t` to the fixed-point identity `φ = 1 + 1/φ`. -/
theorem inv_phi_self_similar :
    (1 / Constants.phi) = 1 / (1 + 1 / Constants.phi) :=
  congrArg (fun t => 1 / t) PhiSupport.phi_fixed_point
THEOREM self_similar_attenuation_forced · IndisputableMonolith/Cosmology/DarkEnergyPhiDilutionDerivation.lean
/-- **The self-similar attenuation ratio is forced to `φ⁻¹`.** Any positive `ρ` solving the
reciprocal self-similarity equation `ρ = 1/(1+ρ)` equals `1/φ`. The proof routes through the
*scale-forcing* theorem: `1/ρ` solves `x = recipShift x` with `x > 1`, hence `1/ρ = φ`. -/
theorem self_similar_attenuation_forced {ρ : ℝ} (hpos : 0 < ρ)
    (hfp : ρ = 1 / (1 + ρ)) : ρ = 1 / Constants.phi := by
  have hsum_ne : (1 + ρ) ≠ 0 := by positivity
  have key : ρ * (1 + ρ) = 1 := by rwa [eq_div_iff hsum_ne] at hfp
  have hρ_lt_one : ρ < 1 := by nlinarith [key, hpos]
  have hx_gt_one : (1 : ℝ) < 1 / ρ := by
    have h := one_div_lt_one_div_of_lt hpos hρ_lt_one
    simpa using h
  have hfix : ReciprocalGenerator.recipShift (1 / ρ) = 1 / ρ := by
    unfold ReciprocalGenerator.recipShift ReciprocalGenerator.recip
    rw [one_div ρ, inv_inv]
    rw [eq_comm, inv_eq_one_div, div_eq_iff hpos.ne']
    linear_combination -key
  have hxphi : 1 / ρ = Constants.phi :=
    (ReciprocalGenerator.recipShift_fixed_iff hx_gt_one).mp hfix
  calc ρ = 1 / (1 / ρ) := (one_div_one_div ρ).symm
    _ = 1 / Constants.phi := by rw [hxphi]
THEOREM occ_eq_pow · IndisputableMonolith/Cosmology/DarkEnergyPhiDilutionDerivation.lean
/-- **The dilution law, derived.** `n` independent dimensions dilute by `φ⁻ⁿ`. -/
theorem occ_eq_pow : ∀ n : ℕ, L.occ n = (1 / Constants.phi) ^ n := by
  intro n
  induction n with
  | zero => rw [pow_zero]; exact L.occ_zero
  | succ k ih =>
      have hc := L.composes k 1
      rw [hc, ih, L.occ_one_eq_inv_phi, pow_succ]
THEOREM derivedTheta_eq_phiFour · IndisputableMonolith/Cosmology/DarkEnergyPhiDilutionDerivation.lean
/-- **Headline: `θ = φ⁻⁴` is forced.** Any dimension-uniform dilution law yields exactly the
four-dimensional φ-dilution `θ = φ⁻⁴` at the forced spacetime dimension. -/
theorem derivedTheta_eq_phiFour (L : DimensionUniformDilution) :
    derivedTheta L = DarkEnergyThetaPhiFour.thetaPhiFour := by
  unfold derivedTheta
  rw [L.occ_eq_pow, dilutionExponent_eq_four]
  unfold DarkEnergyThetaPhiFour.thetaPhiFour
  rw [div_pow, one_pow]

What this page does not claim

The identity alone does not imply anything about dark energy in the physical universe. The framework does not claim to derive the value of the cosmological constant from first principles. The match between φ⁻⁴ and measured dark energy is an empirical observation, not a theorem.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND