; GraphAtlas proof RS-05
; Statement: Beyond the first smoothing point, the weight of the last liquid forward rate, which is (1 - e^(-axh)) over axh, is above zero and not above one. It is not below 1 - axh/2, and axh times it is not above one.
; About: convergenceWeight in src/kernel/curve.ts, with a the convergence parameter and h the horizon in years, both above zero. The solver is told three facts about e^(-axh), each true for a positive axh: it is above 0 and below 1, it is at least 1 - axh, and it is at most 1 - axh + (axh)^2/2. It is given no more than these. 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.5
; 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 () Real)
(declare-fun horizon () Real)
(declare-fun alpha_times_horizon () Real)
(declare-fun exp_of_minus_alpha_horizon () Real)
(declare-fun weight_of_llfr () Real)
(assert (> alpha 0.0))
(assert (> horizon 0.0))
(assert (= alpha_times_horizon (* alpha horizon)))
(assert (> exp_of_minus_alpha_horizon 0.0))
(assert (< exp_of_minus_alpha_horizon 1.0))
(assert (>= exp_of_minus_alpha_horizon (- 1.0 alpha_times_horizon)))
(assert (<= exp_of_minus_alpha_horizon (+ (- 1.0 alpha_times_horizon) (* (/ 1.0 2.0) alpha_times_horizon alpha_times_horizon))))
(assert (= (* weight_of_llfr alpha horizon) (- 1.0 exp_of_minus_alpha_horizon)))

; Goal 1, negated
(push 1)
(assert (not (> weight_of_llfr 0.0)))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (<= weight_of_llfr 1.0)))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (>= weight_of_llfr (- 1.0 (* (/ 1.0 2.0) alpha_times_horizon)))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (<= (* weight_of_llfr alpha_times_horizon) 1.0)))
(check-sat)
(pop 1)