# Reproduction — Day-count & accrual — coupon periods compose exactly (finance)

Machine-checked result `MachLib.Finance.days30E360_additive` in `MachLib.FinanceDayCount` — a proof, not a codegen kernel. Regenerate with `make all`.

> The headline (days30E360_additive) is EXACT: splitting a coupon period at any intermediate date preserves the total day-count, so accrued interest composes exactly (accrual_additive) — no interest is manufactured by moving an accrual boundary, the day-count analogue of amortization's telescoping reconciliation. Plus regularity (equal calendar spacing ⇒ equal day-count ⇒ equal coupons) and a full year = 360. Honest domain point: this uses 30E/360 (Eurobond) precisely BECAUSE it's additive — the US 30/360 'bond basis' is NOT (its end-of-month rule depends on the other endpoint; the sim exhibits a case where US gives 44≠43 while 30E/360 gives 43=43). All pure INTEGER arithmetic — #print axioms is propext + Quot.sound only, not even Classical.choice — and registered in the claim auditor. Honest scope: certifies the day-count convention's algebra, NOT a full calendar/business-day library, and NOT an audit certification.

| stage | artifact | tier |
|---|---|---|
| proof | `MachLib.Finance.days30E360_additive` — ✓ clean (`proof/days30E360_additive.axioms.txt`) | REPLAY (re-derive: TOOLCHAIN — Lean) |
| simulate | `sim/trace.csv`, `sim/daycount.png` — Σ(coupon-period 30E/360 day-counts) − total day-count over the bond (exact integers) = 0 = 0 | LOCAL |
| hardware | — (a money/calendar kernel; the receipt is the proof + a real bond coupon schedule in exact integers, not hardware) | NONE |

**The same claim, two ways.** The Lean theorem `MachLib.Finance.days30E360_additive` proves the 30E/360 day-count is additive — splitting a coupon period at ANY intermediate date preserves the total day-count, so accrued interest composes exactly (no interest created or destroyed by moving an accrual boundary); the simulation shows `Σ(coupon-period 30E/360 day-counts) − total day-count over the bond (exact integers) = 0 = 0` (the 20 semiannual periods each count exactly 180 days and sum to 3600 = the direct issue→maturity count — 30E/360 is additive, so accrued interest composes exactly (total accrued $500,000.00). Honest contrast on 2020-01-15→02-28 split at 01-31: 30E/360 adds (43=43) but US 30/360 does NOT (44≠43) — why the additive convention is the right one); Proved, simulated.