Pith. sign in
module module moderate

IndisputableMonolith.Verification.HubbleTensionCert

show as:
view Lean formalization →

Verification certificate module for the Recognition Science account of the Hubble tension and dark-energy density. It packages the Cosmology.HubbleTension derivation (T13) into a checkable cert object so auditors can confirm the ledger-geometry claims without replaying the full cosmology stack. The module is thin: import plus a named certificate wrapper.

claimA verification certificate for the RS derivation that the early-universe expansion rate $H_{\mathrm{early}}\approx 67.4\,\mathrm{km\,s^{-1}Mpc^{-1}}$ and the dark-energy density follow from ledger geometry, packaging the T13 Hubble-tension formalization for downstream audit.

background

Recognition Science treats cosmology as a readout of ledger geometry on the phi-ladder. The upstream module Cosmology.HubbleTension (T13) formalizes the Hubble tension and dark-energy density from that geometry: observations disagree between an early-universe expansion rate $H_{\mathrm{early}}\approx 67.4$ and local measurements, and RS derives both the split and the dark-energy density from the same cost structure that forces $J$, $\varphi$, the eight-tick octave, and $D=3$.

This Verification module sits one layer above that derivation. It does not restate the forcing chain; it only exposes a certificate object so that the T13 claims can be named and checked in the verification graph. Imports are Mathlib plus Cosmology.HubbleTension.

proof idea

Definition and certificate packaging module, not a proof development. It imports Cosmology.HubbleTension and exposes a sibling certificate (HubbleTensionCert) that witnesses the T13 Hubble-tension and dark-energy claims for the verification layer. No independent lemmas or tactic scripts live here; the mathematical content remains upstream.

why it matters in Recognition Science

Gives the verification domain a named handle on T13 (Hubble tension and dark energy from ledger geometry). Downstream used-by edges are empty in the current graph, so the cert is an audit endpoint rather than an intermediate lemma. It ties the observational $H_{\mathrm{early}}\approx 67.4$ discrepancy and the dark-energy density claim into the same RS stack that forces $J(x)=\cosh(\log x)-1$, $\varphi$, and the eight-tick structure, without reopening those uniqueness proofs.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (1)