# Reproduction — Amortization schedule — reconciles to the penny (finance)

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

> Reconciliation is proven EXACT and rounding-mode-independent (Σ principal = loan, balance closes to exactly $0.00; the final payment absorbs the accumulated rounding). Banker's rounding is separately proven correct to ½¢ per period (roundHalfEven_half_ulp). And the accumulated rounding is now bounded END-TO-END: MachLib.Real.amortization_drift_within_envelope proves the rounded balance never leaves the certified envelope cap_N = c·(gᴺ−1)/(g−1) (c=½¢) around exact arithmetic — the expansion dual of the closed-loop safety envelope. Here the worst-case cap is $5.02 while the measured drift is only ~$0.05 (real roundings mostly cancel — the margin is the point, as in the safety card). Everything is INTEGER CENTS — the reconciliation proof never touches a float; all four finance theorems are sorryAx-free and registered in the claim auditor. Honest scope: this certifies the schedule's reconciliation + rounding + drift envelope, NOT a general decimal library, and it is NOT an audit certification.

| stage | artifact | tier |
|---|---|---|
| proof | `MachLib.Finance.amortization_reconciles` — ✓ clean (`proof/amortization_reconciles.axioms.txt`) | REPLAY (re-derive: TOOLCHAIN — Lean) |
| simulate | `sim/trace.csv`, `sim/amortization.png` — final balance & (Σprincipal − P), in cents (exact integer arithmetic) = 0 = 0 | LOCAL |
| hardware | — (a money kernel; the receipt is the proof + the reconciling schedule computed in exact integer cents, not hardware) | NONE |

**The same claim, two ways.** The Lean theorem `MachLib.Finance.amortization_reconciles` proves a fixed-rate amortization schedule's principal payments sum to EXACTLY the loan amount and the balance closes to exactly $0.00 — in integer cents, for ANY per-period interest rounding; the simulation shows `final balance & (Σprincipal − P), in cents (exact integer arithmetic) = 0 = 0` (schedule reconciles to the penny (final balance $0.00, Σprincipal = $250,000.00, exact integer cents, never float) — AND the rounded balance provably never leaves the certified envelope around exact arithmetic: measured max drift $0.05 ≤ certified cap $5.02 = c·(gᴺ−1)/(g−1)); Proved, simulated.