; GraphAtlas proof IC-03
; Statement: For charges that are not below zero, the quantity under the root of the market charge, in the row of Table 16 for an upward spread stress and in the row for a downward one, and the quantity under the root of the top level of Table 34, are each at least the sum of the squares of the charges and at most the square of their sum. So each aggregate is at least the root of the sum of the squares, which is what no correlation at all gives, and at most the sum of the charges. The charge of a category is real, and diversification never lifts it above the plain sum.
; About: icsRequirement in src/kernel/ics.ts, through aggregate in src/kernel/aggregate.ts, with the two six by six tables that marketTableText gives and TOP_CORRELATION_TEXT as exact decimals. The two tables are the entries of Table 16 for six risks, with the downward stress taken out and with the upward stress taken out. Every entry of the three tables is between 0 and 1, so that each term of the form differs from the plain one by a product of two charges times a number between 0 and 2, and the products are not below zero. The solver checks the two limits for each table.
; Source: IAIS Insurance Capital Standard, Level 2 text of 5 December 2024, L2-203 and L2-335
; Expected: unsat for each of the 31 checks below.
; Check with any SMT-LIB 2 solver, for example: z3 this-file.smt2

(declare-fun interest_rate_charge () Real)
(declare-fun spread_charge () Real)
(declare-fun equity_charge () Real)
(declare-fun real_estate_charge () Real)
(declare-fun currency_charge () Real)
(declare-fun concentration_charge () Real)
(declare-fun life_charge () Real)
(declare-fun non_life_charge () Real)
(declare-fun catastrophe_charge () Real)
(declare-fun market_charge () Real)
(declare-fun credit_charge () Real)
(assert (>= interest_rate_charge 0.0))
(assert (>= spread_charge 0.0))
(assert (>= equity_charge 0.0))
(assert (>= real_estate_charge 0.0))
(assert (>= currency_charge 0.0))
(assert (>= concentration_charge 0.0))
(assert (>= life_charge 0.0))
(assert (>= non_life_charge 0.0))
(assert (>= catastrophe_charge 0.0))
(assert (>= market_charge 0.0))
(assert (>= credit_charge 0.0))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

; Goal 1, negated
(push 1)
(assert (not (let ((a!1 (* spread_charge (+ (+ 0.0 (* (/ 1.0 4.0) interest_rate_charge)) (* 1.0 spread_charge) (* (/ 3.0 4.0) equity_charge) (* (/ 1.0 2.0) real_estate_charge) (* (/ 1.0 4.0) currency_charge) (* 0.0 concentration_charge)))) (a!2 (* equity_charge (+ (+ 0.0 (* (/ 1.0 4.0) interest_rate_charge)) (* (/ 3.0 4.0) spread_charge) (* 1.0 equity_charge) (* (/ 1.0 2.0) real_estate_charge) (* (/ 1.0 4.0) currency_charge) (* 0.0 concentration_charge)))) (a!3 (* real_estate_charge (+ (+ 0.0 (* (/ 1.0 4.0) interest_rate_charge)) (* (/ 1.0 2.0) spread_charge) (* (/ 1.0 2.0) equity_charge) (* 1.0 real_estate_charge) (* (/ 1.0 4.0) currency_charge) (* 0.0 concentration_charge)))) (a!4 (* currency_charge (+ (+ 0.0 (* (/ 1.0 4.0) interest_rate_charge)) (* (/ 1.0 4.0) spread_charge) (* (/ 1.0 4.0) equity_charge) (* (/ 1.0 4.0) real_estate_charge) (* 1.0 currency_charge) (* 0.0 concentration_charge))))) (let ((a!5 (+ 0.0 (* interest_rate_charge (+ 0.0 (* 1.0 interest_rate_charge) (* (/ 1.0 4.0) spread_charge) (* (/ 1.0 4.0) equity_charge) (* (/ 1.0 4.0) real_estate_charge) (* (/ 1.0 4.0) currency_charge) (* 0.0 concentration_charge))) a!1 a!2 a!3 a!4 (* concentration_charge (+ 0.0 (* 0.0 interest_rate_charge) (* 0.0 spread_charge) (* 0.0 equity_charge) (* 0.0 real_estate_charge) (* 0.0 currency_charge) (* 1.0 concentration_charge)))))) (<= (+ 0.0 (* interest_rate_charge interest_rate_charge) (* spread_charge spread_charge) (* equity_charge equity_charge) (* real_estate_charge real_estate_charge) (* currency_charge currency_charge) (* concentration_charge concentration_charge)) a!5)))))
(check-sat)
(pop 1)

