DarkEnergyPredictions
plain-language theorem explainer
The declaration defines a structure that packages the four Recognition Science predictions for dark energy. A cosmologist working inside the RS ledger model would cite it to record that the equation of state is fixed at w = -1, that Lambda scales exactly with H0 squared, and that the component is emergent from the start of expansion. The definition is assembled directly from the module's core ledger-tension insight with no separate proof steps.
Claim. A structure whose fields are the equation-of-state parameter $w$ (a real number), a string describing the scaling of the cosmological constant in terms of the present Hubble parameter $H_0$, and a string classifying the physical nature of dark energy.
background
The module COS-006 derives the cosmological constant from ledger tension: the global J-cost balance requirement must hold while cosmic expansion continually creates new spacetime volume that needs fresh ledger entries. The residual cost per unit volume of maintaining coherence across this expanding ledger is identified with Lambda. Upstream structures supply the necessary J-cost calibration (LedgerFactorization.of), the phi-ladder placement of densities (NucleosynthesisTiers.of), and the self-reference axioms that force the ledger to close (UniversalForcingSelfReference.for).
proof idea
One-line structure definition that directly records the four predictions listed in the module doc-comment; no tactics or lemmas are applied.
why it matters
It supplies the concrete object instantiated by the downstream definition rsPredictions, thereby completing the COS-006 ledger-tension derivation. The structure encodes the framework landmarks that Lambda is set by the ratio of Planck to Hubble scales (mediated by phi) and that no fifth force appears at large distances. It touches the open question of whether the same ledger mechanism can be quantized without reintroducing the usual vacuum-energy divergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.