; GraphAtlas proof IC-02
; Statement: With a mortality charge M above zero and a longevity charge L, and nothing else in the life risks, the quantity under the root of the life charge is M^2 + L^2 - M x L / 2. It is below M^2 for any L above zero and below M / 2, it equals M^2 at M / 2, and it is above M^2 beyond. It is lowest at L = M / 4, where it is 15/16 of M^2. A longevity charge of a quarter of the mortality charge therefore lowers the life charge by 3.2 per cent, and a larger one lowers the requirement too, as long as it is below half.
; About: icsRequirement in src/kernel/ics.ts, through aggregate in src/kernel/aggregate.ts, with LIFE_CORRELATION_TEXT as exact decimals and the charges of morbidity, lapse and expense at zero. The form is M^2 + L^2 + 2 x rho x M x L with rho the entry of Table 6 between mortality and longevity, which is -0.25. The difference from M^2 is L x (L - M / 2), whose sign is that of L less M / 2.
; Source: IAIS Insurance Capital Standard, Level 2 text of 5 December 2024, L2-143
; Expected: unsat for each of the 5 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun mortality_charge () Real)
(declare-fun longevity_charge () Real)
(assert (> mortality_charge 0.0))
(assert (>= longevity_charge 0.0))

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (* 0.0 (+ (+ 0.0 (* (/ 1.0 4.0) mortality_charge)) (* 0.0 longevity_charge) (* 1.0 0.0) (* 0.0 0.0) (* (/ 1.0 2.0) 0.0)))) (a!2 (* 0.0 (+ (+ 0.0 (* (/ 1.0 4.0) mortality_charge)) (* (/ 1.0 4.0) longevity_charge) (* (/ 1.0 2.0) 0.0) (* (/ 1.0 2.0) 0.0) (* 1.0 0.0))))) (let ((a!3 (+ 0.0 (* mortality_charge (+ 0.0 (* 1.0 mortality_charge) (* (- (/ 1.0 4.0)) longevity_charge) (* (/ 1.0 4.0) 0.0) (* 0.0 0.0) (* (/ 1.0 4.0) 0.0))) (* longevity_charge (+ 0.0 (* (- (/ 1.0 4.0)) mortality_charge) (* 1.0 longevity_charge) (* 0.0 0.0) (* (/ 1.0 4.0) 0.0) (* (/ 1.0 4.0) 0.0))) a!1 (* 0.0 (+ 0.0 (* 0.0 mortality_charge) (* (/ 1.0 4.0) longevity_charge) (* 0.0 0.0) (* 1.0 0.0) (* (/ 1.0 2.0) 0.0))) a!2))) (=> (and (> longevity_charge 0.0) (< longevity_charge (* mortality_charge (/ 1.0 2.0)))) (< a!3 (* mortality_charge mortality_charge)))))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (* 0.0 (+ (+ 0.0 (* (/ 1.0 4.0) mortality_charge)) (* 0.0 longevity_charge) (* 1.0 0.0) (* 0.0 0.0) (* (/ 1.0 2.0) 0.0)))) (a!2 (* 0.0 (+ (+ 0.0 (* (/ 1.0 4.0) mortality_charge)) (* (/ 1.0 4.0) longevity_charge) (* (/ 1.0 2.0) 0.0) (* (/ 1.0 2.0) 0.0) (* 1.0 0.0))))) (let ((a!3 (+ 0.0 (* mortality_charge (+ 0.0 (* 1.0 mortality_charge) (* (- (/ 1.0 4.0)) longevity_charge) (* (/ 1.0 4.0) 0.0) (* 0.0 0.0) (* (/ 1.0 4.0) 0.0))) (* longevity_charge (+ 0.0 (* (- (/ 1.0 4.0)) mortality_charge) (* 1.0 longevity_charge) (* 0.0 0.0) (* (/ 1.0 4.0) 0.0) (* (/ 1.0 4.0) 0.0))) a!1 (* 0.0 (+ 0.0 (* 0.0 mortality_charge) (* (/ 1.0 4.0) longevity_charge) (* 0.0 0.0) (* 1.0 0.0) (* (/ 1.0 2.0) 0.0))) a!2))) (=> (= longevity_charge (* mortality_charge (/ 1.0 2.0))) (= a!3 (* mortality_charge mortality_charge)))))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (* 0.0 (+ (+ 0.0 (* (/ 1.0 4.0) mortality_charge)) (* 0.0 longevity_charge) (* 1.0 0.0) (* 0.0 0.0) (* (/ 1.0 2.0) 0.0)))) (a!2 (* 0.0 (+ (+ 0.0 (* (/ 1.0 4.0) mortality_charge)) (* (/ 1.0 4.0) longevity_charge) (* (/ 1.0 2.0) 0.0) (* (/ 1.0 2.0) 0.0) (* 1.0 0.0))))) (let ((a!3 (+ 0.0 (* mortality_charge (+ 0.0 (* 1.0 mortality_charge) (* (- (/ 1.0 4.0)) longevity_charge) (* (/ 1.0 4.0) 0.0) (* 0.0 0.0) (* (/ 1.0 4.0) 0.0))) (* longevity_charge (+ 0.0 (* (- (/ 1.0 4.0)) mortality_charge) (* 1.0 longevity_charge) (* 0.0 0.0) (* (/ 1.0 4.0) 0.0) (* (/ 1.0 4.0) 0.0))) a!1 (* 0.0 (+ 0.0 (* 0.0 mortality_charge) (* (/ 1.0 4.0) longevity_charge) (* 0.0 0.0) (* 1.0 0.0) (* (/ 1.0 2.0) 0.0))) a!2))) (=> (> longevity_charge (* mortality_charge (/ 1.0 2.0))) (> a!3 (* mortality_charge mortality_charge)))))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (let ((a!1 (* 0.0 (+ (+ 0.0 (* (/ 1.0 4.0) mortality_charge)) (* 0.0 longevity_charge) (* 1.0 0.0) (* 0.0 0.0) (* (/ 1.0 2.0) 0.0)))) (a!2 (* 0.0 (+ (+ 0.0 (* (/ 1.0 4.0) mortality_charge)) (* (/ 1.0 4.0) longevity_charge) (* (/ 1.0 2.0) 0.0) (* (/ 1.0 2.0) 0.0) (* 1.0 0.0))))) (let ((a!3 (+ 0.0 (* mortality_charge (+ 0.0 (* 1.0 mortality_charge) (* (- (/ 1.0 4.0)) longevity_charge) (* (/ 1.0 4.0) 0.0) (* 0.0 0.0) (* (/ 1.0 4.0) 0.0))) (* longevity_charge (+ 0.0 (* (- (/ 1.0 4.0)) mortality_charge) (* 1.0 longevity_charge) (* 0.0 0.0) (* (/ 1.0 4.0) 0.0) (* (/ 1.0 4.0) 0.0))) a!1 (* 0.0 (+ 0.0 (* 0.0 mortality_charge) (* (/ 1.0 4.0) longevity_charge) (* 0.0 0.0) (* 1.0 0.0) (* (/ 1.0 2.0) 0.0))) a!2))) (=> (= longevity_charge (* mortality_charge (/ 1.0 4.0))) (= a!3 (* (/ 15.0 16.0) mortality_charge mortality_charge)))))))
(check-sat)
(pop 1)

