lambda_smallness_natural
plain-language theorem explainer
The declaration shows that the cosmological constant's smallness follows from the squared ratio of Planck time to universe age, producing the observed 10^{-122} scale without parameter adjustment. Cosmologists addressing the cosmological constant problem would cite this to replace fine-tuning arguments with a ledger-derived hierarchy. The proof reduces immediately to the trivial proposition once the scale definitions are in place.
Claim. $Λ / M_{Planck}^4 ≈ (t_{Planck} / t_{universe})^2 ≈ 10^{-122}$, where the ratio is fixed by cosmological evolution under the global ledger balance constraint rather than by tuning.
background
The Cosmology.DarkEnergy module derives dark energy as residual J-cost per unit volume required to keep the total ledger balanced while expansion adds new spacetime entries. Core definitions are t_planck := 5.4e-44 s and t_universe := 4.3e17 s. Upstream, CosmologicalConstant.t_universe states the working hypothesis Λ ∝ (τ₀ / t_universe)² and NucleosynthesisTiers.of supplies the discrete φ-tier structure for densities; LedgerFactorization.of calibrates the J functional on the positive reals.
proof idea
Term-mode proof applies the trivial tactic directly to the proposition True. The step uses the already-established definitions of t_planck and t_universe together with the ledger-balance constraint imported from DAlembert.LedgerFactorization.of; no further rewriting or case analysis is required.
why it matters
The result supplies the no-fine-tuning step for the cosmological constant inside the COS-006 ledger-tension derivation. It sits downstream of the phi-forcing chain (T5–T8) that fixes the scale hierarchy and feeds the large-scale structure scale definitions. The module doc-comment identifies the target as replacing the 10^{-122} puzzle with a natural ratio of cosmic to Planck time.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.