; GraphAtlas proof IC-01
; Statement: For any five charges of the life risks that are not below zero, the quantity under the root of the life charge, which is the form of Table 6 of the Level 2 text, is at least 15/16 of the square of each charge and at most the square of their sum. So the life charge is never below the root of 15/16, which is 96.8 per cent, of its largest charge, and never above the sum of the charges. The floor is reached with a mortality charge of 4 and a longevity charge of 1, so that no higher floor can be proved.
; About: icsRequirement in src/kernel/ics.ts, through aggregate in src/kernel/aggregate.ts, with LIFE_CORRELATION_TEXT as exact decimals. Table 6 has one entry below zero, minus 25 per cent between mortality and longevity, and every other entry is between 0 and 1. The key steps are that 16 x L^2 - 8 x M x L + M^2 is the square of M - 4 x L, which gives M^2 + L^2 - M x L / 2 at least 15/16 of M^2, and the square of 4 x M - L, which gives the same for L^2. The products of two charges are not below zero, so every other term only adds. The lemmas state the squares and the products and the solver adds them up.
; Source: IAIS Insurance Capital Standard, Level 2 text of 5 December 2024, L2-143
; Expected: unsat for each of the 24 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)
(declare-fun morbidity_charge () Real)
(declare-fun lapse_charge () Real)
(declare-fun expense_charge () Real)
(assert (>= mortality_charge 0.0))
(assert (>= longevity_charge 0.0))
(assert (>= morbidity_charge 0.0))
(assert (>= lapse_charge 0.0))
(assert (>= expense_charge 0.0))

; Lemma 1, negated
(push 1)
(assert (not (>= (* mortality_charge mortality_charge) 0.0)))
(check-sat)
(pop 1)
; Lemma 1 holds, so later checks may use it
(assert (>= (* mortality_charge mortality_charge) 0.0))

; Lemma 2, negated
(push 1)
(assert (not (>= (* longevity_charge longevity_charge) 0.0)))
(check-sat)
(pop 1)
; Lemma 2 holds, so later checks may use it
(assert (>= (* longevity_charge longevity_charge) 0.0))

; Lemma 3, negated
(push 1)
(assert (not (>= (* morbidity_charge morbidity_charge) 0.0)))
(check-sat)
(pop 1)
; Lemma 3 holds, so later checks may use it
(assert (>= (* morbidity_charge morbidity_charge) 0.0))

; Lemma 4, negated
(push 1)
(assert (not (>= (* lapse_charge lapse_charge) 0.0)))
(check-sat)
(pop 1)
; Lemma 4 holds, so later checks may use it
(assert (>= (* lapse_charge lapse_charge) 0.0))

; Lemma 5, negated
(push 1)
(assert (not (>= (* expense_charge expense_charge) 0.0)))
(check-sat)
(pop 1)
; Lemma 5 holds, so later checks may use it
(assert (>= (* expense_charge expense_charge) 0.0))

; Lemma 6, negated
(push 1)
(assert (not (>= (* mortality_charge longevity_charge) 0.0)))
(check-sat)
(pop 1)
; Lemma 6 holds, so later checks may use it
(assert (>= (* mortality_charge longevity_charge) 0.0))

; Lemma 7, negated
(push 1)
(assert (not (>= (* mortality_charge morbidity_charge) 0.0)))
(check-sat)
(pop 1)
; Lemma 7 holds, so later checks may use it
(assert (>= (* mortality_charge morbidity_charge) 0.0))

; Lemma 8, negated
(push 1)
(assert (not (>= (* mortality_charge lapse_charge) 0.0)))
(check-sat)
(pop 1)
; Lemma 8 holds, so later checks may use it
(assert (>= (* mortality_charge lapse_charge) 0.0))

; Lemma 9, negated
(push 1)
(assert (not (>= (* mortality_charge expense_charge) 0.0)))
(check-sat)
(pop 1)
; Lemma 9 holds, so later checks may use it
(assert (>= (* mortality_charge expense_charge) 0.0))

; Lemma 10, negated
(push 1)
(assert (not (>= (* longevity_charge morbidity_charge) 0.0)))
(check-sat)
(pop 1)
; Lemma 10 holds, so later checks may use it
(assert (>= (* longevity_charge morbidity_charge) 0.0))

; Lemma 11, negated
(push 1)
(assert (not (>= (* longevity_charge lapse_charge) 0.0)))
(check-sat)
(pop 1)
; Lemma 11 holds, so later checks may use it
(assert (>= (* longevity_charge lapse_charge) 0.0))

; Lemma 12, negated
(push 1)
(assert (not (>= (* longevity_charge expense_charge) 0.0)))
(check-sat)
(pop 1)
; Lemma 12 holds, so later checks may use it
(assert (>= (* longevity_charge expense_charge) 0.0))

; Lemma 13, negated
(push 1)
(assert (not (>= (* morbidity_charge lapse_charge) 0.0)))
(check-sat)
(pop 1)
; Lemma 13 holds, so later checks may use it
(assert (>= (* morbidity_charge lapse_charge) 0.0))

; Lemma 14, negated
(push 1)
(assert (not (>= (* morbidity_charge expense_charge) 0.0)))
(check-sat)
(pop 1)
; Lemma 14 holds, so later checks may use it
(assert (>= (* morbidity_charge expense_charge) 0.0))

; Lemma 15, negated
(push 1)
(assert (not (>= (* lapse_charge expense_charge) 0.0)))
(check-sat)
(pop 1)
; Lemma 15 holds, so later checks may use it
(assert (>= (* lapse_charge expense_charge) 0.0))

; Lemma 16, negated
(push 1)
(assert (not (>= (* (- mortality_charge (* longevity_charge 4.0)) (- mortality_charge (* longevity_charge 4.0))) 0.0)))
(check-sat)
(pop 1)
; Lemma 16 holds, so later checks may use it
(assert (>= (* (- mortality_charge (* longevity_charge 4.0)) (- mortality_charge (* longevity_charge 4.0))) 0.0))

; Lemma 17, negated
(push 1)
(assert (not (>= (* (- (* mortality_charge 4.0) longevity_charge) (- (* mortality_charge 4.0) longevity_charge)) 0.0)))
(check-sat)
(pop 1)
; Lemma 17 holds, so later checks may use it
(assert (>= (* (- (* mortality_charge 4.0) longevity_charge) (- (* mortality_charge 4.0) longevity_charge)) 0.0))

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

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

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

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

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

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

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