delta_w0_max
plain-language theorem explainer
The maximum BIT amplitude bound is defined as φ − 3/2, which equals J(φ) ≈ 0.118 with J the Recognition Science cost function. Cosmologists forecasting w(z) under BIT kernels for DESI Y3 analyses cite this value to restrict the amplitude δw₀ to the interval [0, J(φ)]. The declaration performs a direct real-number assignment drawn from the imported phi constant.
Claim. Define the maximum BIT amplitude by $J(φ) = φ - 3/2$, where $J(x) = (x + x^{-1})/2 - 1$ and $φ$ is the golden ratio satisfying $φ^2 = φ + 1$.
background
The module defines three kernel families for the BIT-induced redshift variation δw(z) = δw₀ · K(z), with K(z) equal to the constant 1, the canonical 1/(1 + z) form, or an exponential decay. Each kernel is normalized to 1 at z = 0 and bounded in [0, 1] for z ≥ 0, while the amplitude δw₀ is restricted to [0, J(φ)] by the BIT theorem. This supplies the explicit upper limit φ − 3/2 for the master certificate structure.
proof idea
The declaration is a definition that directly assigns the expression phi minus three halves. No lemmas or tactics are invoked; the value follows at once from the algebraic identity J(φ) = φ − 3/2 already available in the constants module.
why it matters
This supplies the concrete upper bound required by the BITKernelFamiliesCert structure, which asserts kernel normalization at zero together with positivity and the strict upper bound less than 1 on the amplitude. It implements the amplitude limit stated in the BIT theorem of §XXIV, connecting directly to J-uniqueness at T5 and the self-similar fixed point at T6 in the Unified Forcing Chain. The resulting small value keeps predicted w(z) variations inside the narrow alpha band consistent with D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.