; Goal 2, negated
(push 1)
(assert (not (let ((a!1 (* spread_charge (+ (+ 0.0 (* (/ 1.0 4.0) interest_rate_charge)) (* 1.0 spread_charge) (* (/ 3.0 4.0) equity_charge) (* (/ 1.0 2.0) real_estate_charge) (* (/ 1.0 4.0) currency_charge) (* 0.0 concentration_charge)))) (a!2 (* equity_charge (+ (+ 0.0 (* (/ 1.0 4.0) interest_rate_charge)) (* (/ 3.0 4.0) spread_charge) (* 1.0 equity_charge) (* (/ 1.0 2.0) real_estate_charge) (* (/ 1.0 4.0) currency_charge) (* 0.0 concentration_charge)))) (a!3 (* real_estate_charge (+ (+ 0.0 (* (/ 1.0 4.0) interest_rate_charge)) (* (/ 1.0 2.0) spread_charge) (* (/ 1.0 2.0) equity_charge) (* 1.0 real_estate_charge) (* (/ 1.0 4.0) currency_charge) (* 0.0 concentration_charge)))) (a!4 (* currency_charge (+ (+ 0.0 (* (/ 1.0 4.0) interest_rate_charge)) (* (/ 1.0 4.0) spread_charge) (* (/ 1.0 4.0) equity_charge) (* (/ 1.0 4.0) real_estate_charge) (* 1.0 currency_charge) (* 0.0 concentration_charge)))) (a!6 (+ 0.0 (* interest_rate_charge interest_rate_charge) (* spread_charge spread_charge) (* equity_charge equity_charge) (* real_estate_charge real_estate_charge) (* currency_charge currency_charge) (* concentration_charge concentration_charge) (* (+ 0.0 (* interest_rate_charge spread_charge) (* interest_rate_charge equity_charge) (* interest_rate_charge real_estate_charge) (* interest_rate_charge currency_charge) (* interest_rate_charge concentration_charge) (* spread_charge equity_charge) (* spread_charge real_estate_charge) (* spread_charge currency_charge) (* spread_charge concentration_charge) (* equity_charge real_estate_charge) (* equity_charge currency_charge) (* equity_charge concentration_charge) (* real_estate_charge currency_charge) (* real_estate_charge concentration_charge) (* currency_charge concentration_charge)) 2.0)))) (let ((a!5 (+ 0.0 (* interest_rate_charge (+ 0.0 (* 1.0 interest_rate_charge) (* (/ 1.0 4.0) spread_charge) (* (/ 1.0 4.0) equity_charge) (* (/ 1.0 4.0) real_estate_charge) (* (/ 1.0 4.0) currency_charge) (* 0.0 concentration_charge))) a!1 a!2 a!3 a!4 (* concentration_charge (+ 0.0 (* 0.0 interest_rate_charge) (* 0.0 spread_charge) (* 0.0 equity_charge) (* 0.0 real_estate_charge) (* 0.0 currency_charge) (* 1.0 concentration_charge)))))) (<= a!5 a!6)))))
(check-sat)
(pop 1)

