Math Appendix

This appendix summarizes the current public formulas. All protocol arithmetic is integer, bounded, and fail-closed. Live transaction construction must use the current SDK and Lean/Edge API rather than reimplementing these formulas in a client.

Source-local movement

Each source is compared with its own frozen opening state:

source_delta[source] = current_state[source] / opening_state[source] - 1

This avoids averaging incompatible raw price levels.

Bucket and index movement

Inside one bucket:

bucket_delta[bucket] = sum(source_weight[source] * source_delta[source])

Across buckets:

index_delta = sum(bucket_weight[bucket] * bucket_delta[bucket])

Basket weights define the product. The frozen monthly recipe defines source membership and source weights.

Challenge trigger

kill_trigger[source] = max(K_min, min(rho * source_backing[source], K_max))

Example:

source_backing = 10000
rho = 15%
K_min = 500
K_max = 3000
kill_trigger = max(500, min(1500, 3000)) = 1500

Current capped-option payout

Let S be the canonical settlement value. Current V1 contracts use participation 1.0 and one index unit per contract.

For a capped call with strike K and cap U:

g_call(S) = min(S, U) - K, floored at 0

For a capped put with strike K and floor L:

g_put(S) = K - max(S, L), floored at 0

The maximum payout is U - K for the call and K - L for the put. At the current neutral $100 anchor, the call is capped at $112, the put is floored at $88, and each side has a maximum payout of $12 per whole contract.

Aggregate liability and exact reserve

For series i, let q_i_ext be external open interest and g_i(S) its per-contract payout. The sleeve liability at settlement value S is:

L(S) = ceil(sum_i(q_i_ext * g_i(S)) / contract_atomic_scale)

The upward rounding happens once after the complete book is summed. It is not performed once per series.

The exact reserve is:

R = max over canonical candidate settlement points of L(S)

The candidate set contains zero, every payoff breakpoint and its adjacent atomic values, both configured tail boundaries and their adjacent values, and the first value beyond the largest payoff breakpoint when representable. The current bounded implementation supports 32 stored series, 20 live V1 series, and at most 128 candidate points.

If A is accounted sleeve assets, every money-moving transition must preserve:

A >= R
headroom = A - R

Primary premiums are assets; they do not reduce option liabilities or oracle-security exposure.

Primary-auction premium and fee

For whole-contract quantity n, clearing price P, and primary fee rate f_bps:

premium = n * P
fee = ceil(premium * f_bps / 10000)

Accepted premium moves from funded buyer escrow into the sleeve and becomes locked premium. The fee moves separately to the canonical protocol-fee vault. Prices are auction-discovered subject to the sealed policy floor; they are not a fixed protocol return.

Proportional close-to-redeem

Let p be the Flat amount locked for a close and F the snapshot Flat supply. For each series, the required retirement basket is:

retire_i = ceil(p * q_i_ext / F)

After subtracting this basket from external OI, the program recomputes the exact post-close reserve. The final withdrawal is the minimum of:

p
reserve_before - reserve_after
the largest withdrawal safe at every canonical settlement state

The statewise limit is evaluated before liability rounding across the complete book. It prevents the close from shifting value away from remaining Flat holders or making any settlement state insolvent.

Oracle-security exposure

The current conservative mode is the sum of external maximum payouts:

E_gross = sum_i ceil(q_i_ext * max_payout_i / contract_atomic_scale)

An audited exact-envelope mode can instead use:

E_exact = R

Both modes use external OI only. Premium funding is never subtracted from security exposure.

Settlement ledgers

At the sleeve’s one canonical settlement value S_T:

long_reserve = L(S_T)
Flat_residual = A - long_reserve

Long claims consume their allocated long-reserve ledgers. Flat holders burn Flat to claim pro rata from the frozen residual ledger. Because the two ledgers are separated at settlement, either class may claim first without consuming the other class’s assets.

Display-only ratios

A client may display ratios such as:

premium / maximum_payout
(maximum_payout - premium) / premium

These are observations at a particular market-discovered premium, not protocol parameters, guaranteed yields, or return promises.

Robust aggregation methods

If a future product version enables a weighted median, trimmed mean, or another aggregation method, the exact method must be committed before launch. It cannot be silently changed for an active contract.