bitCorrectionBound
Recognition Science cosmology predicts the dark energy equation of state w_0 lies in the open interval (-1 - J(phi), -1). The bitCorrectionBound supplies the explicit numerical value of the upper limit on |delta w| as the algebraic expression 1/phi - 3/2 + 1, which equals J(phi) to the stated approximation of 0.118. Cosmologists fitting supernova or BAO data within the RS framework would cite this number when constraining w_0. The declaration is a direct definition with no lemmas or tactics.
claimThe BIT correction bound is the real number $1/phi - 3/2 + 1$, which equals $J(phi) approx 0.118$ and satisfies $|delta w| leq J(phi)$ where $J(x) = (x + x^{-1})/2 - 1$ and $phi$ is the golden-ratio fixed point.
background
The module models dark energy as a BIT correction that shifts the equation-of-state parameter away from the cosmological-constant value -1 inside an S3 geometry. The J-function quantifies the recognition defect between scales via the Recognition Composition Law, while phi is the unique self-similar fixed point forced at step T6 of the unified forcing chain. The local setting asserts that w_0 belongs to the interval (-1 - J(phi), -1) with the deviation bounded by the value drawn from the OmegaLambdaBITKernelBand construction.
proof idea
The declaration is a direct noncomputable definition that evaluates the closed algebraic expression 1/phi - 3/2 + 1 without applying any lemmas or tactics.
why it matters in Recognition Science
This bound translates the abstract J-uniqueness result from the forcing chain (T5) into a concrete numerical threshold for the dark energy parameter. It anchors the certification of the five dark energy models and the darkEnergyEoSCert predicate listed among the module siblings. The value sits inside the RS-native alpha band and supplies the testable interval required by the Omega Lambda BIT kernel.
scope and limits
- Does not derive the J(phi) expression from the Recognition Composition Law.
- Does not compare the numerical bound against any specific cosmological dataset.
- Does not prove that the actual deviation saturates the bound for any model.
formal statement (Lean)
27noncomputable def bitCorrectionBound : ℝ := 1 / phi - 3 / 2 + 1 -- approximate J(φ) ≈ 0.118
proof body
Definition body.
28
29/-- Five dark energy models. -/