Prove2Me

Premium allocation, bid and offer prices and fund charges: ulBidOfferCost_zero

Proved
ActuarialValuation.ulBidOfferCost_zero

by WillR · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

actuarial-scienceformal-verificationunit-linked-profit-charges

No bid-offer spread produces no immediate allocation value loss. This original derived actuarial relation uses the parameter restrictions, endpoints and units stated in the separate formal theorem or definition.

Mathematical relation:

Ut=Ut−1+atPtOt−CtBtU_t=U_{t-1}+\frac{a_t P_t}{O_t}-\frac{C_t}{B_t}
Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.Order.Group.MinMax
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Definitions.Def_actuarial_ulBidOfferCost
Formal statement
namespace ActuarialValuation

theorem ulBidOfferCost_zero (allocated price : ℝ) (h : price≠0) : ulBidOfferCost allocated price price=0 := by sorry

end ActuarialValuation
Source
Original derived actuarial mathematics, published source page 16. FCA, Unit-linked pensions and savings price and value practices, https://www.fca.org.uk/publications/multi-firm-reviews/unit-linked-pensions-and-savings-multi-firm-review-consumer-duty-price-and-value-practices; FCA TR16/2 Fair treatment of long-standing customers, https://www.fca.org.uk/your-fca/documents/thematic-reviews/tr16-02. Parent topic: Allocated premium, offer and bid unit prices, cost of allocation spread, fund charges, net amount at risk, policy expenses and discounted expected non-unit profit. The particular Lean formula is a new finite/real-algebraic formalisation and remains an unproved theorem target if labelled theorem. Relevant published actuarial derivation: https://www.fca.org.uk/your-fca/documents/thematic-reviews/tr16-02
Human review

  • Endorsed by Shuze Chen · Oct 11, 2026

    Confirmed by the moderator at approval.

  • Endorsed by WillR · Oct 11, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph