; GraphAtlas proof RS-06
; Statement: Beyond the first smoothing point, the forward rate of each horizon lies between the last liquid forward rate and the ultimate forward rate. Its distance from the first is at most axh/2 of the distance between the two, and its distance from the second is at most 1/(axh) of it.
; About: forwardFromFsp and extrapolate in src/kernel/curve.ts, with a the convergence parameter and h the horizon in years. The weight of the last liquid forward rate is given the four facts that the previous proof shows of it, and no more. The ultimate rate is written as the last liquid rate plus the distance between the two, which is a number of its own. Any pair of rates is such a pair.
; Source: EIOPA-BoS-26-198, technical documentation of May 2026, Paragraphs 8.5.5 and 8.5.6
; Expected: unsat for each of the 4 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun alpha_times_horizon () Real)
(declare-fun weight_of_llfr () Real)
(declare-fun llfr () Real)
(declare-fun ufr_less_llfr () Real)
(declare-fun forward_rate () Real)
(assert (> alpha_times_horizon 0.0))
(assert (> weight_of_llfr 0.0))
(assert (<= weight_of_llfr 1.0))
(assert (>= weight_of_llfr (- 1.0 (* (/ 1.0 2.0) alpha_times_horizon))))
(assert (<= (* weight_of_llfr alpha_times_horizon) 1.0))
(assert (let ((a!1 (+ (* (+ llfr ufr_less_llfr) (- 1.0 weight_of_llfr)) (* llfr (- 1.0 (- 1.0 weight_of_llfr)))))) (= forward_rate a!1)))

; Goal 1, negated
(push 1)
(assert (not (>= (* (- forward_rate llfr) ufr_less_llfr) 0.0)))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (>= (* (- (+ llfr ufr_less_llfr) forward_rate) ufr_less_llfr) 0.0)))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (<= (* (- forward_rate llfr) ufr_less_llfr) (* (/ 1.0 2.0) alpha_times_horizon ufr_less_llfr ufr_less_llfr))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (<= (* (- (+ llfr ufr_less_llfr) forward_rate) ufr_less_llfr alpha_times_horizon) (* ufr_less_llfr ufr_less_llfr))))
(check-sat)
(pop 1)