forecastSkill_pos
plain-language theorem explainer
The theorem asserts that forecast skill at horizon k remains strictly positive for every natural number k. Climate researchers applying Recognition Science to operational forecasting would cite it to confirm that skill measures stay positive across all horizons in the phi-ladder model. The proof is a one-line wrapper that applies the positivity of inverses to the positivity of phi raised to the k power.
Claim. For every natural number $k$, $0 < phi^{-k}$, where $phi$ is the self-similar fixed point of the Recognition Science forcing chain.
background
The Climate Forecast Skill from J-Cost module defines forecast skill explicitly as the reciprocal of phi to the power k. This encodes the operational decay of weather and climate forecast accuracy along the phi-ladder, with adjacent-horizon skill ratios approximately 1/phi, five canonical timescales matching configDim D = 5, and consistency with the Lorenz limit near 14 days. The upstream definition states forecastSkill (k : ℕ) : ℝ := (phi ^ k)⁻¹, supplying the concrete expression whose positivity is asserted here.
proof idea
The proof is a one-line wrapper that applies inv_pos.mpr to pow_pos phi_pos k. It invokes the lemma that the multiplicative inverse of a positive real number is positive, together with the fact that phi raised to any natural power remains positive.
why it matters
This supplies the skill_pos component inside the climateForecastCert definition, which assembles the five-timescale count, positive skill, decay law, and Lorenz limit into a single certificate. It closes the positivity requirement for the phi-ladder decay prediction in the climate setting, aligning with the self-similar fixed point forced at T6 and the eight-tick octave structure of the Unified Forcing Chain. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.