; GraphAtlas proof RS-07
; Statement: Beyond the first smoothing point, the zero rate of each horizon lies between the zero rate at the point and the forward rate of that horizon. It is nearer to the one that covers more years, which is the forward rate when the horizon is longer than the point and the zero rate at the point when it is shorter.
; About: extrapolate in src/kernel/curve.ts, with the horizon and the point in years, both above zero. The zero rate is the total of the zero rate at the point times the point and the forward rate times the horizon, divided by the years of both. The quotient is written as the number whose product with its divisor is the dividend, which for a divisor above zero is the same number.
; Source: EIOPA-BoS-26-198, technical documentation of May 2026, Paragraph 8.5.7
; Expected: unsat for each of the 4 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun horizon () Real)
(declare-fun first_smoothing_point () Real)
(declare-fun forward_rate () Real)
(declare-fun zero_rate_at_the_point () Real)
(declare-fun zero_rate () Real)
(assert (> horizon 0.0))
(assert (> first_smoothing_point 0.0))
(assert (= (* zero_rate (+ first_smoothing_point horizon)) (+ (* first_smoothing_point zero_rate_at_the_point) (* horizon forward_rate))))

; Goal 1, negated
(push 1)
(assert (not (or (>= zero_rate zero_rate_at_the_point) (>= zero_rate forward_rate))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (or (<= zero_rate zero_rate_at_the_point) (<= zero_rate forward_rate))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (<= (ite (>= (- zero_rate forward_rate) 0.0) (- zero_rate forward_rate) (- (- zero_rate forward_rate))) (ite (>= (- zero_rate zero_rate_at_the_point) 0.0) (- zero_rate zero_rate_at_the_point) (- (- zero_rate zero_rate_at_the_point)))))) (=> (>= horizon first_smoothing_point) a!1))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (let ((a!1 (<= (ite (>= (- zero_rate zero_rate_at_the_point) 0.0) (- zero_rate zero_rate_at_the_point) (- (- zero_rate zero_rate_at_the_point))) (ite (>= (- zero_rate forward_rate) 0.0) (- zero_rate forward_rate) (- (- zero_rate forward_rate)))))) (=> (>= first_smoothing_point horizon) a!1))))
(check-sat)
(pop 1)