; Goal 3, negated
(push 1)
(assert (not (let ((a!1 (* spread_charge (+ (+ 0.0 (* (/ 1.0 4.0) interest_rate_charge)) (* 1.0 spread_charge) (* 0.0 equity_charge) (* 0.0 real_estate_charge) (* (/ 1.0 4.0) currency_charge) (* 0.0 concentration_charge)))) (a!2 (+ (+ (+ 0.0 (* (/ 1.0 4.0) interest_rate_charge)) (* 0.0 spread_charge)) (* 1.0 equity_charge) (* (/ 1.0 2.0) real_estate_charge) (* (/ 1.0 4.0) currency_charge) (* 0.0 concentration_charge))) (a!3 (+ (+ (+ 0.0 (* (/ 1.0 4.0) interest_rate_charge)) (* 0.0 spread_charge)) (* (/ 1.0 2.0) equity_charge) (* 1.0 real_estate_charge) (* (/ 1.0 4.0) currency_charge) (* 0.0 concentration_charge))) (a!4 (* currency_charge (+ (+ 0.0 (* (/ 1.0 4.0) interest_rate_charge)) (* (/ 1.0 4.0) spread_charge) (* (/ 1.0 4.0) equity_charge) (* (/ 1.0 4.0) real_estate_charge) (* 1.0 currency_charge) (* 0.0 concentration_charge))))) (let ((a!5 (+ 0.0 (* interest_rate_charge (+ 0.0 (* 1.0 interest_rate_charge) (* (/ 1.0 4.0) spread_charge) (* (/ 1.0 4.0) equity_charge) (* (/ 1.0 4.0) real_estate_charge) (* (/ 1.0 4.0) currency_charge) (* 0.0 concentration_charge))) a!1 (* equity_charge a!2) (* real_estate_charge a!3) a!4 (* concentration_charge (+ 0.0 (* 0.0 interest_rate_charge) (* 0.0 spread_charge) (* 0.0 equity_charge) (* 0.0 real_estate_charge) (* 0.0 currency_charge) (* 1.0 concentration_charge)))))) (<= (+ 0.0 (* interest_rate_charge interest_rate_charge) (* spread_charge spread_charge) (* equity_charge equity_charge) (* real_estate_charge real_estate_charge) (* currency_charge currency_charge) (* concentration_charge concentration_charge)) a!5)))))
(check-sat)
(pop 1)

; Goal 4, negated
(push 1)
(assert (not (let ((a!1 (* spread_charge (+ (+ 0.0 (* (/ 1.0 4.0) interest_rate_charge)) (* 1.0 spread_charge) (* 0.0 equity_charge) (* 0.0 real_estate_charge) (* (/ 1.0 4.0) currency_charge) (* 0.0 concentration_charge)))) (a!2 (+ (+ (+ 0.0 (* (/ 1.0 4.0) interest_rate_charge)) (* 0.0 spread_charge)) (* 1.0 equity_charge) (* (/ 1.0 2.0) real_estate_charge) (* (/ 1.0 4.0) currency_charge) (* 0.0 concentration_charge))) (a!3 (+ (+ (+ 0.0 (* (/ 1.0 4.0) interest_rate_charge)) (* 0.0 spread_charge)) (* (/ 1.0 2.0) equity_charge) (* 1.0 real_estate_charge) (* (/ 1.0 4.0) currency_charge) (* 0.0 concentration_charge))) (a!4 (* currency_charge (+ (+ 0.0 (* (/ 1.0 4.0) interest_rate_charge)) (* (/ 1.0 4.0) spread_charge) (* (/ 1.0 4.0) equity_charge) (* (/ 1.0 4.0) real_estate_charge) (* 1.0 currency_charge) (* 0.0 concentration_charge)))) (a!6 (+ 0.0 (* interest_rate_charge interest_rate_charge) (* spread_charge spread_charge) (* equity_charge equity_charge) (* real_estate_charge real_estate_charge) (* currency_charge currency_charge) (* concentration_charge concentration_charge) (* (+ 0.0 (* interest_rate_charge spread_charge) (* interest_rate_charge equity_charge) (* interest_rate_charge real_estate_charge) (* interest_rate_charge currency_charge) (* interest_rate_charge concentration_charge) (* spread_charge equity_charge) (* spread_charge real_estate_charge) (* spread_charge currency_charge) (* spread_charge concentration_charge) (* equity_charge real_estate_charge) (* equity_charge currency_charge) (* equity_charge concentration_charge) (* real_estate_charge currency_charge) (* real_estate_charge concentration_charge) (* currency_charge concentration_charge)) 2.0)))) (let ((a!5 (+ 0.0 (* interest_rate_charge (+ 0.0 (* 1.0 interest_rate_charge) (* (/ 1.0 4.0) spread_charge) (* (/ 1.0 4.0) equity_charge) (* (/ 1.0 4.0) real_estate_charge) (* (/ 1.0 4.0) currency_charge) (* 0.0 concentration_charge))) a!1 (* equity_charge a!2) (* real_estate_charge a!3) a!4 (* concentration_charge (+ 0.0 (* 0.0 interest_rate_charge) (* 0.0 spread_charge) (* 0.0 equity_charge) (* 0.0 real_estate_charge) (* 0.0 currency_charge) (* 1.0 concentration_charge)))))) (<= a!5 a!6)))))
(check-sat)
(pop 1)

