horizon_states_exclusive
plain-language theorem explainer
horizon_states_exclusive shows that no uncertainty ratio r can satisfy both IsWithinHorizon and IsPastHorizon at once. Climate modelers would cite it to certify that the J-cost threshold produces a sharp, non-overlapping predictability cutoff. The argument assumes the conjunction of the two predicates and immediately derives a contradiction from the irreflexivity of strict inequality.
Claim. For every real number $r$, it is impossible that the forecast cost of $r$ is strictly below the predictability threshold while the predictability threshold is at most the forecast cost of $r$.
background
The Climate.PredictabilityFromJCost module defines the predictability horizon via the J-cost on the initial-condition uncertainty ratio $r$. IsWithinHorizon $r$ holds precisely when forecastCost $r$ is strictly less than PredictabilityThreshold; IsPastHorizon $r$ holds when PredictabilityThreshold is less than or equal to forecastCost $r$. This construction follows the Recognition Science treatment in which deterministic forecast skill persists only while J-cost remains below the golden-section quantum $J(φ) ∈ (0.11, 0.13)$. The proof invokes the upstream lemma lt_irrefl, which states that no element is strictly less than itself.
proof idea
The proof is a term-mode one-liner. It introduces the assumed conjunction via rintro, applies lt_of_lt_of_le to obtain forecastCost $r$ < forecastCost $r$, and refutes the result with lt_irrefl.
why it matters
The theorem supplies the mutual-exclusivity clause required by the downstream climatePredictabilityCert certificate. It guarantees that the J-cost threshold functions as a sharp boundary rather than an overlapping region, consistent with the universal RS quantum that gates skill loss, plaque vulnerability, combustion ignition, and magnetic reconnection. The result closes the logical structure needed for the eight-tick octave and phi-ladder predictions to apply cleanly to climate forecast horizons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.