Pith. sign in
module module moderate

IndisputableMonolith.Verification.Preregistered.Hubble.Prediction

show as:
view Lean formalization →

Preregistered Recognition Science predictions for the Hubble ratio and the dark-energy density parameter Ω_Λ. Cosmologists auditing RS against late-universe data cite these frozen formulas. The module only exposes the prediction values; it imports no measurement data, enforcing the structural preregistration split from the test harness core.

claimThe module freezes the Recognition Science predictions for the Hubble ratio $H_{\mathrm{RS}}/H_{\mathrm{obs}}$ and the dark-energy density parameter $\Omega_\Lambda$, with no dependence on measured cosmological data.

background

The preregistered test harness separates three layers: prediction modules, pure measurement modules, and tests that import both. The design goal is to enforce “formula frozen before measurement” structurally, so a prediction file cannot silently depend on the numbers it will later be scored against.

This module sits in the prediction layer for late-universe cosmology. It pulls RS-native constants (including the fine-structure infrastructure from Constants.Alpha and the tick quantum from Constants) and exposes two named prediction objects: the Hubble ratio and $\Omega_\Lambda$. No observational catalogs or likelihood code appear in its import graph.

Sibling names in the module are hubble_ratio and omega_lambda. Downstream tests compare those frozen values to data under relative-error and $1\sigma$ criteria.

proof idea

This is a prediction/definition module, not a theorem module. It declares the frozen RS formulas for the Hubble ratio and $\Omega_\Lambda$ from the constants layer. There is no tactic proof body to walk; the content is the preregistered numeric or closed-form predictions themselves, kept free of measurement imports.

why it matters in Recognition Science

Without a sealed prediction module, any Hubble or $\Omega_\Lambda$ comparison could be accused of post-hoc tuning. This file is the sealed side of that split. It is imported by Verification.Preregistered.Hubble.Test, whose stated job is to score the Hubble ratio on relative error and $\Omega_\Lambda$ within $1\sigma$.

In the broader RS stack the predictions ultimately rest on the forced constants (phi-ladder, alpha band, RS-native $c$, $\hbar$, $G$). The module itself does not re-derive those constants; it only freezes the cosmological outputs so the test layer can audit them cleanly against data.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (2)