t_universe
plain-language theorem explainer
The definition supplies the numerical age of the universe in seconds for scaling Planck quantities to cosmic scales in Recognition Science derivations of dark energy. Cosmologists modeling ledger tension would cite it when computing the suppression factor between tau0 and the Hubble time. The assignment is a direct constant definition with no reduction steps or lemmas.
Claim. Let $t_0$ denote the age of the universe in seconds, assigned the numerical value $4.3 times 10^{17}$.
background
The Cosmology.DarkEnergy module derives the cosmological constant from ledger tension: the J-cost per unit volume required to keep the global ledger balanced while expansion creates new spacetime volume. J-cost is the functional J(x) = (x + x^{-1})/2 - 1 drawn from the Recognition Composition Law and PhiForcingDerived. Upstream structures include the phi-tier discretization of nuclear densities from NucleosynthesisTiers.of and the ledger factorization from DAlembert.LedgerFactorization.of.
proof idea
Direct numerical definition. No lemmas or tactics are applied; the value is a hardcoded approximation to 13.8 billion years in seconds.
why it matters
This supplies the cosmic timescale used by cosmicRatio, cosmic_ratio_large, lambda_order_of_magnitude and the two hypotheses in CosmologicalConstant. It implements the (tau0 / t_universe)^2 suppression that bridges Planck and Hubble scales in the ledger-tension model for Lambda, consistent with the phi-ladder and the target Nature paper on dark energy from ledger tension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.