The de Sitter horizon
Λ = 3π / (ℓP² S) ⟺ S = A / (4ℓP²), A = 4π rH², rH = √(3/Λ) = c/|H|
Move the entropy S of the horizon and watch the cosmological constant, the horizon radius, the Hubble rate and the scale factor follow. Every number is tied to the Lean lemma that proves it.
122.514
branch σ
Λm⁻² · entropyCosmologicalConstant
r_H = √(3/Λ)
A = 12π/Λm² · deSitterHorizonArea_eq
H = σ√(Λ/3)c
S(Λ(S)) / SdeSitterEntropy_entropyCosmologicalConstant
H² − πc²/(ℓ²S)sq_hubbleConstant_entropyCosmologicalConstant (relative)
Λ(S) · cosmologicalConstant_eq_of_deSitterEntropy · entropyCosmologicalConstant_strictAntiOn
r_H and H² against S · deSitterHorizonRadius_eq_div_abs_hubbleConstant
a(t)/a₀ = exp(σ√(Λ/3)c t) · entropyCosmologicalConstant_first/secondOrderFriedmann (ρ = 0, p = 0, k = 0)
What Lean proves
| Lemma | Statement | Hypotheses |
|---|---|---|
| deSitterHorizonArea_eq | A = 12π/Λ | 0 < Λ |
| deSitterHorizonRadius_eq_div_abs_hubbleConstant | rH = c / |H| on the de Sitter solution | 0 < Λ, 0 < c, a₀ ≠ 0, σ = ±1 |
| deSitterEntropy_eq | S = 3π / (ℓ² Λ) | 0 < Λ |
| deSitterEntropy_pos | 0 < S | 0 < Λ, ℓ ≠ 0 |
| cosmologicalConstant_eq_of_deSitterEntropy | Λ = 3π / (ℓ² S) | 0 < Λ, ℓ ≠ 0 |
| deSitterEntropy_entropyCosmologicalConstant | the constant 3π/(ℓ²S) has horizon entropy exactly S | 0 < S, ℓ ≠ 0 |
| entropyCosmologicalConstant_firstOrderFriedmann | de Sitter with Λ = 3π/(ℓ²S) solves the first Friedmann equation | 0 < S, ℓ ≠ 0, a₀ ≠ 0, σ = ±1 |
| entropyCosmologicalConstant_secondOrderFriedmann | and the second Friedmann equation | same |
| sq_hubbleConstant_entropyCosmologicalConstant | H² = π c² / (ℓ² S) | same |
| entropyCosmologicalConstant_strictAntiOn | Λ is strictly decreasing in S on (0, ∞) | ℓ ≠ 0 |
The relation is the Gibbons–Hawking entropy (1977) of the de Sitter horizon. With the observed Λ it gives S ≈ 3.26 × 10¹²². It becomes a prediction only when S = log W is counted independently, without using Λ.