; Goal 5, negated
(push 1)
(assert (not (let ((a!1 (* catastrophe_charge (+ (+ 0.0 (* (/ 1.0 4.0) life_charge) (* (/ 1.0 4.0) non_life_charge)) (* 1.0 catastrophe_charge) (* (/ 1.0 4.0) market_charge) (* (/ 1.0 4.0) credit_charge)))) (a!2 (+ (+ 0.0 (* (/ 1.0 4.0) life_charge) (* (/ 1.0 4.0) non_life_charge)) (* (/ 1.0 4.0) catastrophe_charge)))) (let ((a!3 (+ 0.0 (* life_charge (+ 0.0 (* 1.0 life_charge) (* 0.0 non_life_charge) (* (/ 1.0 4.0) catastrophe_charge) (* (/ 1.0 4.0) market_charge) (* (/ 1.0 4.0) credit_charge))) (* non_life_charge (+ 0.0 (* 0.0 life_charge) (* 1.0 non_life_charge) (* (/ 1.0 4.0) catastrophe_charge) (* (/ 1.0 4.0) market_charge) (* (/ 1.0 4.0) credit_charge))) a!1 (* market_charge (+ a!2 (* 1.0 market_charge) (* (/ 1.0 4.0) credit_charge))) (* credit_charge (+ a!2 (* (/ 1.0 4.0) market_charge) (* 1.0 credit_charge)))))) (<= (+ 0.0 (* life_charge life_charge) (* non_life_charge non_life_charge) (* catastrophe_charge catastrophe_charge) (* market_charge market_charge) (* credit_charge credit_charge)) a!3)))))
(check-sat)
(pop 1)

; Goal 6, negated
(push 1)
(assert (not (let ((a!1 (* catastrophe_charge (+ (+ 0.0 (* (/ 1.0 4.0) life_charge) (* (/ 1.0 4.0) non_life_charge)) (* 1.0 catastrophe_charge) (* (/ 1.0 4.0) market_charge) (* (/ 1.0 4.0) credit_charge)))) (a!2 (+ (+ 0.0 (* (/ 1.0 4.0) life_charge) (* (/ 1.0 4.0) non_life_charge)) (* (/ 1.0 4.0) catastrophe_charge))) (a!4 (+ 0.0 (* life_charge life_charge) (* non_life_charge non_life_charge) (* catastrophe_charge catastrophe_charge) (* market_charge market_charge) (* credit_charge credit_charge) (* (+ 0.0 (* life_charge non_life_charge) (* life_charge catastrophe_charge) (* life_charge market_charge) (* life_charge credit_charge) (* non_life_charge catastrophe_charge) (* non_life_charge market_charge) (* non_life_charge credit_charge) (* catastrophe_charge market_charge) (* catastrophe_charge credit_charge) (* market_charge credit_charge)) 2.0)))) (let ((a!3 (+ 0.0 (* life_charge (+ 0.0 (* 1.0 life_charge) (* 0.0 non_life_charge) (* (/ 1.0 4.0) catastrophe_charge) (* (/ 1.0 4.0) market_charge) (* (/ 1.0 4.0) credit_charge))) (* non_life_charge (+ 0.0 (* 0.0 life_charge) (* 1.0 non_life_charge) (* (/ 1.0 4.0) catastrophe_charge) (* (/ 1.0 4.0) market_charge) (* (/ 1.0 4.0) credit_charge))) a!1 (* market_charge (+ a!2 (* 1.0 market_charge) (* (/ 1.0 4.0) credit_charge))) (* credit_charge (+ a!2 (* (/ 1.0 4.0) market_charge) (* 1.0 credit_charge)))))) (<= a!3 a!4)))))
(check-sat)
(pop 1)