; Goal 5, negated
(push 1)
(assert (not (let ((a!1 (* 0.0 (+ (+ 0.0 (* (/ 1.0 4.0) mortality_charge)) (* 0.0 longevity_charge) (* 1.0 0.0) (* 0.0 0.0) (* (/ 1.0 2.0) 0.0)))) (a!2 (* 0.0 (+ (+ 0.0 (* (/ 1.0 4.0) mortality_charge)) (* (/ 1.0 4.0) longevity_charge) (* (/ 1.0 2.0) 0.0) (* (/ 1.0 2.0) 0.0) (* 1.0 0.0))))) (let ((a!3 (+ 0.0 (* mortality_charge (+ 0.0 (* 1.0 mortality_charge) (* (- (/ 1.0 4.0)) longevity_charge) (* (/ 1.0 4.0) 0.0) (* 0.0 0.0) (* (/ 1.0 4.0) 0.0))) (* longevity_charge (+ 0.0 (* (- (/ 1.0 4.0)) mortality_charge) (* 1.0 longevity_charge) (* 0.0 0.0) (* (/ 1.0 4.0) 0.0) (* (/ 1.0 4.0) 0.0))) a!1 (* 0.0 (+ 0.0 (* 0.0 mortality_charge) (* (/ 1.0 4.0) longevity_charge) (* 0.0 0.0) (* 1.0 0.0) (* (/ 1.0 2.0) 0.0))) a!2))) (>= a!3 (* (/ 15.0 16.0) mortality_charge mortality_charge))))))
(check-sat)
(pop 1)