delta_pos

The module treats the first subleading correction to the RS baryon asymmetry η_B = φ⁻⁴⁴. That leading value sits about 4.5% above the Planck 2018 CMB central value; with no free parameters the gap cannot be tuned, so the module studies an 8-tick washout during the electroweak epoch.

Sphalerons are taken to run for N_sph ≈ φ⁸ cycles of the eight-tick octave. Each cycle the recognition operator reduces defect by a factor δ, defined here as φ⁻⁸ (one φ-ladder rung per active period). The net first-order factor is then roughly (1 − δ), giving η_B⁽¹⁾ = φ⁻⁴⁴(1 − φ⁻⁸).

Positivity of δ is the elementary real-arithmetic fact needed before one can conclude 1 − δ < 1. It rests only on φ > 0, which follows from φ being the self-similar fixed point forced at T6.

One-line term proof. Instantiate Mathlib's zpow_pos at base φ and exponent −8, feeding the existing lemma that φ > 0. No unfolding of δ beyond its definition as φ^(−8) is required.

Immediate parent is correction_factor_lt_one, which unfolds the correction factor as 1 − δ and finishes by linear arithmetic from this positivity fact; that in turn supports the interval certificate that the factor lies in (0, 1). Those bounds are what turn the 8-tick washout sketch into a concrete first-order shift of η_B (from ~6.38×10⁻¹⁰ toward ~6.28×10⁻¹⁰), partially closing the 4.5% CMB gap.

Framework landmarks in play are T6 (φ forced) and T7 (eight-tick octave): δ is exactly one negative octave rung. The surrounding washout mechanism remains hypothesis-level, with the module's stated falsifier bands on measured η_B.