ICS

Before the operational charge, a life, catastrophe or market risk has the part of the insurance risk charge that is its share inside its category, c × (R × c) / A, times the weighted charge of the category over the aggregate. Non-life and credit take their own charge times that factor. The parts add up to the aggregate. The terms c × (R × c) of each table add up to the square of the charge of their category, and the terms of Table 34 add up to the square of the aggregate. Terms that add up to the square of a number add up to it when divided by it. A factor times shares that add up to a charge adds up to the factor times it.

7 checks, decided by Z3 5.3.3.0 (WebAssembly) and rerun from the emitted file by Z3 5.3.3 (native) and cvc5 1.4.2 (native, nl-cov). 5 broken variants are refuted. proofs/smt2/IC-04.smt2

The tax effect taken off the insurance risk charge lies between zero and 80 per cent of the notional effect, which is the requirement times the group effective tax rate, so at least a fifth of the requirement is left. The carry-back component is at most 85 per cent of the notional effect. The net deferred tax asset is at most 15 per cent of the requirement and is never held against a net liability. An asset can only lower what is used, and a sum of components between nothing and the cap is what is used. It holds for any notional effect up to the requirement and any three sub-groups, capacity, earnings and deferred taxes.

10 checks, decided by Z3 5.3.3.0 (WebAssembly) and rerun from the emitted file by Z3 5.3.3 (native) and cvc5 1.4.2 (native, nl-cov). 6 broken variants are refuted. proofs/smt2/IC-05.smt2

For any capital resources and any requirement, what counts and what is left out add up to what is held, for a group that is not mutual and for a mutual. For a group that is not mutual, Tier 1 Limited counts up to 15 per cent of the requirement, Tier 2 up to 50 per cent and the basket up to 15 per cent, and none of the Non-Paid-Up capital counts. For a mutual, Tier 1 Limited counts up to 30 per cent, Non-Paid-Up up to 10 per cent, and Tier 1 Limited and Tier 2 together up to 60 per cent. What Tier 1 Limited has over its limit moves to Tier 2. What is left out is not below zero and what counts is not above what is held.

20 checks, decided by Z3 5.3.3.0 (WebAssembly) and rerun from the emitted file by Z3 5.3.3 (native) and cvc5 1.4.2 (native, nl-cov). 7 broken variants are refuted. proofs/smt2/IC-06.smt2

The five categories are aggregated with Table 34, so life and non-life, which are independent, add in quadrature, and five equal charges give the root of 9.5 times the square. The tax effect comes off the insurance risk charge, and the charge for the non-insurance entities is added after it with no tax effect of its own. A group with nothing has a requirement of zero. The undiversified sum is every charge and the operational charge, and two diversification figures, between the categories and within them, explain the rest. The sample group has the charges that the second program confirms.

tests/kernel/ics.test.ts

The group effective tax rate weights the rate of each entity by the earnings that it made in the previous three years. The example that the IAIS prints, three entities at 30, 25 and 20 per cent, gives 23.03 per cent. Each loss is set to zero in its own year and not against the sum of the three years. The rate of one entity is its own, and the unit of the earnings does not change the result. When no entity made a profit there is nothing to weight the rates by, and the engine refuses, as it does for an entity that is not one.

tests/kernel/ics.test.ts

Under the default rule the tax effect is 80 per cent of the notional effect, which is the requirement times the group effective tax rate. A supervisor can limit it by four components. Component a is the smaller of the share by liabilities of the notional effect and the carry-back capacity of each tax sub-group, summed, less 15 per cent. Component b is half of five years of earnings times the rate, and zero for a projected loss. Component c is a net deferred tax liability and d a net asset held to 15 per cent of the requirement, and a group has one of them. The sum a plus b plus c less d is held between zero and 80 per cent of the notional effect. The IAIS example gives 2,005.

tests/kernel/ics.test.ts

Tier 1 Limited counts up to 10 per cent of the requirement, or 15 per cent when the part above 10 has a loss absorbency mechanism. What is above the limit moves to Tier 2, which counts up to 50 per cent. The Tier 2 basket is half of the pension fund asset, all of the deferred tax asset and a tenth of the software intangibles, held to 15 per cent. A mutual counts Tier 1 Limited up to 30 per cent, Non-Paid-Up up to 10 per cent, and Tier 1 Limited with Tier 2 up to 60 per cent. The limits are shares of the requirement after tax and with the non-insurance charge, so they rise and fall with it, and what does not count is exactly what is above them. The text defines no ICS ratio.

tests/kernel/ics.test.ts

A charge below zero is refused with a message that names it and says that a charge is the fall in capital resources under its stress, so a stress that raises them has a charge of zero. A charge that is not finite, or is above 1,000,000,000,000 in size, is refused by name. A wrong exposure, non-insurance charge or tax rule is refused with a message that says what is wrong. The checks run in a fixed order, charges first, then exposures, the non-insurance charge, the tax rule and last the resources. A group that gives no resources gets no result for them, which is not resources of zero.

tests/kernel/ics.test.ts

The text has no rule for where the capital comes from. The product gives one, the Euler allocation through three levels. A risk takes its share inside its category, the category takes its share of Table 34, and the part of the risk is the product of the two. The parts add up to the insurance risk charge for every case of the second program. The operational charge is a part of its own, and non-life and credit have a line each. Each part is what the insurance risk charge changes by when its charge is scaled, which a numerical derivative confirms for eleven charges. A longevity charge under a quarter of the mortality charge takes a negative part.

tests/kernel/ics.test.ts

The text gives a spread charge for an up stress and for a down stress, and does not say which row of Table 16 the larger of the two uses. The engine reads the row of the direction that gave the larger. So a down stress that grows past the up stress turns the row, and the market charge can then fall, because equity is correlated at 75 per cent with the spread under the up stress and at nothing under the down stress. Only when the two are equal and not zero does the engine take the larger of the two results, and the result says so.

tests/kernel/ics.test.ts

A second program that shares no code with the engine works every case in exact fractions and takes each square root once, to 60 digits. For 50 cases that use both directions of the spread and a tie, every outcome of the tax rule, both lines of operational risk on both of their binds and every limit on capital resources, every figure agrees with the engine to a relative error under 3e-15, and the amounts left out, which are differences of sums, to 1e-14. The saved answers are what the program says now, so that nobody edited them by hand.

tests/kernel/ics.test.tsscripts/verify/ics_oracle.pytests/support/ics-oracle.json

Over generated groups, the requirement doubles when every amount doubles, to the last digit, through the tax rule and the limits. The tax effect never takes the requirement below a fifth of the insurance risk charge, and the parts add up to that charge. A larger charge never gives a smaller requirement, except in a pair that offsets and in the spread. Each category charge lies between its largest part and the sum of its parts. The group tax rate lies between the lowest and the highest rate of the entities that made a profit. The tax effect never falls when earnings, the deferred tax liability or carry-back capacity rise, and never rises with the asset.

tests/kernel/ics.test.ts

The receipt of a calculation holds the rule, every number that went in and every number that came out, in a fixed order. It carries the tax rule with its sub-groups, and no resources as nothing. It is the same for the same input, and different when any input moves by one unit or any choice is turned over. It never carries a minus zero, which would give another hash.

tests/kernel/ics.test.ts