Pith. sign in
module module moderate

IndisputableMonolith.Verification.Preregistered.Hubble.Prediction

show as:
view Lean formalization →

Preregistered Hubble-sector predictions: a frozen hubble_ratio and Ω_Λ, defined without importing any measurement module. Auditors and cosmologists cite it to show the formulas were locked before data. Structure is pure definition against RS constants (and α), not a proved equality to observation.

claimThe module exposes two preregistered quantities: a Hubble ratio (RS prediction versus a fixed reference scale) and the dark-energy density parameter $\Omega_\Lambda$, both written only in terms of Recognition Science constants, with no dependence on measurement modules.

background

Under the preregistered test harness, predictions must live in modules that do not import measurement data. Core states the design goal explicitly: enforce “formula frozen before measurement” structurally; predictions, measurements, and tests are separated, and only tests import both.

This module sits on that prediction side for the Hubble sector. It pulls RS-native constants (including the time quantum and the α stack) and names the two frozen objects used downstream: hubble_ratio and omega_lambda. Nothing here compares to survey values; that comparison is deferred.

Local setting is verification infrastructure, not a derivation of FLRW dynamics. The point is auditability of claim timing, not a new cosmological derivation.

proof idea

Definition and prediction module, not a theorem module. It binds hubble_ratio and omega_lambda to closed-form expressions in the imported Constants / Alpha layer. No measurement lemmas are applied; there is no tactic proof obligation beyond whatever trivial equalities the constant definitions already carry.

why it matters in Recognition Science

Feeds IndisputableMonolith.Verification.Preregistered.Hubble.Test, whose doc-comment states the checks: Hubble ratio (relative error) and Ω_Λ (within 1σ). Without this separation, a referee could not tell whether the formulas were adjusted after seeing data. In the broader RS verification stack it is the Hubble instance of the preregistered pattern: freeze the claim, isolate the data, then test. It does not itself close the Hubble tension; it only locks the predicted side of that comparison.

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)