Formalization Status

This project distinguishes two claims:

Backend verification coverage: active Lean code checks successfully.
Faithful theorem formalization: the checked statement closely matches the course theorem AND the proof is a real derivation, not a structural projection from an axiomatized conclusion.

The first claim is useful engineering evidence. The second is the academic claim. Do not collapse them.

Status Vocabulary

full: a faithful formal derivation of the textbook theorem from its hypotheses. The hypotheses must be encoded honestly (not the conclusion in disguise) and the proof must do real work — ring/simp/rfl on a structure-projection target does NOT qualify.
library_wrapper: the active code directly invokes a named Lean library theorem whose statement matches the benchmark theorem. The library does the real work.
reduced_core: the active code is honest but narrower than the textbook theorem. This includes:
- Algebraic / analytic / distributional core checks (e.g., a constant-θ MGF identity behind Wald's exponential).
- Lean specifications where the textbook conclusion is encoded as a structure field and the proof reads it off via projection. The structure pins down the textbook STATEMENT but does not derive the conclusion.
placeholder: active prover code verifies but does not yet encode a meaningful formal statement of the textbook theorem.

For delivery claims, count only:

full + library_wrapper

Report reduced_core and placeholder separately. Spec-with-axiomatized-conclusion is reduced_core, not full.

Current Audit

Live status (2026-08-17): corpus 367, 336 full + 18 wrappers = 354/367 delivery-ready, 13 reduced cores, 0 placeholders. Ledger 367 fresh / 0 stale / 0 missing; lake build MathFin and lake lint green, pytest 50/50, AxiomAuditGen at 327 guards (231 curated). The contracts tower below is the new round; the Itô chain rule and its coherence pass are the two blocks after it.

2026-08-17 — the contracts tower: a reified payoff language, closed to Black–Scholes (358 → 367). Five new modules under MathFin/Contracts/, nine entries mf-contract-*. Core.lean reifies a payoff as data — Payoff ι / Contract ι inductives over a typed underlying index ι (ι = Unit for the single-asset instances below), not the inline lambda every other payoff in the library is written as. Adapted.lean proves the reification pays for itself, against a future rung: Payoff.measurable_eval_of_obsTimes_le is the adaptedness hypothesis a Payoff will need to be a legitimate stochastic-integral integrand — 𝓕 u-measurability follows from every observation time in obsTimes (a syntactic, sufficient-not-necessary over-approximation) being ≤ u. No theorem in this round consumes it yet — Pricing.lean integrates against a fixed measure, never a filtration, so it has nothing to discharge this hypothesis against. Pricing.lean integrates pathPV against a measure into Contract.value, proves it linear (value_scale unconditional, value_both needing both integrability hypotheses — integral_add is false without them), and proves value_deliverAsset / value_process_martingale from Martingale.condExp_ae_eq and martingale_condExp alone — deliberately no IsEMM hypothesis anywhere in the file, since neither theorem touches the mutual-absolute-continuity content (ac/ac') that turns a martingale measure into an equivalent one. BlackScholes.lean and CappedCall.lean close the loop: value_pay_eq reduces Contract.value on any single-cashflow contract to exactly the payoff integral, so value_europeanCall/value_europeanPut/value_digitalCall reach bs_call_formula / bs_put_formula / bs_cash_or_nothing_formula by one rw each, and value_cappedCall reaches the bull-spread difference by composing value_europeanCall twice through Contract.value_both/value_scale — no third integral. cappedCall_payoff_eq is a separate theorem (mf-contract-capped-call) transporting the existing pointwise identity cappedCall_eq_bull_spread onto the composed contract's pathPV; it, not the definition's name, is what earns cappedCall its name, and the corpus keeps the payoff and value claims as two entries (mf-contract-capped-call / mf-contract-capped-call-value) rather than one that would silently attach the pricing result to whichever entry a reader opens first.

The honest ceiling, stated once for the whole tower. Payoff is a finite inductive walked by List-valued obsTimes, so every instance here is a payoff kernel over a finite observation grid — no continuously-monitored barrier is expressible. Rung (c) (the BlackScholes.lean/CappedCall.lean reductions) is single-asset, ι = Unit, under the BSCallHyp hypothesis bundle each closed form already needed; nothing here prices under a model that is not separately assumed. The martingale rung (value_deliverAsset, value_process_martingale) is the value process, not the hedge: it does not identify Contract.value with the initial wealth of a replicating strategy (that primitive, MarketCompletenessInPrice.exists_replicating_strategy_in_price, landed on main the day before this round and is the natural next rung, deferred). And none of it is a term-sheet formalisation — no calendar, business-day convention, disruption, corporate action or issuer credit exists at any instantiation, and no entry's description or formalization_scope claims one. Consulted as a source, not a template: Bilokon, The Contract Is Not the Model (working paper, 2026); see docs/sources.md for what was taken and what was not. All nine entries axioms-clean, full. Net: corpus 358 → 367, 327 full → 336 full + 18 = 354/367 delivery-ready, 13 reduced, 0 placeholders.

2026-08-17 — coherence pass over the chain-rule tower (corpus unchanged at 358). No new entries; the round is about what the previous one asserted rather than proved.

The uniqueness clause now says what it should. The band identity is summed over a whole simple process (itoIntegralAgainst_simpleProcess), so itoIntegralAgainst_unique_of_riemannStieltjes takes agreement with the written-out sums ∑ₚ V(p)·(M_{p.2} − M_{p.1}) — a hypothesis naming no stochastic integral — rather than agreement with the object being characterised. Closes #195.

A theorem that may have been vacuous is now known not to be. Martingale requires adaptedness pointwise; pricePath, built from Lp classes, supplies only its a.e. version, so PricingMeasureL2Density's martingale hypothesis had no exhibited witness. The statements are now carried on an abstract adapted S agreeing a.e. with the price — the form ContinuousMarket.IsEMM already used, for the same reason — and exists_density_price_martingale supplies the witness via pricePathCondExp, the price rebuilt from μ[· | 𝓕_t]. This is the price-side counterpart of pricesGainsAtZero_self. Nothing in the gate stack could see this: the theorem was true, axiom-clean and green.

A duplicated proof removed and a definition deduplicated. ItoIntegralL2.uncurry_ae_eq_sum_rectTerm_of_ae_fst_ne_zero states the band decomposition for any measure charging the time origin nothing — generalised over the MeasurableSpace too, which is the part that lets a trimmed measure reuse it. elemIntegrand became the primitive and rectTerm its rfl-equal instance. Closes #197.

A hypothesis deleted and one weakened. hDmeas : Measurable ⇑D was derivable (Lp.stronglyMeasurable) and was carried through five theorems and out into the corpus; hD is now a.e. rather than pointwise. lake lint then found bracketMeasure_mulLI's [IsProbabilityMeasure μ] unused.

d⟨ψ●M⟩ = ψ² d⟨M⟩ (bracketMeasure_mulLI): the construction is closed under itself.

Prose corrected. bracketMeasure is defined as φ²·trim_T; the repo constructs no quadratic variation, so the identification with d⟨M⟩ is motivation, and the docstrings and leaps.md now say so. Earning the name is #200; #199 and #201 carry the other deferrals.

2026-08-16 — the chain rule, the integral against a price, and the pricing measure (353 → 358). For a predictable L² driver φ and M = φ●B, the integrands square-integrable against M are the bracket-weighted L²(φ²·trim_T), and ItoIntegralAgainstMartingale.itoIntegralAgainstCLM is itoIntegralCLM_T precomposed with multiplication by φ. Both factors are isometries, so ‖∫ψ dM‖ = ‖ψ‖_{L²(⟨M⟩)} — the Itô isometry against M, and the reason the weighted space is the right domain. Five entries: sc-ito-chain-rule (∫ψ dM = ∫ψφ dB), sc-ito-integral-band (∫ Z·1_{(a,b]} dM = Z·(M_b − M_a), the Riemann–Stieltjes agreement that identifies the construction), sc-simple-dense-bracket (simple processes dense in the weighted L²), gir-replication-in-price, gir-pricing-measure-density.

What changed for the pricing measure. gir-pricing-measure-unique (2026-08-07) assumed PricesGainsAtZero. gir-pricing-measure-density derives it: for S = S₀ + (σ●B) with σ ≠ 0 a.e., a probability measure Q = D·μ with D ∈ L²(μ) under which S is a martingale prices the traded gains at zero, hence agrees with μ on all of 𝓕ᴮ_T. The functional ψ ↦ 𝔼_Q[∫ψ dS] is an inner product against the density composed with an isometry, so continuity is innerSL's; it vanishes on a band because that integral is a bounded predictable weight against a Q-martingale increment, then on simple processes by linearity and the Lp band decomposition, then everywhere by density.

Scope, stated plainly, and unchanged where it was already honest. Square-integrability of the density is not removable by this argument — it is exactly what buys continuity. The price is driftless by construction; a drift term is additive and is what the HJM bond dynamics need. σ ≠ 0 a.e. is required (only that — no uniform lower bound; the weighted norm rescales). Only complete ⟹ unique is delivered, the Jacod–Yor converse being untouched, and the agreement Q = μ is on 𝓕ᴮ_T, saying nothing off that σ-algebra. The single-band identity does not come with a stated summed version over a general simple process: what exists is the Lp decomposition simpleAssemblyOfMeasure_eq_sum_bands it would follow from, and itoIntegralAgainst_unique correspondingly takes agreement on simple processes rather than on written-out sums. Degenne's axiomatic IsStochasticIntegral characterisation is the right frame for that uniqueness clause but exists only on v4.33.0-rc1, so instantiating it waits for a stable pin.

Superseded status (2026-08-07): corpus 353, 322 full + 18 wrappers = 340/353 delivery-ready, 13 reduced cores, 0 placeholders. Ledger 353 fresh / 0 stale / 0 missing; lake build and lake lint green with no #guard_msgs failure. The round covered martingale representation + market completeness, then the localized Itô formula naming its integrand, then the description-semantics fix below; the last two entries are the downside-performance-metrics work of #173 and the von Neumann–Morgenstern lotteries of #178. itoIntegralCLM_T was already a LinearIsometry from the predictable L²(dt⊗dμ) integrands into L²(μ). MathFin/Foundations/MartingaleRepresentation.lean identifies its image exactly: itoIntegralCLM_T_surjective_onto_centered says the Itô integrals together with the constants exhaust lpMeas ℝ ℝ 𝓕ᴮ_T 2 μ, and itoIsometryEquiv bundles the isometry as an equivalence onto the centered part. The route is orthogonal decomposition against the (closed, because isometric) range, plus totality of the step-integrand Doléans exponentials (WienerExponentialTotality.eq_zero_of_orthogonal_stepDoleans, DoleansStepRepresentation.stepDoleans_sub_one_mem_range), settled on the dyadic cylinder σ-algebras of BrownianCylinderGeneration, whose supremum is the natural filtration (iSup_cylinderFiltration_eq_natFiltration). No Malliavin calculus and no adapted-integrand Itô formula. Centering, 𝔼[∫₀ᵀ φ dB] = 0, is proved a floor down as ItoIntegralProcessGeneral.integral_itoIntegralCLM_T, not assumed. gir-thm-9.3.4 flips reduced_core → full (14 → 13 reduced cores): it had been a Prop structure whose conclusion was a bundled field read off by projection, and it now re-exports martingale_representation, the process form the entry states. Three new entries. gir-mrt-range-surjective is the submodule form above. gir-market-completeness (MathFin/Foundations/MarketCompleteness.lean, exists_replicating_strategy) is the finance reading: every L² 𝓕ᴮ_T-claim is the terminal wealth 𝔼_μ[H] + ∫₀ᵀ φ dB of a strategy, with a unique hedge. gir-pricing-measure-unique (measure_eq_of_pricesGainsAtZero) is uniqueness of the pricing measure on the Brownian filtration, for measures that price the traded gains at zero.

Scope of the uniqueness result, stated plainly. gir-pricing-measure-unique is not the unconditional second FTAP, and it does not follow from IsEMM alone. The textbook argument needs the replicating wealth to be a stochastic integral against the price S, hence a martingale under every EMM; the wealth process martingale representation builds is an integral against B, and S and B share only a filtration. That fair-game step is therefore a named hypothesis, PricesGainsAtZero Q: every terminal Itô integral is Q-integrable with zero Q-mean. What is hypothesised is step (i) of the textbook proof; what is proved is step (ii). The hypothesis is guarded by two proved facts rather than asserted: pricesGainsAtZero_self (μ satisfies it, so nothing here is vacuous) and pricesGainsAtZero_of_gains_martingale (it follows from the textbook gains-martingale condition). The corollary emm_unique_of_complete consumes only the isProb and ac fields of IsEMM; its martingale field rides along unused, kept so the statement stays in the vocabulary a reader looks it up under. Only complete ⟹ unique is delivered — the converse needs the Jacod–Yor extreme-point characterisation and is out of scope. The companion superReplication_eq_emm_price is the continuous-time superreplication duality, and its "EMM price" is 𝔼_μ[H]. It does not close #39: Foundations/SuperhedgingDuality is a finite-state one-period matrix model whose Farkas gate is untouched. The two equalities hold for structurally different reasons, separation there and martingale representation here, and neither implies the other. The hedging strategy class is the Itô-integrable predictable integrands, wider than ContinuousMarket.SimpleStrategy; the widening is forced, since a general L² claim is not the terminal value of any piecewise-constant holding. ContinuousMarket itself is untouched apart from a scope paragraph. All four entries axioms-clean.

The localized Itô formula now names its integrand (#183, closed 2026-08-07; no corpus entries added, five strengthened). The chain ito_formula_td_L2_bddDeriv → cutoff_bddDeriv → ito_formula_td_localized → ito_formula_itoProcess → ito_formula_gbm/ito_formula_expBrownian → discountedGBM_eq_itoIntegral was a run of bare existentials, so no consumer could identify the diffusion coefficient — the library could not say "the delta is σŜ". Every link now carries gfx =ᵐ [the integrand], ending at gfx =ᵐ [σ·Ŝ(·)] for the discounted GBM, and sc-thm-7.1.2, sc-ito-formula-localized, sc-ito-formula-gbm, sc-discounted-gbm-ito and sc-ito-formula-ito-process state it. This closed a fidelity gap, not just a convenience one: all five entries' description and docstring already wrote the integral as ∫₀ᵀ f_x(s,B_s) dB_s / ∫₀ᵀ σŜ(s) dB_s while the Lean said only ∃ gfx — the prose was ahead of the statement. The identification argument is a general Lp fact (ae_eq_of_tendsto_Lp_of_tendsto: an L² limit agrees a.e. with a pointwise limit of a.e. representatives, via subsequence a.e. convergence) applied to the observation that each cutoff's chain-rule integrand is eventually constant at f_x(·, B) at every point. L² membership of f_x(·, B_·) comes out of the identification rather than being a prerequisite. The forgetful wrapper ito_formula_td_L2_bddDeriv, whose only job was to drop the conjunct ito_formula_td_L2_bddDeriv_explicit already carried — the mechanism that created the gap — is merged away: the two are one theorem under the shorter name.

The audit that followed (2026-08-07, corpus unchanged). Two overstatements in one day stopped being a one-off, so the class was swept repo-wide. sc-thm-7.1.1 had the identical defect one tower over — description writing ∫₀ᵗ f'(B_s) dB_s over an ∃ gf' — now fixed through itoIntegralCLM_T_of_bdd_cont → ito_formula_L2_bddDeriv → _mk. Four descriptions corrected where they claimed the textbook theorem and the entry delivers less (cm-thm-4.3.10 no L^p convergence, sc-thm-8.2.5 uniqueness not existence, sc-thm-7.4.5 constant σ, sc-thm-9.2.1 the Feynman–Kac identification not PDE uniqueness). The README's landmark row for ito_formula_unrestricted was rendering a local-martingale theorem as an integral identity. And ae_fst_mem_Ioc_trimMeasure_T existed six times across five files; five retired. The mechanical slice is now gated (test_prose_does_not_outrun_statement, negative-controlled against the three conjuncts it exists to protect); the judgment slice is a standing first pass in the values-review protocol and in CLAUDE.md.

description now has one job (2026-08-07, closing that open item). All 36 textbook-framed descriptions were read against their statements and 15 — 42% — claimed more than the Lean proved. Beyond the five already corrected: a sign error (mart-prop-2.5.5 wrote (X_n−a)⁻ where the theorem proves the submartingale (X_N−a)⁺); a stale description contradicting its own status (gir-thm-9.1.8 said "Kept reduced_core" on a full entry); a multivariate claim delivered only in 1-D (dist-thm-B.1.2-affine); [B,B]_t = t where the theorem proves the L¹-mean E[Σ(ΔB)²] → t (sc-thm-6.1.1); plus local-vs-global Hölder, one of two tower equalities, unclaimed continuity of a stopped process, and two Poisson entries stating increment laws for a pair where the prose said "process" and "family".

The rule is now: description states the theorem as this entry proves it; where an entry delivers less than the source theorem it is named after, the description says so. The structural cause was an asymmetry — formalization_scope, the honest per-entry disclosure, exists on every entry and was not exported, while description was. The claim shipped and the disclosure stayed home. tools/verify/hf_dataset.py now publishes both.

Record correction (2026-08-04, drafter attribution — no theorem changed): corpus 348, 316 full + 18 wrappers = 334/348 delivery-ready, 14 reduced cores, 0 placeholders — all unchanged; this touched metadata.provenance only, and the ledger stayed 348 fresh because the input-hash covers snippet + imports + pins, not metadata. mf-performance-gain_to_pain and mf-performance-upside_capture recorded statement_source: magistral-autoform. They landed 2026-07-31; Magistral left the drafter on 2026-07-27 (foundry 17ac296), so they cannot have been drafted by it. The name was baked in at ENQUEUE rather than written by the stage that ran — the defect assemble.py::sanitize_provenance exists to stop, added after these had already merged. Both are scrubbed to the drafter-agnostic autoform via that same function, so their formalization_scope prose now reads "autoformalized statement" rather than "magistral-drafted statement". mf-fixedincome-swap (#66) and mf-insurance-premium-principles (#85) landed 2026-07-18, genuinely in the Magistral era, and keep their attribution — the correction is not a rename. formalization.yaml had a second fault of the same family: it derived the drafter from provenance correctly and then attached it to the TOTAL, crediting one drafter with all four entries. It now tallies per drafter ("Magistral (2) and an unnamed drafter (2)"), with test_the_disclosure_does_not_generalize_one_drafter_to_every_entry asserting the property. Full rationale in values-review.md.

Prior (2026-07-31, speed greeks + caplet/floorlet parity — closes #8, #27): corpus 348, 316 full + 18 wrappers = 334/348 delivery-ready, 14 reduced cores, 0 placeholders. Three entries finishing two contributions that had been open since June (#36, #38, mertunsall) and had gone stale against the pin bump. mf-bs-speed (BlackScholes/HigherGreeks): speed ∂³V/∂S³ = ∂Γ/∂S = -ϕ(d₁)(d₁ + σ√τ)/(S²σ²τ). Placed beside vanna/volga/charm rather than in the PDE file — gamma is the quotient ϕ(d₁)/(S σ √τ) (hasDerivAt_bsV_SS), so speed is one quotient rule away, with ϕ'(d₁) = -d₁ϕ(d₁) supplying the numerator derivative. The contribution also corrected the formula in issue #8, which was algebraically wrong. mf-black76-speed (Futures/Black76Greeks): the discount factor is F-independent, so the Black-76 speed is a bare-term const_mul of the r = 0 BS speed, with e^{-rT} live in both the function and the value — matching the sibling greeks, so the r binder is load-bearing. mf-caplet-floorlet-parity (Futures/Black76): V^caplet - V^floorlet = α·(F - K), derived by applying swaption_payer_receiver_parity rather than re-running the same Phi-symmetry argument — blackCaplet_eq_blackPayerSwaption records that a caplet is the payer swaption's formula with the accrual factor where the annuity sits. The caplet and floorlet price definitions carry no benchmark entry of their own: price-equals-definition closes by rfl, so they are exercised through the parity identity and the ledger instead, and the definitional-rfl allowlist stays empty. Axioms-clean.

Prior (2026-07-31, forward-rate agreement — closes #67): corpus 345, 313 full + 18 wrappers = 331/345 delivery-ready, 14 reduced cores, 0 placeholders. mf-fixedincome-fra (FixedIncome/FRA, closes #67; the first outside contribution to the corpus): the simple forward rate F = (P(0,T₁)/P(0,T₂) - 1)/δ, FRA value V = δ·P(0,T₂)·(F-K), its expanded discount-factor identity, and the fair-rate equivalence V = 0 ↔ K = F. The generic discount-factor algebra is stated once and instantiated on the existing zcb curve; P(0,T₂) ≠ 0 is derived from zcb_pos rather than assumed, leaving δ ≠ 0 as the only hypothesis — the natural-generality discipline applied without prompting. The proof structurally consumes MathFin.zcb; it does not encode the conclusion in a let binding or close a benchmark with rfl.

Prior (2026-07-31, gain-to-pain + upside capture — closes #161, #162): corpus 344, 312 full + 18 wrappers = 330/344 delivery-ready, 14 reduced cores, 0 placeholders. mf-performance-gain_to_pain and mf-performance-upside_capture (Performance/RatiosExtended): the two realised-path ratios join the four moment ratios already in that module. gainToPain is written on Mathlib's positive/negative parts (r⁺, r⁻) rather than open-coded max _ 0, which buys posPart_sub_negPart and hence one_le_gainToPain_iff — the ratio clears 1 exactly when the period was profitable, the statement that makes the definition worth having. upCapture_smul is degree-one homogeneity in the portfolio leg.

Both landed as one refined change consolidating four duplicate autoform PRs (#163/#165 for #161, #164/#167 for #162 — the pipeline drafted each target twice). Each draft carried a spurious division guard (0 < ∑ r⁻, ∑ b ≠ 0) that neither issue asked for and neither proof needs: in Lean x / 0 = 0, so nonnegativity and homogeneity both hold unconditionally. The guards are dropped, so the merged statements are strictly stronger than the drafted ones. Each draft also created a new one-lemma module instead of the RatiosExtended module both issues named; consolidated. Axioms-clean.

Prior (2026-07-18, in-out barrier parity — closes #53): corpus 342, 310 full + 18 wrappers = 328/342 delivery-ready, 14 reduced cores, 0 placeholders. mf-barrier-inout-parity (BlackScholes/BarrierParity, closes #53): knock-in / knock-out in-out parity V_in + V_out = V_vanilla — the barrier-hit event A and its complement partition every path, so the discounted expected payoffs add to the vanilla price (pure linearity of expectation; no barrier density, in the register of chooser_integral_decomp). The proof lifts the pathwise payoff split barrier_payoff_partition (𝟙_A·f + 𝟙_{Aᶜ}·f = f, Set.indicator_self_add_compl) through integral_indicator + integral_add_compl. New def discountedValue D Q g = D·E_Q[g] — the present-value functional the pricing files had only ever written inline, now named so the three barrier values (knockInValue / knockOutValue / vanillaValue) are thin specialisations and parity reads as an identity about values. Axioms-clean. Provenance: the target the autoform pipeline repeatedly failed to draft (depth-gate, then a hallucinated MathFin.zcb); authored by hand as the bottleneck-locating control.

Prior (2026-07-18, second refined autoform PR — loaded premium principles): corpus 341, 309 full + 18 wrappers = 327/341 delivery-ready, 14 reduced cores, 0 placeholders. mf-insurance-premium-principles (Actuarial/ActuarialInsurance, closes #85; the second autoform-pipeline PR — the generalization run's output, Leanstral-drafted and -proved, human-refined at review): the three classical loaded premium principles — expected-value (1+θ)·μ, variance μ + α·σ², standard-deviation μ + β·σ — each with its own named nonnegative-loading bound (expectedValuePremium_ge_mean via le_mul_of_one_le_left, variancePremium_ge_mean / stdDevPremium_ge_mean via one-term mul_nonneg certificates), and the bundle premium_ge_mean assembled from them. The loadings sit on top of the net premium of Actuarial/Insurance.lean (prose seam; the net-premium algebra there is Mathlib's eq_div_iff consumed directly, same certificate family as the swap par identity). Refinery diff vs the draft: signature-bound def arguments + docstrings (the docBlame red), the never-used coupling hypothesis hσ_eq : σ = √σ² dropped, the unused Insurance import dropped, per-principle lemmas extracted so the bundle is a ⟨…, …, …⟩ of certificates rather than three nlinarith calls.

Prior (2026-07-18, first refined autoform PR — the vanilla swap par identity): corpus 340, 308 full + 18 wrappers = 326/340 delivery-ready, 14 reduced cores, 0 placeholders. mf-fixedincome-swap (FixedIncome/InterestRateSwap, closes #66; the first autoform-pipeline PR to land — Leanstral-drafted and -proved, human-refined at review): the par identity payerSwapValue P₀ Pₙ K A = 0 ↔ K = parSwapRate P₀ Pₙ A, proved abstractly for any nonzero annuity (payerSwapValue_eq_zero_iff, a two-rewrite sub_eq_zero/eq_div_iff certificate) and instantiated on the zcb curve (payerSwapValue_zcb_eq_zero_iff) where positivity is discharged by zcb_pos + annuity_pos — assumed nowhere. New defs annuity (A = δ·∑ P(0,Tᵢ) — the numéraire slot blackPayerSwaption consumes), payerSwapValue, parSwapRate. The refinery diff vs the drafted statement: derivable positivity hypothesis dropped, member-witness binders replaced by s.Nonempty, flat-curve specialization demoted from theorem to corollary, snake_case def names and missing docstrings fixed (the classes the pipeline now gates itself).

Prior (2026-07-18, jump calculus — the Itô–Lévy integral CLM): corpus 339, 307 full + 18 wrappers = 325/339 delivery-ready, 14 reduced cores, 0 placeholders. The jump/Lévy axis now carries the compensated-Poisson (Itô–Lévy) stochastic integral all the way to a continuous linear operator and its L² isometry — cgarryZA/LevyStochCalc's (Apache-2.0, cited) axiom #6 in full generality (sc-levy-integral-clm-isometry, Foundations/PoissonCompensatedIntegralOperator). The integral H ↦ ∫ H dÑ is built on marked simple integrands (levySimpleModule, a Finsupp submodule of adapted bounded space-time-box coefficients), shown an isometry there (assembly_isometry, summing the overlapping-box bilinear pairing sc-levy-bilinear-pairing: 𝔼[(φa·Ñ(boxa))(φb·Ñ(boxb))] = 𝔼[φa·φb]·ν̂(boxa∩boxb)), then extended by continuity (LinearMap.extendOfNorm) to its whole L²(dP⊗dν̂) closure — itoLevyIntegralL2 : levyClosure N →L[ℝ] L²(P) with ‖itoLevyIntegralL2 H‖ = ‖H‖. Design win: defining the target as topologicalClosure(range emb) makes the density hypothesis a soft IsInducing.subtypeVal.dense_iff fact — no from-scratch marked-predictable σ-algebra (the route the continuous Itô CLM needed a bespoke trimmed measure for). The simple-integrand rungs sc-levy-isometry-compensated-simple (the grid double sum 𝔼[(∑ⱼ∑ₗ φⱼₗ·Ñ((tⱼ,tⱼ₊₁]×Aₗ))²] = ∑ⱼ∑ₗ 𝔼[φⱼₗ²]·(tⱼ₊₁−tⱼ)·ν(Aₗ), Foundations/PoissonCompensatedIntegralL2) and sc-levy-isometry-normform (norm form 𝔼[(∫ H dÑ)²] = ‖H‖²_{L²(dP⊗dt⊗dν)}) proved axiom #6 at the simple level via the single independent-scattering PRM field indep_of_disjoint_region (with the diagonal Poisson second moment 𝔼[Ñ(B)²]=ν̂(B), a Mathlib gap-fill via the pmf index-shift (n+1)·c_r(n+1)=r·c_r(n)); the integral CLM closes their declared dense-extension follow-up. Honest scope: all four sc-levy-* entries are axiom-clean full; PRM existence (LevyStochCalc's axiom #2 — Mathlib has no PRM substrate) remains a declared, deferred Summit.

Prior (2026-07-16, multi-asset matrix Riccati): the two matrix-Riccati full entries mf-mm-matrix-riccati / mf-mm-matrix-value (Foundations/MatrixMarketMakingRiccati, BEGV Proposition 2): the spectral-reduction closed form a(t) = U·diag(riccatiCoeff(λᵢ))·Uᴴ solving a'(t) = a(t)·a(t) − Â·Â and its market-making instantiation A' = 2·A·D₊·A − (γ/2)·Σ; the B/C coefficients, general-d value verification, and optimal-control substrate remain deferred.

Prior (2026-07-16, single-asset market-making Riccati): corpus 333, 301 full + 18 wrappers = 319/333 delivery-ready, 14 reduced cores, 0 placeholders. Three new full entries open optimal market making (Foundations/MarketMakingRiccati) — the single-asset (d = 1) closed-form approximation of Bergault–Evangelista–Guéant–Vieira (arXiv:1810.04383): the Riccati coefficient mf-mm-riccati (a(t) = Â·tanh(Â(T−t)) solves a' = a² − Â²; the tanh derivative is derived locally, Mathlib carrying none at this pin), the value-function verification mf-mm-value-function (the quadratic ansatz θ̌ = −Aq² − Bq − C solves the approximate quadratic-Hamiltonian Hamilton–Jacobi equation given the Riccati/linear ODE system — Prop. 1 at d = 1, the B/C coefficients certified by the ring closure), and the closed-form quotes mf-mm-quotes (constant half-spread + inventory-linear skew, instantiated at the Model-A quoteConstA and Model-B quoteConstB constants). Honest scope (mirroring mf-almgren-chriss-EL): we verify the closed-form solution of the approximate HJ equation only; the stochastic optimal-control substrate (existence of the true value function, the verification theorem linking θ to optimal quotes), the approximation-to-truth (numerical in the paper), the multi-asset matrix-Riccati case, and the T → ∞ ergodic limit are out of scope / deferred follow-ups.

Prior (2026-07-12, continuous first-FTAP frame): corpus 330, 298 full + 18 wrappers = 316/330 delivery-ready, 14 reduced cores, 0 placeholders. Four new full entries land the model-agnostic continuous-market EMM frame (Foundations/ContinuousMarket): the general forward FTAP gir-continuous-emm-forward (isEMM_noArbitrageSimple — an equivalent martingale measure precludes arbitrage against simple piecewise-constant predictable bounded strategies, proved directly via the bilinear conditional-expectation pull-out condExp_bilin_of_stronglyMeasurable_left with innerSL ℝ and a vanishing primitive ae_zero_of_nonneg_of_integral_zero shared with the discrete FTAP); its F = ℝ instance gir-discounted-gbm-emm (discountedGBM_isEMM, Q = P: the discounted GBM is already a full-horizon P-martingale, so P is its own EMM); the corollary gir-discounted-gbm-no-arbitrage; and the standalone foundational lemma gir-martingale-reindex (a Q-martingale sampled along a monotone schedule is a discrete Q-martingale). Honest scope: meaning-1 (simple strategies). The physical-measure Girsanov EMM Q ≠ P is intrinsically bounded-horizon (Q = withDensity Z_T is a martingale measure only on [0,T]), so a horizon-aware EMM is tracked as follow-up; general admissible strategies / NFLVR / the converse (Delbaen–Schachermayer) are the deferred meaning-2.

Prior (2026-07-11, survival-model foundation): corpus 326, 294 full + 18 wrappers = 312/326 delivery-ready, 14 reduced cores, 0 placeholders. Two new full entries open the life-contingencies foundation (issue #112): the survival-ratio keystone mf-survival-ccdf-ratio (tpₓ = S_X(x+t)/S_X(x) for t ≥ 0 — the conditional-probability definition of survive, built on Mathlib's conditional measure cond, collapses to the ratio) and mf-survival-ccdf-zero (S_X(0) = 1), in Actuarial/SurvivalModel. Provenance: the design and proofs are our own, in this library's Mathlib idiom; Yosuke Ito's Isabelle/HOL AFP entry Actuarial Mathematics (Survival_Model, BSD) was consulted as a source for the classical result set and is cited, with the author's kind permission. The disclosure is mechanical — metadata.provenance.source == afp-actuarial-mathematics, counted in formalization.yaml.

Prior (2026-07-11, finance-breadth sprint): corpus 324, 292 full + 18 wrappers = 310/324 delivery-ready, 14 reduced cores, 0 placeholders. Five new full finance entries land and one reduced_core flips to full, so mathematical_finance is now 224/225 full: (1) the n-date geometric-Asian option — driver law mf-asian-geom-n-driver ((1/n)∑ B_{τᵢ} ~ N(0, (1/n²)∑∑min(τᵢ,τⱼ))) and closed-form price mf-asian-geom-n-price (reduction to one effective BS driver), BlackScholes/AsianGeometricN; (2) binomial barrier/lookback via the reflection principle — the counting identity mf-barrier-reflection-count and the running-maximum law mf-barrier-maximal-distribution (#{max ≥ a} = 2·#{end > a} + #{end = a}), consuming the previously-stranded reflectionPrincipleEquiv_below, Binomial/BarrierReflection; (3) the Girsanov-grounded quanto forward mf-quanto-forward-grounded — the −ρ σ_S σ_FX drift adjustment derived from a joint-Gaussian FX model + change of measure rather than posited, BlackScholes/QuantoGrounding; and (4) the compound-Poisson aggregate-loss MGF mf-compound-poisson-mgf (reduced_core → full), the n-claim iid-sum MGF composed with the Poisson pgf, Actuarial/CompoundPoissonMGF. Honestly deferred: the fully general 2D Itô formula sc-thm-7.5.2 stays reduced_core — its continuous-time covariation form is a summit-scale build, not a breadth item.

Prior (2026-07-10, bounded-PREDICTABLE Girsanov — Rung 1): corpus 319, 286 full + 18 wrappers = 304/319 delivery-ready, 15 reduced cores, 0 placeholders. New full entry gir-thm-9.1.8-predictable (girsanov_predictable_qbm, Foundations/GirsanovPredictableTheta.Btheta_isQBrownianMotion_predictable_of_bdd) strengthens the continuous-adapted gir-thm-9.1.8 to a bounded predictable θ — the honest domain of the Itô L² integral, dropping the path-continuity assumption. B^θ_u = B_u + driftContinuousMod θ̂ u (the genuinely-𝓕-adapted modification of ∫₀ᵘθ ds) is a Q-Brownian motion under Q = μ.withDensity(exp(−∫₀ᵀθ dB − ½∫₀ᵀθ² ds)). Still spine-free, over a Route-B marshalled density approximation: θ is approximated in L² by clamped dense simple processes marshalled into single-partition (s,c) form (so isExpQMartingale_BthetaSimple applies per n); the stochastic integral, drift, AND quadratic variation each converge in μ-measure (via the drift-modification tower's L²-slice energy identity), fused through a common a.e.-subsequence (exists_subseq_tendsto_ae₂) into the same set-integral engine tendsto_setIntegral_of_subseq_ae_of_sq_bound plus a generic Fatou-L² limit (memLp_two_of_subseq_ae_of_sq_bound), with the partition-generic uniform L⁴/L² moment bounds of GirsanovSimpleDoleansMoments. Axioms-clean, lake build green (8860 jobs), gates + ledger fresh. Girsanov ladder: constant → simple-adapted → continuous-adapted → predictable (Rung 1); only the strictly more general L²/progressive-θ under Novikov (unbounded, Rung 2) remains reduced_core, at sc-thm-9.1.8.

Prior (2026-07-09, continuous-adapted Girsanov closes gir-thm-9.1.8): corpus 318, 285 full + 18 wrappers = 303/318 delivery-ready, 15 reduced cores, 0 placeholders. gir-thm-9.1.8 flips reduced_core → full: girsanov_adapted_continuous_qbm (Foundations/GirsanovAdaptedTheta.Btheta_isQBrownianMotion_adapted) derives the complete Q-Brownian motion — zero start, Gaussian 𝒩(0,t−s) increments, independence of disjoint increments — for a bounded (|θ| ≤ C), 𝓕-adapted, path-continuous θ, under Q = μ.withDensity(exp(−∫₀ᵀθ dB − ½∫₀ᵀθ² ds)) with B^θ_u = B_u + ∫₀ᵘθ ds. Spine-free: rather than a continuous Doléans stochastic exponential proved to be a martingale (a Novikov crux), the simple-θ exponential-martingale identity isExpQMartingale_BthetaSimple (uniform-partition approximants c⁽ⁿ⁾_i = θ(tᵢ)) is passed to the limit — the stochastic exponent Wⁿ = ∑θ(tᵢ)ΔBᵢ → ∫θ dB in L², the drift parts converge everywhere, and the mixed-time set-integral limit ∫_A exp(a·Yⁿ−½)·Zⁿ_T → ∫_A exp(a·Y−½)·Z_T goes through the a.e.-subsequence engine tendsto_setIntegral_of_subseq_ae_of_sq_bound with a route-A L⁴/AM-GM uniform L² bound, then isQBrownianMotion_of_expMartingale reads off the three properties (no adapted-integrand Itô formula). Axioms-clean, lake build green, gates + ledger fresh. This is the culmination of the Girsanov Track-α arc (constant → simple → continuous adapted). Only the strictly more general L²/progressive-θ under Novikov (unbounded) remains reduced_core, at sc-thm-9.1.8.

Prior (2026-07-08, geometric-Asian lognormality + the Wiener-indicator identity): corpus 318, 284 full + 18 wrappers = 302/318 delivery-ready, 16 reduced cores, 0 placeholders. One new full entry plus a reusable foundational brick, both axioms-clean (lake build green, gates + ledger fresh). mf-asian-geom-driver-gaussian (BlackScholes/AsianGeometric.asianGeom_driver_hasLaw): the two-date geometric-Asian log-driver (B_s + B_t)/2 — the Gaussian part of log √(S_s·S_t) under GBM — is Gaussian N(0, (3s+t)/4), the variance the Brownian covariance sum (s + 2·min(s,t) + t)/4. This turns the geometric average into a priceable lognormal, complementing the AM-GM payoff bound mf-asian-geom-le-arith-two. The enabling brick is Foundations/WienerIntegralIndicator.wienerIntegralLp_stepIndicator (∫ 𝟙_{(s,t]} dB = B_t − B_s, from LinearMap.extendOfNorm_eq on the single-basis coefficient), which lets a sum of Brownian values be read as a single Wiener integral of a deterministic step kernel — the same route the Vasicek bond price takes for the integrated rate; here the kernel is a sum of indicators. The law then comes from wienerIntegralLp_hasLaw_gaussian, its variance the kernel L²-norm evaluated on the Ω-side through integral_mul_eval (∫ B_u·B_v = min(u,v)) and zero start B_0 = 0 a.s. Honest scope: two dates (matching the AM-GM entry); the n-date extension is the Finset covariance sum (1/n²)∑∑min(tᵢ,tⱼ), unblocked by the same crux. This closes the geometric-Asian item flagged open by the 2026-07-07 note below.

Live status (2026-07-07, finance breadth — the Vasicek affine bond price + the T-forward measure): corpus 317, 283 full + 18 wrappers = 301/317 delivery-ready, 16 reduced cores, 0 placeholders. Two new full fixed-income entries, both consuming machinery already load-bearing (no new frontier; lake build 8852 green, all 19 gates + ledger 317 fresh, both axioms-clean). (1) mf-vasicek-bond-price (FixedIncome/VasicekBondPrice.vasicekBondPrice_affine): the Vasicek zero-coupon bond price P(0,T) = 𝔼[exp(−∫₀ᵀ r_s ds)] as the Gaussian Laplace transform of the integrated short rate, collapsing to the affine term structure P(0,T) = A(T)·exp(−B(T)·r₀), B(T) = (1−e^{−κT})/κ. The integrated rate ∫₀ᵀ r_s ds = M(T) + σ∫₀ᵀ g dB is carried in its Wiener representation (integrated OU kernel g(u) = (1−e^{−κ(T−u)})/κ; the deterministic time-order swap is the modelling bridge, cited — parity with the OU-solution model of mf-vasicek-sde-terminal-gaussian), its Gaussian law N(M, σ²V) from wienerIntegralLp_hasLaw_gaussian + the FTC variance integral ∫₀ᵀ g² = V(T), and the price factors exp(−M)·𝔼[exp(−σ∫g dB)] = exp(−M + σ²V/2) by the centred Gaussian MGF integral_exp_mul_gaussianReal_zero at −σ. Second deterministic-integrand-Wiener consumer in FixedIncome. (2) mf-forward-measure-spot (FixedIncome/ForwardMeasure.forwardMeasure_bs_expected_terminal): the T-forward measure Q^T (zero-coupon bond as numéraire) with 𝔼^{Q^T}[S_T] = S_0·e^{rT} = S_0/P(0,T) = F(0,T) — the forward price — as a changeOfNumeraire instance (bond slots N_T = P(T,T) = 1, N_0 = P(0,T) = e^{−rT}), the natural next numéraire instance after the stock and S²-numéraires. Honest scope: under the constant-rate ZCB the density dQ^T/dQ = 1 so Q^T = Q coincides with the risk-neutral measure; the construction carries verbatim to a stochastic short rate. CVaR's Rockafellar–Uryasev variational theorem + the coherence quartet were found already complete (RockafellarUryasev, CoherentAxioms); the geometric-Asian closed-form price (only the AM-GM inequality bound exists) remains a genuine open item (needs the BM joint-Gaussian covariance).

Prior (2026-07-03, SDE existence made pathwise — the E-fixed point as a sample-path process, #19 → existence bridge): corpus 312 (unchanged — a Foundations-level formalization advance, not a new benchmark entry). The strong solution, previously banked only as the abstract L²-fixed point picardSolution ∈ E, is now realized as a genuine pathwise process: Foundations/SDEPathwise.sde_pathwise_decomposition slices the fixed-point equation X = Φ(X) (which holds in E) into the sample-path identity X_t(ω) = η(ω) + driftContinuousMod(b∘X)_t(ω) + itoContinuousMod(σ∘X)_t(ω) for a.e. (t, ω). The enabling crux is Foundations/DriftProcessModification.driftProcessAssembled_coeFn: the abstract extendOfNorm drift operator's coeFn equals the honest pointwise-limUnder process driftContinuousMod a.e. It is proved (not, as on the Itô side, true by construction) via two convergences of driftSimpleProcessLp Vₙ — CLM-continuity to the operator and a.e. to the pathwise limit (driftContinuousMod_tendsto, a direct Chebyshev maximal bound — no martingale — plus Borel–Cantelli, the drift analog of itoContinuousMod_tendsto) — unique in measure on the finite trim space, the a.e. convergence lifted from per-slice to the trim measure through the predictable-measurable convergence set. All axiom-clean ([propext, Classical.choice, Quot.sound], pinned in AxiomAudit). The drift term is now the honest single Lebesgue integral (#33, this session): DriftProcessModification.driftContinuousMod_eq_setIntegral proves driftContinuousMod g t ω = ∫₀ᵗ ⇑g(s,ω) ds a.e. for every t ≤ T — the elementary drifts ∫₀ᵗ Vₙ ds converge to driftContinuousMod, and the ω-slice energies Dₙ(ω) = ∫₀ᵀ(⇑Vₙ − ⇑g)² ds decay in L¹(μ) (= ‖simpleAssembly_T Vₙ − g‖²), so a subsequence has Dₙₖ(ω) → 0 a.e., whence the interval Cauchy–Schwarz |∫₀ᵗ(⇑Vₙₖ − ⇑g)| ≤ √(T·Dₙₖ(ω)) → 0 matches the two limits. SDEPathwise.sde_pathwise_drift_eq_setIntegral specializes it to b∘X, so the strong solution's drift term is the recognizable SDE integral ∫₀ᵗ b(X_s(ω)) ds, not merely an abstract limit. All axiom-clean. sc-thm-8.2.5's existence half stays the conditional-c < 1 E result; this bridge makes that solution's sample paths — and now its drift integral — explicit.

Prior (2026-07-03, SDE strong-solution uniqueness — the L²-energy Grönwall keystone, #19): corpus 312, 278 full + 18 wrappers = 296/312 delivery-ready, 16 reduced cores, 0 placeholders. The uniqueness half of Theorem 8.2.5 is now a genuinely derived theorem, not an assumed field. Foundations/SDEUniqueness.IsL2SolutionPair.uniqueness (entry sc-thm-8.2.5, flipped reduced_core → full) proves two L² strong solutions of dX = μ(X)dt + σ(X)dB sharing the driver agree a.s. at every time, via the classical L²-energy argument: E t = 𝔼[(Xₜ−Yₜ)²] satisfies E t ≤ (2·Cdrift·t + 2·Cdiff)·∫₀ᵗ E, and gronwall_zero_of_le_const_mul_integral (a reusable integral Grönwall, built from Mathlib's differential form via the FTC primitive G t = ∫₀ᵗ E) forces E ≡ 0. The drift energy bound is derived from Lipschitz μ (drift_energy_le: Cauchy–Schwarz in time + Tonelli), the diffusion from the Itô isometry. Honest scope: (i) this is the uniqueness half — existence stays the separately-banked conditional-L² Picard result (sde-picard-existence-uniqueness); (ii) the diffusion enters through an operator Iσ whose sole assumed property is the Itô isometry energy bound (the isometry field of IsL2SolutionPair) — a genuine, proven property of the Itô integral (itoProcessCLM_norm_sq), not the conclusion in disguise; (iii) a non-vacuity guard (the zero solution) certifies the IsL2SolutionPair field set is satisfiable. This replaces the prior reduced_core encoding, whose uniqueness was an assumed structural field read off by projection.

Prior (2026-07-03, the change of numéraire — the IV↔I seam): corpus 312, 277 full + 18 wrappers = 295/312 delivery-ready, 17 reduced cores, 0 placeholders. The library now has a general change-of-numéraire theorem plus both of its seam directions. (1) Foundations/Numeraire.changeOfNumeraire (entry mf-change-of-numeraire, full) proves price is numéraire-invariant: with Q^N = Q.withDensity((N_T·B₀)/(N₀·B_T)), every terminal claim X satisfies N₀·𝔼^{Q^N}[X/N_T] = B₀·𝔼^Q[X/B_T] — a pure measure-transport identity plus cancellation of N_T, needing no integrability hypothesis. The backbone is consumed, not orphaned: StockNumeraire.stockNumeraireMeasure_eq_numeraireMeasure exhibits the BS stock numéraire as the instance B_T = e^{rT}, B₀ = 1, N = S, and ExchangeOption.exchangeOption_numeraire_price (entry mf-exchange-numeraire, full) exhibits Margrabe's S²-numéraire valuation as the instance X = exchange payoff, N = S². (2) Performance/KellyNumeraire.kellyNumeraire_isRiskNeutral (entry mf-kelly-numeraire-emm, full) delivers the numéraire-portfolio ⟹ EMM direction: the growth-optimal (Kelly) wealth, used as deflator, turns the physical measure into the risk-neutral one (q₊·b + q₋·(−1) = 0), the p-independence being exactly the Kelly first-order condition. Honest scope: the portfolio⟹EMM direction is the discrete, two-outcome market — the elementary shadow of the continuous Long/Platen benchmark theorem (deflated prices are P-martingales, EMM density ∝ 1/N*), which still needs a state-price-density / market model absent from the Itô tower. Garman's normal form is post-integration closed-form algebra (no measure), so it is not a numeraireMeasure instance and none was fabricated.

Prior (2026-07-02, SDE existence — the Picard fixed point, #44): corpus 309, 274 full + 18 wrappers = 292/309 delivery-ready, 17 reduced cores, 0 placeholders. The strong solution of dX = b(X)dt + σ(X)dB is now constructed as a Picard fixed point. Foundations/SDEExistence.picardMap_exists_unique_fixedPoint (entry sde-picard-existence-uniqueness, full) builds the Picard iterate Φ(X) = η + ∫₀ᵗ b(X)ds + ∫₀ᵗ σ(X)dB as a self-map of the predictable L² space E = Lp 2 (trimMeasure_T T) — its diffusion term the actual Itô integral assembled in the tower — proves the a priori contraction estimate ‖Φ X − Φ Y‖ ≤ (T·L_b + √T·L_σ)‖X − Y‖ (drift operator norm T × Cauchy–Schwarz, Itô operator norm √T × the isometry), and obtains existence and uniqueness of the fixed point via Banach's theorem. Honest scope: the L²/E formulation, conditional on the small-horizon contraction constant < 1. The abstract-operator benchmark sc-thm-8.2.5 (ℝ-time, intervalIntegral drift, opaque Iσ) stays reduced_core pending the ℝ≥0↔ℝ-time translation + a Bielecki all-T extension.

Prior (2026-06-30, Phase 2 — Girsanov: the EMM as an explicit change of measure): corpus 308, 273 full + 18 wrappers = 291/308 delivery-ready, 17 reduced cores, 0 placeholders. The Black–Scholes risk-neutral measure is now constructed as a Girsanov density change, not taken as given. Foundations/Girsanov.bs_discounted_isQMartingale (entry gir-bs-emm-girsanov, full) tilts the physical measure by Q = withDensity(exp(−θX_T − ½θ²T)) (constant market price of risk θ = (μ−r)/σ) and proves the discounted stock is a Q-martingale on [0,T] — retiring the Wald shortcut of discountedGBM_isMartingale, which took Q = P from the start. It stands on a reusable Bayes change-of-measure engine Foundations/ChangeOfMeasure.changeOfMeasure_setIntegral_eq (entry gir-change-of-measure-engine, full): if Z and Z·D are both P-martingales then D is a Q-martingale on [0,T] — no stochastic calculus, only conditional expectations (a Bayes pull-out and a martingale set-integral). The one new estimate is the mixed-time integrability of D_u·Z_T, via AM–GM (exp(σX_u)exp(−θX_T) ≤ exp(2σX_u)+exp(−2θX_T), each Gaussian-MGF-integrable). This partially wires the architecture doc's Girsanov seam (I↔II, the martingale side; see mathematical-architecture.md). The distributional side is now fully closed for constant θ (2026-07-05): Foundations/GirsanovConstantTheta.Btheta_isQBrownianMotion proves the drift-corrected B^θ_t = X_t + θ t is a genuine Q-Brownian motion — zero start, Gaussian increments B^θ_t − B^θ_s ~ N(0, t−s), and independence of disjoint increments (corpus gir-const-theta-qbm, full; the marginal law is gir-const-theta-marginal, full). All three properties are now read off in one application of the process-agnostic exponential characterization Foundations/ExpMartingaleQBrownian.isQBrownianMotion_of_expMartingale (2026-07-06): the const-θ exponential martingale exp(a·B^θ − ½a²·) (expBtheta_isQMartingale, from the Bayes engine + two Wald exponentials) is packaged as IsExpQMartingale, and the characterization derives the marginal law, the increment law, and independence — the same reusable module now scheduled to power the simple-/continuous-θ cases (Route α). The increment independence, previously flagged as a Mathlib gap ("conditional-MGF ⟹ independence" is absent — only the reverse condExp_indep_eq exists), is reached WITHOUT that lemma: via Mathlib's indepFun_iff_charFun_prod, the joint characteristic function at w = (w₁, w₂) is the charFun-at-1 of the Gaussian law of the linear combination w₁·I₁ + w₂·I₂ (from the joint-MGF factorisation — a condExp_mul_of_stronglyMeasurable_left pull-out), so it factors into the two marginal Gaussian characteristic functions (charFun_gaussianReal) — no adapted-integrand Itô formula.

Simple (piecewise-constant) adapted θ — now full (2026-07-06): gir-simple-adapted (Foundations/GirsanovSimpleTheta.Btheta_simple_isQBrownianMotion) proves B^θ_t = X_t + ∑_i c_i (s_{i+1}∧t − s_i∧t) is a Q-Brownian motion under Q = P.withDensity(E^{−c}_T) for bounded 𝓕_{s i}-measurable multipliers — the general bounded-adapted-θ Girsanov for the simple case, strictly beyond constant θ, via one application of isQBrownianMotion_of_expMartingale (no charFun chain re-derived). The two simple-θ-specific ingredients: the spine simple_spine_ae (E^{−c}·exp(a·B^θ − ½a²·) =ᵐ E^{a−c}) and the mixed-time integrability integrable_expBthetaSimple_mul_density (an L² Hölder: Z_T² = E^{−2c}_T·exp(∑ c_i²Δτ_i) with ∑ c_i²Δτ_i ≤ K²T).

Continuous adapted θ — now full (2026-07-09): gir-thm-9.1.8 (Foundations/GirsanovAdaptedTheta.Btheta_isQBrownianMotion_adapted) closes the bounded adapted continuous case by exactly the L²-approximation route anticipated here: the simple-θ identity isExpQMartingale_BthetaSimple (on the uniform-partition approximants c⁽ⁿ⁾_i = θ(tᵢ)) passed to the limit through the a.e.-subsequence set-integral engine tendsto_setIntegral_of_subseq_ae_of_sq_bound (route-A L⁴/AM-GM uniform L² bound on the mixed-time product exp(a·Yⁿ−½)·Zⁿ_T), then one application of isQBrownianMotion_of_expMartingale — no adapted-integrand Itô formula, no continuous stochastic-exponential-is-a-martingale (Novikov) crux. Open (still reduced_core): only the strictly more general L²/progressive-θ under Novikov (unbounded, merely progressively measurable), at sc-thm-9.1.8.

Prior round (2026-06-29, Phase 1 — the convex-duality unification: pricing = risk): corpus 306, 271 full + 18 wrappers = 289/306 delivery-ready, 17 reduced cores, 0 placeholders. The FTAP (pricing) and the coherent-risk representation (risk) are now proved to be the same Hahn–Banach theorem. A shared cone-separation root lives in Foundations/ConvexDuality.lean — the cone↔simplex separation exists_pos_separating_of_cone_disjoint_simplex + the point↔cone companion exists_separating_of_not_mem_cone, sharing two atoms (functional_eq_sum_single, functional_nonneg_on_cone). Four new full corpus entries stand on it: mf-convex-duality-root (the root); the FTAP kernel exists_pos_dual_of_disjoint_stdSimplex re-derived in place from it (signature byte-identical → no consumer churn); mf-coherent-risk-representation (RiskMeasures/AcceptanceSet.coherentRisk_isLUB, the finite-state ADEH representation stated as an IsLUB, acceptance-set closedness derived from the four axioms, not assumed); mf-worstcase-risk-representation (RiskMeasures/WorstCaseRisk.worstCase_isLUB, a concrete instance — worst-case loss = sup over the whole probability simplex); and mf-superhedging-emm-bound (Foundations/SuperhedgingDuality.emm_le_superReplication, every equivalent martingale measure prices a claim ≤ its super-replication cost). This realizes the architecture doc's #1 seam (I↔IV; see mathematical-architecture.md). Open: the superhedging strong-duality equality (superhedge = sup_{EMM}), blocked on a finite-dimensional Farkas / polyhedral-cone closedness absent from Mathlib at this pin; the Gaussian CVaR robust form.

Prior round (2026-06-29, Summit C in Degenne's IsLocalMartingale typeclass — the wrapper completed): corpus 302, 267 full + 18 wrappers = 285/302 delivery-ready, 17 reduced cores, 0 placeholders. The unrestricted-C³ residual M is now a genuine IsLocalMartingale (Foundations/ItoFormulaUnrestrictedLocMart.lean, entry sc-ito-formula-unrestricted-islocalmartingale, full): the one ingredient beyond the explicit form — adaptedness of M (residual_stronglyMeasurable), i.e. of the drift primitive D_t = ∫₀ᵗ drift (driftPrimitive_stronglyMeasurable, time-clamp + Carathéodory + StronglyMeasurable.integral_prod_right) — discharged; then StronglyAdapted.stoppedProcess_indicator + the all-time agreement assemble Locally (Martingale ∧ cadlag) with the exit-time localizer σ_N. Itô's formula now holds for a general C³ f with NO growth/boundedness hypothesis (Foundations/ItoFormulaUnrestricted.lean, entry sc-ito-formula-unrestricted-local, full): the residual M_t = f(t,B_t) − f(0,B_0) − ∫₀ᵗ(f_t+½f_xx)ds is a continuous local martingale in explicit form — a localizing sequence σ_N = min(τ_N, N) ↑ ⊤ (exit times capped in time) plus per-N continuous true martingales agreeing with M on {t ≤ σ_N}. The engine is the double cutoff f(φₙ·,φₙ·) (time and space), whose globally-bounded derivatives let ito_formula_td_process apply; the all-time agreement is indistinguishable_on_stochInterval. The Degenne-IsLocalMartingale-typeclass packaging remains as drift-integral-adaptedness plumbing. The time-dependent Itô formula now holds as a process identity for every t ≤ T simultaneously (Foundations/ItoFormulaProcess.lean, entry sc-ito-formula-td-process, full): f(t,B_t) − f(0,B_0) =ᵐ (itoProcessL2Inf t F) + ∫₀ᵗ (f_t + ½f_xx)(s,B_s) ds, the stochastic term the genuine Itô-integral process (f_x(·,B) ● B)_t — a continuous L² martingale admitting an everywhere-continuous local-martingale modification on the null-augmented Brownian filtration. So the compensated process f(t,B_t)−f(0,B_0)−∫₀ᵗ drift is (a modification of) a continuous local martingale: Itô's lemma as a semimartingale decomposition. This makes the [0,∞) continuous-local-martingale tower load-bearing as an Itô-formula consumer for the first time, and is the prerequisite for the unrestricted-C² (stopping-time localization) Itô formula. The construction is entirely inside the Itô tower — no Markov property, no PDE: the terminal formula's witness is now canonical (ito_formula_td_L2_bddDeriv exposes gfx =ᵐ [f_x(·,B)]), zero-extended to a [0,∞) integrand F (exists_fullHorizon_extension) and matched to each horizon via the existing consistency itoProcessL2Inf_eq_itoProcessCLM. Earlier (corpus 298): the Itô formula decomposes f(X) for a general C³ exp-growth f against a constant-coefficient Itô process X_t = X₀ + b·t + σ B_t (Foundations/ItoFormulaItoProcess.lean, sc-ito-formula-ito-process, full), f(X_T) − f(X₀) =ᵐ itoIntegralCLM_T gfx + ∫₀ᵀ (f'(X)·b + ½f''(X)·σ²) ds, gfx =ᵐ [σ·f'(X_·)]. Earlier: Geometric Brownian motion is decomposed by the genuine continuous Itô integral (Foundations/ItoFormulaGBM.lean, entries sc-ito-formula-gbm and sc-discounted-gbm-ito, both full) — the first pricing-ward consumer of the analytic Itô tower, which until now had none (GBM/BS pricing ran via separate algebraic towers and the Wald exponential). ito_formula_gbm gives Ŝ(T) − Ŝ(0) =ᵐ itoIntegralCLM_T gfx + ∫₀ᵀ m·Ŝ ds with gfx =ᵐ [σ·Ŝ(·)] for the GBM value Ŝ(t)=S₀ exp((m−σ²/2)t+σ B_t), the stochastic term the real Itô integral. The route is the classic one — localization in time: the GBM value is t-exponential (fails the localized formula's t-uniform growth), so the localized formula is applied to the time-localized exponent S₀ exp((m−σ²/2)·φₙ(t)+σx) (φₙ = smooth cutoff, n=⌈T⌉₊), the identity on [0,T] yet globally bounded; there φₙ=id, φₙ'=1, so the localization drift (m−σ²/2)·Ŝ and the Itô correction ½σ²·Ŝ collapse to m·Ŝ. Setting m=0 (discountedGBM_eq_itoIntegral) makes the drift vanish — the Itô-integral content of the discounted-GBM martingale (discountedGBM_isMartingale, there via the Wald exponential). Axioms-clean [propext, Classical.choice, Quot.sound]. Earlier: The time-dependent Itô formula reaches at-most-exponential growth (Foundations/ItoFormulaLocalized.lean, entry sc-ito-formula-localized, full): ito_formula_td_localized lifts the bounded-derivative ito_formula_td_L2_bddDeriv to f with |f_• t x| ≤ C·exp(λ|x|), so it reaches the Black–Scholes/GBM value function f(t,x)=S₀ exp((r−σ²/2)t+σx) — the named out-of-scope gap of 7.1.1/7.1.2. An L²-cutoff localization consumes the bounded engine: smooth truncation φₙ (a ContDiffBump antiderivative), the cutoff fₙ=f(t,φₙ(x)) through cutoff_bddDeriv, then n→∞ — boundary and drift converge in L²(μ) (Brownian marginals have every exponential moment, BrownianExpMoment; the drift dominator is the new base stone pathIntegral_expGrowth_memLp), so aₙ=itoIntegralCLM_T gfxₙ is Cauchy, the Itô isometry transfers Cauchy-ness to the integrands, completeness gives the witness, CLM continuity identifies the limit, and an a.e.-identification pass names it (gfx =ᵐ [f_x(·,B_·)]). Axioms-clean [propext, Classical.choice, Quot.sound]. Earlier: The unbounded-horizon Itô integral is a continuous local martingale on the whole half-line ℝ≥0 (Foundations/ItoIntegralProcessLocalMartingaleInfinite.lean, entry sc-ito-infinite-local-martingale, full): an everywhere-continuous representative modifying the process at every t. The per-horizon [0,T=n] continuous local martingales are glued — horizon consistency (itoProcessL2Inf_eq_itoProcessCLM, resting on a hand-built [0,T] clamp of Degenne's SimpleProcess) makes each a modification of the same unbounded-horizon process and indistinguishable_of_modification_on agrees them on overlaps — into one path continuous on all of ℝ≥0; with no horizon clamp, the martingale property is the global itoProcessL2Inf_isMartingale through condExp_sup_nulls. This crowns the pathwise-regularity layer (2026-06-26): the L²-valued process (φ●B)_t has a continuous modification on [0,T] (Foundations/ItoIntegralProcessContinuousModification.lean, entry sc-ito-general-continuous-modification, full) — the first sample-path result for the general integrand, via Degenne's continuous-time Doob maximal inequality + Borel–Cantelli on a fast subsequence — upgraded to a genuine continuous local martingale (Foundations/ItoIntegralProcessLocalMartingaleGeneral.lean, entry sc-ito-general-local-martingale, full): the everywhere-continuous representative, adapted to the null-augmented Brownian filtration 𝓕ᴮ ⊔ 𝓝, meets Degenne's IsLocalMartingale interface. The measure-theoretic core is condExp_sup_nulls (cond-expectation invariance under the null augmentation, its σ-algebra crux consuming Mathlib's eventuallyMeasurableSpace); both are axioms-clean and non-redundant with Degenne's sorry-backed general càdlàg modification. Earlier this day: the d-asset one-period FTAP ftap_one_period_vector (Foundations/FTAPOnePeriodVector.lean, entry mf-ftap-one-period-vector, full) is the unrestricted Föllmer–Schied 1.6 for a discounted excess return valued in any finite-dimensional inner-product space F (the ℝᵈ market is F = EuclideanSpace ℝ (Fin d)) — no non-redundancy hypothesis. The explicit Esscher / minimal-divergence EMM minimises the convex softplus potential θ ↦ ∫ log(1 + exp⟪θ,Y⟫); it is constant along the gains kernel N = {θ : ⟪θ,Y⟫ = 0 a.e.} and coercive on Nᗮ, so a minimiser on Nᗮ is automatically global (redundant directions are absorbed, dropping the earlier non-redundancy assumption), and its first-order condition (differentiation under the integral) hands back the strictly-positive bounded density σ⟪θ₀,Y⟫. No Hahn–Banach, no L⁰-closedness, no measurable selection — those remain only for the general-Ω multi-period DMW. General-Ω one-period Fundamental Theorem of Asset Pricing (Föllmer–Schied 1.55 / one-period Dalang–Morton–Willinger): ftap_one_period — for a scalar L⁰ excess return on an arbitrary probability space, no arbitrage ⟺ ∃ equivalent martingale measure Q ~ P with Y integrable and E_Q[Y] = 0 (Foundations/FTAPOnePeriod.lean, entry mf-ftap-one-period-general), backward via a bounded-density reduction to L¹, the scalar no-arbitrage dichotomy, and a two-region balancing withDensity — no Hahn–Banach, no Kreps–Yan. This is the genuine measure-theoretic step beyond the finite-Ω Harrison–Pliska ftap_discrete (no arbitrage ⟺ ∃ EMM, multi-period, finite Ω, scalar discounted asset; Foundations/FTAPDiscrete.lean, entry mf-ftap-discrete-complete), itself backward via a global geometric Hahn–Banach separation of the attainable-gains subspace from the standard simplex (the reusable kernel Foundations/ConvexSeparation.lean) and forward via martingale-transform telescoping; plus the single-period multi-state biconditional hasEMM_multi_iff_not_hasArbitrage (entry mf-ftap-single-period-complete). Open follow-on: the general-Ω multi-period DMW (L⁰-closedness + measurable selection, absent from the pin) — the d-asset one-period case is now closed in full (ftap_one_period_vector, redundant assets included). Since B3: D1 (the bilinear Itô isometry — the [0,T] Itô CLM bundled as a LinearIsometry, so it preserves the L²-inner product by polarization: 𝔼[(∫φ dB)(∫ψ dB)] = ⟪φ, ψ⟫, the diagonal recovering the isometry; Foundations/ItoIntegralCovariation.lean, entry sc-ito-covariation-bilinear-isometry). Earlier on the Itô tower: B2 (unbounded-horizon [0,∞) σ-finite Itô integral CLM itoIntegralL2, Foundations/ItoIntegralL2Dense.lean, entry sc-ito-infinite-horizon-isometry) and B3 (the elementary Itô integral as a continuous local martingale — pathwise continuity + Degenne's Martingale.IsLocalMartingale, Foundations/ItoIntegralProcessLocalMartingale.lean, entry sc-ito-simple-process-local-martingale). The figures further below are the historical 2026-05-20 audit record, kept as provenance.

Summit B / B1b round (2026-06-12). The general-integrand Itô integral (φ●B)_t = ∫₀ᵗ φ dB for a general predictable φ ∈ L2Predictable[0,T], as a continuous L² martingale on [0,T] (Foundations/ItoIntegralProcessGeneral.lean). It extends B1a (simple integrands) by density along the same simpleAssembly_T embedding that builds the terminal CLM itoIntegralCLM_T, so the bridge to B1a is definitional (extendOfNorm_eq). The key identity (φ●B)_t = E[∫₀ᵀ φ dB | 𝓕_t] (the condExpL2 projection of the terminal integral) yields the L² martingale property (condExp tower), a.e.-adaptedness, the Itô contraction ‖(φ●B)_t‖ ≤ ‖φ‖, the terminal isometry ‖(φ●B)_T‖ = ‖φ‖, and L²-continuity (uniform approximation via the t-free contraction). 3 new full entries: sc-ito-general-martingale / -terminal-isometry / -l2-continuity. Honest scope: finite-horizon [0,T], L² sense.

Isometry round (2026-06-12). The explicit per-t isometry E[(φ●B)_t²] = ∫₀ᵗ E[φ²] ds — deferred at B1b — is now proved (itoProcessCLM_norm_sq, Foundations/ItoIntegralProcessIsometry.lean, entry sc-ito-general-time-isometry): the band-restricted simple-process isometry (B1a's per-endpoint-∧t-truncated rectangle double sum = the joint-overlap-∩(0,t] double sum, equal by a pure-ℝ interval-length identity) transfers to all predictable φ by DenseRange.equalizer — both ‖(φ●B)_t‖² and ∫_{(0,t]}φ² (= ‖truncCLM φ‖², the band-truncation CLM) are continuous and agree on the dense simple processes. The generic lp_two_norm_sq was de-privatised in ItoIntegralL2 and reused (no duplication). Net: corpus 280 → 281, 245 → 246 full; lake build 8724 jobs green, axioms-clean. (B2 — the infinite-horizon [0,∞) σ-finite extension — landed 2026-06-13: itoIntegralL2 / itoIntegralL2_norm in Foundations/ItoIntegralL2Dense.lean, corpus entry sc-ito-infinite-horizon-isometry.)

Refresh with:

python3 -m tools.verify.coverage_report

Coverage as of 2026-06-22 (extended mathematical-finance pass: put greeks, higher-order BS greeks including charm, Bachelier greeks, digital greeks, BS-Merton with dividends, Garman-Kohlhagen FX, Black-76 greeks; second pass: Bachelier γ/θ, asset-or-nothing γ, BS-Merton δ/γ/vega, American options in binomial tree; third pass: CRR drift-quotient limit closing the analytic content of CRR-to-BS; fifth pass: cash-or-nothing digital gamma closing the previously deferred quotient-rule item; sixth pass: full digital ρ/vega/θ matrix for cash and asset variants — 6 theorems closing the remaining digital Greek gap; seventh pass: Black-76 ρ and θ closing the futures-options Greek set; eighth pass: CRR drift limit n-form n·(2p_n−1)·σ·√(T/n) → (r−σ²/2)T closing the previously deferred substitution work; ninth pass: Phase 5 broader mathematical-finance — fixed-income ZCB pricing/yield/duration/convexity, two-asset Markowitz portfolio theory with completing-the-square factorization, CAPM beta + portfolio linearity — 12 theorems extending the project beyond derivatives pricing into fixed income and portfolio theory; tenth pass: Phase 6 quant-risk + N-asset portfolio + bond immunization — Gaussian VaR/CVaR closed forms with affine/scaling identities, bond portfolio rate sensitivity + Redington-style first-order immunization, N-asset Markowitz variance via Finset double sum with diagonal/iid/PSD/two-asset specializations — 15 theorems; eleventh pass: Phase 7 performance / coherent risk / fixed-income depth / static bounds / two-fund separation — Sharpe (√T scaling + scale invariance) + Kelly criterion, gaussian VaR/CVaR coherent risk-measure axioms (translation, homogeneity, monotonicity, gaussian subadditivity via joint-stdev triangle inequality), annuity geometric-series closed form + forward/spot consistency + coupon-bond YTM monotonicity, Phi ≤ 1 + BS call/put price upper bounds + box-spread arbitrage identity, capital market line equation + Sharpe invariance + two-fund decomposition — 23 theorems extending the project into performance measurement, axiomatic risk, and multi-fund portfolio theory; twelfth pass: Phase 8 extended performance / second-order immunization / Asian option inequality — Sortino/Treynor/Information ratios + tracking-error decomposition, second-derivative bond rate sensitivity ∂²P/∂r² = C_P·P + Redington second-order convexity-matching immunization, two-element and equal-weight n-element AM-GM with two-date geometric ≤ arithmetic Asian payoff bound — 13 theorems; thirteenth pass: Phase 9 credit-risk + strike Greeks + multi-period Kelly — reduced-form credit spread under constant hazard with survival monotonicity, BS strike-direction derivatives (∂_K bsV, ∂_K bsP, ∂²_K bsV) via magic-identity collapse + put-call parity, multi-period Kelly criterion with myopia + fraction sign analysis — 14 theorems): 267 / 284 delivery-ready (249 full + 18 library wrappers), 17 reduced cores, 0 placeholders.

2026-08-07 — vNM expected-utility round (#178). Added one full benchmark entry covering the mixture algebra of finite-outcome lotteries, affinity of expected utility in the mixture, the von Neumann–Morgenstern axioms verified for the expected-utility preference (completeness, transitivity, independence, Archimedean continuity with the indifference weight exhibited), and invariance of the preference under positive affine rescaling of the utility. Soundness direction only — the representation theorem (axioms ⟹ ∃u) is deliberately out of scope and the module doc records it.

2026-08-02 — downside-performance round (#73). Added one full benchmark entry covering finite-state Omega nonnegativity and its threshold identity, maximum-drawdown nonnegativity and nonnegative scaling on finite price paths, and positive-scaling invariance of the Calmar ratio. The corrected drawdown theorem deliberately assumes 0 ≤ c; negative scaling reverses peak-to-trough order and is not claimed.

Poisson cluster + Itô-QV upgrade round (2026-06-05). Four reduced cores earned full by replacing statement-level specs with genuine derivations, each backed by a new Foundations/ module: pp-thm-3.3.9 (superposition — the Poisson convolution identity Poisson(a) ∗ Poisson(b) = Poisson(a+b), absent from Mathlib, proved by singleton-ext + binomial collapse; PoissonSuperposition.lean), pp-thm-3.3.10 (thinning — the binomial-marking factorisation into Poisson(pr) ×ₘ Poisson((1−p)r), so the thinned marginals AND the independence of the streams are derived; PoissonThinning.lean), pp-thm-3.3.5 (marginal law re-earned via the interarrival-construction route this file had flagged: Erlang arrival law composed with the new Gamma-CDF difference identity ∫₀ᵗ γ_k − ∫₀ᵗ γ_{k+1} = e^{−rt}(rt)ᵏ/k!; PoissonCounting.lean), and sc-thm-7.4.5 (QV of an Itô process in the constant-σ/Lipschitz-drift regime — drift contributes nothing, with explicit 1/n L² rates; ItoProcessQV.lean; the previous spec was degenerate — its "stochastic piece" was a Lebesgue integral of σ). pp-prop-3.3.6 stays reduced_core honestly but its core is now derived, not assumed: the FIRST interarrival is proved exponential from the counting axioms and the memoryless survival factorisation is proved from independent increments (PoissonInterarrival.lean); the full-sequence iid claim still needs the strong Markov property (upstream-gated). Net: 225 full + 18 wrappers = 243 / 261 delivery-ready, 18 reduced cores.

Finance layer over the Poisson/QV track (2026-06-06). Six new full entries make the freshly-derived foundations load-bearing in the pricing layer: mf-variance-swap-drift-immunity (realized variance of GBM log-returns → σ²T in L² for ANY drift — the variance-swap fair strike is a QV functional, immune to the physical-vs-risk-neutral drift; strengthens the phase-34 expectation-level limit; VarianceSwapDriftImmunity.lean, first pricing consumer of ItoProcessQV), mf-first-to-default-spread (FtD basket spread = Σ single-name hazards under independence — ExpMin.minimum_survival bridged into the Credit.lean vocabulary; FirstToDefault.lean), dist-poisson-pgf (the Poisson pgf E[x^N] = e^{r(x−1)} for every real x, absent from Mathlib; PoissonPgf.lean), and the Merton (1976) jump-diffusion trio (mf-merton-call-series, mf-merton-spot-recombination, mf-merton-put-call-parity): the price is defined as the expectation over the Poisson jump count, so the textbook series, the compensation identity E[spot_N] = S₀ (the pgf at 1+k), and parity C − P = S₀ − Ke^{−rT} are theorems — and every series term is separately proved equal to a discounted conditional expected payoff (bs_call_formula on (ℝ, gaussianReal 0 1)). Terminal-mixture-law scope, exactly parallel to BSCallHyp: the compound-Poisson jump SDE is upstream-gated and not claimed (MertonJumpDiffusion.lean). Net: 231 full + 18 wrappers = 249 / 267 delivery-ready, 18 reduced cores (corpus 261 → 267).

Merton dominance + classic display; Markov path law (2026-06-06, second round). Two new full entries deepen the Merton layer: mf-merton-dominance — jump risk is never free, C_BS(S₀,σ) ≤ C_Merton(S₀,σ,k,δ,Λ) for every Λ, δ, k > −1, proved by pricing the two jump channels separately: per-term vol-monotonicity (bsV_strictMonoOn_sigma, vega) lowers the jump vol to δ = 0, and there a Jensen floor comes from the new spot-direction convexity bsV_spot_convexOn (gamma ≥ 0 second-derivative test, the S-direction dual of bsV_strike_convexOn; SpotConvexity.lean) whose supporting tangent at S₀ has its linear term integrate to zero by the compensation identity integral_mertonSpot (MertonDominance.lean). And mf-merton-classic-display — the textbook Λ′ = Λ(1+k) form, driven by the rate-shift invariance bsV K r σ (S·e^{cτ}) τ = e^{cτ}·bsV K (r+c) σ S τ (bsV_spot_exp_rate_shift) at c_n = r_n − r plus Poisson-weight absorption (MertonClassicDisplay.lean). One reduced core earned full: mc-thm-1.1.2 (path distribution of a Markov chain) — the chain's law is now constructed via the pin's Ionescu–Tulcea trajectory kernels (Kernel.trajMeasure) from kernels that read only the last history coordinate, and P(X₀=i₀,…,Xₙ=iₙ) = init(i₀)·∏ P(iₖ,iₖ₊₁) is derived by induction through the comp-product recursion of the marginals, replacing the prior definitional rfl (Foundations/MarkovPathMeasure.lean; the converse characterization is not claimed). The same Kernel.traj re-cost found the other five Markov reduced cores still honestly gated: recurrence needs renewal theory / fundamental-matrix algebra, convergence needs Perron–Frobenius, the ergodic theorem needs both, stationarity-uniqueness needs recurrence, and the strong Markov property needs stopping-time kernels — none in the pin. Net: 234 full + 18 wrappers = 252 / 269 delivery-ready, 17 reduced cores (corpus 267 → 269).

Values-gates round (2026-06-06, evening). The honesty conventions this file documents became mechanically enforced: tests/test_values.py adds (1) a forbidden-text scan over MathFin/ sources (no sorry/admit/native_decide/polyrith/?-suggestion tactics/hammer/loogle/ leansearch outside comments), (2) a definitional-rfl tripwire — no full entry may cite a theorem whose proof is bare rfl/unfold; rfl (the reduced_core pattern in disguise), (3) blueprint-spine ⊆ curated audit, (4) byte-freshness of the new GENERATED exhaustive audit MathFin/AxiomAuditGen.lean, which #guard_msgs-pins every proof-position MathFin constant cited by the corpus (222 names vs the curated file's headliners). CI (build.yml) now runs pytest + ledger status before the Lean build, so these gates and ledger freshness are push-enforced, not session discipline. First-run catches: the tripwire demoted mf-kelly-n-periods-linearity full→reduced_core (its cited lemma states T·kellyGrowth = T·(unfolded formula) by rfl; the genuine multi-period iid model is not formalized — same class as the 2026-05-29 newton-raphson demotion, now pinned in EXPECTED_REDUCED_CORE_THEOREMS), and the blueprint-coverage check found seven spine headliners unguarded (including bs_identity), now pinned in the curated audit. Net: 233 full + 18 wrappers = 251 / 269 delivery-ready, 18 reduced cores.

Summit A′ round (2026-06-07). Two reduced cores earned full, each by replacing the named gap with the actual mathematics. (1) mf-kelly-n-periods-linearity — repairing the previous round's definitional-rfl demotion: the n-period iid model is now real measure theory (Performance/Kelly.lean): one period's wealth multiplier is the two-point law kellyReturnMeasure p b f, n periods are its n-fold Measure.pi, and E[∑ log Rᵢ] = n·kellyGrowth p b f is computed via linearity of expectation through the product measure's coordinate evaluations. (2) sc-thm-7.1.2 — the time-dependent Itô formula (Summit A′): f(T,B_T) − f(0,B₀) = ∫₀ᵀ f_x(s,B_s) dB_s + ∫₀ᵀ (f_t + ½f_xx)(s,B_s) ds a.e., the classical df = f_x dB + (f_t + ½f_xx) dt, with the stochastic integral the genuine itoIntegralCLM_T. The three Summit-A limit arguments redone with (t,x)-dependence: WeightedQuadraticVariation generalized to bounded adapted weight processes (the fluctuation engine never cared the weight was g(B_s); tendsto_riemann_L2_process exported standalone for the drift term), the 2D Itô–Taylor remainder vanishing at O(1/n) (ItoFormulaTDRemainder.lean — time/cross/space split bounded by C_tt Δt² + C_tx|ΔB|Δt + C_xxx|ΔB|³), and the time-dependent Riemann↔CLM bridge (ItoIntegralRiemannBridgeTD.lean). Assembly in Foundations/ItoFormulaTD.lean; f_t's joint continuity is derived from its bounded partials (jointly Lipschitz), not assumed; unbounded coefficients stay the named gap, as in 7.1.1. All four new headliners axiom-pinned in the curated audit and the spine node thm:ito-formula-td-l2 added. Net: 235 full + 18 wrappers = 253 / 269 delivery-ready, 16 reduced cores.

Deferred-cleanup round (2026-06-09). Executed the round-5 values-review follow-up catalogue. (1) Corpus faithfulness — sc-thm-8.2.5 (SDE existence/uniqueness) encoded its diffusion as a Lebesgue ∫σ ds, leaving the Brownian driver B dead (a random-IC ODE, not an SDE); fixed to an opaque adapted stochastic-integral process IσX (= ∫₀ᵗ σ dB), mirroring sc-thm-7.5.2's opaque Itô-integral fields. Stays reduced_core, now faithful. (Round-6 correction, 2026-06-09: that rewrite's uniqueness clause quantified a free per-candidate integral IσY, which made the spec uninhabitable — any process discharges the solution premise by taking its own residual as "integral". Repaired with an opaque integral-operator encoding Iσ : (ℝ → Ω → ℝ) → ℝ → Ω → ℝ consumed as Iσ X / Iσ Y, the uniqueness conclusion scoped to 0 ≤ t, a : Prop ascription, and an in-snippet inhabitant example guarding non-vacuity.) (2) Orphan wiring — three documented-but-unwired Foundations bridges became full corpus entries: mf-ftap-multi-state-forward (Phase 42 forward FTAP, EMM ⟹ no-arbitrage in arbitrary finite state + assets), mf-pricing-kernel-butterfly (Phase 53 FTAP state-price butterfly no-arbitrage), mf-variance-swap-equivalence (Phase 45 log-payoff strike = realised-variance QV limit). The literal anti-wrapper re-export varianceSwap_equivalence (subsumed by the genuine two-functional theorem) was removed. StochasticInterval was reflected on and kept — it is the Degenne #440 upstream-PR body, anchored by two AxiomAudit entries and named as the ElementaryPredictableSet gap in the deferred Itô-CLM coherence record. (3) Blueprint — the keystone bsV_satisfies_bs_pde_via_feynmanKac and the kernel heat equation feynmanU_heat_equation are now @[blueprint] spine nodes (with curated AxiomAudit guards); the regenerated spine shows the FK tower linking into the existing bsCall node. Net: 239 full + 18 wrappers = 257 / 273 delivery-ready, 16 reduced cores (corpus 270 → 273). lake build 8708 jobs, axiom-clean; ledger 273/273 fresh; gate tests green.

2026-06-09 — values round 6 (whole-repo, 8-lens panel). Three blockers found and fixed: sc-thm-8.2.5's round-5 rewrite was uninhabitable (free per-candidate IσY; repaired with the opaque integral-operator encoding + conclusion scoped to 0 ≤ t + an in-snippet inhabitant guard — refutation and inhabitant both daemon-checked); Vasicek's claimed-but-absent limit theorem (added for real: vasicekDeterministic_tendsto_mean); RatiosExtended's claimed-but- absent variance expansion (de-claimed). Corpus honesty: mf-compound-poisson-mgf demoted to reduced_core (exp-algebra core only); mf-credit-spread-time-avg-hazard now exports the definitional identity and the substantive FTC recovery; André's reflection principle wired as the new full entry mf-reflection-principle-counting. PricingKernel recomposed so its FTAP lineage and statePricePricing consumption are definitional. Net: corpus 273 → 274, 239 full + 18 wrappers = 257 / 274 delivery-ready, 17 reduced. lake build 8708 jobs green, ledger 274/274 fresh, 19 gate tests green. Full findings ledger: docs/values-review.md.

Feynman–Kac → Black–Scholes-PDE keystone round (2026-06-08). The new full entry sc-bs-pde-feynman-kac (bsV_satisfies_bs_pde_via_feynmanKac) re-derives the Black–Scholes PDE −∂_τV + ½σ²S²∂_SSV + rS∂_SV − rV = 0 from the Feynman–Kac representation — through the heat kernel's joint Fréchet-differentiability (hasFDerivAt_heatKernel) and a parametric differentiate-under-the-integral skeleton, not from Itô — closing the long-standing two-tower gap between the deep heat-kernel/Itô foundations and the pricing layer (the orphaned feynmanU heat flow is now load-bearing for pricing; Foundations/FeynmanKacHeatEquation.lean + BlackScholes/PDEFromFeynmanKac.lean). In the same pass the Feynman–Kac scope note on sc-thm-9.2.1 was de-staled: its "~300–500 lines left as upstream work" claim was false — that infrastructure is now built and consumed by the keystone. Net: 236 full + 18 wrappers = 254 / 270 delivery-ready, 16 reduced cores (corpus 269 → 270).

Duplication + status audit (2026-06-03). A five-reviewer sweep of all 216 then-full entries asked two questions: does any MathFin module re-derive content already in pinned Mathlib / Degenne's BrownianMotion package, and is any full really a wrapper? The foundations tower came back clean — the package at pin fa590b1 has no sorry-free L²-adapted stochastic integral (it stops at the elementary simple-process integral), no strong-type Doob L^p (weak-type only — same as Mathlib, whose own docstring defers the L^p version), no Wald/X²−t martingales, no Itô formula; our Wiener-vs-Itô division and the BrownianMartingale division-of-labor header were re-verified accurate. The Portfolio/Performance/Risk/FixedIncome slice had zero findings (geometric series, Cauchy–Schwarz etc. are consumed from Mathlib, never re-proved). Verified findings, all applied: full→library_wrapper: ce-prop-2.1.11-jensen (Mathlib's ConvexOn.map_condExp_le_of_finiteDimensional proves textbook Jensen from bare convexity; our explicit-subgradient derivation was strictly weaker — Foundations/CondExpJensen.lean deleted, benchmark now wraps Mathlib), mf-carr-madan-log (was a Real.log_div alias; alias lemma deleted), cv-prob-space (measure_univ/measure_empty). full→reduced_core: pp-thm-3.3.5 and mc-thm-1.1.2 (THEOREM-named entries whose conclusion is a projected structure field / definitional rfl; definition entries bm-def-5.1.1/cv-poisson-def/mc-def-1.1.1 keep the documented definitional-full convention). Coherence fix: am_gm_two now specializes Mathlib's Real.geom_mean_le_arith_mean2_weighted instead of re-proving it; documented-distinction cross-references added for the Carr–Madan second-order remainder (the n = 1 case of Mathlib's taylor_integral_remainder, kept in explicit-HasDerivAt form) and the StandardNormal MGF (pdf-form vs Mathlib's measure-form mgf_gaussianReal). New guardrail: test_expected_reduced_cores_stay_reduced_core. Upstream opportunity recorded in docs/bridges.md (our L² martingale convergence could discharge the package's sorry'd SquareIntegrable targets).

Honesty re-audit (2026-05-29). A dedicated benchmark-formalization_status sweep (four adversarial reviewers over all 11 files / 251 theorems, every finding source-verified) reclassified 13 over-credited entries, dropping delivery-ready from 235→222. The pattern was the same one found in the Itô stack: a benchmark named after a deep theorem but proving only an algebraic shadow / a conclusion read off a hypothesis / an unfaithful library wrapper. Reclassified full→reduced_core: mf-tangent-portfolio-foc (FOC by ring, no calculus), mf-american-supermartingale + mf-american-intrinsic-bound (le_max on the Bellman def, not the measure-theoretic supermartingale), mf-kmv-merton-pd (only the ≤1 bound proved), mf-markowitz-n-psd (conclusion-in-hypothesis), mf-newton-raphson-fixed-at-root (definitional unfold), mart-thm-2.3.6 (wraps the bounded-time submartingale inequality, not the UI optional-stopping equality). full→library_wrapper: bm-thm-5.1.5 (one-line Degenne re-export). library_wrapper→reduced_core: the 5 markov_chains entries whose library_wrapper credit rested on a since-removed second backend while the active Lean code is a structural specification (matching how poisson_processes already tiers its structural entries). See docs/deep-review-2026-05-29.md.

Upgrade-properly round (2026-05-29). Rather than only relabel down, two of those entries were earned back to full by re-pointing the benchmark at the genuine derivation that already existed in the library (the benchmark had been wrapping the shallow algebraic lemma instead): mf-tangent-portfolio-foc now wraps sharpeSqTwo_critical_iff_crossProduct_FOC (the Sharpe FOC as a genuine HasDerivAt critical-point characterisation), and mf-kmv-merton-pd now wraps kmvPD_eq_one_sub_survival_probability (KMV PD = the actual risk-neutral default probability 1 − Q(V_T>F), via riskNeutralProb_S_T_gt_K). Both re-pointed snippets were compile-verified. Balancing this, the algebraic shadow mf-kmv-survival-Phi-d2 (the normal-CDF symmetry 1 − Φ(−x) = Φ(x), previously full) was demoted to reduced_core. Net: 222→223 delivery-ready, but now backed by the genuine theorems. The remaining reduced_core entries are either inherently one-line facts (no deeper theorem exists) or gated on machinery not yet in Lean — relabeling those up would re-introduce the overclaim.

Summit A — continuous-time Itô formula (2026-06-02). Promoted sc-thm-7.1.1 (Itô's Formula) reduced_core→full: the bounded-derivative continuous-time L² Itô formula f(B_T)−f(B_0) = itoIntegralCLM_T gf' + ½∫₀ᵀ f″(B_s) ds is now derived from foundational primitives, with the stochastic integral the genuine continuous Itô integral itoIntegralCLM_T gf' (the L²-limit of the Riemann–Itô sums). The proof chain (Summit A): tendsto_weighted_qv (weighted quadratic variation) + tendsto_ito_remainder (vanishing Itô–Taylor remainder) + itoIntegralCLM_T_of_bdd_cont (Riemann↔CLM bridge), assembled in ito_formula_L2_bddDeriv. Scope: f ∈ C³ with bounded f′,f″,f‴ — a faithful but strictly C³-bounded specialization of the C² textbook statement (the gap to unrestricted C² is Summit C localization, not yet formalized). All four Summit-A theorems are #print axioms-clean (AxiomAudit-pinned). coverage_report: stochastic_calculus.json 4→5 full, 7→6 reduced.

Engine→pricing coherence — deliberate stop (2026-06-03). The continuous Itô engine itoIntegralCLM_T has its flagship consumer (itoIntegralCLM_T_brownian: ∫₀ᵀ B dB = ½(B_T²−B₀²−T) through the CLM), and the operational continuous-time pricing result — the discounted GBM is a Q-martingale (discountedGBM_isMartingale, via the Wald exponential) — is already proved (an AxiomAudit-pinned library theorem). The one missing link, identifying the discounted price with the engine (e^{−rt}S_t = S₀ + itoIntegralCLM_T(σ·e^{−r·}S_·)), was scoped and declined: the GBM exponential is unbounded, so it is not a short argument but a second keystone (~400 lines — a parallel clamp-truncation layer plus the martingale-difference L² limit ∑σM_{t_k}ΔB → M_T−1). It would yield an alternative derivation route to a theorem already held, not a new result, so it is recorded here as a known, bounded, not-pursued build. See Geometric Brownian motion / Continuous-time first FTAP in blueprint.md.

Path-1 upgrades (2026-06-04). Seven reduced cores earned full by the upgrade-properly discipline (build the genuinely deeper theorem; never relabel): mart-thm-2.3.6 — the conditional-expectation-form optional sampling inequality for submartingales (Foundations/OptionalSamplingInequality.lean), absent from Mathlib, derived as optional sampling equality + monotone compensator through the Doob decomposition; mf-markowitz-n-psd — PSD derived from genuine L² random returns via the self-dot variance identity, consuming Mathlib's variance_sum' (Portfolio/CovariancePSD.lean); mf-cvar-rockafellar-uryasev — the genuine Rockafellar–Uryasev variational theorem (IsLeast) for the Gaussian loss, minimality by the pointwise tail certificate (RiskMeasures/RockafellarUryasev.lean, which previously recorded only the additive identity and explicitly deferred this); mf-newton-raphson-fixed-at-root — genuine local quadratic convergence at the sharp Newton–Kantorovich constant (L/(2m))·e² (integral form of the Taylor remainder) + basin convergence of the Newton iterates (BlackScholes/NewtonConvergence.lean); mf-kmv-survival-Phi-d2 — re-pointed at the probabilistic survival statement Q(V_T > F) = Φ(DD) through the lognormal tail; mf-american-supermartingale + mf-american-intrinsic-bound — the path-space Snell envelope (Binomial/SnellEnvelope.lean): payoff dominance, supermartingale property, adaptedness, and minimality over arbitrary path-processes, plus the identification theorem snell = e^{−rk}·americanPrice exhibiting the scalar Bellman recursion as the Markov instance (the conditional expectation is the explicit node average, which on a finite tree it is — same pathwise idiom as Binomial/MartingaleRepresentation.lean). All new load-bearing theorems are AxiomAudit-pinned.

Post-audit values sweep (2026-06-04, follow-up). A second adversarial audit (four fresh reviewers over the Path-1 commit) confirmed the load-bearing layer — counts, statuses, scope notes, axiom pins, and the absence of all five headline theorems from Mathlib/BrownianMotion all re-verified independently — and surfaced finishing work, applied in full: submartingale_optional_sampling now consumes Mathlib's Submartingale.monotone_predictablePart (the local helper had re-derived it verbatim) and documents the BrownianMotion package's sorry-stubbed ⊓-form sibling as an upstream-donation candidate; portfolioVarN_covariance_eq_variance consumes variance_sum' instead of re-tracing its bilinearity chain; Newton sharpened to the textbook constant — (L/(2m))·e² via the integral form of the Taylor remainder, basin relaxed to L·δ ≤ m (the uniform mean-value bound had silently cost a factor 2); two dead haves and an orphaned @[simp] lemma removed; the seven upgraded entries' stale description fields rewritten (four still asserted pre-upgrade "NOT the stronger result" disclaimers); and the build log swept clean — six ring-falls-back-to-ring_nf info sites and one simpa lint fixed at root (congr/convert depth bumps so ring sees a genuine ring goal instead of exp A = exp B).

Headline-theorem wiring (2026-06-04, same day). The library's deepest results were benchmark-orphaned — proved on main since 2026-05-30 and AxiomAudit-pinned, but visible in no benchmark entry. Three entries added, each verified L5 in-container before landing: mf-crr-gaussian-limit (crr_tendsto_gaussian_inDistribution — the distributional CLT for the CRR tree: per-step charFun computed exactly, upgraded to weak convergence by Lévy's continuity theorem), mf-crr-bs-call-convergence (binomialPrice_call_tendsto_bs_closed — the n-step binomial call price converges to the literal S₀·Φ(d₁) − K·e^{−rT}·Φ(d₂); bounded-put + put-call-parity route, no uniform-integrability machinery), and gir-continuous-ftap (discountedGBM_isMartingale — the discounted GBM is a martingale under the risk-neutral measure: the EMM property, i.e. the operational continuous-time first FTAP). The stale mf-crr-prob-half scope sentence claiming the distributional convergence "is upstream-gated on triangular-array CLT" (false since 2026-05-30) was corrected to point at the new entries. In the same pass, all 157 stale lean/MathFin/<X>.lean prose path references (the pre-reorg flat layout) were remapped to the real MathFin/<Section>/<X>.lean paths, using each entry's own compiled imports as the authoritative mapping (the old combined files that were split in the reorg — e.g. StrikeConvexityAndRiskAdditivity.lean — map to different targets per entry, which a global rename table would have gotten wrong); the ten entries whose snippet docstrings changed were re-verified in-container.

FTAP tower (2026-06-24 through 2026-06-26, corpus 285→289). Three new FTAP rungs, each full, built in sequence: (1) finite-Ω multi-period FTAP ftap_discrete (mf-ftap-discrete-complete) — Harrison–Pliska for a scalar discounted excess return on a full-support finite probability space and a finite discrete filtration; backward via a global geometric Hahn–Banach separation of the attainable-gains subspace from the standard simplex (the reusable kernel Foundations/ConvexSeparation.lean) and forward via martingale-transform telescoping (Foundations/FTAPDiscrete.lean). (2) General-Ω one-period scalar FTAP ftap_one_period (mf-ftap-one-period-general) — Föllmer–Schied 1.55 for an arbitrary probability space and a single scalar L⁰ excess return; backward via a bounded-density reduction to L¹, the scalar no-arbitrage dichotomy, and a two-region balancing withDensity — no Hahn–Banach, no Kreps–Yan (Foundations/FTAPOnePeriod.lean). (3) D-asset one-period FTAP ftap_one_period_vector (mf-ftap-one-period-vector) — Föllmer–Schied 1.6 for any finite-dimensional inner-product space F; the Esscher/minimal-divergence EMM minimises the convex softplus potential θ ↦ ∫ log(1 + exp⟪θ,Y⟫), which is coercive on Nᗮ (the orthogonal complement of the gains kernel N = {θ : ⟪θ,Y⟫ = 0 a.e.}), so its minimiser on Nᗮ is automatically global; the first-order condition (differentiation under the integral) produces the strictly-positive bounded density; redundant assets are absorbed by N, dropping the earlier non-redundancy assumption (Foundations/FTAPOnePeriodVector.lean). isEquivProbMeasure_withDensity de-duplicated into Foundations/EquivMeasure.lean. Net: corpus 285 → 289, 254 full + 18 = 272/289 delivery-ready, 17 reduced. Open rung: general-Ω multi-period DMW (L⁰-closedness + measurable selection).

Itô pathwise regularity arc (2026-06-25 through 2026-06-26, corpus 289→292). Three full entries complete the pathwise-regularity layer. (1) Continuous modification on [0,T] (sc-ito-general-continuous-modification, exists_continuous_modification_itoProcess, Foundations/ItoIntegralProcessContinuousModification.lean, corpus 290): the general-integrand Itô process t ↦ (φ●B)_t admits an a.s.-continuous representative agreeing a.e. with the L² value at each t ≤ T. Route: Degenne's continuous-time Doob maximal inequality → Chebyshev on simple-process maxima → Borel–Cantelli on a fast subsequence (geometric 2⁻ⁿ bounds) → pathwise uniform convergence on the subsequence → continuous limit process itoContinuousMod. The running-max keystone binds the pathwise norm under the supremum over [0,T]. (2) Continuous local martingale on [0,T] (sc-ito-general-local-martingale, exists_continuous_localMartingale_modification, Foundations/ItoIntegralProcessLocalMartingaleGeneral.lean, corpus 291): the continuous modification is upgraded to a genuine IsLocalMartingale on the null-augmented Brownian filtration 𝓕ᴮ ⊔ 𝓝. The measure-theoretic core is condExp_sup_nulls (conditioning on the null augmentation agrees a.e. with conditioning on 𝓕ᴮ, its σ-algebra crux consuming Mathlib's eventuallyMeasurableSpace); the null-augmentation setup shows every (𝓕 ⊔ 𝓝)-measurable set is a.e. a 𝓕-set. Non-redundant with Degenne's (sorry-backed) general càdlàg modification. (3) Continuous local martingale on [0,∞) (sc-ito-infinite-local-martingale, exists_continuous_localMartingale_modification_infinite, Foundations/ItoIntegralProcessLocalMartingaleInfinite.lean, corpus 292): the per-horizon [0,T=n] continuous local martingales are glued into one path continuous on all of ℝ≥0. Horizon consistency (itoProcessL2Inf_eq_itoProcessCLM, resting on a hand-built [0,T] clamp of Degenne's SimpleProcess and the band-restriction CLM restrictToBand) makes each finite-horizon local martingale a modification of the same unbounded-horizon process; indistinguishable_of_modification_on agrees them on overlaps. With no horizon clamp, the martingale property is the global itoProcessL2Inf_isMartingale delivered through condExp_sup_nulls. All three entries are axioms-clean and values-panel PASS. Net: corpus 289 → 292, 257 full + 18 = 275/292 delivery-ready, 17 reduced, 0 placeholders.

Itô → pricing bridge: the deterministic-integrand Wiener integral is Gaussian, and the Vasicek terminal law derived (2026-06-27, corpus 292→294). The deep Itô tower (complete through the [0,∞) continuous local martingale) gained its first deterministic-integrand pricing consumer. sc-wiener-integral-gaussian (wienerIntegralLp_map_eq_gaussianReal, Foundations/WienerIntegralGaussian.lean): a deterministic-integrand Wiener integral is gaussianReal 0 ‖f‖² — the distribution the isometry construction left open — by the characteristic-function route (simple-process Gaussianity via IsGaussianProcess.of_isGaussianProcess + map_eq_gaussianReal, lifted to all L² by a |t|-Lipschitz-charFun DenseRange.induction_on + Measure.ext_of_charFun). Its consumer mf-vasicek-sde-terminal-gaussian (vasicekShortRate_hasLaw_gaussian, FixedIncome/VasicekSDEGaussian.lean) derives the Vasicek terminal law r_T ~ N(vasicekSDEMean, σ²(1−e^{−2κT})/(2κ)) that VasicekSDE.lean previously only posited — variance via the FTC integral ∫₀ᵀ e^{−2κ(T−s)} ds, affine transport via gaussianReal_const_mul/gaussianReal_const_add. First Itô-tower consumer in FixedIncome. Both axioms-clean. Net: corpus 292 → 294, 259 full + 18 = 277/294 delivery-ready, 17 reduced, 0 placeholders.

The line below is the pre-re-audit historical record (kept for provenance): 235 / 251 delivery-ready (211 full + 24 library wrappers), 16 reduced cores, 0 placeholders.

History

Per-pass session logs and the pre-2026-05 hybrid-backend validation records were removed from this file on 2026-05-30, when the SymPy and Isabelle backends were stripped (the project is Lean-only). They remain in git history. The 2026-05-29 honesty re-audit — the basis for the current counts above — is also recorded in docs/deep-review-2026-05-29.md.

Navigation Menu

Uh oh!

Formalization Status

Status Vocabulary

Current Audit

History

Uh oh!

FilesExpand file tree

coverage.md

Latest commit

History

coverage.md

File metadata and controls

Formalization Status

Status Vocabulary

Current Audit

History