Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
This work is motivated by the IFoA CM1 financial and life-contingent mathematics syllabus (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). Actuarial life insurance pricing is incomplete without the link between gross premiums, future reserve liabilities, emerging cashflow profits and risk capital requirements. The IFoA CM1 syllabus explicitly includes gross prospective and retrospective reserves, death strain, mortality profit, profit signatures, profit testing for unit-linked business and elimination of negative non-unit profit cashflows by reserve zeroisation. Dickson, Hardy and Waters (2009), Chapter 11 (Emerging costs for traditional life insurance) supplies the broader profit testing theory. We combine these elements into one connected mission with an optimisation property as its capstone.
The established CM1 modelling conventions and previously known actuarial identities provide the conceptual background, while the following larger original-derived Lean results still need accepted proofs. The stated nontrivial capstone excludes vacuous equal cashflow or zero-duration substitutes. Each accepted module could become reusable infrastructure for future actuarial formalisation missions.
A contract has dated benefit payments, expenses, premiums and probability/discounter weights over a finite horizon N. Gross level premium divides the total expected benefit and expense PV by a nonzero premium annuity factor. A prospective reserve equals expected future outgo less future premiums, and a retrospective reserve uses prior accumulated premiums less outgo on the same valuation basis. Death strain at risk measures the claim amount net of the next reserve release. For unit-linked products the unit fund develops through allocation, charges and investment returns. Non-unit projected cashflow c(t) combines premium and charges less expenses and claims. The non-unit reserve R(t), growth factor g(t)>0 and survival/continuation weight s(t)≥0 determine projected profit Π(t)=c(t)+g(t)R(t)-s(t)R(t+1), with terminal reserve R(N)=0.
All declarations below are original derived CM1-style formal results. The supporting milestone order builds an intentional mathematical chain to a single root theorem.
This block contributes 10 theorem targets and 4 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1ExpectedBenefitPV_add_last:
Finite expected benefit PV recurses correctly when one extra payment term is appended.
This block contributes 11 theorem targets and 5 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1MortalityProfit_favourable:
With positive death strain, fewer actual deaths than expected produce favourable mortality profit.
This block contributes 10 theorem targets and 5 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1ProfitMargin_nonneg:
Profit margin is nonnegative if projected profit is nonnegative and the premium base positive.
This block contributes 12 theorem targets and 2 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1ZeroisationOptimality_fundamental:
The finite-horizon capstone proves that a backwards-zeroised reserve produces nonnegative projected profits and is pointwise minimal among all nonnegative feasible reserve paths with the same terminal boundary.
The main target is ActuarialValuation.cm1ZeroisationOptimality_fundamental. The finite-horizon capstone proves that a backwards-zeroised reserve produces nonnegative projected profits and is pointwise minimal among all nonnegative feasible reserve paths with the same terminal boundary.
The established actuarial syllabus identifies the relevant relationships and applications (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). The zeroisation recursion can be used to eliminate projected negative future non-unit profits while avoiding excessive reserve financing. It is valuable to show that the backwards reserve is not only feasible but pointwise minimal among all competing nonnegative reserve profiles satisfying the same profit and terminal constraints. Such a theorem is an auditable dynamic optimisation guarantee, not merely a spreadsheet check. It also provides a bridge from earlier finite cashflow PV and insurance reserve missions to modern policy profit testing. The intermediate theorem groups separate gross premium equivalence, death strain, reserve valuation, unit funds, discounted profit signatures and zeroisation.
The formal model carefully distinguishes net benefit cashflows and reserve-adjusted profit, and never calls a gross premium formula universally correct without its equivalence assumptions. In zeroisation, g(t) must be strictly positive before division and multiplication inequalities can be reversed, while s(t)≥0 is necessary to compare different next-year reserve requirements. The floor max(0,(sRnext-c)/g) is a genuine feasibility threshold. The minimality result needs backward induction from the same terminal reserve, not a false forward monotonicity argument. Negative non-unit cashflows and zero survival are meaningful cases. The result does not equate the risk discount rate used for net present value with the investment growth rate g(t).
This is a finite-horizon deterministic expected-cashflow model rather than a fully stochastic regulatory reserve basis. Probability, benefit and expenses schedules enter as given finite arrays. Gross premiums use the simplified actuarial equivalence principle and not arbitrary commission or investment-profit target structures. The non-unit zeroisation capstone is conditional on a reserve path satisfying the specified backward recursion; its existence can be constructed by a later recurrence theorem and should not be replaced by a hidden axiom. All explicitly stated profit constraints and nonnegative reserve bounds are maintained for each pre-terminal valuation date. The theorem is meaningful even when cashflow c(t) is negative.
These are original derived finite/analytic CM1 formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
This work is motivated by the IFoA CM1 financial and life-contingent mathematics syllabus (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). Financial mathematics provides the time-value backbone of actuarial pricing and pension liability management. The CM1 formula sheet records effective interest and discount rates, annuity-certain relationships, loan amortisation and bond duration. These should be proved as one connected mathematical construction culminating in the local Redington immunisation conditions, rather than as separate missions of two-line rearrangements. A correct proof handles actual discounted dated cashflows and the consistency of their rate derivatives. The IFoA 2026 CM1 financial mathematics syllabus provides the subject boundaries.
The established CM1 modelling conventions and previously known actuarial identities provide the conceptual background, while the following larger original-derived Lean results still need accepted proofs. The stated nontrivial capstone excludes vacuous equal cashflow or zero-duration substitutes. Each accepted module could become reusable infrastructure for future actuarial formalisation missions.
Real-valued effective annual interest i is restricted to i greater than minus one where cashflow discount factors need to remain positive. A finite dated cashflow c(k) is payable at time k+1. The annual discount factor is (1+i) raised to the negative integer horizon, implemented as a reciprocal of an accumulated factor. Unit annuities in advance and arrears use dates k and k+1 respectively. The cashflow valuation V(i) is a finite weighted sum. A loan balance at t is the present value of remaining loan installments. Duration and convexity numerators aggregate discounted times and squared-time coefficients of cashflows. Asset and liability streams are compared at a single flat effective rate, so rate derivatives are well-defined on the positive accumulation domain.
All declarations below are original derived CM1-style formal results. The supporting milestone order builds an intentional mathematical chain to a single root theorem.
This block contributes 10 theorem targets and 4 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1NominalInterest_scale:
Nominal rate scales the periodic effective interest input.
This block contributes 11 theorem targets and 3 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1IncreasingImmediate_succ:
Increasing annuity recurrence uses the next arithmetically increasing payment.
This block contributes 10 theorem targets and 2 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1LoanBalance_nonneg:
Remaining positive scheduled loan payments have nonnegative prospective value.
This block contributes 12 theorem targets and 4 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1RedingtonImmunisation_fundamental:
The genuine Redington second-derivative test gives a local surplus minimum at the matching effective yield; it does not assert global or arbitrary curve immunisation.
The main target is ActuarialValuation.cm1RedingtonImmunisation_fundamental. The genuine Redington second-derivative test gives a local surplus minimum at the matching effective yield; it does not assert global or arbitrary curve immunisation.
The established actuarial syllabus identifies the relevant relationships and applications (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). Matching current assets and liabilities without checking interest-rate sensitivity is inadequate. A valuation system should reconcile cashflow present values, annuities, prospective loan balances, duration and convexity, and verify that asset surplus cannot turn negative under sufficiently small yield movements when Redington's strictly positive second-derivative condition holds. These equations are reused in actuarial annuity and pension schemes. The mission formalises genuine financial relationships as a graph: compound accumulation leads to discount factors, then discounted cashflow valuation and rate derivatives, ending with a strict local minimum argument. The latter is more substantial than algebraic definition expansion.
Theorems must preserve distinctions between interest and discount rates and between annuities in advance and arrears. Positive accumulation is essential where inverse factors are cancelled or differentiated. Loan prospective value must include only payments remaining after the valuation date. Duration is a ratio whose denominator must be nonzero. Redington immunisation is a genuinely local twice-differentiable result requiring matched PV, first derivative and strictly positive second derivative at an interior yield. It does not provide protection from arbitrary nonparallel yield-curve shifts or sufficiently large interest-rate movements. A proof must establish smoothness of the finite rational cashflow surplus near i₀, rather than assuming local minimisation as a hidden premise.
The model is deterministic finite cashflow financial mathematics. Mortality-weighted uncertain payments can later be inserted as expected cashflow amounts. Explicit coupon, redemption, loan and annuity terms share the same discounting convention. The capstone uses the actual finite asset-minus-liability discounted cashflows. This is a flat-yield Redington local test only. It is mathematically strong and may be difficult to complete because the second derivative theorem requires calculus and finite-sum differentiability, but no artificial axiom or proof placeholder may count as a solved result.
These are original derived finite/analytic CM1 formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
A defined benefit pension commencement lump sum cannot generally be determined by multiplying the pre-commutation pension by a cash conversion factor without considering the remaining pension. HMRC's Pensions Tax Manual PTM063240 (https://www.gov.uk/hmrc-internal-manuals/pensions-tax-manual/ptm063240) establishes the applicable amount for a DB arrangement and gives a simplified exact solution 20fg/(20+3f) when the pension is partially surrendered at commutation factor f. PTM063230 (https://www.gov.uk/hmrc-internal-manuals/pensions-tax-manual/ptm063230) identifies other statutory allowance restrictions. This mission formalises the HMRC arithmetic under explicit assumptions, and then extends the model to separate pension tranche reductions rather than pretending all pensions must use a single commutation factor.
Let g denote the annual pension before commutation, L the pension commencement cash and f the cash paid per pound of annual pension surrendered. The remaining annual pension is P_B=g−L/f. For the simplified DB arrangement with no disqualifying pension credit and no other relevant linked lump sum, the statutory test becomes 3L≤20P_B. Solving this with f>0 gives the maximum applicable cash L_max=20fg/(20+3f). A real value A can represent an externally determined available allowance, giving the capped amount min(L_max,A). For a collection of tranches, annual reduction x(i) and individual cash factor f(i) generate cash contributions f(i)x(i). The residual annual pension is the sum of P(i)−x(i).
The following declarations are original derived results, not direct quotations of numbered textbook or statutory theorems. Exact hypotheses and corner cases are fixed by the formal Lean statements.
The named result ActuarialValuation.dbCommutedPension_zero_cash captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. If no pension is commuted, the original annual DB pension remains unchanged. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.
The named result ActuarialValuation.dbCappedPCLS_le_max captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. The allowance cap cannot increase cash above the base applicable amount. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.
The named result ActuarialValuation.dbPCLSMaximum_fundamental captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. The capstone proves the attained basic HMRC cash limit, verifies the allowance-limited cash remains admissible, and retains a nonnegative pension tax headroom. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.
Additional supporting theorems establish cancellations, finite-sum identities, positivity and uniqueness. In all cases the generated formal theorem type rather than an informal diagram is authoritative.
The equations are financially useful because the HMRC basic limit depends on the annual pension remaining after cash has been commuted. Using the original pension instead of P_B would overstate the permitted amount. HMRC PTM063240 (https://www.gov.uk/hmrc-internal-manuals/pensions-tax-manual/ptm063240) gives the explicit formula and examples, while PTM063230 (https://www.gov.uk/hmrc-internal-manuals/pensions-tax-manual/ptm063230) explains the allowance components of the permitted maximum. The formal result provides a check of cash amount, pension reduction, binding constraint and residual HMRC headroom. Separate tranche cash and residual pension definitions are appropriate when benefit tranches have different commutation factors and noncommutable components. They will support more advanced finite optimisation and pension rights constraints.
Cross multiplication and the residual pension test require f strictly positive. Without this, division by f does not correspond to a legal pension surrender and reversed inequality steps are possible. The formula L_max is required to attain zero HMRC headroom in the simplified case, and every lower nonnegative cash amount must satisfy the same basic maximum relation. Allowance caps must themselves be nonnegative to preserve a nonnegative paid amount. An actual arrangement can also have disqualifying pension credits, other linked lump sums, protected rights, scheme minimum pensions or a finite available lump sum and death benefit allowance. The reduced mathematics must not be misrepresented as covering these cases automatically.
The Lean model uses exact real arithmetic for the single-factor formula and finite sums for the separate-tranche amounts. It proves basic nonnegativity, monetary identities, headroom monotonicity, the cash upper bound and an allowance-capped admissible solution. Noncommutable GMP and scheme-specific rules are deliberately outside this first formal capstone, with reductions of zero available as an abstract representation of such tranches. The external allowance input does not calculate a member's statutory tax allowances. This limits the formal claims to the HMRC simplified applicable-amount formula, while providing separate tranche arithmetic that a subsequent mission can enrich with survivor minimums, GMP guarantees and more involved cash waterfalls.
Existing actuarial valuation theory gives the financial identities motivating these new formal obligations, but the exact original Lean declarations have no accepted proofs yet. The proposed capstone is nontrivial because arbitrary benefit dates, positivity hypotheses and boundary cases cannot be excluded or replaced with a degenerate zero-cashflow special case. The algebraic components are reusable in future UK scheme valuation and administration missions. For source interpretation, a valuation basis means the explicit package assumptions and a benefit constraint means a scheme-specific rule, not an implicit mathematical axiom.
The pinned Mathlib revision is 0df444a360eaa60ab8c11dca51a86af692955474. All source declarations use targeted imports, with no unrelated namespace opening. An authoring compilation with open sorry targets checks source elaboration but does not prove a mathematical statement. The full actuarial benefit schedule may require further scheme-specific data beyond this theorem graph.
Defined benefit pension schemes may contain multiple legally different benefit tranches. Their pension increases, retirement ages, survivor benefits, guarantees and death-in-deferment provisions need not be identical. Applying one arithmetic average factor to a total pension would ignore differences in complete present value. The controlled UK DB Retirement Factors Mathematical Framework (2026, Chapter 18, equations 58–60) specifies a separately derived factor for each tranche, and treats a shared factor only when scheme provisions actually permit it. Dickson, Hardy and Waters (2009, Pension mathematics, Chapter 9, https://doi.org/10.1017/CBO9780511800146) explain pension cashflows and service-table valuation. This mission defines formal monetary equivalence for every tranche separately, retaining each actuarial package.
Take a finite number n of pension tranches. For each index i, P(i) denotes accrued annual pension measured in pounds per year, A(i) the complete early-date immediate retirement package value in annuity years, and D(i) the alternative normal-retirement comparator in the same units. Each package can itself be the sum of discounted expected payments at tranche-specific dates. The individual factor f(i)=D(i)/A(i) is applied only to the original pension in tranche i, giving R(i)=P(i)f(i). Its immediate monetary value is R(i)A(i). Total retirement pension and total actuarial liability must be formed by summing their respective tranche contributions. The model never substitutes a pension-only average factor.
The following declarations are original derived results, not direct quotations of numbered textbook or statutory theorems. Exact hypotheses and corner cases are fixed by the formal Lean statements.
The named result ActuarialValuation.trancheAnnuityLedgerValue_zero captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. A tranche with no ledger payment dates has zero immediate package value. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.
The named result ActuarialValuation.trancheSchemePension_zero captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. No tranches means no payable scheme pension. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.
The named result ActuarialValuation.separateTrancheFactors_fundamental captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. The capstone asserts per-tranche and aggregate monetary equivalence simultaneously, without computing or applying a common averaged factor. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.
Additional supporting theorems establish cancellations, finite-sum identities, positivity and uniqueness. In all cases the generated formal theorem type rather than an informal diagram is authoritative.
Tranche-specific monetary valuation is crucial for pension administration, where two pensions with identical nominal amounts may carry different spouse percentages, indexation and normal retirement dates. The actuarial cost of each unit of pension can consequently vary, and the conditions for equivalence differ. Dickson, Hardy and Waters, pension mathematics (2009, https://doi.org/10.1017/CBO9780511800146), provides the standard actuarial valuation background, while the UK retirement-factor framework 5.3.0 demonstrates the particular multi-tranche application. The resulting identity is useful in migration audits, administering benefit rectifications, reconciling aggregate valuation, and checking that rounding or source ordering has not silently changed benefit values. Separate original benefit rights remain authoritative.
The denominator A(i) must not vanish when cancelling the value ratio. In particular, the real-number convention that division by zero has a defined total Lean value does not make its ordinary actuarial quotient meaningful. Even when total monetary values happen to match, separate per-tranche equality cannot be inferred without additional assumptions. The formal task must retain all individual tranche indices and not count a benefit twice. Zero pension tranches, empty pension schedules and appending another tranche are meaningful cases, rather than mathematical errors. Every unit package must be valued on its own scheme-rule basis, including its relevant discount and contingent cashflows.
The declarations use exact real arithmetic and finite sums. In particular, the discount, survival, pension increases, guarantee and survivor entitlement details may be assembled into each package ledger as inputs. Their stochastic derivation is an additional task and not silently asserted by a generic real-valued annuity factor. The central identity is P(i)f(i)A(i)=P(i)D(i), and the whole scheme result sums these monetary equivalence equations over finite tranches. The derived calculation remains exact before administration rounding, with no common average factor theorem and no claim that all tranches have the same normal retirement age. It is a reusable base for more detailed pension option missions.
Existing actuarial valuation theory gives the financial identities motivating these new formal obligations, but the exact original Lean declarations have no accepted proofs yet. The proposed capstone is nontrivial because arbitrary benefit dates, positivity hypotheses and boundary cases cannot be excluded or replaced with a degenerate zero-cashflow special case. The algebraic components are reusable in future UK scheme valuation and administration missions. For source interpretation, a valuation basis means the explicit package assumptions and a benefit constraint means a scheme-specific rule, not an implicit mathematical axiom.
The pinned Mathlib revision is 0df444a360eaa60ab8c11dca51a86af692955474. All source declarations use targeted imports, with no unrelated namespace opening. An authoring compilation with open sorry targets checks source elaboration but does not prove a mathematical statement. The full actuarial benefit schedule may require further scheme-specific data beyond this theorem graph.
Retiring earlier changes the number of pension payments and may introduce payments before normal retirement age. Retiring later removes some payments but may entitle the member to an uplift and missed increases. A defensible actuarial equivalence calculation compares complete benefit packages, including contingent benefits, at the same valuation date. The UK DB Retirement Factors Mathematical Framework 5.3.0 (2026, Chapters 8 to 11) explicitly treats early and late benefit routes, guaranteed periods, pension increases and pre-commencement death. Dickson, Hardy and Waters (2009, Chapter 9, https://doi.org/10.1017/CBO9780511800146) provide independent actuarial pension valuation background. This mission first formalises a carefully delimited factor-independent death-benefit model and retains explicit differences between pure and total late-retirement factors.
For early retirement, A_E is the immediate retirement package, D_E the normal retirement comparator, and F_E=D_E/A_E the unrounded reduction factor. The comparator may contain a death-before-retirement component plus survival-to-normal-age probability p times an appropriate discount v and normal pension annuity A_N. For late retirement N is the value of the benefit package at normal retirement, D the value of death benefits payable while commencement is postponed, and A_L the immediate package at the late date. The positive multiplier m represents pension increases that would otherwise have accrued while in payment. The pure LRF F_L solves N=D+pvm A_L F_L. The total pension multiplier M_L=mF_L includes both late uplift and missed increases.
The following declarations are original derived results, not direct quotations of numbered textbook or statutory theorems. Exact hypotheses and corner cases are fixed by the formal Lean statements.
The named result ActuarialValuation.pensionEarlyComparator_nonneg captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. Nonnegative disjoint death and surviving deferred-annuity route values yield a nonnegative comparator. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.
The named result ActuarialValuation.pensionLatePureFactor_nonneg captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. The net value available for deferred pension is nonnegative once factor-independent death costs are deducted. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.
The named result ActuarialValuation.pensionRetirementEquivalence_fundamental captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. The capstone validates both early and late monetary equivalence and proves that the pure factor and total missed-increase multiplier represent the same late pension liability. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.
Additional supporting theorems establish cancellations, finite-sum identities, positivity and uniqueness. In all cases the generated formal theorem type rather than an informal diagram is authoritative.
The distinction prevents a common implementation error: treating the total missed-increase pension multiplier as the pure actuarial LRF and then applying increases a second time. The financial basis and cashflow boundaries must be stated before taking an algebraic ratio. The UK retirement factor methodology v5.3.0 details the pension ledger and explicitly separates pure and total late multipliers. Pension mathematics and contingent annuities in Dickson, Hardy and Waters (2009, https://doi.org/10.1017/CBO9780511800146) explain the broader framework. The resulting small formal theorem can be combined with exact-dated benefit ledgers and numerical models to test early and late valuation reconciliation before rounding. That reuse is important when individual tranches have different dates and benefit conditions.
Both ratio definitions need nonzero annuity packages or survival-weighted denominators. If normal survival probability is zero, a late pension cannot compensate financially in the ordinary quotient model, and Lean division must not hide that failure. The death benefit during late postponement is assumed independent of the eventual pure factor, an explicit limitation. Factor-dependent death benefits require solving a different potentially nonlinear root equation; simply dividing a fixed numerator would be wrong. Increases accrued while waiting are distinct from in-payment increases already present in A_L. All route components are valued at a common date, and different death and survival outcomes are treated as disjoint events.
The theorem graph establishes early comparator positivity, factor existence and uniqueness, and exact equivalence when an annuity denominator is nonzero. It separately proves late pension value and uniqueness under the corresponding nonzero survival-discount-increase-annuity product. The capstone reconciles the early option and the two equivalent late expressions: using the pure late factor and using the total multiplier mF_L. The underlying cashflow package values are abstract real inputs, which enables later missions to supply actual discounted mortality-weighted schedules. The current restricted identity does not claim to model every dependant, guarantee, calendar increase or factor-linked death benefit. Scheme-specific cashflow rights remain controlling.
Existing actuarial valuation theory gives the financial identities motivating these new formal obligations, but the exact original Lean declarations have no accepted proofs yet. The proposed capstone is nontrivial because arbitrary benefit dates, positivity hypotheses and boundary cases cannot be excluded or replaced with a degenerate zero-cashflow special case. The algebraic components are reusable in future UK scheme valuation and administration missions. For source interpretation, a valuation basis means the explicit package assumptions and a benefit constraint means a scheme-specific rule, not an implicit mathematical axiom.
The pinned Mathlib revision is 0df444a360eaa60ab8c11dca51a86af692955474. All source declarations use targeted imports, with no unrelated namespace opening. An authoring compilation with open sorry targets checks source elaboration but does not prove a mathematical statement. The full actuarial benefit schedule may require further scheme-specific data beyond this theorem graph.
Philosophers of physics ask when a formulation of a theory carries excess structure: mathematical distinctions between models that make no physical difference. The standard example is electromagnetism written with a vector potential . Potentials that differ by a gauge transformation have the same field strength , and on the usual view they represent the same physical situation.
Weatherall (2016) made this precise with category theory. Each formulation becomes a category of models, and a translation between formulations becomes a functor. A functor that is faithful and essentially surjective but not full forgets structure. One that is full and faithful but not essentially surjective forgets properties. One that is full and essentially surjective but not faithful forgets stuff. Weatherall's Proposition 1 says the functor from potentials to field strengths forgets only structure, provided the arrows between potentials are spacetime symmetries that preserve . His Proposition 2 says the principal-bundle formulation, whose arrows include gauge transformations, forgets nothing. His footnote 15 notes that adding gauge transformations as arrows between potentials yields a category equivalent to that of field strengths (Weatherall, arXiv:1411.5757).
These arguments work on Minkowski space, which is contractible. Weatherall's footnote 9 sets topology aside for that reason. The follow-up literature, for example Nguyen, Teh and Wells (2018), compares these and related functors further. This mission states the comparison exactly on a finite cell complex, where topology cannot be set aside. Each of the three ways a functor can forget information then corresponds to one cohomology group.
A finite oriented 2-complex has vertices, edges and faces, together with integer incidence numbers and satisfying for every face and vertex . Nothing beyond this identity is required, so the incidence data need not come from a geometric complex; all results hold for any such integer data. Fix an additive commutative group of coefficients, for example , , or as a discrete stand-in for . The cochains are (gauge parameters ), (potentials ) and (field strengths ). The coboundaries are
and .
There are three categories, with spacetime symmetries taken to be trivial:
The field-strength functors and send . In the second functor every gauge arrow goes to an identity.
Cohomology vanishing is stated elementarily:
For every finite 2-complex and coefficient group , the functor satisfies
circle3 with coefficients, the potential equal to on one edge has the same field strength as . No gauge arrow connects the two, so the functor is not full.The result. The classification turns a qualitative philosophical diagnostic into a cohomological criterion.
Formalizing it. No machine-checked version of the theories-as-categories programme for gauge theory is known to the author of this mission. This mission is the base case of a planned discrete gauge-functor development: non-abelian groups, nontrivial symmetry groups, and holonomy-based equivalences.
The mathematics is elementary once stated. The work is in making the categorical notions line up with the cochain conditions. Three points need care:
The concrete milestones require computations on explicit complexes, including a gauge-invariant obstruction for the Aharonov–Bohm example.
Fin types, and the incidence numbers are integer-valued. The complex is finite but may be empty in any dimension.AddCommGroup, and integers act on it by zsmul.Fld and Pot0 are Mathlib Discrete categories. PotG carries a hand-written Category instance whose arrows are the structure GaugeHom.Functor.Full, Functor.Faithful and Functor.EssSurj.delta0, delta1, ) is proved in the definitions file and is reusable for discrete gauge theory and toric-code missions.The Bühlmann–Straub credibility method allocates weight to individual observed claims experience according to total exposure and variability. It balances the expected value of process variance EPV with the variance of hypothetical means VHM. More exposure raises the statistical information carried by the policyholder's observed rate and should weakly improve the resulting optimal linear prediction error. The established credibility formula and its interpretation are developed in Loss Data Analytics (https://openacttexts.github.io/LDAVer2/ChapCredibility.html). The new mission formalises how these exact deterministic weight and risk formulae change with exposure.
Let P be a nonnegative real representing total risk exposure. EPV is strictly positive, while VHM is nonnegative and may equal zero for a homogeneous risk class. The credibility factor Z(P) is P times VHM divided by the sum of P times VHM and EPV. A credibility premium combines the policyholder's experience rate with the collective mean using weights Z(P) and 1-Z(P). A normalised optimal quadratic prediction error is EPV times VHM over the same positive denominator. A scaled quadratic expression captures the trade-off between random process noise and between-risk heterogeneity.
The formal targets progress from structural boundary identities to financial sensitivity and the full capstone. Supporting theorems remain genuine Open declarations until accepted Lean proofs are submitted; no previously accepted proof is silently assumed.
The exact theorem name is ActuarialValuation.exposureCredibilityWeight_zero. Without any exposure, the experience credibility weight must be zero, provided the process variance is strictly positive.
The exact theorem name is ActuarialValuation.exposureCredibilityPremium_between. As the credibility weight lies in the unit interval, a lower observed claim rate produces a premium bounded by the observed and collective rates.
The exact theorem name is ActuarialValuation.exposureCredibilityAccuracy_fundamental. The capstone reconciles exposure-driven increases in credibility with the monotone decline of minimum expected squared error, including the zero heterogeneity boundary.
The graph also contains separately stated supporting inequalities and exact definitions, with the intended original derived mathematical identity written out in every milestone.
Experience-rating systems can be checked for sensible monotonicity when an additional policy year or risk exposure enters the rating base. Larger exposure should not decrease the weight assigned to otherwise unchanged policy experience and should not increase the theoretically optimal error. The classical structure of Bühlmann credibility and its use of EPV and VHM are described by Loss Data Analytics (https://openacttexts.github.io/LDAVer2/ChapCredibility.html). These precise algebraic statements are reusable for downstream weighted risk models, rating systems and numerical sensitivity checks.
Credibility is a rational function whose denominator could vanish under an invalid zero-process-variance model. The hypotheses impose strictly positive EPV and retain zero VHM as a legitimate boundary. Monotonicity is therefore weak, not strict, since a homogeneous portfolio provides no justification for relying more on experience. Comparisons between two exposures must use the same structural parameters, otherwise a change of class could reverse the effect. The theorem relating quadratic risk and the credibility weight is a genuine completing-square identity, while the mission does not assert that an arbitrary Bayesian posterior has linear form.
Lean uses exact real arithmetic for exposure, EPV, VHM, premium and risk formulae. The finite statistical model is reduced to its deterministic structural-parameter consequences; estimation of the parameters and robustness of individual claims are outside the scope. The theorem graph begins with positivity and zero-exposure boundaries, continues through weight and premium identities, and ends with a conjunction linking increasing credibility to decreasing minimal prediction error. The mathematical framework is known, but the newly stated Lean specialisations have to be proved and exclude vacuous denominator cases.
The pinned Mathlib revision and the precise Lean type of each definition or proposition are authoritative. The imported source must use targeted Mathlib modules; one large aggregate compiler check never substitutes for testing individual definition imports and obsolete namespace openings. The source-specific intermediate statements separate units and hypotheses. The finite index always counts claims, scenarios, or observations according to the declaration, not an implicit probability measure. In an insurance pricing setting the difference between a gross loss, a ceded payment, a net premium and a credibility risk estimate is financially important. A positive coefficient does not by itself imply the coefficients sum to one. Likewise a deterministic algebraic identity does not grant stochastic independence or a forecast model. These restrictions preserve the distinction between a purely algebraic result and a probabilistic interpretation. The formal theorem declarations have to maintain exactly the same quantifiers, arithmetic operations and endpoint conventions as the descriptions, including meaningful boundary cases. Future extensions can introduce richer distributions and dependence without altering the precise finite identities established here.
S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015, printed page 489. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
Frees and colleagues, Loss Data Analytics: Experience Rating Using Credibility Theory, 2024. https://openacttexts.github.io/LDAVer2/ChapCredibility.html
The stop-loss transform is the expected value of the positive excess of a claim above an attachment, an important building block of actuarial risk ordering. Increasing retention should never increase an otherwise unchanged pure reinsurance premium. A second useful criterion is that the decrease in price should not exceed the increase in retention, once scenario probabilities are normalised. Insurance mathematics describes stop-loss premiums as decreasing functions of the deductible (https://www.researchgate.net/publication/4958878_The_Concept_of_Comonotonicity_in_Actuarial_Science_And_Finance_Theory). This mission additionally identifies their convexity in retention and develops finite verification targets for the exact bound.
A real loss X(s), a real attachment d and a real scenario weight w(s) determine a positive excess payment max(X(s)-d,0). The pure stop-loss premium at d is the weighted finite sum across s in the range from zero through bound B. Scenario weights are nonnegative for premium-order and convexity theorems. Their finite total W may be arbitrary, while W=1 expresses a genuine probability distribution and yields a sharp unit Lipschitz constant. Two attachments a and b can be combined by d(theta)=(1-theta)a+theta b, with interpolation weight theta between zero and one.
The formal targets progress from structural boundary identities to financial sensitivity and the full capstone. Supporting theorems remain genuine Open declarations until accepted Lean proofs are submitted; no previously accepted proof is silently assumed.
The exact theorem name is ActuarialValuation.retentionExcessPositive_nonneg. An excess loss payment cannot be negative even for signed real inputs, since the positive part is the maximum against zero.
The exact theorem name is ActuarialValuation.retentionStopLossPremium_zero_weight. With no scenario mass, a finite net premium is zero regardless of loss amounts and attachment.
The exact theorem name is ActuarialValuation.retentionStopLossSensitivity_fundamental. The capstone states the three structural constraints on an actuarially valid premium curve, including convex interpolation, when finite scenario weights are normalized.
The graph also contains separately stated supporting inequalities and exact definitions, with the intended original derived mathematical identity written out in every milestone.
These conditions provide powerful reasonableness checks for treaty pricing functions. An actuary can diagnose a premium that rises with retention, or an implausibly large fall inconsistent with maximum ceded-payment change, before relying on a stochastic model. The classical stop-loss transform is extensively studied in insurance finance (https://www.researchgate.net/publication/4958878_The_Concept_of_Comonotonicity_in_Actuarial_Science_And_Finance_Theory). The reusable finite inequalities connect claim severity, scenario weights and contract terms, and can support downstream optimisation, layered reinsurance sensitivity and refinement of discrete tail distributions.
The positive part is a maximum of two affine functions, which is convex but not differentiable when the claim equals the retention. The finite theorem must not assume every claim is above a or b: a distribution can straddle both attachment points. The premium derivative is not required, since pointwise algebraic inequalities suffice to justify convex interpolation and monotone order. The mass-dependent Lipschitz bound becomes one only when total mass is one, so probability normalisation must be stated. Claim severity need not be nonnegative for the algebraic result, while weights must be nonnegative for order preservation.
The Lean representation uses real numbers for claim severities, deductibles, masses and convex interpolation. Finite scenarios are represented by natural indices and Finset.range. Positive excess is a maximum of two real numbers. All inequalities are original derived finite specialisations of well-known stop-loss facts, with explicit mathematical types and numerical boundary conventions. The formalisation intentionally excludes continuous distributions, derivatives, infinite-dimensional weak convergence and loaded commercial premium assumptions. The main goal is nontrivial because it demands the general weighted convexity and Lipschitz properties for an arbitrary finite loss table.
The pinned Mathlib revision and the precise Lean type of each definition or proposition are authoritative. The imported source must use targeted Mathlib modules; one large aggregate compiler check never substitutes for testing individual definition imports and obsolete namespace openings. The source-specific intermediate statements separate units and hypotheses. The finite index always counts claims, scenarios, or observations according to the declaration, not an implicit probability measure. In an insurance pricing setting the difference between a gross loss, a ceded payment, a net premium and a credibility risk estimate is financially important. A positive coefficient does not by itself imply the coefficients sum to one. Likewise a deterministic algebraic identity does not grant stochastic independence or a forecast model. These restrictions preserve the distinction between a purely algebraic result and a probabilistic interpretation. The formal theorem declarations have to maintain exactly the same quantifiers, arithmetic operations and endpoint conventions as the descriptions, including meaningful boundary cases. Future extensions can introduce richer distributions and dependence without altering the precise finite identities established here.
S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015, printed page 409. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
Denuit and colleagues, The Concept of Comonotonicity in Actuarial Science and Finance: Theory, 2002. https://www.researchgate.net/publication/4958878_The_Concept_of_Comonotonicity_in_Actuarial_Science_And_Finance_Theory
Sampling an entire finite-state execution is a different computational task from recognizing a supplied word. A membership circuit must answer correctly on its given input. A sampler instead chooses the input together with its associated output, while preserving their joint distribution. This distinction is relevant when finite-state models describe allowable executions and when parallel generation should avoid a sequential pass through every transition. The source paper establishes constant-depth sampling results for regular languages and finite Markov chains in Appendix E (Zhang et al., 2026).
The mission concerns that appendix's finite-state sampling results. It formalizes all six numbered results E.1–E.6, together with the seed bounds stated in the surrounding text. Each milestone points to a published theorem with a separately checked proof. The objects to sample are complete words, word–acceptance pairs, and complete state trajectories. Sampling only the final state would lose the joint temporal information required by the targets.
A binary deterministic finite automaton has finitely many states, a designated start state, a transition for each state and bit, and a set of accepting states. Starting from its initial state, a binary word of length determines a run. Let be the set of words whose final state is accepting. Put . An arbitrary such automaton represents an arbitrary binary regular language, with no assumption that membership belongs to .
A finite Markov chain consists of a nonempty finite state set , an initial probability vector , and a row-stochastic transition matrix . Entries are nonnegative real numbers, not restricted to rational numbers. For , its probability is . The distribution of all states is denoted . For , conditioning is allowed when the probability that is positive.
A randomized sampler is a deterministic Boolean circuit supplied with independent, unbiased random bits. AND and OR gates have unbounded fan-in; NOT gates and Boolean constants are permitted. Its size is polynomial and its depth has a constant bound independent of trajectory length. Approximate families are nonuniform in both and their real error tolerance : existence does not require efficiently computing circuit descriptions or numerical tables from a supplied transition matrix.
The main goal is the conjunction of all results E.1–E.6, including the linear seed guarantee for E.5. This organizational theorem is not an additional numbered result attributed to the paper. All six milestones must be proved for the goal to hold. The exact Markov sampling criterion in Theorem E.5 is one component. A nonnegative real number is dyadic if it equals for natural numbers , including zero. A chain is path-dyadic when every finite trajectory, including a trajectory of length zero, has a dyadic probability. The target is
On the left, the family has polynomial size in and depth bounded independently of . A supporting target records the linear fair-bit budget when path-dyadicity holds. Lemma E.4 supplies another target: every path-dyadic chain is the coordinatewise projection of a finite chain whose initial and transition probabilities are all dyadic. Path-dyadicity must not be replaced by the stronger requirement that the original transition matrix itself be dyadic (Appendix E.3).
Theorem E.1 concerns exact sampling of a uniformly random word together with its acceptance indicator:
The sampler uses exactly fair bits, polynomial size, and depth depending only on the fixed automaton. This is a sampling assertion and does not assert that membership can be computed in constant depth on an arbitrary externally supplied word.
Theorem E.2 concerns the uniform law on nonempty . For every , the target is
Every possible output is accepted. Size is polynomial in and , and depth depends only on the fixed language or its automaton. In particular, the leading coefficient of the term in the random-bit bound is one (Appendix E.2).
Theorem E.6 is the corresponding approximate target for trajectories conditioned on . It requires total variation error at most , only positive-probability outputs ending in , fair bits, polynomial size in and , and depth depending only on the chain. There is no lower bound on the conditioning probability beyond strict positivity (Appendix E.4).
Lemma E.3 supplies the exact representation used in the Markov construction. A transition-dyadic chain is represented by one binary DFA and a fixed state projection. On a uniform input of length , with positive constants , the states observed after bits project to exactly the complete trajectory law of the chain. The same DFA and projection work for every length, including zero.
These results separate sampling an input together with its finite-state behavior from computing that behavior on a prescribed input. They also identify a precise obstruction to exact sampling with a finite fair-bit seed: each output probability must be dyadic. Approximate sampling allows arbitrary real transition probabilities while retaining the valid trajectory support. The complete trajectory requirement preserves correlations among all time coordinates.
The formalization makes the circuit model, seed accounting, support guarantees and asymptotic quantifiers explicit and reusable. The theorem statements and their separately submitted proofs have passed the platform verifier. The goal proof imports all six milestones; its E.5 milestone in turn imports both the equivalence and the linear seed theorem. Thus the platform dependency graph covers the entire appendix. Platform verification establishes the formal statements; semantic correspondence is documented in the statement descriptions and source references.
A literal step-by-step implementation of a run makes circuit depth grow with , so it does not meet the constant-depth target. Recognition results alone do not furnish the required joint sampler. For approximate word sampling, an error estimate alone is insufficient: the output must remain in the accepted support, and the coefficient-one seed bound must also hold. For exact Markov sampling, unreachable states and non-dyadic individual transitions prevent identifying the desired criterion with entrywise dyadicity. Conditioning on a rare terminal event must not introduce an unstated dependence on its probability.
States are indexed by finite types . Binary words have type ; trajectories have coordinates. Markov vectors and matrices are real-valued and carry normalization and nonnegativity proofs. Sampling probabilities are defined by counting all seeds that give a particular encoded outcome and dividing by . Total variation is half the finite sum of absolute probability differences.
The circuit representation is an explicit topologically ordered gate list with checked wire references. Size counts input bits, gates, gate-input wires and output wires; this yields the usual polynomial-size class. State trajectories use a fixed one-hot encoding at each time coordinate. The invalid-output predicate is checked over every seed, so neither arbitrary decoders nor unrepresented outcomes can satisfy an exact or support-preserving claim. The encodings used by the targets are injective. The circuit family is existentially quantified after the fixed finite-state model; the depth and polynomial constants precede and .
Zero-length words and zero-transition Markov paths are included. The word target excludes empty accepted slices. The conditioned target excludes zero-probability conditioning events. Definitions of division by zero still exist as total Lean functions, but the hypotheses exclude those cases from approximate claims. Extensions of these results, reusable finite-state probability lemmas, and further circuit constructions are welcome. No sampler-existence axiom, vacuous model or final-state-only replacement is part of the interface.
Per-occurrence excess and aggregate excess have different financial triggers. One aggregate deductible applies once to the sum of claims, while a per-risk retention is charged against each loss. Combining many small claims may exhaust an aggregate deductible without producing a payment under any separate per-claim policy. HMRC explains how non-proportional reinsurance differs across individual risks and catastrophe or aggregate protections (https://www.gov.uk/hmrc-internal-manuals/general-insurance-manual/gim8060). The valuation question is how the ceded amounts and their pure expected costs are ordered when otherwise identical annual experience and deductibles are used.
The individual claims x(i), their finite number n, and the deductible d are natural-number monetary quantities. Gross aggregate loss S(n) is the sum of the first n claims. Aggregate recovery is positive excess of S(n) above d; separate per-claim recovery is the sum of each claim's positive excess over d. Finite scenario weights w(s) are real. A scenario maps to an entire loss sequence, and its total claim portfolio is evaluated consistently under both treaty designs. Weighted claims are aggregated for indices from zero to a finite bound B, allowing the scenario count itself to be zero or the probability weights to lack normalisation.
The formal targets progress from structural boundary identities to financial sensitivity and the full capstone. Supporting theorems remain genuine Open declarations until accepted Lean proofs are submitted; no previously accepted proof is silently assumed.
The exact theorem name is ActuarialValuation.aggregateLossTotal_zero. An empty collection of claims has zero gross claims and therefore defines the base case for deductible comparisons.
The exact theorem name is ActuarialValuation.aggregateDeductibleCeded_zero_attachment. With attachment zero, the aggregate excess treaty covers every unit of gross annual claims.
The exact theorem name is ActuarialValuation.aggregateVsPerClaim_fundamental. The capstone joins the nontrivial pointwise reinsurance coverage inequality to the same ordering of expected pure premiums, without conflating a whole-year treaty with a per-claim deductible.
The graph also contains separately stated supporting inequalities and exact definitions, with the intended original derived mathematical identity written out in every milestone.
The comparison can diagnose material pricing errors, since an aggregate deductible and a per-risk deductible with the same quoted monetary value should not normally have the same technical premium. HMRC's treatment of non-proportional reinsurance (https://www.gov.uk/hmrc-internal-manuals/general-insurance-manual/gim8060) makes this distinction a contractual reality. The formal theorem is useful for ceded reserve reconciliation, claims-data audit, treaty design, and future models including several occurrence covers within a separate annual limit. In each case exact mathematical relationships are more valuable than approximate simulation agreement.
The algebra of positive-part natural subtraction differs from ordinary subtraction over integers or real values. The aggregate deductible is taken once, whereas the per-event premium subtracts the same amount separately from each positive claim. The theorem is a weak inequality and must remain valid even when every event is below the separate retention but the aggregate exceeds the annual attachment. The model explicitly includes zero claims, zero deductible, empty portfolios and nonnegative scenario weights. Signed weights would make the expectation order invalid and are not silently permitted in that result.
Lean treats all claim amounts, event counts, attachment values and scenario bounds as natural numbers. Real numbers occur only in the finite expected ceded amounts. Each individual-claim sum uses Finset.range and the pure premium is a further finite sum over scenarios. This is an exact deterministic relationship between two reinsurance structures rather than an assumption of independence or identical event distributions. No catastrophe frequency model, claims adjustment expenses or risk load is included. The established contractual idea motivates original derived finite relations, and the formal statements remain open until proved.
The pinned Mathlib revision and the precise Lean type of each definition or proposition are authoritative. The imported source must use targeted Mathlib modules; one large aggregate compiler check never substitutes for testing individual definition imports and obsolete namespace openings. The source-specific intermediate statements separate units and hypotheses. The finite index always counts claims, scenarios, or observations according to the declaration, not an implicit probability measure. In an insurance pricing setting the difference between a gross loss, a ceded payment, a net premium and a credibility risk estimate is financially important. A positive coefficient does not by itself imply the coefficients sum to one. Likewise a deterministic algebraic identity does not grant stochastic independence or a forecast model. These restrictions preserve the distinction between a purely algebraic result and a probabilistic interpretation. The formal theorem declarations have to maintain exactly the same quantifiers, arithmetic operations and endpoint conventions as the descriptions, including meaningful boundary cases. Future extensions can introduce richer distributions and dependence without altering the precise finite identities established here.
S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015, printed page 389. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
HM Revenue & Customs, General Insurance Manual: Non-proportional reinsurance, GOV.UK, 2023. https://www.gov.uk/hmrc-internal-manuals/general-insurance-manual/gim8060
Hattendorff's theorem allocates the variance of an insurer's life-contingent loss to policy years. In a fully discrete life insurance model, each policy year's contribution depends on the discounted net amount at risk, the probability of dying in that year, and the conditional probability of surviving the year. Shiu and Xiong (1) derive the classical loss-at-issue formula and the corresponding discrete Hattendorff variance through reserve identities and a summation-by-parts argument. Gerber [2, §6.7] discusses the actuarial allocation of total loss to individual policy years.
The related Missions XVI and XIX address two complementary parts of that argument. XVI specifies death/survival masses for a finite lifetime distribution and proposes proofs of centred annual mortality innovations, cross-year orthogonality and variance. XIX describes a pathwise, year-by-year accounting identity expressing insurer loss, including the terminal reserve, as the opening reserve plus discounted mortality innovations. The present mission is the mathematical bridge combining these structures.
It targets the full finite-horizon reserve-loss expectation and variance theorem under consistent conditional mortality probabilities and the annual prospective reserve recurrence. Unlike a purely algebraic zero-covariance lemma, the mortality model supplies the orthogonality. Unlike a standalone cashflow telescoping lemma, the result calculates the variance of the insurer's actual policy loss.
Fix a finite scenario space , with nonnegative probabilities summing to one, and a curtate future lifetime . An insured with dies during policy year .
Define the in-force and death-year probability masses
The disjoint survival/death partition gives . For each year covered by the policy valuation horizon, assume positive in-force mass, , so that the conditional death and survival rates are well-defined:
These rates are derived from one joint lifetime distribution. The annual death indicators are therefore linked across years and are not independent. The zero-covariance result must be derived from the nested survival-event structure rather than assumed.
Let denote the finite number of years covered, a deterministic annual discount factor, the beginning-of-year premium, the death benefit payable at time , and the prospective reserve at time for a policy still in force.
Assume that, for each year , the prospective reserve satisfies
The realised insurer loss, valued at issue, is
The terminal reserve is explicitly included if the insured survives beyond the chosen horizon. Thus , a life may remain insured after year , and neither nor is assumed zero. The original Shiu–Xiong complete-life issue-loss formula is recovered only under appropriate terminal/residual liability conditions; the present finite-horizon formula is the reserve-inclusive extension needed for a finite theorem.
The year- mortality innovation is
The discounted net amount at risk is
By the annual reserve recurrence and the in-force event partition, the change in the insurer's loss across a policy year equals . Summing over years gives the exact pathwise representation
Mission XIX describes this pointwise reserve-loss identity. The present formalisation must bridge XIX's realised-death-year indicator and reserve-derived innovation to XVI's scenario-based mortality innovation. They represent the same object when the death probabilities are calculated from the same model.
From the finite scenario lifetime law and , the annual innovations satisfy
The final factor is the conditional one-year survival probability and is essential to the fully discrete variance formula. It must not be replaced by an assumed independence condition or omitted by importing a continuous-time formula.
Taking expectations of the pathwise identity, using , yields
The variance of an insurer loss is unaffected by adding a deterministic opening reserve when the probability weights have unit total mass. Consequently,
The capstone combines these two results, with no unproved independence assumption. Its mathematical hypotheses explicitly include nonnegative, normalised scenario weights, positive in-force probability for every year in the range, and the one-year reserve recurrence with conditional rates computed from the given lifetime distribution.
The theorem remains valid at : the insurer's finite-horizon loss is deterministically , and the variance sum is empty and equals zero.
The exact final theorem is ActuarialValuation.finiteHattendorffReserveLoss_fundamental. This result is nontrivial at positive horizons. The formal model does not assert independence, fix the opening reserve to zero, or substitute a deterministic insurer loss.
The annual decomposition separates valuation assumptions from stochastic fluctuations in mortality. Shiu and Xiong's classical fully discrete treatment (https://doi.org/10.1007/s13385-020-00256-9) emphasises that a survival factor remains in each annual variance contribution. Preserving this factor makes the result useful for actuarial risk allocation and for reconciling the valuation reserve with actual finite-period insurer loss.
The finite-scenario definitions are reusable in downstream insurance valuation missions, for example multiple-decrement reserves and explicit conditional mortality shock models. The result also supplies finite boundary tests for nonzero opening reserves, death exactly at the horizon, and survival beyond the final premium year.
Annual death events arise from the same curtate lifetime, so their indicator variables have nested dependence. Their centred innovations have vanishing cross-year covariance only under the correct conditional in-force rates and probability-weighting conventions. Incorrect denominators or an unproved independence assumption would change the result.
The pathwise identity also accounts for different timing of premiums and benefits, and includes a terminal reserve for survivors. At the last covered year a policy death and survival are disjoint, so the last benefit and terminal reserve must not both be counted. The exact Lean imports must retain the definitions and parameter order of the previously published mortality and loss modules.
The Lean 4 model uses a finite scenario type with Fintype, real-valued weights, a natural-number curtate lifetime, and the published definition modules from related actuarial missions. Four new definitions and 13 Open theorem obligations form the formal graph, including 12 supporting targets before the conjunction capstone. The accepted proof status of another theorem is never inferred merely from its publication.
The result is finite horizon, finite probability space and fully discrete. The source's complete-life identity would additionally require justified limiting arguments, the disappearance (or valuation) of terminal reserves, integrability and interchange of expectation, variance and limit. None of those conditions is silently assumed here. There is no continuous-time martingale or Lévy-process result in this mission.
The classical full-life result is known mathematically, while the specific finite-horizon Lean declarations remain open proof targets. A compiler-accepted declaration with a sorry body does not establish a proof.
A bounded linear operator between Banach spaces is Fredholm if its kernel is finite-dimensional and its range is closed and of finite codimension. Its index
is an integer that survives deformation: it does not change under small perturbations or under compact perturbations, and it is additive under composition. These properties make Fredholm operators the setting for index theorems. Elliptic differential operators on compact manifolds, Toeplitz operators, linearized Cauchy–Riemann operators in symplectic topology, and the linearizations of nonlinear Fredholm maps in transversality arguments (Sard–Smale) all rest on them. Atkinson's theorem characterizes Fredholm operators as those invertible modulo compact operators. For endomorphisms this says that the image in the Calkin algebra is invertible.
This mission formalizes the abstract theory on Banach spaces over or , following N. Bourbaki, Théories spectrales, Chapitre III, §§ 3–5 (Springer, 2023). It builds on Mathlib's ContinuousLinearMap.IsFredholm, which already provides the definition and its equivalent descriptions on topological vector spaces. It adds the index and the results listed below.
is or . , , are Banach spaces over , and is the Banach space of bounded linear maps with the operator norm.
IsCompactOperator).is Fredholm if and only if there is such that and are compact (Bourbaki III, §5, Corollaire 1, TS III.74).
The result. Atkinson's theorem identifies the Fredholm operators with the units modulo the compact ideal. Together with the stability of the index under compact and small perturbations, it is the abstract input of every Fredholm index computation. Examples are the Fredholm alternative for integral equations, the index of Toeplitz operators, and the index of elliptic and Cauchy–Riemann operators on compact or punctured surfaces.
Formalizing it. Mathlib defines Fredholm operators on topological vector spaces (ContinuousLinearMap.IsFredholm) and proves that four descriptions agree (isFredholm_tfae). It has no index, no statement about compositions, and no perturbation theory. Its documentation lists the Banach-space criterion (milestone 2) and the restriction statement (milestone 5) as not yet formalized. The library built here is intended for reuse by any later index computation.
The statements combine linear algebra and topology. The index is a difference of dimensions of a subspace and a quotient space, and every statement about it carries a Fredholm hypothesis, since Module.finrank is on infinite-dimensional spaces. Openness and local constancy are statements about the operator-norm topology on , and the perturbation statements involve operators that are compact but not necessarily of finite rank. The completeness hypotheses are part of the statements: over incomplete normed spaces, a range of finite codimension need not be closed.
FredholmBanach. The definition module FredholmBanach_Setting defines only index. Fredholm operators are Mathlib's ContinuousLinearMap.IsFredholm and compact operators are Mathlib's IsCompactOperator.[RCLike 𝕜], [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E], and likewise for F and G. Bourbaki states several results for locally convex or Fréchet spaces; this mission specializes all of them to Banach spaces.index u = finrank 𝕜 u.ker - finrank 𝕜 (F ⧸ u.range) in ℤ. Module.finrank is on infinite-dimensional spaces, so index is meaningful only for Fredholm u. Every statement about it assumes u.IsFredholm.finrank 𝕜 (E ⧸ E₁), and "finite codimension" is FiniteDimensional 𝕜 (E ⧸ E₁). The restriction in milestone 5 is ContinuousLinearMap.restrict.E ≃L[𝕜] F. "Finite rank" is FiniteDimensional 𝕜 (u - e).range.Contributions welcome: reusable general-purpose lemmas about bounded and compact operators between Banach spaces.
Let be a loop of symmetric matrices. The asymptotic operator
acts on loops . It appears wherever a pseudoholomorphic curve approaches a periodic orbit. Near a puncture, a finite-energy curve in a symplectization converges to a Reeb orbit, and in a trivialization along that orbit the linearized Reeb flow is . The operator is the Hessian of the action functional at that orbit. The rate of approach and the winding of the curve around the orbit come from its eigenfunctions (Hofer–Wysocki–Zehnder 1995). In Floer theory the operator is the Hessian of the symplectic action at a -periodic orbit, and the gradient-flow operator is the linearized Floer operator (Robbin–Salamon 1995).
The operator links functional analysis to the linear algebra of stage I. is nondegenerate, i.e. is not an eigenvalue, exactly when the time-one map of the linearized flow has no eigenvalue . Then lies in and has a Conley–Zehnder index. The Fredholm index formula for Cauchy–Riemann operators on punctured surfaces is written in terms of the Conley–Zehnder indices of the asymptotic operators at the punctures (Wendl, Lectures on SFT, Lecture 3).
This is stage II of a series that formalizes the Fredholm theory of linearized Cauchy–Riemann operators. Stage I (Conley–Zehnder Index I: Axiomatic Characterization on Paths of Symplectic Matrices) characterizes the Conley–Zehnder index on . This stage sets up the spectral theory of asymptotic operators: the operator itself, self-adjointness, discrete spectrum, compact resolvent, and the dictionary between the kernel of and the time-one map. Later stages are the Fredholm theory of in Banach spaces, elliptic regularity for , and the index formula.
with its Haar probability measure. has coordinates and the Euclidean inner product, and
is continuous with for every .
For every continuous loop of symmetric matrices:
The result. These are the analytic facts that every use of asymptotic operators relies on. Self-adjointness and the discrete spectrum define the eigenvalue branches and the spectral flow. The compact resolvent makes Fredholm of index for every real , and the weighted Sobolev spaces of the later Fredholm theory are chosen with weights avoiding the spectrum. The kernel dictionary identifies nondegenerate asymptotic operators with the paths of stage I. It is the bridge through which Conley–Zehnder indices enter the index formula.
Formalizing it. All results here are classical. Mathlib has partially defined linear maps and their adjoints, the Fourier basis of on the circle, and compact operators. It has no Sobolev spaces on the circle, no unbounded operator with discrete spectrum beyond trivial cases, and no first-order differential operator treated as an unbounded operator. This stage builds the first such example. The same pattern applies to other first-order elliptic operators on , and the library is reusable for spectral flow and for Floer-type operators.
is unbounded and not defined on all of , so self-adjointness is a statement about the domain of the adjoint, not a symmetry identity. The spectral statements concern the resolvent of a first-order differential operator with non-constant coefficients, as an operator on . The kernel dictionary relates classes, defined through Fourier coefficients, to classical solutions of a linear ODE. The statements about concern linear ODEs whose coefficients are only continuous.
AsymptoticOperator; all definitions are in AsymptoticOperator_Setting, which imports stage I's ConleyZehnder_Setting (for Mat n, J₀, IsSymplectic and SP).UnitAddCircle () with AddCircle.haarAddCircle. is Lp (EuclideanSpace ℝ (Fin n ⊕ Fin n)) 2 haarAddCircle, a real Hilbert space.fourierCoeff, applied to the componentwise complexification . and act on through the real-to-complex coercion.LinearPMap, defined by choice as the map whose graph is the set of pairs satisfying the coefficient identity. The fallback is , and milestone 1 makes it unreachable. Self-adjointness is Mathlib's IsSelfAdjoint for LinearPMap, and symmetry is IsFormalAdjoint.HilbertBasis of eigenvectors whose eigenvalues tend to in absolute value along the cofinite filter. This covers , where .Contributions welcome: reusable lemmas on Sobolev spaces of vector-valued functions on the circle (Fourier characterization, continuity of functions), on unbounded self-adjoint operators with compact resolvent, and on linear ODEs with continuous periodic coefficients.
A small insurance fund or participant with limited resources can gain or lose capital repeatedly and be forced to stop at one of two barriers. This is the familiar gambler's ruin problem, useful as a discrete illustration of capital adequacy, finite-state absorption and the distinction between ruin and eventual success. Promislow's treatment derives fair and biased cases using finite capital and a bounded opponent, and Grinstead and Snell present related random-walk absorption probabilities (https://stats.libretexts.org/Bookshelves/Probability_Theory/Introductory_Probability_%28Grinstead_and_Snell%29/12%3A_Random_Walks/12.02%3A_Gambler%27s_Ruin). The practical distinction is whether a probability refers to absorption at some eventual time or only to absorption within a fixed number of additional bets.
A unit-stake capital process occupies a natural-number capital state i between zero and a positive upper barrier N. With probability p the next bet raises capital by one unit; with complementary probability one minus p it lowers capital by one unit. Capital zero and capital N are absorbing. The fair case has p equal to one-half and a linear harmonic success function. In the biased case, a down-to-up odds ratio r is defined by (1−p)/p. An additional finite-horizon model records separately the chance of hitting the upper barrier and the chance of hitting zero before a given step count, leaving unresolved paths in the interior.
The fair finite-capital eventual upper-absorption harmonic candidate is named actuarial_gamblerFairSuccess in the Lean development. A fair unit-stake random walk on capital states zero through positive target N has eventual upper-barrier success probability i/N when starting from integer capital i in the bounded interval. This source defines the harmonic candidate, not the underlying stochastic stopping-time construction.
The downward-to-upward transition probability ratio is named actuarial_gamblerOddsRatio in the Lean development. The fixed probability of an up step is p; the probability of a down step is 1−p. Their ratio (1−p)/p controls the biased harmonic solution and requires p>0 to be interpreted as transition odds.
The biased finite-capital upper-absorption harmonic candidate is named actuarial_gamblerBiasedSuccess in the Lean development. For a biased unit-stake walk with r=(1−p)/p different from one and a positive upper barrier N, the formula gives the eventual probability of hitting N before zero: (1−r^i)/(1−r^N). The denominator must be nonzero. The fair p=1/2 case requires the separate linear formula.
The probability of hitting upper capital target within finitely many steps is named actuarial_gamblerFiniteSuccess in the Lean development. The bounded random walk makes unit upward jumps with probability p and unit downward jumps with probability 1−p. It is absorbed at capital zero or at or above target N. This finite-horizon recursion records only the probability of reaching the success barrier by time n; ongoing paths at the horizon remain unresolved.
The probability of reaching zero capital within finitely many steps is named actuarial_gamblerFiniteRuin in the Lean development. The second finite-horizon recursion tracks absorption at zero capital, the ruin boundary. Successful absorption at the upper target contributes zero ruin probability. At an interior state it mixes successor ruin probabilities, and paths still active at horizon n contribute to neither finite success nor finite ruin.
The formal targets are ordered from elementary boundary and consistency claims to their combined capstone. The exact Lean identifiers below are the authoritative local targets; none of the listed theorem bodies is already accepted as a machine-checked proof. The mathematical results themselves are established actuarial or probability identities.
The declaration ActuarialValuation.gamblerFairSuccess_zero states the following relation. The fair candidate's numerator is zero at the lower absorbing boundary, so the proposed upper-barrier success probability is zero even if the target denominator is algebraically zero.
The declaration ActuarialValuation.gamblerFiniteRuin_nonneg states the following relation. Ruin starts at the boundary indicators zero or one and evolves through nonnegative weighted averages at every interior capital state. Therefore finite-horizon absorption-at-zero probability cannot be negative under valid win probabilities.
The declaration ActuarialValuation.gamblerBoundedRuin_fundamental states the following relation. The capstone formalises the correct first-step harmonic equations for the fair and biased finite-capital random walk and nonnegative bounded finite-horizon absorption-event probabilities. Unlike an infinite-horizon gambler's ruin theorem, it does not assert that every path has already been absorbed by a finite horizon or identify finite success directly with the harmonic candidate.
The exact harmonic functions identify candidate upper-absorption probabilities for fair and biased walks, while the finite-horizon recursions quantify how much absorption can have occurred after a specified number of steps. The latter distinction matters for capital planning because some solvent paths may still be active when an assessment period ends. Standard treatments show the importance of the bias ratio and the two absorbing barriers (https://stats.libretexts.org/Bookshelves/Probability_Theory/Introductory_Probability_%28Grinstead_and_Snell%29/12%3A_Random_Walks/12.02%3A_Gambler%27s_Ruin). The mathematical identities themselves are known; a Lean representation offers checkable conventions around capital zero, positive target, finite horizon and the singular fair limit. Its state-recursion definitions can be reused in finite Markov reward and insurance capital models.
The fair success expression cannot simply be obtained by substituting p=one-half into the biased quotient: both its numerator and denominator become zero. The separate linear expression needs its own fair-case convention. A second easy mistake is to regard finite-horizon success and ruin as exhaustive complementary events. They are disjoint, but an interior path may reach neither barrier during the available number of steps. At extreme probabilities zero or one, the odds ratio may be undefined or degenerate, and an eventual absorption assertion requires hypotheses not present in a finite first-step equality. These boundary distinctions are central to the stated target.
Lean uses natural numbers for capital, positive upper barrier and finite horizon, with real-valued probabilities and harmonic candidate functions. Both boundary states are absorbing; ruin is capital equal to zero, unlike the strictly negative surplus convention in another insurance reserve model. The biased quotient is used only when its normalising denominator is nonzero, and the fair case is represented separately. The source does not assert almost-sure absorption or equality of finite-horizon success with an eventual harmonic function, and it does not equate unresolved paths with failure. Mathlib finite recursion and rational function arithmetic support the scope. Reusable contributions include independent success/ruin state operators, boundary-state lemmas and nonnegative weighted continuation bounds.
The five local definitions form the available mathematical vocabulary: actuarial_gamblerFairSuccess, actuarial_gamblerOddsRatio, actuarial_gamblerBiasedSuccess, actuarial_gamblerFiniteSuccess, actuarial_gamblerFiniteRuin. Their support conditions, nonzero denominators, and variable types are fixed by the Lean declarations rather than inferred from examples. The nontrivial mathematical content must not be replaced by a vacuous premise or by a special case that bypasses the model boundaries. The existing paper mathematics is known, while these particular theorem declarations remain formalisation targets with no accepted proofs. Contributions that strengthen reusable finite identities or expose missing boundary hypotheses are appropriate, provided they preserve the exact authoritative theorem types.
S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
Charles M. Grinstead and J. Laurie Snell, Introduction to Probability, American Mathematical Society, 1997. https://stats.libretexts.org/Bookshelves/Probability_Theory/Introductory_Probability_%28Grinstead_and_Snell%29/12%3A_Random_Walks/12.02%3A_Gambler%27s_Ruin
Non-proportional reinsurance allows an insurer to retain ordinary claims while transferring part of the cost of larger claims to a reinsurer. Such contracts specify both an attachment point and a maximum amount the reinsurer will pay. Confusing the retention with the limit changes ceded payments, claims reporting and the net expected treaty cost. HMRC describes common non-proportional arrangements and their layers in its general-insurance technical guidance (https://www.gov.uk/hmrc-internal-manuals/general-insurance-manual/gim8080). Pricing systems must distinguish an unlimited excess claim from the finite reimbursement available under one layer, including claims exactly at the attachment or at the upper layer boundary.
A gross claim x, attachment d and layer width L are nonnegative natural-number amounts in the same currency unit. An unlimited excess contract pays only the positive part of x minus d. A capped ceded layer pays the smaller of that gross excess and L. Amounts beyond the top of the layer, d plus L, form a separate higher excess. The expected treaty cost is evaluated under a bounded severity distribution with nonnegative mass w(x) at each integer claim amount from zero through the finite bound B. An unlimited stop-loss expected cost uses the same distribution without a layer cap.
The single-claim positive excess over an attachment is named actuarial_layerExcessLoss in the Lean development. The claim amount remaining above the insurer's retained attachment is natural-number positive-part subtraction. Below attachment it is zero, matching the gross excess payment of an unlimited stop-loss treaty.
The capped single-layer reinsurance payment is named actuarial_layerCededPayment in the Lean development. For a claim amount x, a reinsurance layer of width or limit L attaching at d reimburses the lesser of excess x−d positive part and the layer limit. It pays zero below attachment and cannot pay more than L.
The remaining gross excess above the top of the layer is named actuarial_layerHigherExcess in the Lean development. Any part of the claim above the layer's upper attachment d+L is left for higher reinsurance layers or the ultimate insurer. It is the positive excess loss above the sum of the lower attachment and the stated layer width.
The finite aggregate expected ceded loss cost of a layer is named actuarial_layerExpectedCeded in the Lean development. The finite bounded claim-severity mass model computes the net expected excess-of-loss reinsurance premium by weighting each loss payment of the capped layer by its claim probability. Expected ceded cost excludes risk loading and expenses.
The finite unlimited stop-loss expected payment is named actuarial_layerExpectedExcess in the Lean development. The net stop-loss premium above an attachment d is the finite weighted expected excess claim amount without an upper layer cap. The difference of this value at d and at d+L will equal the capped layer's expected ceded cost.
The formal targets are ordered from elementary boundary and consistency claims to their combined capstone. The exact Lean identifiers below are the authoritative local targets; none of the listed theorem bodies is already accepted as a machine-checked proof. The mathematical results themselves are established actuarial or probability identities.
The declaration ActuarialValuation.layerExcessLoss_below states the following relation. When the claim amount does not exceed the attachment, no monetary loss lies above the retention. Saturating natural-number subtraction gives zero excess exactly.
The declaration ActuarialValuation.layerExpectedCeded_stoploss_difference states the following relation. The expected capped ceded payment equals the expected unlimited excess above attachment d, less the excess above the upper layer attachment d+L. The identity follows termwise from the exact pointwise loss partition and finite linearity, with no distribution-normalisation assumption.
The declaration ActuarialValuation.layerCededValuation_fundamental states the following relation. The capstone unifies a bounded single-claim excess-of-loss treaty's payment decomposition with the exact net layer premium as difference of two unlimited stop-loss premiums, and establishes its nonnegative bound against gross excess. It does not assert an expense-loaded reinsurance price or infinite-support integration.
The difference between net unlimited excess payments at two attachments gives an immediately auditable valuation of a finite reinsurance layer. A treaty administrator can reconcile the covered amount, the higher excess and the original unlimited amount without making assumptions about claim frequencies or total policyholder losses. This separation is useful in exposure rating and in modelling multiple reinsurance towers, including arrangements described in the HMRC guidance at https://www.gov.uk/hmrc-internal-manuals/general-insurance-manual/gim8080. The identity is already a standard insurance-payment relation; formalising its finite version would produce reusable payment functions and expected-cost inequalities rather than announcing a new result about treaty markets. It would also distinguish claim indemnities from premiums loaded for operating costs and capital.
An intuitive subtraction of the reinsurance limit from the gross excess can become negative and cannot describe the remaining claim burden below the top of a layer. Likewise, a formula that gives every loss above attachment an unlimited reimbursement silently overstates the provider's maximum liability. Natural-number subtraction in Lean saturates at zero, so any stated decomposition must respect positive-part semantics at both the lower and upper treaty thresholds. There are also two independent directions of monotonicity: increased layer width raises coverage, while a larger retention generally reduces the covered part. The capstone fixes only the former and the precise difference of stop-loss expected amounts.
The source uses natural numbers for money, including the deductible and treaty limit, and real numbers for bounded claim coefficients and expected ceded payment. There is no independent hidden frequency distribution, and the finite claim grid can include zero severity and zero layer width. Nonnegative weights are explicitly required for order and positivity conclusions, while pointwise payment identities hold without probability normalisation. The formalisation does not collapse a capped layer into a trivial unlimited excess contract, nor assume an expense-loaded market premium is equal to an actuarial expectation. Reusable contributions include positive-part payments, min-limited cover, finite layer aggregation and higher-attachment functions. Later models may combine several layers or add claims-inflation adjustments.
The five local definitions form the available mathematical vocabulary: actuarial_layerExcessLoss, actuarial_layerCededPayment, actuarial_layerHigherExcess, actuarial_layerExpectedCeded, actuarial_layerExpectedExcess. Their support conditions, nonzero denominators, and variable types are fixed by the Lean declarations rather than inferred from examples. The nontrivial mathematical content must not be replaced by a vacuous premise or by a special case that bypasses the model boundaries. The existing paper mathematics is known, while these particular theorem declarations remain formalisation targets with no accepted proofs. Contributions that strengthen reusable finite identities or expose missing boundary hypotheses are appropriate, provided they preserve the exact authoritative theorem types.
S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
HM Revenue & Customs, General Insurance Manual: Non-proportional reinsurance, UK government technical guidance, accessed 2026. https://www.gov.uk/hmrc-internal-manuals/general-insurance-manual/gim8080
An insurer can expect premium income to exceed claims and nevertheless become insolvent because the timing and size of claim payments are uncertain. Ruin theory asks about the chance of crossing an insolvency boundary before a specified date or eventually. The classic actuarial approach uses the distribution of yearly net cashflows and, when it exists, an exponential adjustment condition to bound risk as starting capital increases. Finite-state random walks provide a related illustration of first-passage probability and absorption (https://stats.libretexts.org/Bookshelves/Probability_Theory/Introductory_Probability_%28Grinstead_and_Snell%29/12%3A_Random_Walks/12.02%3A_Gambler%27s_Ruin). The mission isolates the finite-horizon inequality that can be stated without imposing the measure-theoretic hypotheses of an infinite stopping-time theorem.
An annual aggregate claim X is a nonnegative integer taking values zero through a fixed maximum B, with annual probabilities w(k). The insurer starts at signed integer surplus u, receives nonnegative integer premium c each year and pays an independent claim from the same finite distribution. The next signed surplus is current surplus plus c minus that claim. Strict ruin occurs as soon as surplus becomes negative, including at time zero if the initial reserve is negative. A finite-horizon ruin probability assigns one to an already-ruined state, zero to a solvent state at zero horizon, and a probability-weighted continuation at other states.
The one-period integer insurance surplus update is named actuarial_ruinNextSurplus in the Lean development. The insurer begins a period with an integer surplus, receives a fixed nonnegative integer premium, then pays the period's aggregate integer claim. The next surplus can be negative, so it is represented as an integer rather than a natural number with saturating subtraction.
The total annual claim probability on a bounded integer grid is named actuarial_ruinClaimMass in the Lean development. The finite annual aggregate-claim model has possible integer loss amounts 0 through B. Its total probability is the sum of those coefficients, required to equal one in the genuine probability interpretation of the recursion.
The exponential moment of one period's net insurance loss is named actuarial_ruinAdjustmentMoment in the Lean development. The adjustment coefficient R compares the annual aggregate claim X with the premium c via the exponential moment E[exp(R(X−c))]. When this quantity is no greater than one and R≥0, the exponential capital bound becomes a supermartingale-style one-step estimate.
The lundberg exponential benchmark for an integer initial surplus is named actuarial_ruinExponentialBound in the Lean development. The benchmark at current surplus u is exp(−Ru). For R≥0 this is at least one if u is negative, allowing it to bound an already-ruined state whose ruin indicator equals one; for a nonnegative initial reserve it falls exponentially with additional starting capital.
The first-passage ruin probability over a finite number of annual periods is named actuarial_ruinProbabilityFinite in the Lean development. The probability of ruin by horizon n records whether surplus was ever strictly negative. Already-ruined integer states have probability one at any horizon. Otherwise the next-year claim distribution mixes the ruin probabilities of all possible updated signed surpluses, recursively for n further years. The horizon is finite and annual claims are modelled as conditionally independent copies of w.
The formal targets are ordered from elementary boundary and consistency claims to their combined capstone. The exact Lean identifiers below are the authoritative local targets; none of the listed theorem bodies is already accepted as a machine-checked proof. The mathematical results themselves are established actuarial or probability identities.
The declaration ActuarialValuation.ruinNextSurplus_zero_claim states the following relation. If the insurance portfolio generates no claim payment during a period, only the fixed premium c affects the insurer's capital. The signed next-period surplus is therefore the old surplus plus the earned premium.
The declaration ActuarialValuation.ruinProbabilityFinite_le_one states the following relation. With an annual claim mass function summing to one, every solvent state averages predecessor-horizon ruin probabilities with nonnegative weights of total one. Since the base and already-ruined values lie at most one, induction establishes that the finite-horizon ruin probability never exceeds one.
The declaration ActuarialValuation.ruinFiniteHorizon_fundamental states the following relation. The capstone formalises a bounded annual integer-claim surplus recursion with an absorbing strict-negative ruin condition. Proper nonnegative annual claim probabilities keep finite-horizon ruin probability within the unit interval. A nonnegative exponential adjustment parameter satisfying E[exp(R(X−c))]≤1 then bounds it by exp(−Ru) for every finite horizon and signed starting capital.
A valid exponential upper bound gives a transparent relationship between initial capital and probability of failure over every finite number of years. It can be used to compare capital buffers or to test an insurer's response to a changed premium and annual claims distribution. The bounded recursive setting is particularly relevant when annual severity is itself computed by exact portfolio convolution. Classical first-passage models distinguish eventual absorption from a finite-horizon crossing event (https://stats.libretexts.org/Bookshelves/Probability_Theory/Introductory_Probability_%28Grinstead_and_Snell%29/12%3A_Random_Walks/12.02%3A_Gambler%27s_Ruin). The formal target is the known exponential comparison property, not a new adjustment-root existence result. It yields reusable recursion and exponential-moment definitions for subsequent finite insurance reserve analysis.
A tempting representation of surplus as a natural number is incorrect for insolvency, because saturating subtraction hides the negative state that defines ruin. A second mistake is to present the exponential capital function as an unconditional bound. It can fail when the claim-loss exponential moment exceeds one, even in a deterministic one-year example. The argument also needs the negative-surplus boundary, at which ruin probability is already one. These complications are visible at finite horizons and cannot be repaired merely by assuming that premium income has a positive expected margin.
The Lean source uses signed integers for surplus and natural numbers for annual claim amounts, premium, severity bound and horizon. Annual probabilities and adjustment exponent are real. The event is strictly negative first-passage ruin, distinct from reaching exactly zero in a gambler's ruin model. A nonnegative adjustment exponent and an explicit upper bound of one on its net-claim exponential moment are mandatory. The source gives the finite recursive quantity algebraically, not an independently constructed probability space, an infinite-horizon supremum or a theorem that a positive adjustment root exists. Reusable developments include finite weighted expectation operators, signed reserve transitions and nonnegative probability bounds; meaningful contributions may extend these to random premiums or general annual claim distributions.
The five local definitions form the available mathematical vocabulary: actuarial_ruinNextSurplus, actuarial_ruinClaimMass, actuarial_ruinAdjustmentMoment, actuarial_ruinExponentialBound, actuarial_ruinProbabilityFinite. Their support conditions, nonzero denominators, and variable types are fixed by the Lean declarations rather than inferred from examples. The nontrivial mathematical content must not be replaced by a vacuous premise or by a special case that bypasses the model boundaries. The existing paper mathematics is known, while these particular theorem declarations remain formalisation targets with no accepted proofs. Contributions that strengthen reusable finite identities or expose missing boundary hypotheses are appropriate, provided they preserve the exact authoritative theorem types.
S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
Charles M. Grinstead and J. Laurie Snell, Introduction to Probability, American Mathematical Society, 1997. https://stats.libretexts.org/Bookshelves/Probability_Theory/Introductory_Probability_%28Grinstead_and_Snell%29/12%3A_Random_Walks/12.02%3A_Gambler%27s_Ruin
Insurers model annual claim frequency to price collections of policies and assess how often unusually large numbers of claims may arrive together. A Poisson count model has equal mean and variance, but heterogeneity between policyholders can produce materially more dispersion. The negative-binomial family is an established alternative, including as a marginal count law obtained by mixing the Poisson intensity over a Gamma distribution. The mathematical relationship, with explicit Gamma shape and rate parameters, is set out in the Stanford discussion of mixture models (https://web.stanford.edu/class/bios221/MixtureLecture.html). A reliable formal description must specify which negative-binomial probability parameter is being used, since actuarial and statistical literature adopt incompatible success and failure conventions.
A negative-binomial count variable N records a nonnegative integer number of claims. The integer shape parameter r is strictly positive, and a real count probability parameter p lies between zero and one, with the upper endpoint excluded when calculating moments. In this convention p is associated with powers of the claim count n, while 1 minus p is associated with powers of the shape r. The Gamma-mixed Poisson model starts from a Gamma-distributed intensity with positive rate beta and integer shape r; at one future exposure unit its negative-binomial count parameter equals the reciprocal of beta plus one.
The negative-binomial claim count coefficient is named actuarial_negBinCountMass in the Lean development. Defines a negative-binomial frequency coefficient for n claims and positive integer shape r, with p the count probability parameter and 1−p the Bernoulli success probability. The finite choose expression is mathematically the conventional formula only for shape r≥1.
The expected claim count under nb size and count parameter is named actuarial_negBinCountMean in the Lean development. For 0≤p<1 and positive integer shape, the negative-binomial mean count equals r p divided by one minus p. This p denotes count rather than Bernoulli success probability, so the formula differs from sources that reverse the parametrisation.
The negative-binomial count variance is named actuarial_negBinCountVariance in the Lean development. For valid negative-binomial parameters, the variance exceeds the mean because uncertainty in the Poisson event frequency introduces additional dispersion. The exact variance is r p divided by (1−p) squared.
The unit-exposure gamma-poisson predictive count parameter is named actuarial_negBinGammaProbability in the Lean development. A Gamma mixing distribution with positive rate beta and positive integer shape yields a negative-binomial mixed-Poisson count law at one exposure unit with the count parameter p=1/(beta+1). This is the reciprocal rate-plus-one, not beta/(beta+1), which is the complementary success parameter.
The integer-shape gamma-poisson predictive count coefficient is named actuarial_negBinGammaPredictive in the Lean development. The model uses a shape/rate Gamma prior for a Poisson rate at unit exposure. The predictive count mass is the integer-shape negative-binomial coefficient evaluated at the rate-derived count parameter. The declaration encodes the known mixture result algebraically without asserting an integral identity.
The formal targets are ordered from elementary boundary and consistency claims to their combined capstone. The exact Lean identifiers below are the authoritative local targets; none of the listed theorem bodies is already accepted as a machine-checked proof. The mathematical results themselves are established actuarial or probability identities.
The declaration ActuarialValuation.negBinGammaProbability_pos states the following relation. Prior Gamma rate b positive implies denominator b+1 strictly positive, so its reciprocal is a valid strictly positive negative-binomial count parameter.
The declaration ActuarialValuation.negBinGammaMean_unit_exposure states the following relation. The frequency mean for the negative-binomial predictive law derived from a Gamma shape/rate prior at one future exposure is shape divided by rate. This agrees with the prior Gamma mean Poisson intensity, not shape times rate.
The declaration ActuarialValuation.negBinClaimFrequency_fundamental states the following relation. The capstone combines the exact integer-shape negative-binomial count-mass recursion and the unit-exposure Gamma-Poisson mixture parameterisation. It verifies both predictive moments and coefficient nonnegativity, without claiming an infinite PMF normalisation proof or a Gamma mixture integral in Lean.
The ability to compute neighbouring frequency coefficients from one another supports actuarial claim-table construction without repeatedly evaluating large factorial ratios. The difference between count variance and mean provides a direct overdispersion diagnostic when comparing heterogeneous risks with a Poisson benchmark. Under a Gamma prior, the mixed frequency mean and variance recover the Gamma shape/rate moments, linking pricing assumptions to uncertainty in latent risk intensity. Panjer's work on recursive compound distribution evaluation shows why stable frequency recurrences matter for downstream aggregate insurance claims (https://doi.org/10.1017/S0515036100006796). The results are known mathematics; an exact formalisation would make the parameter conventions and real-valued boundary assumptions machine checkable and provide coefficient lemmas reusable by collective-risk computations.
The main hazard is a parameterisation mismatch. Some publications place p on the Bernoulli success count and others put p on the recorded total of failures or claims; the mean and Gamma mapping change accordingly. The integer-binomial coefficient must also be interpreted with positive shape: allowing r=0 while retaining the expression choose(n+r−1,n) introduces natural subtraction at a degenerate boundary. Moment formulas include one-minus-p in a denominator and therefore cannot be stated as ordinary probability facts at p=1. Finally, the algebraic coefficient sequence alone does not supply a probability-space proof that Gamma integration produces the count law.
The Lean representation uses natural numbers for integer shape and count, and real numbers for the probability parameter, Gamma prior rate and moment expressions. The combinatorial coefficient is Nat.choose, and all arithmetic is within Mathlib. The zero-shape index is excluded from the conventional distribution claim, although some sign statements remain algebraically valid there. This mission does not assert an infinite normalisation sum, an unrestricted non-integer shape model or a vacuous Gamma-mixture identity proved by defining the mixture as the desired result. Reusable contributions include count-ratio recurrences, nonnegative binomial coefficient calculations and parameter conversion lemmas. Future work could connect those components to a genuine Gamma integral or a separately formalised Panjer aggregate recursion.
The five local definitions form the available mathematical vocabulary: actuarial_negBinCountMass, actuarial_negBinCountMean, actuarial_negBinCountVariance, actuarial_negBinGammaProbability, actuarial_negBinGammaPredictive. Their support conditions, nonzero denominators, and variable types are fixed by the Lean declarations rather than inferred from examples. The nontrivial mathematical content must not be replaced by a vacuous premise or by a special case that bypasses the model boundaries. The existing paper mathematics is known, while these particular theorem declarations remain formalisation targets with no accepted proofs. Contributions that strengthen reusable finite identities or expose missing boundary hypotheses are appropriate, provided they preserve the exact authoritative theorem types.
S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
Harry H. Panjer, Recursive evaluation of a family of compound distributions, ASTIN Bulletin, 1981. https://doi.org/10.1017/S0515036100006796
A pair of insurance portfolios can have the same expected aggregate claim while requiring different ceded premiums or capital to withstand severe outcomes. Expected loss alone cannot identify the difference: the distribution of loss across small and large events also matters. The stop-loss order compares expected loss above every retention level and provides a concrete way to rank riskiness for excess-of-loss contracts. Müller studied wider relationships among such risk orders and their stop-loss transforms (https://doi.org/10.1016/0167-6687(96)90002-5). The present object is a local, explicit change in an integer loss distribution that preserves its first moment but shifts probability from a middle amount towards two neighbouring outcomes.
A bounded aggregate-loss distribution has nonnegative coefficients w(s) for integer losses s between zero and a finite maximum B, with total coefficient mass usually equal to one. Its gross expected claim is the weighted sum of loss amounts and its stop-loss premium at integer deductible d is the expected positive excess above d. A proposed new coefficient array moves an amount delta out of one interior integer claim centre c, placing equal halves at the adjacent claim sizes c minus one and c plus one. Strictly positive centre and a top neighbour no higher than B keep the change within the declared support.
The bounded discrete expected excess above an integer attachment is named actuarial_orderStopLossPremium in the Lean development. The actuarial stop-loss transform multiplies each aggregate loss's excess over the attachment point by its real coefficient and sums over the finite covered loss grid. A nonnegative probability mass law gives its net excess-of-loss reinsurance premium.
The bounded aggregate loss expectation is named actuarial_orderAggregateMean in the Lean development. The finite aggregate claims mean uses the claim amount at each integer index as its payment and multiplies it by its probability mass. Comparing mean claims is necessary when interpreting stop-loss order as mean-preserving convex order.
The aggregate probability within a finite loss bound is named actuarial_orderAggregateMass in the Lean development. The sum of all coefficients on the finite aggregate-loss support is the bounded probability mass, whose value is one for a normalised distribution. An explicit mass operator makes the mean-preserving spread's total-mass conservation separately checkable.
The mean-preserving symmetric transfer from one claim amount to adjacent values is named actuarial_orderNeighbourSpread in the Lean development. A fixed amount δ of probability mass is moved away from an interior integer claim level centre: half is allocated one unit below, and half one unit above. Under 1≤centre and centre+1≤B these three loss levels lie within the support and the transfer preserves the aggregate mean.
The finite-grid stop-loss ordering of aggregate risks is named actuarial_orderStopLossDominates in the Lean development. The first aggregate loss distribution is no riskier in stop-loss order than the second when its expected excess payment never exceeds the other's for any integer attachment d. Equal means and unit total masses can be imposed separately to obtain a mean-preserving spread interpretation.
The formal targets are ordered from elementary boundary and consistency claims to their combined capstone. The exact Lean identifiers below are the authoritative local targets; none of the listed theorem bodies is already accepted as a machine-checked proof. The mathematical results themselves are established actuarial or probability identities.
The declaration ActuarialValuation.orderStopLossPremium_zero states the following relation. Since every nonnegative integer loss exceeds or equals attachment zero, the stop-loss payment equals the gross loss in each scenario. Thus the expected excess premium at attachment zero coincides exactly with the original aggregate expected claim.
The declaration ActuarialValuation.orderNeighbourSpread_stoploss states the following relation. The payment function (s−d) positive-part is convex in the claim amount s. Transferring nonnegative mass symmetrically from centre to its adjacent lower and higher losses can only increase its expected value, with a difference equal to δ/2 times the nonnegative discrete second difference at c.
The declaration ActuarialValuation.orderNeighbourSpread_fundamental states the following relation. The capstone shows that a feasible symmetric probability transfer to adjacent losses produces a valid nonnegative bounded coefficient distribution, preserves the aggregate total probability and mean, yet weakly raises every stop-loss expected excess premium. This is an explicit constructive mean-preserving spread and a finite-lattice convex-order result.
A mean-preserving spread separates the effect of greater claim variability from a change in the underlying expected loss. By conserving total mass and gross mean, the comparison can be attributed to the redistribution of outcomes rather than an increase in total claim cost. Its downstream consequence is a weak rise in the expected ceded payout for every positive-part reinsurance retention. This connects aggregate frequency/severity valuation to ordered risks and tail measures, consistent with wider stop-loss ordering results studied in https://doi.org/10.1016/0167-6687(96)90002-5. Formalising the finite construction provides a reusable bounded-grid example of stochastic-order consequences without requiring an axiomatic treatment of all convex functions.
The obvious claim that any symmetric redistribution increases expected excess is false if the transfer is allowed to cross the boundary of the support or remove more probability than the central cell contains. At centre zero the intended lower neighbouring loss is negative and no longer exists in a natural-number grid. If delta exceeds the centre's initial coefficient, the resulting array is not a probability distribution. Equality of expected claim amounts by itself also does not imply stop-loss order. The formal statement must account for the actual positive-part payment at each possible deductible, including deductions outside the claim support.
Lean represents loss indices, attachment points and the spread centre as naturals, and probability coefficients and expected claims as reals. The claim grid is finite, and the full probability-normalisation equation is separate from local mass conservation. The capstone explicitly requires nonnegative starting coefficients and a feasible interior transfer. It does not substitute a trivial comparison between identical distributions, nor claim general continuous convex order or a complete converse representation of risk ordering. Mathlib finite sums and arithmetic over nonnegative parts are enough for the declared scope. Reusable infrastructure includes finite aggregate means, bounded mass totals and stop-loss order on arrays, suitable for later reinsurance layers and capital-risk measures.
The five local definitions form the available mathematical vocabulary: actuarial_orderStopLossPremium, actuarial_orderAggregateMean, actuarial_orderAggregateMass, actuarial_orderNeighbourSpread, actuarial_orderStopLossDominates. Their support conditions, nonzero denominators, and variable types are fixed by the Lean declarations rather than inferred from examples. The nontrivial mathematical content must not be replaced by a vacuous premise or by a special case that bypasses the model boundaries. The existing paper mathematics is known, while these particular theorem declarations remain formalisation targets with no accepted proofs. Contributions that strengthen reusable finite identities or expose missing boundary hypotheses are appropriate, provided they preserve the exact authoritative theorem types.
S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
Alfred Müller, Orderings of risks: A comparative study via stop-loss transforms, Insurance: Mathematics and Economics, 1996. https://doi.org/10.1016/0167-6687(96)90002-5
Insurers routinely estimate next-period frequency from policyholders who have accumulated unequal historical exposure. A raw observed rate can swing markedly when the exposure base is small, while a collective rate may ignore evidence of persistent individual risk differences. The Gamma–Poisson model gives a precisely defined compromise: a posterior expected claim intensity that responds to observed counts and earned exposure. The literature on credibility analysis documents the distinction between process variation and variation across risks, including the role of Bayesian conjugacy (https://openacttexts.github.io/LDAVer2/ChapCredibility.html). The relevant question is how the posterior parameters and credibility premium behave under sequential reporting, zero-data boundaries and different exposure amounts.
The latent claim frequency is measured in expected events per insured exposure unit. A Gamma prior has shape alpha greater than zero and rate beta greater than zero, so beta is the reciprocal of the Gamma scale. Conditional on this frequency, the observed number of claims C is Poisson with mean equal to exposure E times the intensity. Distinct observed blocks contribute counts C and D and exposures E and F. The formal declarations use natural numbers for counts and real numbers for rates, exposures and expected frequencies. The posterior shape/rate update and credibility-weight equations are the objects of the stated algebraic model.
The gamma posterior shape after observing claim count is named actuarial_gammaPoissonPosteriorShape in the Lean development. The Gamma prior uses the shape-and-rate parameterisation and starts with prior shape α. Observing a nonnegative integer aggregate count C increases the posterior shape to α+C. This is an algebraic conjugacy update rather than a complete formalisation of the Gamma probability density.
The gamma posterior rate after exposure volume is named actuarial_gammaPoissonPosteriorRate in the Lean development. The Gamma distribution's second parameter is a rate, not a scale. The posterior rate is prior rate β plus observed insured exposure E; this explicit convention prevents the common reciprocal-scale error in Poisson-Gamma credibility.
The posterior expected claim frequency per exposure unit is named actuarial_gammaPoissonPosteriorMean in the Lean development. For a Poisson count model and shape/rate Gamma prior, the posterior expected frequency per unit exposure is updated shape divided by updated rate. Positive prior rate and nonnegative exposure ensure an ordinary positive denominator.
The exposure-dependent exact bayesian credibility coefficient is named actuarial_gammaPoissonExperienceWeight in the Lean development. The exact credibility weight in the Poisson-Gamma conjugate model is E divided by β+E. When β>0 and E≥0 this lies between zero and one, approaching greater reliance on claim experience as accumulated exposure increases.
The weighted experience and collective frequency is named actuarial_gammaPoissonCredibilityBlend in the Lean development. The credibility premium combines observed aggregate claims per unit exposure C/E and the Gamma prior population frequency α/β, with respective weights E/(β+E) and β/(β+E). The usual representation requires E>0 and β>0; at zero exposure the claim rate C/E is not a valid observed experience statistic.
The formal targets are ordered from elementary boundary and consistency claims to their combined capstone. The exact Lean identifiers below are the authoritative local targets; none of the listed theorem bodies is already accepted as a machine-checked proof. The mathematical results themselves are established actuarial or probability identities.
The declaration ActuarialValuation.gammaPoissonPosteriorShape_zero states the following relation. When no claims are observed, the sufficient statistic added to the shape is zero. The updated Gamma posterior shape therefore equals its prior shape, even before imposing positivity required by the probabilistic model.
The declaration ActuarialValuation.gammaPoissonCredibilityBlend_exact states the following relation. With positive prior rate and positive observed exposure, the observed claim frequency and collective mean are both well-defined. Substituting weight E/(β+E) and simplifying proves the exact Bayesian credibility decomposition of posterior mean (α+C)/(β+E).
The declaration ActuarialValuation.gammaPoissonCredibility_fundamental states the following relation. The capstone combines exact Gamma-Poisson experience credibility at positive exposure with associative sequential count/exposure updates and admissibility of the Bayesian experience weight. It formalises the conjugate-model parameter and premium algebra without claiming a full measure-theoretic Gamma likelihood integral.
Exact agreement between the posterior mean and the collective/individual premium blend allows underwriting calculations to be reconciled across reporting intervals. Exposure aggregation must not alter the end-of-period estimate when the underlying sufficient statistics are unchanged. The additional Gamma predictive parameter variance explains why a future claim count can exhibit dispersion beyond that of a Poisson distribution with deterministic intensity. These are established properties of conjugate credibility models, rather than new claims about the existence of a posterior distribution; the mathematical background is described in https://openacttexts.github.io/LDAVer2/ChapCredibility.html. The formal output would certify the numeric parameter identities and boundary assumptions in Lean, allowing subsequent developments to reuse the same frequency and credibility conventions.
The common failure is to confuse a Gamma rate with a Gamma scale: this reverses the update and the ratio used as the experience credibility weight. Another false shortcut is to take the product of a zero exposure weight and an undefined observed count divided by zero as a meaningful zero experience contribution. Those algebraic terms are distinguishable in Lean's totalised division and in actuarial modelling. The exact mixture identity needs positive observed exposure, whereas the no-data statement requires both zero exposure and zero observed claims. Strict positivity is also essential when the total rate appears in a denominator.
The Lean development uses Mathlib real arithmetic and natural claim counts. The source represents the posterior parameter update directly and does not formalise an underlying Gamma density, conditional-expectation kernel or integration proof of conjugacy. In particular, no vacuous statistical assumption is allowed to stand in for a parameter identity, and the nonzero-exposure requirement is retained where observed frequency occurs. Reusable contributions include real-valued exposure-ratio identities, independent positivity facts, sequential sufficient-statistic updates and sharply stated data boundaries. Further work could construct the probability-space interpretation or the negative-binomial predictive count law without changing the current capstone.
The five local definitions form the available mathematical vocabulary: actuarial_gammaPoissonPosteriorShape, actuarial_gammaPoissonPosteriorRate, actuarial_gammaPoissonPosteriorMean, actuarial_gammaPoissonExperienceWeight, actuarial_gammaPoissonCredibilityBlend. Their support conditions, nonzero denominators, and variable types are fixed by the Lean declarations rather than inferred from examples. The nontrivial mathematical content must not be replaced by a vacuous premise or by a special case that bypasses the model boundaries. The existing paper mathematics is known, while these particular theorem declarations remain formalisation targets with no accepted proofs. Contributions that strengthen reusable finite identities or expose missing boundary hypotheses are appropriate, provided they preserve the exact authoritative theorem types.
S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
OpenActTexts contributors, Loss Data Analytics: Experience Rating Using Credibility Theory, online actuarial textbook, accessed 2026. https://openacttexts.github.io/LDAVer2/ChapCredibility.html
Elias S. W. Shiu and Xiaoyi Xiong (2021), An elementary derivation of Hattendorff's theorem, European Actuarial Journal 11, 319–323, https://doi.org/10.1007/s13385-020-00256-9. In that paper equation (1) defines the fully discrete insurer's complete-life loss; equation (2) gives the Hattendorff variance formula, and equations (3)–(5) connect annual reserve recursion to the net amount at risk by summation by parts.
The present mission proposes an original countable-outcome and L²-convergence formalisation of that discrete formula. It is not asserted that the authors stated this exact Lean theorem, and it does not inherit proofs from the earlier finite-scenario missions.
Let be the realised curtate lifetime, the number of full years remaining until the year of death. Its possible values are not uniformly bounded. Set , where and . Assume the survival tail is positive in every year:
These are unconditional death masses and conditional mortality and survival rates . Some individual may be zero. The outcome space is genuinely countable; a finite Fintype of realised death years would force a bounded support and undermine the claimed infinite-horizon extension.
The annual mortality martingale difference is defined pathwise by
For , ; at death , ; and after death , it is zero. Let the discounted net amount at risk for the payment at year-end be . This matches Shiu–Xiong's year-end death-benefit timing. The truncated centred reserve loss and the pathwise complete-life centred loss are
The complete-life variable is well-defined on each realised finite and whenever . These definitions only model the centred innovation component. A separate cashflow reserve-recursion bridge, as in earlier missions, is needed to identify a given insurer contract loss with ; this mission does not silently assert that for arbitrary premium sequences.
The discrete expectations are weighted countable sums. Show, under summability and positive in-force mass,
Using finite sums and cross-year orthogonality first gives
The capstone introduces the mathematically substantive L² risk condition
This implies that the sequence of truncated centred losses is Cauchy in the probability-weighted L² space; its limit equals the pathwise stabilised . Hence
The capstone explicitly assumes nonnegative weights, unit total mass, positive survival tails, countable weight summability and risk-variance summability. The formal statement must not be weakened to merely a pointwise convergence or an unjustified interchange of infinite sums.
A geometric law with , , and gives
Its finite-year variance is . The repository includes exact-rational tests for 13 horizons. The model allows an individually zero death mass but requires positive tails. Every scenario terminates in some finite year; adding a outcome with positive weight would require a separate transversality condition and is not part of this mission.
The mission supplies four mathematical definitions, eleven supporting milestone theorems and one combined capstone theorem. Prove the indicator identities, the countable weighted first and second moments, finite orthogonality and finite allocation, and finally the L² passage to the unbounded lifetime. The target Lean namespace is `ActuarialValuation` in the pinned Mathlib environment. Finite-year results from earlier actuarial missions are background, not automatic countable-measure proof imports. None of the present open theorem statements is an accepted proof.
A prospective insurance reserve is the conditional expected amount needed to fund the remaining liabilities of an in-force policy. Annual realised claims differ from their conditional expectations, and the variation in total discounted insurer loss can be allocated to these unexpected annual outcomes. Hattendorff's theorem expresses that allocation as a sum of year-specific variance contributions. The fully discrete case contains an important factor: the conditional probability of surviving the policy year.
Shiu and Xiong's article An elementary derivation of Hattendorff's theorem [1] gives a direct discrete derivation. With curtate lifetime , annual death benefits paid at time , premiums paid at time , discount factor and prospective reserve , their formulas include
In particular, the variance identity they derive has a mortality-year survival factor,
This mission establishes the finite-scenario mortality-innovation component of that result. It derives the orthogonality of annual death surprises rather than assuming it. It does not yet identify their weighted sum with the full insurance loss ; that requires the separate time-dependent reserve recursion and summation-by-parts identities in [1, equation (3)]. Those insurance cashflow bridge obligations are explicitly reserved for the next mathematical stage.
Let be a finite scenario space, its weights and a curtate future lifetime, where means death during year , at the end of which the death benefit is payable.
For policy duration , define the in-force probability mass and the death-year mass:
For probabilistic interpretation assume in addition . The exact algebraic statements do not generally require weight normalisation, though they explicitly require nonnegative weights for probability inequalities.
The disjoint identity
gives . If , the conditional one-year death and survival probabilities are
Division by is totalised as a Lean real expression but is not interpreted as conditioning on an impossible event. All substantive annual-innovation results impose positive in-force mass for the years used.
For each outcome and policy year define the mortality innovation
It equals for death in year , equals for an individual surviving that year, and equals zero after death. Under ,
The orthogonality is more than a generic assumption. For , if then the policy is still in force at , so the preceding year must have been survived and . If , the product is also zero. Thus, pointwise,
Taking the weighted expectation and using the centring of gives
These innovations can be uncorrelated despite being highly dependent events generated by the same curtate lifetime. They must not be claimed independent.
By conditioning on the death-year and survival outcomes, the squared mortality surprise has expected value
The final conditional survival factor is characteristic of the fully discrete actuarial Hattendorff identity. It is not an arbitrary variance weight, and it cannot be dropped by borrowing a continuous-time formula.
For a finite horizon , let be any deterministic year-specific net-amount-at-risk coefficient. Define the discounted innovation portfolio
When for each , the annual zero-mean and cross-year orthogonality identities yield
For nonnegative unit-sum weights this is the usual finite-scenario variance. The capstone couples the derived pairwise cross-year zero moments with the resulting finite-horizon variance formula. No reserve balance, actuarial premium equation or conditional L² filtration theorem is silently assumed.
The formal graph contains seven definitions: survival and death masses, conditional death and survival rates, the mortality innovation, its finite discounted portfolio and a finite weighted variance. Supporting theorems establish event partitions, nonnegativity, , behaviour after death, innovation centring, a pointwise earlier/later product identity, orthogonality, the discrete second-moment formula, zero horizon and portfolio moments. The capstone packages zero covariance and the mortality-weighted variance allocation.
The variance theorem is valid for arbitrary deterministic coefficient sequence and any finite number of years with positive survival mass; it does not presume every life dies before that horizon. is covered by the empty sum. For standard actuarial application choose , as in [1]. A future bridge must show that this particular innovation portfolio equals the centred insurer loss under the correct reserve recursion and endpoint conventions.
The root theorem is therefore a genuine probabilistic predecessor, not an assertion that the entire traditional Hattendorff theorem has already been proved. The mission is proposed for formal proof: private remote statement elaboration and finite rational tests, if accepted, do not constitute public Prove2Me proof acceptance.
[1] Shiu, Elias S. W. and Xiong, Xiaoyi (2021), “An elementary derivation of Hattendorff's theorem”, European Actuarial Journal, 11, pp. 319–323, equations (1)–(3). This is the direct source for the fully discrete variance factor, net amount at risk and finite summation-by-parts strategy.
[2] Gerber, Hans U. (1997), Life Insurance Mathematics, third edition, Springer, Chapter 6, §6.7, Allocation of the Overall Loss to Policy Years. The reserve-change and annual-loss decomposition provides broader actuarial context.
[3] Gerber, Hans U., Leung, Bartholomew P. K. and Shiu, Elias S. W. (2003), “Indicator Function and Hattendorff Theorem”, North American Actuarial Journal, 7(1), pp. 38–47. Explains the central role of indicator functions and the relationship to uncorrelated martingale increments.
An insurer may adjust its reinsurance retention or other risk-management decision repeatedly, rather than optimising a single future year's payments. Current action choices affect both the immediate net reward and the state of the business next year, which changes the value of all later decisions. A finite-horizon Markov decision process makes this multi-year optimisation precise.
Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Chapter 4 [1], develops the finite-horizon Bellman equations and existence of optimal deterministic Markov policies for finite decision problems. Mission XV introduces a finite-action Bellman operator and excess-of-loss claim splitting, but is still under moderator review. This mission formalises the full finite-horizon backward recursion and optimal deterministic policy existence, without importing an unreviewed declaration.
The reinsurance motivation comes from Brachetta and Ceci's optimal excess-of-loss study [2]. Their original problem is a continuous-time stochastic-factor and HJB verification problem. The present mission is strictly a finite-state, finite-action, discrete-time precursor. Neither the stochastic-factor diffusion nor the jump-process verification theorem is asserted here.
Let be a finite state type, and let be a finite nonempty set of admissible control actions. A state can encode a simplified surplus, rating, claims regime or any finite risk-class abstraction. At the beginning of a policy year the insurer is in state and selects an action .
Let be the transition weight for next state , and the immediate reward. The usual Markov model requires and for every . The general algebraic definitions accept real matrices, while the economic probabilistic interpretation requires valid row-stochasticity.
If is the continuation value in state , the return from action is
where is a deterministic annual discount factor. The discount is applied to following-year continuation, not to the current reward. For policy interpretation is conventional, but finite-horizon algebra makes sense at other fixed real as well.
The one-year Bellman optimisation is
The maximum is attained because is finite and nonempty. Both this attainment and the inequality are explicit supporting theorem obligations.
Let denote a terminal benefit or terminal value. A deterministic nonstationary Markov policy is a mapping
Here is the action chosen when decisions remain, so the index counts backwards towards the terminal time. This makes the recursion valid for a homogeneous one-step transition model without reversing calendar-time transitions.
For a fixed policy, recursively define
The policy is nonstationary because its choice at the same state may differ according to remaining time . It is Markov because the action depends only on current state and remaining horizon, not on the entire historical path. The mission does not introduce a path-space filtration or general history-dependent randomised policy, so the precise capstone compares deterministic nonstationary Markov policies.
Define by the finite Bellman recursion
Under and , a larger continuation function cannot reduce the value of any action; taking a finite maximum preserves this monotonicity. That simple inequality allows induction on the remaining horizon to show
The second substantive step is existence of an attaining policy. Since is finite and nonempty, at each remaining horizon and each state there is at least one maximising action. Choosing such actions and combining them recursively gives a single nonstationary deterministic Markov policy satisfying
The capstone combines the universal upper bound and existence of an attaining policy. This is genuinely more than a one-step maximum: it is an optimality result over an arbitrary finite number of sequential decisions.
A complete optimality result against all history-dependent randomised policies would need an additional equivalence argument showing no improvement from extra history or randomisation. Such an extension is well-known for suitable finite Markov models but is not silently claimed by this narrower Lean target.
Four proposed definitions encode the one-step action return, the finite Bellman maximum, policy evaluation and recursively optimal horizon value. Eleven supporting theorem targets establish zero-discount behaviour, action domination and attainment, monotonicity of action and Bellman values, zero-horizon and successor recursions, policy domination and existence of an attaining policy. The capstone packages the latter two results.
At there are no decisions and both values are precisely . At , any continuation is irrelevant to the one-step value. Nonnegative weights and discount are explicit hypotheses for monotonicity and policy domination, rather than false claims for signed matrix weights. The existence of an attaining maximiser in each finite action set does not itself require stochastic row-sum assumptions.
To obtain a reinsurance model from this graph, one must specify how each action corresponds to an admissible retention, how the retention changes reinsurance premiums and retained claim distributions, and how those assumptions determine the transition matrix and rewards . That specialised bridge is separate from the finite-horizon mathematical result.
All theorems are proposed Lean proof targets. Preliminary remote elaboration establishes statement well-formedness only if verified by the authoritative compiler. It does not constitute a completed proof or approval of the mission's mathematical design.
[1] Puterman, Martin L. (1994), Markov Decision Processes: Discrete Stochastic Dynamic Programming, Chapter 4, Finite-Horizon Markov Decision Processes, Wiley. This is the direct mathematical reference for finite-horizon Bellman recursions, backward induction and existence of optimal deterministic policies under finite-state/action assumptions.
[2] Brachetta, Matteo and Ceci, Claudia (2019), “Optimal Excess-of-Loss Reinsurance for Stochastic Factor Risk Models”, Risks 7(2), article 48. This motivates insurance retention as a controlled decision but uses a continuous-time stochastic-factor/HJB model not established by this mission.
[3] Schäffeler, Maximilian and Abdulaziz, Mohammad (2022), “Formally Verified Solution Methods for Markov Decision Processes”, computer-assisted formalisation of Bellman equations, value iteration and optimal policy existence in Isabelle/HOL. This is methodology context only; no proof code is imported into Lean from that project.
A tall matrix with independent standard normal entries is, with high probability, a near-isometry: all its singular values lie in up to Gaussian fluctuations. This is Gordon's theorem together with Gaussian concentration (Vershynin 2012, Theorem 5.32 and Corollary 5.35), the non-asymptotic counterpart of the Bai–Yin law and the model result for the whole theory of non-asymptotic random matrices. In randomized numerical linear algebra the same two ingredients give the expected spectral norm of (Halko–Martinsson–Tropp 2011, Proposition 10.1 (10.2)), its second moment (Tropp–Webber 2023, Lemma B.1), and the lower tail of of a Gaussian sketch, which controls the inverse moments that appear in the analysis of sketching algorithms with rank truncation. None of these results is available in Mathlib; this mission proves them.
A standard Gaussian matrix has independent entries; its law is . Its extreme singular values are
the infimum and supremum over the unit sphere of (); is the spectral norm. For a wide matrix , , the usual is . The Frobenius norm is ; a function on matrices is -Lipschitz if . A chi-square variable with degrees of freedom is for independent standard normals . The letter denotes Euler's number.
For every , with probability at least ,
This is the goal because it is the statement users of Gaussian matrices quote: a quantitative near-isometry with explicit sub-Gaussian deviations. It follows from the expectation bounds (Gordon) and concentration, both of which are milestones.
The results. Gordon's theorem is sharp: and are pinned to within of the Bai–Yin limits for every . Gaussian concentration upgrades it to tail bounds with the optimal sub-Gaussian rate, and the Chevet-type bound is the same mechanism for , where it yields the expected spectral error of the randomized SVD. The small-ball bound covers the other regime, , with polynomial decay of the exact order ; together the two tails make every negative moment , , finite and explicitly bounded, which is what the early-truncated analysis needs.
Formalizing them. Mathlib has the standard Gaussian measure on finite-dimensional inner product spaces but neither Gaussian concentration for Lipschitz functions, nor Slepian's or Gordon's comparison inequalities, nor any result on singular values of random matrices. These are foundational pieces of high-dimensional probability whose formalization would be reused far beyond this series.
The upper bound in Gordon's theorem is proved by Slepian's comparison lemma for the Gaussian process on , and the lower bound by Gordon's minimax comparison inequality for ; both require a theory of Gaussian processes indexed by continuous parameter sets, or at least a discretization argument with careful limits. Gaussian concentration (Tsirelson–Ibragimov–Sudakov) is usually proved through the Gaussian logarithmic Sobolev inequality or the Ornstein–Uhlenbeck semigroup, with a smoothing step to pass from smooth to Lipschitz functions. Both are long developments with no Mathlib support. The elementary alternatives do not reach the stated constants: an -net argument bounds by with , and a union bound over rows for the small-ball estimate is exactly how the stated bound is obtained, but it needs the fact that the distance from a Gaussian vector to a fixed -dimensional subspace is a variable, which again rests on rotational invariance.
Matrices are sampled from the product measure on arrays. is sMin, the real infimum over the unit sphere of ; is assumed so the sphere is nonempty, and is not assumed for Gordon's theorem (for one has and the lower bound is trivial, as in the source). is Mathlib's operator norm. Expectation bounds are stated together with integrability of their integrands, so the Lean convention that non-integrable functions integrate to cannot trivialize them. Probabilities are measures in compared with of the real bound; the goal's lower bound uses truncated subtraction and is vacuous for , exactly as in the source. Gaussian concentration is stated with and , which the sources leave implicit (for or the event has probability one). Results that the sketching literature states for wide matrices are stated here for tall matrices via , with .
Welcome contributions: Gaussian concentration for Lipschitz functions on (any proof), Slepian's and Gordon's inequalities, the -Lipschitz property of and , the chi-square Chernoff bounds, and the law of the distance from a Gaussian vector to a subspace.
Shared definitions: the items of this mission import Definitions.Def_GaussianMatrix_basic, a draft of Mission I; submit that proposal first so the import resolves at compile time.
Series: I. Rotation Invariance and Moment Identities · II. Inverse Moments of the Pseudoinverse · III. Extreme Singular Values and Concentration. All three missions share the definition bundle GaussianMatrix_basic, published with Mission I, and the namespace GaussianMatrix.
Randomized algorithms for low-rank approximation — the randomized SVD of Halko, Martinsson and Tropp (HMT 2011), generalized Nyström, randomized subspace iteration, one-pass sketching (Tropp–Webber 2023) — multiply the input matrix by a random test matrix with independent standard normal entries. Every error bound for these methods rests on a small number of facts about such standard Gaussian matrices: they are invariant under rotations, disjoint blocks of a rotated copy are independent, and the second and fourth moments of a linearly transformed Gaussian matrix are given by explicit formulas. These facts are classical, but none of them is available in Mathlib, so a Lean development of randomized numerical linear algebra currently has to carry every one of them as an explicit hypothesis of its main theorems. This mission removes those hypotheses.
For , a standard Gaussian matrix of size is a random matrix whose entries are independent random variables. Its law, written , is the product measure on real arrays.
For a real matrix , is the squared Frobenius norm; is the dimension of its column space. A matrix has orthonormal columns when ; a square such matrix is orthogonal. For , a matrix with independent entries is written with , so that is an unbiased sketch of the identity.
For fixed , and with independent entries,
This is the exact mean-squared error of the sketched product as an estimator of , a direct consequence of Isserlis' pairing formula for Gaussian fourth moments. It is the goal because it is the one fourth-moment computation the series needs and because every other identity in the mission is a step towards it.
The results. Rotational invariance and block independence are the mechanism behind every conditioning argument in randomized linear algebra: writing the right singular vectors of the input as , the sketch splits into independent standard Gaussian blocks and , and one may condition on while treating as fresh. The second-moment identity then turns the deterministic range-finder bound into , and the approximate-multiplication identity gives the one-pass error terms. Almost-sure full rank is what makes a genuine pseudoinverse.
Formalizing them. Mathlib has the one-dimensional Gaussian measure, product measures, independence of coordinate projections, and (recently) the standard Gaussian measure on a finite-dimensional inner product space together with its invariance under linear isometries. None of the matrix-level statements above is in Mathlib. Once proved here they are reusable by every later mission in the series and by any formalization of randomized low-rank approximation, whose expectation-level inputs (e.g. ) follow from these milestones together with the inverse moments of Mission II.
Rotational invariance is not a computation with densities on that Mathlib supports out of the box: the clean route is through characteristic functions or through the basis-independence of the standard Gaussian on an inner product space, transported along the linear isometry of with the Frobenius inner product. Independence of the blocks requires identifying with a product measure and then projecting onto disjoint coordinate sets, with a completion of to an orthogonal matrix when . The moment identities are finite computations, but the fourth-moment identity needs the Gaussian moments , organized through Isserlis' pairing formula over a four-fold sum of indices; the obvious entrywise expansion produces terms that must be collapsed symbolically. Almost-sure full rank is the statement that the zero set of a nonzero polynomial ( of a maximal square submatrix) is Lebesgue-null, which must be established for the product Gaussian measure.
The sample space is the function type with the product -algebra; a sample is viewed as a matrix through the identity map . Expectations are real Bochner integrals: for an identity with a nonzero right-hand side this forces integrability, and the integrands here are polynomials in Gaussian entries. Laws are stated as equalities of pushforward measures; independence is Mathlib's IndepFun. Dimensions may be ; all statements remain true in that case. The hypothesis silently forces (vacuous otherwise), which matches the source.
The definition bundle GaussianMatrix_basic supplies the law , , , the spectral norm (Mathlib's operator norm), the smallest singular value and the pseudoinverse ; it is shared by the whole series. Welcome contributions: the Gaussian integration-by-parts and Isserlis lemmas for finite index sets, the identification of with Mathlib's stdGaussian on the Frobenius inner product space, and the "polynomial zero sets are null" lemma for product measures.
Series: I. Rotation Invariance and Moment Identities · II. Inverse Moments of the Pseudoinverse · III. Extreme Singular Values and Concentration. All three missions share the definition bundle GaussianMatrix_basic, published with Mission I, and the namespace GaussianMatrix.
Many insurance benefits depend on a policyholder's health or membership state rather than simply on being alive or dead. A disability annuity pays while a life occupies a disabled state; a critical illness or death benefit may be triggered by moving from one state to another. A rigorous multiple-state valuation therefore distinguishes payments for occupying a state from payments for a transition between states, and must also specify the timing of the payments.
The discrete-time models in Promislow, Fundamentals of Actuarial Mathematics, third edition, Chapter 19 §§19.2.1–19.2.3 [1], provide these two actuarial payment categories. Dickson, Hardy and Waters, Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 8 [2], develop related multiple-state assumptions, transition probabilities, premium values and policy values. Norris, Markov Chains, §1.1 [3], supplies the finite-state stochastic-matrix foundation.
This mission develops the corresponding finite-horizon present-value formulas. It is the cashflow extension of the finite-state transition algebra in Mission X, but is designed as a self-contained draft while Mission X's definitions remain unpublished. The key mathematical obligations are correctly weighted transition benefits, state occupation annuities, finite-state distribution propagation, homogeneity and a capstone valuation decomposition.
Let be a finite set of insurance states. At the start of policy year , let represent the probability of state , and let be the conditional probability of occupying state at the end of the year, conditional on state at its start.
A state distribution must satisfy
A valid one-year transition kernel has nonnegative entries and rows summing to one:
The next year's marginal state distribution is obtained by propagating the current distribution through that kernel:
The supporting theorems show that nonnegativity and total probability are preserved by this operation. The transition kernels are allowed to change from one year to the next. A separate path-space process need not be constructed to establish these finite-sum valuation identities, but and must obey the propagation relationship to represent one coherent Markov insurance model.
Let be the payment made at the beginning of policy year to a contract then occupying state . For example, it could represent a disability annuity paid only while the person is disabled. The expected amount at that payment time is
The expected present value of the state-occupation cashflows over policy years is
A payment due at time zero is not discounted. A constant amount paid irrespective of state has its own expected value unchanged because the marginal state probabilities add to one. This is consistent with the state-occupation cashflow structure in [1, §19.2.3, equation (19.6)].
Let be the benefit payable at the end of policy year when the contract transitions from state to state over that year. The expected one-year amount is
The contract's expected present value of those transitions is
Unlike a reward depending only on the destination state, a transition-specific benefit may distinguish, for example, from . Keeping the pair explicit is necessary to represent such insurance benefits. This is the payment timing and transition structure considered in [1, §19.2.2, equations (19.2)–(19.4)].
The mission defines the complete finite-horizon value by adding the two types of cashflow:
Because finite sums are linear, scaling both monetary benefit schedules by a constant scales the entire expected present value by :
The capstone combines decomposition of the occupation and transition components with this scaling principle. Related milestones establish the zero-year, zero-benefit and one-year limits. For a one-year contract the exact timing reduces to
The displayed formula is deterministic expected-value algebra for finite state probabilities, rather than a claim about a pathwise cashflow random variable. The later development of a stochastic path-space model, conditional benefits and second moments remains a separate task.
The proposed Lean draft contains five definitions: a finite-state probability distribution, one-step distribution propagation, expected transition-stage reward, expected occupation-stage reward and the combined finite-term PV. Thirteen supporting theorems prove probability propagation, zero and constant payments, scaling, valuation decomposition and the one-year boundary. The final capstone packages the overall value decomposition and benefit scaling.
The formal theorem statements do not require the cashflow amounts to be nonnegative because their linearity is algebraic. Probability interpretation additionally requires legitimate state probabilities and transition kernels. The source explicitly avoids interpreting arbitrary arrays and as the marginals of one Markov chain unless they satisfy the propagation identity.
These declarations are proposed mathematical obligations, not accepted proofs. Individual Lean modules import only the definitions their statements actually use, with all imports before Lean commands. Because the local definitions are not yet published as importable Prove2Me modules, downstream theorem previews must be revisited after their definitions are confirmed and published.
[1] Promislow, S. David (2015), Fundamentals of Actuarial Mathematics, third edition, Wiley, Chapter 19, Multi-state Models, §§19.2.1–19.2.3. Equations (19.2)–(19.4) address transition-based insurance benefits and equation (19.6) addresses occupation-based annuity benefits.
[2] Dickson, David C. M., Hardy, Mary R. and Waters, Howard R. (2009), Actuarial Mathematics for Life Contingent Risks, first edition, Chapter 8, Multiple State Models, especially §§8.3–8.7 on states, transition probabilities, premiums and policy values.
[3] Norris, J. R. (1997), Markov Chains, Cambridge University Press, Chapter 1, §1.1 on stochastic matrices and discrete-time transition probabilities. The matrix-multiplication setting here permits different kernels at successive durations, in line with Promislow's non-stationary treatment.