# Values review — the upgrade engine (not a pass/fail gate)

The mechanical gates (`tests/test_values.py`, `AxiomAudit*.lean`, the
verification ledger, the CI gates in `build.yml`) enforce everything a
machine can check. This protocol covers what a machine cannot: the eight
judgment lenses that define the repo's quality bar. Its output is **not a
pass/fail stamp** — a green "8/8 PASS" checkmark is exactly how a library
quietly settles into being a *fine* dump. The lenses are read as
**gradients**: for each, where is the work strongest (the exemplar to
propagate) and what is the next concrete **upgrade** that raises its ceiling?
Each review produces a ranked backlog of value-aligned upgrades and the
upgrades executed that session — and the session's job is to *do the top
ones*. The **pipeline enforces the cadence** (not a quality threshold):
`tests/test_values.py::test_values_review_is_current` fails when the corpus
has grown more than 12 entries past the last recorded review. A regex cannot
check "beautiful"; it can check "nobody refreshed the backlog."

## The eight lenses

1. **Inspired math quality** — each result earns its place: a structural
   fact or a clean mechanism, not bookkeeping dressed as a theorem.
2. **Mathlib / BrownianMotion (Degenne) coherence** — consume the libraries'
   machinery, never re-derive it; choose the canonical upstream API; no thin
   wrappers around single upstream lemmas.
3. **Zero slop** — no opaque discharges where a certificate-shaped proof
   exists, no ring-fallback hiding the conceptual step, no duplicated
   sub-derivations, no dead hypotheses.
4. **Architectural ingenuity** — the decomposition is the right shape: each
   lemma carries one idea, the pieces compose so future results get cheaper,
   nothing is proved at the wrong level of generality.
5. **First principles** — conclusions are derived from honest hypotheses;
   no hypothesis secretly contains the conclusion; no theorem that is its
   own definition unfolded.
6. **Mathlib / BrownianMotion idiomatic register** — naming, hypothesis
   style, namespace and `variable` discipline, statement shapes a Mathlib
   reviewer would accept.
7. **Concept clarity** — every docstring tells the honest mathematical
   story (what is proved, from what, what is *not* claimed); a strong
   probabilist reads the statement and says "yes, that is the theorem."
8. **Beautiful, elegant math** — the proof is the obviously-right argument
   once seen; the writeup neither obscures a beautiful idea nor dresses up
   a trivial one.

## Protocol

- **When**: at the close of any session that adds or changes proof content;
  at latest every 12 corpus entries (the CI ratchet's slack — one session's
  growth).
- **How**: at least three independent review agents, the lenses split among
  them, reading the work and its context (read-only; never running Lean) —
  then **adjudicated by the maintainer** against the settled doctrine (the
  wrapper taxonomy, the two-tower direction) and `grep`-confirmed usage,
  because panel agents lacking that context systematically over-escalate
  (calling a consumed rewrite-handle "slop") or under-escalate (all-green
  sycophancy). For each lens, name the current **exemplar** (the bar to
  propagate) and the next **upgrade** (the gradient). Genuine slop uncovered
  is fixed in-session; larger upgrades become ranked backlog items with
  owners (usually a future session's opening move).
- **The standing first pass — read the prose against its own statement.**
  Before the lenses, for everything the session touched: does the docstring,
  the corpus `description`, or the doc paragraph claim more than the Lean
  says? This is not a hypothetical failure. On 2026-08-07 five corpus
  entries described the stochastic term as `∫₀ᵀ f_x(s,B_s) dB_s` while
  stating only `∃ gfx`; the README's landmark table rendered
  `ito_formula_unrestricted` as an integral identity when the theorem proves
  only that a residual is a continuous local martingale; and four more
  descriptions claimed a textbook theorem (`L^p` convergence, existence *and*
  uniqueness, general `σ(s)`, uniqueness of a bounded classical PDE solution)
  where the entry delivered a narrower result. Nobody wrote a false claim on
  purpose — the prose described the theorem everyone had in mind and the
  statement quietly said less.
  The mechanical half is now `test_values.py::test_prose_does_not_outrun_statement`
  (an `∃`-statement whose witness is never pinned down while the prose writes
  the integral that would pin it down). The judgment half stays here, and it
  is the larger half: `description` is published in the HF dataset and
  documented as "natural-language mathematical statement", so it is an
  outward-facing claim, not a private note. Where an entry's `description`
  states the **textbook target** rather than the delivered result — 36 entries
  do — the delivered scope must be explicit in the same field, not left to
  `formalization_scope`.
- **Record**: append a review block below, headed
  `## YYYY-MM-DD — corpus <N> — <one-line title>` (the freshness test parses
  the date and the `corpus <N>` count anywhere in the heading; a
  `commit <sha>` provenance segment is optional — older entries carry it,
  working-tree entries omit it). Record (i) the **upgrades executed** this
  session, (ii) the refreshed **ranked backlog** of value-aligned upgrades,
  and (iii) the evidence/context (mechanical floor, panel findings confirmed
  or dissolved). This is a record of **direction, not a grade** — there is no
  PASS line to award; the failure mode the model guards against is a review
  that finds nothing to improve.

## Review log

Entries from 2026-06-29 (corpus 302, the whole-repo review below) onward use the **upgrade-driven model**
(per-lens exemplar → next upgrade; upgrades executed + ranked backlog). Earlier entries are historical
PASS / PASS-WITH-NOTES verdicts, kept as-is — the transition itself was an upgrade to lens 4 (the review
should *generate work*, not certify "OK").

## 2026-08-07 — corpus 351 — martingale representation on the Brownian filtration, and continuous-time completeness

Scope: the nine-task program behind `Foundations/{BrownianCylinderGeneration, ItoIntegralLocality,
DoleansStepRepresentation, WienerExponentialTotality, MartingaleRepresentation, MarketCompleteness}`,
its cleanup pass, and the corpus work that landed with it. Corpus 348 → **351** (320 `full`,
18 `library_wrapper`, 13 `reduced_core`, 0 placeholder); `gir-thm-9.3.4` moved `reduced_core → full`.

Protocol deviation, named as the last round named its own: this was not a three-agent panel at the
close. It was eleven scoped review passes, one or two per task, plus this closing read of the shipped
modules against the program record. Every pass was independent and adversarial — several overturned an
implementer's claim, one overturned the controller's own strategy — but each saw a single task. Nobody
read the program whole until now, which is why the recurring cross-task pattern below took nine tasks to
become visible. Re-run the panel at the next proof session.

Per-lens **exemplar → next upgrade**:

- **1 Inspired math.** *Exemplar:* the re-framing that made the theorem cheap. Issue #49 had filed
  representation as a consequence of the adapted-integrand Itô formula. It is not one. Surjectivity of
  an isometry onto a closed subspace is a *totality* statement about its range, and the whole proof is
  an orthogonal decomposition — no Itô formula for `f(∫θ dB)`, no pathwise quadratic variation. Second
  exemplar, one floor down: `itoIntegralCLM_T_restrictAfterCLM`, "restricting an integrand to `(u,T]`
  removes exactly the past of its integral," which is what turns the *terminal* identity an Itô formula
  hands out into an identity for an inner increment. That single lemma is what lets a Doléans
  exponential over a partition be assembled at all. *Upgrade (HIGH):* the theorem proves `φ` exists and
  is unique and never says what it is. Two routes were named here, #182 (Clark–Ocone) and #183 (the
  localized Itô formula's integrand). **#183 landed 2026-08-07** and reaches the capability for claims
  the Itô formula already covers — `discountedGBM_eq_itoIntegral` now states `gfx =ᵐ [σ·Ŝ(·)]`, a
  stated delta. It does *not* touch the representation's `φ` for a general `L²` claim, which is what
  #182 is for; the upgrade stays HIGH on that half.
- **2 Coherence.** *Exemplar:* `Measure.ext_of_charFunDual` consumed as Cramér–Wold in one step, and
  `condExpL2` used through the Hilbert API because it is *definitionally*
  `Submodule.orthogonalProjectionOnto` — neither argument is re-derived in finance clothing.
  *The finding, and it is the headline:* three separate general lemmas landed in application files and
  each had to be moved. `itoIntegralCLM_T_simpleAssembly_T` existed in **three** copies; the locality
  facts sat in `DoleansStepRepresentation` when `ItoIntegralLocality` exists to hold them;
  `itoProcessCLM_zero_time` and `integral_itoIntegralCLM_T` sat in `MartingaleRepresentation` when
  `ItoIntegralProcessGeneral` is their floor. Three in one program is a rate. *Upgrade (HIGH):* ask the
  placement question at **dispatch**, not at review — a task brief that names the destination file for
  each general fact it expects to produce. #185 clears the residue (`mulBddCLM` vs the older hand-rolled
  `truncCLM`, `inner_eq_integral_mul` inlined at seven sites, an MGF-to-Gaussian-law block written three
  times in `ExpMartingaleQBrownian`).
- **3 Zero slop.** *Exemplar:* four specified statements turned out false or underivable and every one
  was reported rather than forced through. `coeFn_smulAdapted` as drafted was false (`(t,ω) ↦ Z ω` is
  not predictable for merely `𝓕_a`-measurable `Z`; the repair multiplies by `𝟙_{a<t}·Z`, which is a
  generating predictable rectangle and a bonus total CLM). Two statements in `WienerExponentialTotality`
  were missing `IsPreBrownianReal B μ` and were false without it, with a counterexample sharp enough to
  distinguish the *right* one (`B ≡ Z`, time-constant but random) from a wrong one that fails for the
  wrong reason (`B ≡ 0` collapses `𝓕_T` to `⊥`). And `constDoleans_sub_one_eq_itoIntegral` was reported
  first as "unprovable" and corrected to "not derivable from the exported API" — the weaker, true claim.
  Then the strengthening: `hF1` was a hypothesis `eq_zero_of_orthogonal_stepDoleans` did not need, and it
  was **dropped from the public signature**, not underscored. A second instance,
  `stepDoleans_sub_one_mem_range`'s `(_hs0 : s 0 = 0)`, was underscored to clear a `lake lint` error and
  logged as #184 — the underscore being the tell that it silences the linter and leaves the theorem
  weaker than what was proved. The final whole-branch review ruled it fix-now rather than issue-later,
  on the grounds that it was a *new* declaration, so the branch would have introduced the very defect
  this review ranks HIGH. Dropped in `6530fae`; the hypothesis was inert (`stepDoleansExp … 0` is the
  empty product, and the worker `stepDoleans_aux` never took it).
- **4 Architectural ingenuity.** *Exemplar:* the crown is stated as **surjectivity of an isometry the
  library already had**, not as a bespoke theorem. `itoIsometryCentered` corestricts `itoIntegralCLM_T`
  to `centeredBrownianL2 := lpMeas 𝓕ᴮ_T ⊓ (ℝ ∙ 1)ᗮ`, `itoIsometryCentered_surjective` closes it, and
  `itoIsometryEquiv` is one `LinearIsometryEquiv.ofSurjective` call. So `itoIntegralCLM_T` gains a
  structure theorem and the library gains no parallel construction. The codomain's *definition* is the
  mathematical content. *Upgrade (MED):* `mulBddCLM` was extracted mid-proof as the general operator
  (bounded multiplication on `L²`, arbitrary measure) and instantiated twice in the same file, which is
  the right instinct — but it sits **above** the special case it should absorb. The extraction and the
  DAG placement are the same question, asked once (see lens 2).
- **5 First principles.** *Exemplar:* `PricesGainsAtZero` is hypothesised and then *guarded*.
  `pricesGainsAtZero_self` proves `μ` satisfies it, so nothing downstream is vacuous;
  `pricesGainsAtZero_of_gains_martingale` derives it from the textbook condition. The header states
  plainly which step of the textbook second-FTAP proof is hypothesised (EMM ⟹ gains are a fair game,
  which needs `∫ φ dS`) and which is proved. Elsewhere the same discipline: `𝔼[∫₀ᵀ φ dB] = 0` is proved
  one floor down rather than assumed, and `M 0` being a.e. constant is the representation read at
  `t = 0` rather than a hypothesis. And the corpus flip is the anti-smuggle — `gir-thm-9.3.4` was a
  `Prop`-structure whose conclusion was a bundled field read off by projection, and it is now the real
  theorem. *Upgrade (MED):* the two guards are never **composed**. Guard 1 is proved directly, so the
  file never exhibits guard 2's hypothesis triple as inhabited. Routing `pricesGainsAtZero_self` through
  the guard makes it load-bearing, and wants the general-integrand Itô process bundled as a `Martingale`
  — an object worth having on its own. #186.
- **6 Idiomatic register.** *Exemplar:* `omit [IsProbabilityMeasure μ]` applied exactly where the callee
  does not need it, verified against the callees rather than cargo-culted; and the `have`-binder rule
  becoming *binding in the plan* after it recurred, instead of being re-raised per task. *Upgrade
  (MED):* the two `lake lint` failures on underscored `def` names landed in consecutive rounds because
  the first fix swept the reported instance and not the class. The class is real and discoverable
  without CI: every other `_T` def in this tower (`itoIsometry_T`, `trimMeasure_T`, `itoIntegralCLM_T`,
  `simpleAssembly_T`, `itoAssembly_T`, `timeMeasure_T`) lives in a sub-namespace, and
  `MartingaleRepresentation` declares only `namespace MathFin`. Either sub-namespace it or record the
  rule where an author reads it before pushing.
- **7 Concept clarity.** *Exemplar:* the docstrings record the **amendments in the artifact**, not only
  in session reports. `WienerExponentialTotality`'s "why the hypotheses are what they are" carries the
  counterexample that forced `hB`, and says why the obvious counterexample fails.
  `ItoIntegralLocality`'s header opens with "the definitional wrinkle it has to survive" and states the
  falsity that was discovered mid-task. `MarketCompleteness` says which `IsEMM` fields the corollary
  consumes (`isProb`, `ac`) and that `martingale` rides along unused so the statement stays in the
  vocabulary a reader looks it up under. A reader learns the mathematics *and* what it cost.
  *The counterweight, and it is not small:* the `## Result` section that `CONTRIBUTING.md:103` requires
  was missing from four of the six new modules. Root cause is worth stating flatly — implementers were
  pointed at an exemplar file that also omits it. The exemplar beat the written rule four times before
  anyone checked the rule, and when the cleanup pass went to fix it, the *destination* file for the
  lemma moves (`ItoIntegralProcessGeneral`) had none either. The drift is older than this program.
  *Upgrade (HIGH, cheap):* make it mechanical. `tests/test_router.py` already enforces
  `@[expose] public section` on every `module`-header file; a `## Result` presence check is the same
  gate and would have caught five files.
- **8 Beautiful math.** *Exemplar:* the sentence the whole theorem reduces to. `z ⊥ range`, so
  `∫ z·D = ∫ z·(D−1) + ∫ z = 0` for every step Doléans `D`: the first term dies because `D−1` is in the
  range, the second by centering, and totality kills `z`. Alongside it, the observation that the
  totality theorem needs no centering hypothesis at all, because the family already contains the
  constant `1` (take `h ≡ 0` over one cell, where every factor is `exp 0`). *Upgrade (MED):* the
  argument's shape is only tested in one dimension. Step B of the totality proof is already stated over
  an arbitrary `Fintype ι` and pushes into `ℝ^ι`, so it generalizes to a vector driver for free; the
  Doléans rung does not, because of the cross terms. #180 is where we find out whether the decomposition
  was the right shape or the convenient one.

**Upgrades executed this session (the program).**

1. **Three general-lemma relocations** (lens 2/4): the three-way `itoIntegralCLM_T_simpleAssembly_T`
   dedup to one definition site; the locality facts into `ItoIntegralLocality`; `itoProcessCLM_zero_time`
   (now public `@[simp]`) and `integral_itoIntegralCLM_T` into `ItoIntegralProcessGeneral`.
2. **A spurious hypothesis removed from a public signature** (lens 3/5): `hF1` gone from
   `eq_zero_of_orthogonal_stepDoleans`, which is strictly stronger than what was specified.
3. **The crown stated as a structure theorem** on an existing isometry, plus the bundled
   `itoIsometryEquiv` (lens 4).
4. **`mulBddCLM`** extracted as the general bounded-multiplication operator over an arbitrary measure
   (lens 2/4); **dead API deleted** (`itoIntegralCLM_T_smulAdapted_mem_range`, zero consumers after the
   route changed) (lens 3).
5. **`PricesGainsAtZero` guarded rather than asserted**, with the hypothesis-minimal
   `measure_eq_of_pricesGainsAtZero` as the public form and `emm_unique_of_complete` as its corollary
   (lens 5).
6. **`## Result` sections** added to five files, including the pre-existing gap in
   `ItoIntegralProcessGeneral` (lens 7); `inner_eq_integral_mul` hoisted public.
7. **`gir-thm-9.3.4` `reduced_core → full`** — a `Prop`-structure projection replaced by the theorem
   (lens 5).
8. **`patterns.md`** gained the 2026-08-06 batch in-flight, not batched at the end, and `roadmap.md`
   gained the localized-Itô-integrand gap as a standing known gap (lens 7).

**Refreshed ranked backlog.**

1. **[HIGH] Ask the placement question at dispatch.** Three general lemmas in the wrong file in one
   program, and the sharpest data point is self-directed: the third copy of
   `itoIntegralCLM_T_simpleAssembly_T` was found because **this file had already recorded it** as a LOW
   item on 2026-07-10 (`docs/values-review.md:433`) and nobody acted on it for four weeks. The review
   model's stated failure mode is a review that finds nothing to improve. The subtler one is a review
   that finds it, ranks it, writes it down, and then does not do it. Concrete form: task briefs name the
   destination file for each anticipated general fact, and LOW backlog items get an issue number instead
   of a bullet. #185 clears the current residue.
2. **[HIGH] The underscore is a signal, not a fix.** *(#184, executed before merge in `6530fae` — the
   final whole-branch review ruled it fix-now, since `stepDoleans_sub_one_mem_range` is a new
   declaration and shipping it would have introduced the defect this item names.)* Dropping
   `(_hs0 : s 0 = 0)` was the second instance of the class in six weeks (the first was
   the 2026-07-31 spurious division guards, `docs/patterns.md:1031`), and both times a public signature
   shipped a theorem weaker than the one proved, past every gate. The 2026-07-31 necessity prober only
   runs on foundry drafts. Hand-authored `MathFin/` has no equivalent, and a `_`-prefixed binder in a
   **public** signature is a cheap, precise trigger for one.
3. **[HIGH, cheap] A `## Result` presence gate** in `tests/test_router.py`, beside the
   `@[expose] public section` check. Five files were caught by hand this session; the written rule lost
   to an exemplar four times in a row, which is what a written rule does when nothing checks it.
4. **[MED] Compose the `PricesGainsAtZero` guards** (#186), which needs the general-integrand Itô
   process as a bundled `Martingale`. The bundle is the object every "the gains process is a martingale"
   statement wants to be stated on, so the cost is not sunk in this one file.
5. **[MED] Name the integrand.** ~~#183 (the localized Itô formula's four-theorem chain)~~ **executed
   2026-08-07** — the whole chain down to `discountedGBM_eq_itoIntegral` now states
   `gfx =ᵐ [σ·Ŝ(·)]`, so the diffusion coefficient of the discounted price is sayable. This panel's
   qualification is what settled it: `roadmap.md` had deferred #183 for want of a consumer, and the
   note here was that the absence of a consumer was partly an artifact of Task 3 *rearranging itself
   to avoid needing it*. It was. Two things the deferral had not priced in: the naming conjunct
   already existed one rung down (`ito_formula_td_L2_bddDeriv_explicit`) behind a forgetful wrapper,
   and five corpus entries were already *describing* the named integrand in prose while stating only
   `∃ gfx` — so this was a fidelity repair, not only a capability. **Still open: #182** (`L¹`/`H¹`
   plus Clark–Ocone), which is what names the *representation's* `φ` for a general claim; #183 names
   the Itô *formula's* integrand, a different and weaker thing.
6. **[MED] The vector driver** (#180), gated on the two-process Itô formula (#48). Half the argument
   already generalizes; the Doléans rung is where the cross terms bite.
7. **[MED] The second-FTAP converse** (#181), and behind it the missing `∫ φ dS` that would let `IsEMM`
   supply `PricesGainsAtZero` outright instead of hypothesising it.
8. *(Carried from prior panels, unchanged:)* the discrete general-Ω multi-period **DMW crown**; the
   general **2D covariation Itô** tower (#48); **Girsanov L²/Novikov**; and hoisting the private
   std-normal Gaussian MGF to a shared home, now sharpened by #185's third item, which is the same fact
   written three times in `ExpMartingaleQBrownian`.

**Evidence / context.** Mechanical floor green: `lake build MathFin` + `lake lint` clean with no
`#guard_msgs` failures, `ledger status` 351/351 fresh, 42/42 python gates, `AxiomAuditGen` 304 → **308**
guards, five curated axiom pins whose messages were *observed* against the daemon rather than guessed,
four `@[blueprint]` nodes. The honesty rule the reviews extracted is now enforced in prose:
`emm_unique_of_complete` is **not** the unconditional second FTAP — `IsEMM` contributes `isProb` and
`ac`, and the fair-game step is a hypothesis. The wording that passes is "uniqueness of the pricing
measure on the Brownian filtration, for measures that price the traded gains at zero." Issue #49 was
closed against the landed commits and split; #179 carries `sc-thm-9.1.1` alone, with what it actually
needs.

**A note on the shape of this round.** Two failures in this program had the same structure, and the pair
is more instructive than either. A `sorry`-typecheck verified that a signature *elaborates* and was read
as verifying that it says what was meant, which is how two theorems shipped without the hypothesis that
makes them true. An isolation probe verified that `obtain ⟨ψ,hψ⟩ := hy` *elaborates* and was read as
licensing the edit, which is how a cosmetic pass broke the build on hypothesis lifetime — both the
implementer and its reviewer read `id hy` as noise. Both are a green check answering a different
question than the one asked, and in each case the check was real, cheap, and honestly run. `patterns.md`
now records the pair. The generalizable form: when a probe comes back green, say out loud which property
it established, and compare that sentence to the property at risk.

## 2026-07-31 — corpus 348 — open-PR review round: the spurious-guard class

Scope: the eight open PRs, not a new proof program. Deviation from protocol worth naming — this
round was adjudicated by a single reviewer rather than a three-agent panel, so treat the per-lens
gradients below as one reading, and re-run the panel at the next proof session.

**Upgrades executed.**

1. **Lens 3 (zero slop) + lens 5 (first principles) — the headline.** All four autoform PRs for
   #161/#162 shipped a **division guard the theorem does not need**: `0 < ∑ r⁻` on gain-to-pain
   nonnegativity, `∑ b ≠ 0` on upside-capture homogeneity. In Lean `x / 0 = 0`, so `div_nonneg`
   over two nonneg sums and `mul_div_assoc` both discharge unconditionally. Neither issue asked
   for the guard — the drafter added it. Both dropped; the merged statements are strictly
   stronger than what was drafted. This is the *dead-hypothesis* failure mode, and it is the one
   the kernel cannot see: a weaker theorem type-checks exactly as happily as a strong one.
2. **Lens 2 (coherence).** `gainToPain` restated on Mathlib's `posPart`/`negPart` (`r⁺`, `r⁻`)
   instead of open-coded `max _ 0`. That is not cosmetic: it is what makes
   `posPart_sub_negPart` available, and hence `one_le_gainToPain_iff`.
3. **Lens 1 (inspired math).** `0 ≤ gainToPain` is bookkeeping — it says a quotient of
   nonnegatives is nonnegative and nothing about finance. `one_le_gainToPain_iff` (the ratio
   clears 1 exactly when `0 ≤ ∑ r`) is the statement that makes the definition worth having, and
   it is where a positivity hypothesis is genuinely load-bearing. Added alongside.
4. **Lens 4 (architecture).** Four PRs created four new one-lemma modules
   (`GainToPain`, `PerformanceRatios`, `UpCapture`, `PerformanceRatiosExtended`) when both issues
   named `Performance/RatiosExtended.lean`, beside the four ratios they belong with. Consolidated
   into one change in that module; four duplicate PRs closed.
5. **Lens 4 again, on the two stale outside PRs (#36, #38).** Both had sat six weeks with
   review feedback unaddressed and had gone stale against the pin bump; finished in-session
   rather than closed. Two placement/derivation calls beyond the original submissions: *speed*
   moved out of `BlackScholes/PDE.lean` into `HigherGreeks.lean` beside vanna/volga/charm, since
   gamma is literally the quotient `ϕ(d₁)/(S σ √τ)` and speed is one quotient rule off it; and
   *caplet-floorlet parity* is now `swaption_payer_receiver_parity` **applied**, not the same
   `Phi`-symmetry argument run twice — `blackCaplet_eq_blackPayerSwaption` says why (the caplet
   is the payer swaption with the accrual factor in the annuity slot). The submitted `rfl`-backed
   price entries were dropped rather than allowlisted, keeping `DEFINITIONAL_RFL_ALLOWLIST`
   empty. Note the pin interaction: the original proof used `HasDerivAt.mul`, which no longer
   elaborates against the goal's instances on Mathlib 81a5d257 — `HasDerivAt.div` with a pinned
   expected type does, and is the conceptually right rule anyway.
6. **Lens 6 (idiomatic register).** `upCapture_scale_invariant` renamed `upCapture_smul`: the
   claim is degree-one homogeneity, and `_scale_invariant` is already taken in this namespace by
   Sortino/Treynor/IR, which genuinely *are* invariant (`f (c • x) = f x`). Scalar leg stated as
   `c • p`. Also removed: unused `open MeasureTheory ProbabilityTheory` / `open scoped NNReal
   ENNReal BigOperators` in every draft, and an `@[simp]` attached to an `example` (a no-op).

**Ranked backlog — all four executed the same day (2026-07-31).** Recorded as a
backlog first, then built; kept here in the original order with what shipped.

1. **A necessity prober in the foundry gate chain.** ✅ `probe/strengthen.py`, wired
   into `vibe_prove._cmd_gate` (`NECESSITY=0` disables). **The first writing of this
   item was wrong and the correction is the interesting part.** It said "delete each
   binder and re-elaborate; anything that still compiles was decorative" — but that
   pass already existed (`autoformalize.strengthen_candidate`, keyed on
   unused-variable warnings), and neither it nor a deletion probe catches the observed
   cases, because both drafts genuinely *use* the guard (`have hden := h.le`;
   `field_simp [h]`). No warning fires, and deleting the binder just breaks the proof.
   The distinction that matters is **used by this proof** vs **needed by this
   theorem**, and only re-proving without it can tell them apart. What shipped: a free
   elaboration filter (a binder the signature depends on never reaches the prover),
   then a fixed tactic sweep on what survives — daemon-only and zero tokens, because
   the gate phase holds the Lean slot while the vibe harness is down — accepted only
   on a full re-gate. Open limit, stated: a fixed sweep will miss hypotheses whose
   removal needs a real proof.
2. **`AxiomAuditGen` misses bundle-shaped proof terms.** ✅ #171. The extractor now
   walks each declaration's proof body, bounded by the next declaration so the
   proof-position scope holds. 284 → **304** guards; the two FRA names moved out of
   the curated headliner file into the generated one. The other 18 were constants
   already load-bearing in proof position that had simply never been pinned —
   `bs_pde_holds`, `hasDerivAt_bsV_SS`, `newtonSeq_tendsto_root` among them, which is
   the more sobering half of the finding.
3. **`formalization.yaml`'s disclosure pinned to a retired pipeline.** ✅ #171, and
   *not* by renaming. The drafter and model list are read off the corpus's own
   per-entry provenance, so the sentence cannot outlive the pipeline it describes.
   Output today is unchanged — all four autoform entries really were magistral-drafted
   and keep that attribution — while an entry recorded drafter-agnostically no longer
   inherits it. What the disclosure should say once a Claude-drafted entry lands is
   still R's call; the generator just stops asserting what the corpus does not record.

   > **Correction (2026-08-04).** "All four autoform entries really were
   > magistral-drafted" was wrong, and wrong when written. Magistral left the drafter on
   > **2026-07-27** (foundry `17ac296`); `mf-performance-gain_to_pain` and
   > `mf-performance-upside_capture` landed **2026-07-31**, so they cannot have been
   > drafted by it. They carried `magistral-autoform` only because provenance was
   > stamped at ENQUEUE rather than by the stage that ran — the exact defect
   > `assemble.py::sanitize_provenance` was built to stop, added too late for entries
   > already merged. The review checked that the generator derived its claim from the
   > corpus, and did not check whether the corpus itself was true. Both markers are now
   > scrubbed to `autoform`; #66/#85 (2026-07-18, genuinely Magistral-era) keep theirs.
   > The generator also over-generalized: it named one drafter beside the TOTAL count,
   > crediting Magistral with all four. It now tallies per drafter, with a regression
   > test (`test_the_disclosure_does_not_generalize_one_drafter_to_every_entry`).
4. **`patterns.md`: fold in the guard rule.** ✅ 891aec8, beside the existing
   sign-check and natural-generality rules, plus two repair-table rows earned the same
   day (a `convert` on `HasDerivAt` left an instance-equality goal after the v4.32.0
   pin moved `HasDerivAt.mul` under a June-era proof; and the `√τ`-cancellation move).

**Also shipped in the foundry the same day** (`docs/upgrade-backlog.md` R–V, 465 tests
green): placement now honours the issue's `location:` line — `assemble.splice_into_module`
merges declarations into an existing module, which is what makes honouring it safe,
since the old failure was a whole-file write deleting the module's theorems; a
ground-truth duplicate backstop that asks GitHub rather than trusting a mutable state
file; a provenance sanitizer at the corpus boundary plus four migrated queue entries;
and emit hygiene (post-gate `trim_unused_opens`, inert attributes on `example`,
implicit type binders).

**Evidence / context.** Mechanical floor green throughout: full `lake build` 8981 jobs on the
integrated tree, `ledger status` 348/348 fresh (every new entry re-verified through the daemon at
the v4.32.0 pin, plus the siblings the edited modules restaled), 31/31 python gates,
`AxiomAuditGen` byte-fresh at 304 guards. Note the pin interaction that would otherwise have
pushed main red: every one of the eight open PRs was built against the pre-#168 toolchain, so all
of them carried stale entry hashes.

**A note on the shape of this round.** Three of the four backlog items were found by *reading the
pipeline's shipped artifacts back against the issues that seeded them* — not by reviewing new
proof content. The corpus grew by 7 entries; the durable output was four gates and a corrected
belief about which one was missing. Worth repeating when the merge queue next backs up.

## 2026-07-16 — corpus 335 — multi-asset matrix Riccati (BEGV Prop 2) via spectral reduction

`Foundations/MatrixMarketMakingRiccati` (M1 abstract matrix Riccati `a' = a·a − ·Â` solved in closed
form for any Hermitian `Â`; M2 market-making instantiation `A' = 2·A·D₊·A − (γ/2)·cov`), + 2 `full`
entries `mf-mm-matrix-{riccati,value}` (corpus 333 → **335**). **Mechanical floor green:** `lake build
MathFin` + `lake lint` (8869 jobs), ledger fresh at 335, both bench-checks green, `AxiomAudit` +
`AxiomAuditGen` axioms-clean (`[propext, Classical.choice, Quot.sound]`), `test_router`/`values`/`ledger`
pass. Reviewed by an opus code-review (mergeable) **and** a 3-agent read-only values panel (8 lenses
split), maintainer-adjudicated below.

Per-lens **exemplar → next upgrade** (gradient, not a grade):

- **1 Inspired math.** *Exemplar:* `hasDerivAt_matrixRiccatiCoeff` on `matrixRiccatiCoeff_spectral_sq`
  — the spectral-reduction idea (define the solution already-diagonalised `U·diag(riccatiCoeff λᵢ)·Uᴴ`,
  so the matrix ODE collapses to n scalar ODEs already proven) sidesteps BOTH missing pieces at the pin
  (matrix `tanh` and `Matrix.exp` differentiation) with one move. *Upgrade (MED):* the `T→∞` matrix
  ergodic limit `matrixRiccatiCoeff h T 0 → Â` (per-eigenvalue `tanh→1`), gated on the absent
  `tanh`-at-`atTop` limit.
- **2 Coherence.** *Exemplar:* `matrixRiccatiCoeff_spectral_sq` uses Mathlib's own spectral-computation
  idiom verbatim (`rw [hÂ.spectral_theorem, ← map_mul, diagonal_mul_diagonal, conjStarAlgAut_apply]`);
  panel grep-confirmed all seven upstream APIs canonical against the checkout, and the scalar
  `riccatiCoeff` is the one source of the `tanh` derivative, consumed matrix-side. *Upgrade (MED):*
  extract a `conj_diagonal_mul` private helper — the conjugated-diagonal-square collapse is derived
  twice (`_spectral_sq` for `²`, inline `hsq` for `a·a`).
- **3 Zero slop.** *Exemplar:* the ODE derivative-equality discharged by one certificate-shaped `rw`
  chain (`rw [hsq, matrixRiccatiCoeff_spectral_sq hÂ, ← hU, ← sub_mul, ← mul_sub, ← diagonal_sub]`) — the
  conceptual step (both sides are `U·diag(…)·Uᴴ`) is *visible*. Forbidden-tactic grep: none. No dead
  hypotheses — `cov` is deliberately **not** assumed symmetric/PSD (the algebra doesn't need it), so the
  theorem is the honestly-general conditional.
- **4 Architectural ingenuity.** *Exemplar:* M2's derivative is literally
  `(((hasDerivAt_matrixRiccatiCoeff …).const_mul Dm).mul_const Dm).const_smul (1/2)` — M1 does all the
  calculus, M2 pays only change-of-variables algebra; combined with cross-module reuse of the single-asset
  scalar `riccatiCoeff` as the diagonal core. *Upgrade (MED → HIGH once a 2nd matrix consumer lands):*
  the global `attribute [instance] Matrix.linftyOp…` (the L∞ norm commitment) is declared in a leaf
  finance module — correct today (grep confirms MathFin has no other matrix-analytic usage, so no
  diamond) but at the wrong altitude; hoist it + `matrixRiccatiCoeff_spectral_sq` into a shared
  `Foundations/Matrix…` prelude so the finance leaf *imports* the commitment.
- **5 First principles.** *Adjudicated headline — the "Â by hypothesis" charge is HONEST, not a smuggle.*
  M2's `hÂsq : · = γ•(S·cov·S)` is `t`-free constant-matrix algebra; the conclusion is a `HasDerivAt`
  in `t` — the hypothesis cannot be the conclusion unfolded. It defers only matrix-sqrt *existence* (a
  separable fact); the theorem proves "for any witnessing `Â`, the change of variables solves the
  Riccati," consistent with the accepted single-asset `valueFunction_satisfies_approxHJ` (A/B/C by
  hypothesis, `full`). The anti-smuggle: `matrixRiccatiCoeff_spectral_sq` **derives** `²=U·diagλ²·Uᴴ`
  from `spectral_theorem` rather than positing it. *Exemplar:* that lemma. *Upgrade (HIGH):* prove the
  PSD matrix-sqrt existence `∃ Â, Â.IsHermitian ∧ · = γ•(S·cov·S)` for `cov` PSD — turns " assumed"
  into "Â constructed," retiring the sole deferred algebraic caveat (needs Mathlib Hermitian/PSD CFC).
- **6 Idiomatic register.** *Exemplar:* `set … with` discipline — every `with` is consumed by a later
  `rw` (`hU`/`hS`/`hDm`), and the one that shouldn't have it (`set a := …`, line 211) had it **removed
  this session**. *Upgrade (LOW, repo-wide):* the `=>`→`↦` sweep — a standing convention item, not to be
  fragmented file-by-file.
- **7 Concept clarity.** *Exemplar:* the module Scope block's `Â`-clause (a probabilist sees exactly
  which object is assumed and that it is the paper's own construction). *Upgrade (LOW):* tighten
  `roadmap.md` "formalizes BEGV Prop 2" → "the matrix-Riccati **core** of BEGV Prop 2" (Prop 2 also
  carries `B`/`C` + the verification).
- **8 Beautiful math.** *Exemplar:* `matrixRiccatiCoeff_spectral_sq`'s three-rewrite `← map_mul`
  collapse — two conjugated diagonals become one conjugated product-of-diagonals, the "why the reduction
  works" certificate in one line. *Upgrade (MED–HIGH):* make `conjStarAlgAut U (diagonal (riccatiCoeff∘λ))`
  the **primary** definition (terminal ⇒ `map_zero`, `a·a` ⇒ one-step `map_mul`, ODE ⇒ push the
  continuous `⋆`-alg-hom through `d/dt`) — the elegant unification the module is 90% toward.

**Upgrades executed this session:** (i) dropped the unused `set … with ha` (lens 6, from the code
review); (ii) added norm-independence + prose-`tanh` clarity clauses to the §1 docstring — `L∞` is
MathFin's instance choice, not a mathematical restriction (finite-dim ⇒ norms equivalent ⇒
norm-independent), and no matrix `tanh` object is built in Lean (lens 7, Panel C); (iii) distilled the
reusable technique batch into `docs/patterns.md` (spectral reduction, operator-norm matrix `HasDerivAt`,
`diagonalLinearMap` lift, positive-diagonal collapses, ℕ-vs-ℝ smul trap) in-flight (lens 2/7). **Panel
suggestion DISSOLVED on adjudication:** the proposed `simpa only [Function.comp_def] using …` fold of the
`hD` lift (lens 6 checklist) breaks the build — the goal needs `exact` to bridge the operator-norm
`AddCommGroup` (only *defeq* to the default `Matrix.addCommGroup`), which `simpa`'s syntactic
post-simp match cannot; reverted, with an in-code comment recording why (the panel lacked the
instance-defeq context — the exact over-escalation the protocol's adjudication step guards against).

**Refreshed ranked backlog (top)** — *re-ranked on maintainer reflection; the earlier draft over-weighted
within-the-Riccati refinements. Governing decision (see the roadmap "Direction" note): these two entries are
a finished **flag-plant** (first matrix-analytic finance), NOT a market-making build-out. The Riccati is the
LQ-**approximation** view; the fundamental structure is the exact Hopf–Cole/GLFT linearisation. So:*

- **Stop the Riccati drill.** The items that only deepen the *approximation* — `B`/`C` coefficients, PSD
  matrix-sqrt existence ("Â constructed" not "Â assumed"), the `T→∞` matrix ergodic limit — are **deprioritised**
  (do not pick these up as opening moves; they grow a satellite island, not the spine).
- **The honest deep target *if* we return to market making** is the **exact linearisation** (the Hopf–Cole
  reduction of the Avellaneda–Stoikov HJB to a linear ODE system / matrix exponential — the structural gem the
  Riccati approximates), a real project gated on matrix-exponential calculus (absent at the pin) — *not* more
  Riccati refinement.
- **Cheap in-module hygiene, only if the file is touched again** (not worth a dedicated pass): extract
  `conj_diagonal_mul` (DRY the conjugated-square collapse, derived twice); add `mmMatrixValueCoeff_isHermitian`
  consuming the orphaned `matrixRiccatiCoeff_isHermitian`; and — the one architectural item worth doing before a
  *second* matrix consumer lands — hoist the L∞ norm-policy instance + `matrixRiccatiCoeff_spectral_sq` into a
  shared matrix prelude so the finance leaf imports the norm commitment instead of declaring it.
- **The real leverage is the depth spine** (Itô → Girsanov → FTAP), where results compound: the discrete
  general-Ω multi-period **DMW FTAP** crown, the general **2D covariation Itô** tower, and **Girsanov L²/Novikov**.
  *(Carried:)* Appendix-A jump (Brémaud–Jacod) point-process Girsanov — a candidate only because it wires into
  the existing change-of-measure engine; and hoisting the private std-normal Gaussian-MGF to a shared home.

## 2026-07-12 — corpus 330 — continuous first-FTAP frame (meaning 1), DS-shaped for meaning 2

The model-agnostic continuous-market EMM frame (`Foundations/ContinuousMarket` + the `Q = P`
Black–Scholes instance in `ContinuousFTAP`): six commits, all axiom-clean (`AxiomAudit` +
`AxiomAuditGen` green), ledger fresh at 330, `lake build` green. Reviewed per-task (opus on the crux
forward theorem); this is the close-of-session gradient read, not a PASS stamp.

- **Coherence (lens 2/4) — the session's spine.** The forward theorem and the discrete
  `emm_implies_no_arbitrage` genuinely SHARE the closing primitive `ae_zero_of_nonneg_of_integral_zero`
  (nonneg + `∫=0` ⟹ null), each supplying its own zero-integral. The first cut extracted a
  *martingale-shaped* core the continuous side never used — caught in-session, re-split to the honestly
  shared shape. The proof CONSUMES Mathlib's bilinear `condExp` pull-out
  (`condExp_bilin_of_stronglyMeasurable_left` + `innerSL ℝ`) rather than reproving it (the general-`F`
  pull-out, not a scalar fallback).
- **Architectural ingenuity (lens 4).** `IsEMM` is stated *on a process* — exactly the object DS
  produces — so meaning 2 is an additive extension (new strategy class + theorem), not a rewrite; the
  frontier is a docstring'd marker, not vaporware. Sub-namespaced `MathFin.ContinuousMarket` per the
  `OnePeriod`/`OnePeriodVector` variant pattern (a name collision the build gate caught, the isolated
  daemon missed).
- **First principles / honesty (lens 5/7) — the headline.** The BS instance uses `Q = P` because the
  physical-measure Girsanov EMM `Q ≠ P` is *intrinsically bounded-horizon* (`Q = withDensity Z_T` is a
  martingale measure only on `[0,T]`); rather than freeze a process or fake a full-horizon claim, the
  scope is stated plainly in the theorem docstring, the benchmark scope text, and the plan, and the
  horizon-aware EMM is tracked as explicit backlog. The orphaned `martingale_comp_monotone` (unused by
  the direct proof) had its docstring corrected from "the bridge" to an honest standalone-lemma framing
  (user decision: keep + benchmark).
- **Concept clarity (lens 7).** `docs/patterns.md` was elevated to a first-class citizen (user
  directive): the session's reusable pointers — the bilinear pull-out, `Martingale`-is-a-bare-`And`
  accessors, the shared-vanishing-primitive lesson — were distilled in-flight, folded into the proof
  commit, not deferred.

**Upgrades executed this session:** lifted the genuinely-shared no-arbitrage primitive (lens 2/4);
delivered the general forward continuous FTAP via the direct term-by-term route (lens 5/8); made
`patterns.md` a standing first-class artifact (lens 7).

**Refreshed backlog (top):** (1) **horizon-aware EMM** (`IsEMM`-on-`[0,T]` or a stopped price) so the
Girsanov change-of-measure EMM `Q ≠ P` becomes a first-class instance — the natural meaning-1.5 next
step; (2) the **discrete general-Ω multi-period DMW crown** (the nearer FTAP summit, one rung below
DS); (3) **meaning 2** proper: NFLVR, general admissible strategies / `∫φ dS`, the closedness-of-K
(Kreps–Yan) converse; (4) still open from prior panels — the general **2D covariation Itô** tower and
hoisting the private std-normal Gaussian-MGF to a shared home.

## 2026-07-11 — corpus 324 — finance-breadth sprint (Asian / barrier / quanto / compound-Poisson)

A four-deliverable finance-breadth sprint, all axiom-clean (`AxiomAuditGen` green), ledger fresh,
`lake build` green (8864 jobs). `mathematical_finance` is now **224/225 full**. The unifying values
angle was **coherence (lens 2/4): each deliverable cashes in a foundational asset that was previously
built but under-consumed**, rather than adding standalone bookkeeping:

- **(A) n-date geometric-Asian** (`BlackScholes/AsianGeometricN`): generalizes the two-date driver law
  to arbitrary `n` via the same Wiener step-kernel + Brownian-covariance route, then reduces the
  geometric average to *one effective BS driver* (`bsTerminal Ŝ₀ r σ_G T`) and prices it through
  `bs_call_formula` — the Margrabe move. Makes `wienerIntegralLp_stepIndicator` (WG.3, built 2026-07-08)
  load-bearing for a real exotic price, not just the two-date law.
- **(B) binomial barrier/lookback** (`Binomial/BarrierReflection`): consumes the **stranded**
  `reflectionPrincipleEquiv_below` (PathReflection's own docstring flagged "the `Fintype.card` identity is
  … not separately stated here") — the exact "stranded generic" theme the 2026-07-10 panel named. Ships
  the counting identity **and** the substantive running-maximum law `#{max ≥ a} = 2·#{end>a} + #{end=a}`.
- **(C) Girsanov-grounded quanto** (`BlackScholes/QuantoGrounding`): upgrades `mf-quanto-correction-factor`
  from a *definitional* identity (the `−ρσ_Sσ_FX` drift baked into `quantoForward`) to a **derivation** —
  the cross-term emerges from an FX Esscher tilt + independent-normal decomposition + the Gaussian MGF.
  First-principles lens (5): the correction is now *earned* from the correlation.
- **(D) compound-Poisson MGF** (`Actuarial/CompoundPoissonMGF`): flips `mf-compound-poisson-mgf`
  `reduced_core → full`, replacing the algebraic shell `e^{−λ}e^{λM}=e^{λ(M−1)}` with the real
  composition — the n-claim iid-sum MGF (`iIndepFun.mgf_sum`) integrated against the Poisson pgf.

**Honesty note (lens 5/7):** the fourth intended item, the fully general **2D Itô formula**
(`sc-thm-7.5.2`), stays `reduced_core`. Its continuous-time covariation form (`∫ ∂_xy f d⟨X,Y⟩`) is a
summit-scale tower, not a breadth item — recorded as a depth-track item, not forced or faked.

**Refreshed backlog (top):** (1) the general **2D covariation Itô** tower (unlocks `sc-thm-7.5.2` +
multi-asset basket/spread rigorously); (2) hoist the private `integral_exp_mul_stdNormal` (std-normal MGF)
to a shared Gaussian-MGF home — it is re-derived across QuantoGrounding / Vasicek / Asian; (3) the
arithmetic-Asian price (needs a lognormal-sum approximation, genuinely harder than geometric); (4) carry
the barrier maximal-distribution to an actual knock-in/knock-out *option price* summed over a payoff.

## 2026-07-11 — corpus 319 — executed backlog #1: adapted Girsanov grid→generic wiring

The top HIGH item from the 2026-07-10 panel, done. `GirsanovAdaptedTheta`'s uniform-partition density
moment lemmas (`sq_integral_Zn_le`, `memLp_Zn_two`, `quad_integral_Zn_le`, `integrable_Zn_four`,
`measurable_Zn`) now instantiate the partition-generic `SimpleDoleansMoments` tower directly (`Zⁿ` *is*
`simpleDoleansExp` at `s = unifPart T n`; the grid's `unifPart T n n = T` supplies the generic's
`T ≤ s N` coverage; `n = 0` is the constant-`1` density). The literal `sq_mul_le_half_add_pow4`
duplicate and the now-orphaned `driftSqSum_le` / grid `simpleDoleansExp_scaled_eq` are deleted.
**Net −102 lines**, one file, crown untouched (name-preserving re-exports), axiom-clean, ledger fresh
(the 2 crown entries re-verified).

**Two refinements of the panel's plan, found in execution.** (1) The ~180-line estimate was optimistic:
the `Dn`/`fn` drift-exponential and mixed-product lemmas are KEPT, not routed — their grid proofs bound
the drift for *all* `n` via `simpleDriftUnif_abs_le`, strictly more general than the generics'
`hNT : T ≤ s N` coverage requirement, so routing them would *regress* (an `n = 0` special case for no
gain). (2) No `simpleStochSum = riemannσ` / `simpleQuadVar = driftSqSum` bridges were needed — the moment
lemmas route directly. Remaining top backlog: the generic Riemann-bridge core, the Taylor-remainder
hoist, the marshalled-prologue dedup, and the pricing/portfolio items.

## 2026-07-10 — corpus 319 — whole-repo style sweep + 8-lens values panel (243 files)

**Scope**: a full-repo pass, not a single-theorem review. Two tracks. (1) A **mechanical/idiomatic
house-style sweep** across all 243 `MathFin/*.lean` files: `fun … =>` → `fun … ↦` (4318 arrows, 180
files); 28 unused `set … with h` handles dropped; 7 `have h := e; simp only […] at h; exact h` folded
to `simpa`; 45 gratuitous `classical` removed (each individually confirmed to still elaborate without
it; 7 load-bearing kept). The ~104 `exact_mod_cast` and ~50 explicit `↑` were reviewed and
**deliberately kept** — genuine numeric casts and ℝ→ℂ coercions the elaborator needs, load-bearing not
slop. (2) A **whole-corpus 8-lens values panel**: four independent read-only review agents (Itô/
martingale tower · Girsanov/FTAP/SDE/processes · pricing · portfolio/risk/actuarial + cross-cutting
naming/docstrings), maintainer-adjudicated against grep-confirmed usage and a green `lake build`. The
panels were rigorous — each shipped an over-escalation-filtered section (false positives explicitly
cleared: `crr_drift_limit_h` is a benchmark handle; the Greeks/PDE "duplication" is false;
`GaussianGirsanov` is a distinct Esscher lane; no `full` benchmark is `rfl`-backed) — and **converged**
across agents on the same top coherence debt.

**The dominant, repo-wide finding** (four agents, independently): *generic Mathlib-shaped lemmas
duplicated or stranded in specialised files.* The exemplar of the fix is
`Foundations/UnifIntegrableL2.lean` — it names the exact Mathlib gap it fills, states fully generic
theorems, gives certificate-shaped proofs, and is consumed by all three Girsanov files. It is the home
every "trapped-generic" lemma below wants.

**Upgrades executed this session:**
- **(lens 2/4) Hoisted `memLp_two_of_subseq_ae_of_sq_bound` to `UnifIntegrableL2`** beside its pair
  `tendsto_setIntegral_of_subseq_ae_of_sq_bound`, and retrofitted the continuous `memLp_ZT_two` from a
  hand-rolled ~44-line `lintegral`/`liminf` Fatou argument to a 6-line application. (Backlog #2, closed.)
- **(lens 2/3) Deduped `tendstoInMeasure_congr_left`** — byte-identical in `SimpleProcessPartition` and
  `GirsanovAdaptedTheta` — into a single generic `UnifIntegrableL2` theorem consumed by all four sites.
- **(lens 7) Honest `PathReflection` docstring** — softened the "headline cardinality theorem" overclaim
  to state what the file delivers (the bijection + IVT direction), naming the `Fintype.card` identity as
  the unstated corollary.
- Plus the mechanical/idiomatic sweep above (arrows · set-handles · simpa-folds · classical).

**Refreshed ranked backlog** (fresh whole-repo panel; owners = future opening moves):

*Foundations coherence (highest ROI — the dominant theme):*
1. **[HIGH] Wire `GirsanovAdaptedTheta`'s grid lemmas through `SimpleDoleansMoments`.** 1:1 generic
   superset confirmed (incl. the literal `sq_mul_le_half_add_pow4` duplicate); needs 2 bridges
   (`simpleStochSum (unifPart)=riemannσ`, `simpleQuadVar=driftSqSum`) + an `n=0` special-case +
   **name-preserving re-exports** so the crown `Btheta_isQBrownianMotion_adapted` stays untouched.
   ~180–200 net lines removed. Risk LOW via re-exports (MED-HIGH if done naively). The dedicated
   next-session item; supersedes old backlog #1.
2. **[MED-HIGH] Lift one generic Riemann-bridge core.** `ItoIntegralRiemannBridge{,Adapted,TD}` re-roll
   structurally identical `memLp_riemann*`/`itoSimple_step*`/`itoIntegralCLM_T_step*` for φ(B)/θ/φ(t,B);
   one generic adapted-bounded-multiplier core, three instantiations. Feeds the Itô summits + adapted crown.
3. **[MED] Hoist the 3 pure-analysis Taylor lemmas** (`abs_sub_le_of_hasDerivAt`, `abs_taylor1_le`,
   `abs_discreteTaylorRemainder_le`) to a generic mean-value module; the order-2 remainder re-inlines the
   order-1 ladder byte-identically — build it *on* order-1.
4. **[MED] Dedup the marshalled-convergence prologue** (`tendstoInMeasure_marshalDrift` vs `_marshalQuadVar`,
   ~22 identical lines incl. `hD0`) into a private `slice_energy_facts` helper. (Old backlog #3.)
5. **[LOW] Small dedups/relocations:** `isCadlag_of_continuous` (triplicated private), `memLp_increment_two`
   (dup), the `itoIntegralCLM_T_simpleAssembly_T` name-clash, and trapped-generics
   `continuous_uncurry_of_bdd_partials` / `continuous_timeMeasure_primitive` / `Lp_real_two_norm_sq` →
   generic homes.

*Pricing:*
6. **[MED] CRR one-step identity `p·u+(1−p)·d=eʳ` proved 5×** → route the 3 inline `field_simp;ring` bodies
   + 1 alias through the canonical `crrUpProb_mul_up_add` (`Binomial/Model.lean`).
7. **[MED] ZCB and constant-hazard Credit** (`exp(-(r·(T-t)))`, byte-identical) → route `zcb_pos` /
   `survival_pos` through the `ExponentialDiscount` principle they claim to instance; share a constant-rate core.
8. **[MED] Greeks:** promote `hasDerivAt_bsd1_sigma_clean` public + add `hasDerivAt_exp_neg_mul` in `PDE.lean`,
   retiring ~13 re-inlined `d/dx exp(−x·c)` micro-derivations; complete `PathReflection` by stating the
   `Fintype.card` corollary.
9. **[LOW] `exp(−r)·exp(r)=1`** re-derived ~14× across the Binomial cluster → one shared helper; SnellEnvelope
   minimality proved twice (verify the corollary is shorter first); trim `Call.lean`'s un-machine-checked
   numeric-audit docstring.

*Portfolio / Risk / Actuarial:*
10. **[MED-HIGH] Portfolio quadratic-form primitives.** `marginalVariance`/`portfolioVariance`/`portfolioReturn`
    are defined in the application-named `CAPMEquilibrium.lean` yet consumed as generics, and `portfolioVarN`
    is the same form with swapped args — extract to `Portfolio/Primitives.lean`, standardise the `(s,kernel,w)`
    order, and have `CAPMEquilibrium` import them.
11. **[MED] Risk-parity two-tower gap.** `RiskParityFOC`'s docstring promises a bridge no lemma delivers; add
    `riskParityWeightTwo_isRiskParity` mirroring the proven `tangentTwo_isTangentPortfolioN`.
12. **[LOW] Relocate Lundberg/compound-Poisson** out of `Actuarial/Mortality.lean` into `Insurance`/`RuinTheory`
    (and into that file's `## Results` block); fix the `isLundbergAdjustmentCoefficient` casing; standardise the
    covariance-kernel name (`Sg`); drop `let`-in-statement (`RiskParity`, `TangentPortfolio`).

**Evidence/context**: whole-repo `lake build MathFin` green covering the sweep + the executed upgrades;
`exact_mod_cast`/`↑` reviewed-and-kept (not churned); over-escalations filtered per-agent. Cross-cutting
naming/docstring verdict: **excellent** — `Is*` predicates, `hasDerivAt_*`, honest `Scope`/`What is not in
this file` blocks, no overclaims; the one structural blemish is the Portfolio-primitive layer (#10).

## 2026-07-10 — corpus 319 — bounded-PREDICTABLE-θ Girsanov: `B^θ` is a `Q`-Brownian motion (Rung 1)

**Scope**: the whole new `Foundations/GirsanovPredictableTheta.lean` (the bounded-predictable-θ assembly,
`Btheta_isQBrownianMotion_predictable_of_bdd`, corpus `gir-thm-9.1.8-predictable` **full**, 318→319 /
285→286 full), plus the two generic moment bounds added to `GirsanovSimpleDoleansMoments.lean`
(`sq_integral_simpleDoleans_le`, `memLp_simpleDoleans_two`) and `driftContinuousMod_stronglyAdapted`
in `DriftProcessPredictable.lean`. Reviewed by **two independent panel agents** (slop/idiom/coherence;
architecture/clarity/first-principles/inspired/elegance), read-only, then maintainer-adjudicated against
`grep`-confirmed usage and the green `lake build` (8860 jobs) + axiom-clean audit + fresh ledger. The
panels were **not sycophantic** and **converged** on the same top slop (the strongest signal it is real):
both independently confirmed a **byte-identical ~25-line prologue** duplicated between
`tendstoInMeasure_marshalDrift` and `tendstoInMeasure_marshalQuadVar`. Over-escalation was filtered:
`clampM_marshalMult_abs_le` (a consumed 10× rewrite-handle) and the `memLp_simpleDoleans_two` inline
domination (a necessary verbose mirror; both `MemLp` and `∫≤M` are genuinely independent engine inputs)
were checked and cleared, not flagged.

**Upgrades executed this session** (during authoring, before the panel):
- **(lens 4/2) one generic Fatou-`L²` principle, consumed twice.** `memLp_two_of_subseq_ae_of_sq_bound`
  (uniform 2nd moment + one a.e.-subsequence ⟹ limit ∈ `L²`) is proved once and instantiated for *both*
  the Doléans density (`memLp_ZTpred_two`) and the mixed-time product (`memLp_gpred_one`) — the limit-side
  argument the continuous file (`memLp_ZT_two`) still hand-rolls once, factored here into a reusable lemma.
- **(lens 2) the partition-generic back half feeds two consumers.** The `SimpleDoleansMoments` uniform
  L⁴/L² bounds serve *both* the set-integral engine's `M` (`sq_integral_mixedProduct_le`) and the Fatou
  limits (`sq_integral_simpleDoleans_le`) — one abstract `(s,c)` back half, no grid-vs-marshalled fork.
- **(lens 3) dead code removed pre-merge.** `sq_integral_driftExp_le` was written for a `memLp_contD_two`
  route later dissolved by Fatou-on-the-product; deleted before merge rather than left as an orphan.
- **(lens 5/7) faithful benchmark statement.** The public `Btheta_isQBrownianMotion_predictable_of_bdd`
  obtains its `L²` approximating sequence internally (`exists_approxSeq`), so the corpus entry's hypotheses
  are the honest ones (bounded predictable θ), with no approximating-sequence artefact leaking into the
  statement.

**Refreshed ranked backlog** (owners = a future session's opening move; the top two are the highest-ROI
coherence upgrades and pair naturally):
1. **[HIGH, coherence] Wire the adapted case through `SimpleDoleansMoments`.** `GirsanovAdaptedTheta.lean`
   still hand-rolls `simpleDoleansExp_{neg,scaled}_eq` / `sq_mul_le_half_add_pow4` (a *literal* duplicate of
   `GirsanovSimpleDoleansMoments.lean:286`) / `driftSqSum_le` / `sq_integral_Zn_le` / `quad_integral_Zn_le`
   / `memLp_Zn_two` / `integrable_{Zn,Dn}_four` — the grid-specialisation the generic tower now subsumes.
   Add `simpleStochSum = riemannσ` / `simpleQuadVar = driftSqSum` bridges and delete ~10 grid lemmas; the
   `SimpleDoleansMoments` sub-namespace name-clash is the visible symptom, and it dissolves with the merge.
2. **[HIGH, coherence] Hoist `memLp_two_of_subseq_ae_of_sq_bound` to `UnifIntegralL2.lean`** (beside its
   pair `tendsto_setIntegral_of_subseq_ae_of_sq_bound`). It sits in the *downstream* predictable file, so
   the continuous `memLp_ZT_two` — the identical `lintegral`/`liminf` argument — *cannot* consume it (file
   order). Move it upstream, retrofit both `memLp_ZT_two` and `memLp_ZTpred_two`, delete ~40 duplicated lines.
3. **[MED, slop] Dedup the marshalled-convergence prologue.** `tendstoInMeasure_marshalDrift` vs
   `_marshalQuadVar` share a byte-identical `θhat`/`W`/`D`/`hDnn`/`hDint`/`hD0`/`hg_prod`/`hg_slice` block.
   Extract a private `slice_energy_facts (W) (g)` returning `(hDnn, hDint, hg_slice)` (generic in the step
   sequence and the `Lp` integrand); `hD0` stays per-caller (marshalled-specific). ~25 lines removed.
4. **[MED, architecture] Internalise `V`/`hV`.** The approximating sequence threads through 9 internal
   declarations and leaks into `Btheta_isQBrownianMotion_predictable`, yet the conclusions are
   `V`-independent and `driftContinuousMod` already canonicalises via `(approxSeq …).choose`. Mark the
   `V`-taking versions `private` (or thread `(exists_approxSeq …).choose` internally) and expose only the
   `_of_bdd` form. The `(μ := μ)` pinning itself is correct (`BthetaPred` genuinely depends on μ via the
   trim-space representative) — keep it.
5. **[LOW, coherence] `continuous_clampM`.** `stronglyMeasurable_clampM_marshalMult` re-derives
   `Continuous (clampM C)` via `unfold clampM; fun_prop`; add `continuous_clampM` next to `measurable_clampM`
   (`ItoIntegralBrownian.lean:73`) and consume it. Also drop the dead `set … with h` names
   (`hr`/`hθhat`/`hW` in the two convergence lemmas).
6. **[LOW, clarity] μ-independent benchmark corollary.** Optionally restate the headline on the honest
   `B_u + ∫₀ᵘθ ds` (via the `driftContinuousMod_eq_setIntegral` a.e.-bridge) so the corpus statement does
   not carry the trim-space representative. Defensible reuse today; the docstrings are already honest.

**Evidence/context**: mechanical floor green (`lake build` 8860 jobs, `AxiomAuditGen` pins
`Btheta_isQBrownianMotion_predictable_of_bdd` at the three standard axioms, ledger fresh, router+ledger
tests pass). The two HIGH items are the same coherence debt from the other direction (generic-vs-grid
duplication + a limit-side lemma stranded downstream) and are best done together as the next session's
opening move on the continuous file.

## 2026-07-09 — corpus 318 — continuous bounded-adapted-θ Girsanov: `B^θ` is a `Q`-Brownian motion (Track-α closes)

**Scope**: `Foundations/GirsanovAdaptedTheta.lean` (the α4 assembly, `Btheta_isQBrownianMotion_adapted`)
and the α5 flip of `gir-thm-9.1.8` `reduced_core → full` (corpus 318 unchanged — an entry flipped, not
added: 284→285 full, 16→15 reduced). Reviewed by **two independent panel agents** (slop/idiom/coherence;
architecture/clarity/first-principles), read-only, then maintainer-adjudicated against `grep`-confirmed
usage and the green `lake build`. The panel was **not sycophantic** — both enumerated the clean dimensions
explicitly, and their findings **converged** on the same structural slop (the strongest signal that it is
real). Over-escalation was filtered: the two nlinarith clusters were checked individually (three are
genuinely linear, three genuinely nonlinear), and the biggest refactor was scoped to the backlog rather
than rushed before merge.

**Upgrades executed this session:**
- **(lens 2/3) `memLp_ZT_one` deleted a full Fatou proof.** It re-proved `Z_T ∈ L¹` by the same
  `lintegral`-`liminf` argument as `memLp_ZT_two` (`Z_T ∈ L²`). On the probability measure `μ`, `L² ⊆ L¹`:
  moved `memLp_ZT_two` above it and replaced the ~35-line body with
  `(memLp_ZT_two …).mono_exponent (by norm_num)` — the canonical upstream `MemLp.mono_exponent` (the repo's
  own `Bachelier.lean` idiom), consumed instead of a hand-rolled second Fatou.
- **(lens 3/8) linarith for the three linear density discharges.** The `Zⁿ`-side `p`-moment bounds
  (`sq_integral_Zn_le`, `memLp_Zn_two`, `quad_integral_Zn_le`, `integrable_Zn_four`) reduce — after the
  stochastic exponent `riemannσ` cancels — to a linear multiple of `driftSqSum ≤ C²T`; switched
  `nlinarith [driftSqSum_le …] → linarith`. This makes "which step is nonlinear" self-documenting: the
  `Dⁿ`-side bounds keep `nlinarith` because they genuinely form the product `a²·u ≥ 0`.
- **(lens 3/4) shared per-path Doléans convergence.** `tendsto_fn_ae_subseq` re-inlined the exact
  `exp ∘ (−riemannσ − ½·driftSqSum)` reconstruction already in `tendsto_Zn_ae_subseq`. Extracted
  `tendsto_simpleDoleansExp_of_tendsto_riemannσ` (one per-`ω` lemma); both consumers apply it.
- **(lens 4/7) the curated `AxiomAudit.lean` now tells the whole arc.** Added a Track-α section pinning the
  reusable abstraction `isQBrownianMotion_of_expMartingale` plus all three regimes
  (`Btheta_isQBrownianMotion` const → `Btheta_simple_isQBrownianMotion` simple →
  `Btheta_isQBrownianMotion_adapted` continuous), with the const→simple→continuous narrative — the storied
  headliner file now records the marquee arc, not just the generated exhaustive audit.

**Per-lens read (exemplar → next upgrade):**
1. **Inspired math** — exemplar: the **spine-free** route — pass the *simple* exponential-martingale
   identity to the limit rather than build a continuous Doléans stochastic exponential and prove it a
   martingale (the Novikov crux the tower cannot yet reach). Upgrade: the fully-general L²/progressive-θ
   under Novikov (`sc-thm-9.1.8`).
2. **Mathlib/Degenne coherence** — exemplar: consuming `isQBrownianMotion_of_expMartingale` (charFun chain
   ONCE), `MemLp.mul`, `tendsto_of_subseq_tendsto`, and now `MemLp.mono_exponent`. Upgrade: two Mathlib-shaped
   lemmas (`tendstoInMeasure_congr_left`, `sq_mul_le_half_add_pow4`) are parked in the Girsanov file and want
   their honest homes (`UnifIntegrableL2` / a general-inequalities spot; check Mathlib first).
3. **Zero slop** — exemplar: the three deduplications executed above. Outstanding: the simple-Doléans
   `p`th-moment bound is written ~4× in this file (and a 5th time in `GirsanovSimpleTheta`) — backlog #1.
4. **Architectural ingenuity** — exemplar: the a.e.-subsequence engine keeps exp/product composition at the
   a.e. level (where `Continuous.comp`/`·` are free), sidestepping the `TendstoInMeasure` algebra Mathlib
   lacks. Upgrade: hoist the `p`-moment Novikov brick and the `contDrift` basics to shared modules so future
   Girsanov/SDE/Feynman–Kac work consumes rather than rebuilds them (backlog #1, #2).
5. **First principles** — exemplar: the `reduced_core` structure spec is *replaced* by a real derivation
   from bounded-adapted-continuous hypotheses; no hypothesis contains the conclusion. Nothing outstanding
   beyond the Novikov generalization.
6. **Idiomatic register** — exemplar: `contDoleansExp`/`contDrift`/`BthetaCont` mirror the simple-θ
   `simpleDoleansExp`/`simpleDrift`; `riemannσ`/`driftSqSum` lowercase (no capital Σ); `variable`/`omit`
   discipline. No upgrade outstanding.
7. **Concept clarity** — exemplar: docstrings state the spine-free strategy and name what is *not* used (no
   adapted-integrand Itô formula, no Novikov); both panel agents found zero overclaims. No upgrade outstanding.
8. **Beautiful math** — exemplar: reading the martingale field as a mixed-time product and passing it through
   the engine, with the AM–GM `2D²Z² ≤ D⁴+Z⁴` (`sq_mul_le_half_add_pow4`) as the clean route-A combiner — no
   `rpow`/Cauchy–Schwarz square roots. Nothing outstanding.

**Ranked backlog:**
1. **The `p`th-moment Novikov brick.** State once in `SimpleDoleansExponential.lean`:
   `∫ (E^{−c})^p ≤ Real.exp ((p²−p)/2·K²·T)` (+ a `MemLp … p` corollary), off `simpleDoleansExp_scaled_eq`.
   Collapses `sq_integral_Zn_le`/`quad_integral_Zn_le`/`memLp_Zn_two`/`integrable_Zn_four` here and the `hZT2`
   block in `GirsanovSimpleTheta.integrable_expBthetaSimple_mul_density` to one-liners — the reusable moment
   bound any future Novikov regime needs. Medium-large. *(Owner: next Girsanov/Novikov session's opening move.)*
2. **Relocate the `contDrift` API.** `contDrift` + `contDrift_zero`/`_abs_le`/`stronglyMeasurable_contDrift`
   are process-agnostic facts about `∫₀ᵘθ ds`; move to `DriftRiemannConvergence` (or a `ContinuousDrift`
   module) so SDE existence/uniqueness and Feynman–Kac get a ready bounded-adapted-drift API.
3. **Hoist the withDensity transport + generic lemmas.** `setIntegral_withDensity_ofReal` (the AEMeasurable
   variant) belongs beside its measurable twin in `ChangeOfMeasure.lean`, consumed by both engines;
   relocate `tendstoInMeasure_congr_left` and `sq_mul_le_half_add_pow4` to their Mathlib-shaped homes.
4. **`martingale_Zn` extraction.** The `_Zn` cluster (`measurable_Zn`/`integrable_Zn`/`integral_Zn_eq_one`)
   re-instantiates the `E^{−c}` martingale ~6×; extract one `martingale_Zn` and derive the three off it
   (fold with backlog #1, which reshapes these signatures anyway).
5. **`sc-thm-9.1.8`** — the strictly-more-general L²/progressive-θ under Novikov (unbounded), still
   `reduced_core`; needs Novikov + a progressively-measurable integrand realization.

**Evidence/context.** corpus 318 (gir-thm-9.1.8 flipped `reduced_core → full`); full `lake build` green
(8857 jobs pre-upgrade; the three in-file upgrades re-verified on the warm daemon, 0 sorries, 0 warnings);
gates green; ledger 318 fresh; AxiomAuditGen byte-fresh + the curated `AxiomAudit` Track-α section builds
(all four pins axioms-clean `[propext, Classical.choice, Quot.sound]`). Panel convergence on the `p`-moment
duplication (both agents, independently) is the session's clearest signal; it is backlogged, not rushed.

## 2026-07-08 — corpus 318 — finance breadth: Vasicek bond, T-forward measure, geometric-Asian lognormality

**Scope**: the finance-delivery push — `FixedIncome/VasicekBondPrice.lean`,
`FixedIncome/ForwardMeasure.lean`, `Foundations/WienerIntegralIndicator.lean`,
`BlackScholes/AsianGeometric.lean` (corpus `mf-vasicek-bond-price`, `mf-forward-measure-spot`,
`mf-asian-geom-driver-gaussian`; 315→318, all `full`). Reviewed self-critically against the green
`lake build` (8854 jobs) and `grep`-confirmed usage — not a sycophantic panel. **Recon-first paid off
twice**: CVaR's Rockafellar–Uryasev variational theorem + the coherence quartet were found ALREADY COMPLETE
(`gaussianCVaR_isLeast_ruObjective`), so not rebuilt; and `FeynmanKacHeatEquation` only *assumes* `B 0 = 0`
(never derives it), confirming this session's `brownian_start_zero` (zero-start from `IsPreBrownianReal` via
`∫ B_0² = 0`) is a genuine addition, not a re-derivation.

**Upgrade executed this session (lens 3, zero slop — de-duplication):** `VasicekBondPrice.lean` had the
kernel-integral derivation (`∫ g² = V(T)`) and the centred-Wiener-law step duplicated *verbatim* across
`vasicekIntegratedRate_hasLaw_gaussian` and `vasicekBondPrice_eq`. Extracted three single-source private
lemmas — `vasicekIntegratedKernelLp_integral_sq`, `vasicekBondV_nonneg`, `vasicekWienerLaw` — consumed by
both. ~20 lines of duplicated sub-derivation removed; the Vasicek Gaussian law now has one home.

**Per-lens read (exemplar → next upgrade):**
1. **Inspired math** — exemplar: the "sum/integral of Brownian values = one Wiener integral of a
   deterministic step kernel" mechanism, shared by the Vasicek integrated rate (smooth kernel) and the
   geometric-Asian driver (indicator kernel). Upgrade: the n-date geometric-Asian (Finset covariance sum).
2. **Mathlib/Degenne coherence** — exemplar: `wienerIntegralLp_stepIndicator` consumes
   `LinearMap.extendOfNorm_eq` (extension-agrees-on-generators) rather than re-proving agreement. The
   HasLaw a.e.-transfer is hand-rolled `⟨aemeasurable.congr, (map_congr).symm.trans map_eq⟩`; a named
   `HasLaw.congr` pays off only at ≥2 consumers (currently 1) — deferred, not slop.
3. **Zero slop** — exemplar: the de-duplication above. Nothing else outstanding (the `integral_add`
   lambda-form boilerplate and `Pi.zero_apply` massaging are Mathlib friction, not slop).
4. **Architectural ingenuity** — exemplar: the crux `wienerIntegralLp_stepIndicator` as a one-idea
   foundational brick that makes n-date basket laws cheap. Upgrade: hoist `brownian_start_zero` from
   private-in-a-finance-file to the crux module (a foundational BM fact currently mislocated) — small.
5. **First principles** — exemplar: the Vasicek bond price is DERIVED from the Gaussian law (the
   hypothesis — the Wiener representation of the integrated rate — does not contain the conclusion). Honest
   gap: the stochastic-Fubini bridge `∫ r = M + σ∫g dB` is CITED, not proved (parity with the OU-solution
   model of `mf-vasicek-sde-terminal-gaussian`). Upgrade: derive it.
6. **Idiomatic register** — exemplar: `vasicekBondB/V/A`, `asianGeom_driver_hasLaw`, naming + `variable`
   discipline. No upgrade outstanding.
7. **Concept clarity** — exemplar: the docstrings state the modelling bridge (Vasicek), the constant-rate
   degeneracy (forward measure: `Q^T = Q`), and the two-date scope (Asian) HONESTLY. No upgrade outstanding.
8. **Beautiful math** — exemplar: reading `(B_s + B_t)/2` as `∫ ½(𝟙_{(0,s]} + 𝟙_{(0,t]}) dB` — the
   obviously-right argument once seen, sidestepping the joint-Gaussian-process apparatus. Nothing outstanding.

**Ranked backlog:**
1. **n-date geometric-Asian price** — extend `asianGeom_driver_hasLaw` to a `Finset` of dates (variance
   `(1/n²)∑∑min(tᵢ,tⱼ)`), then the closed-form geometric-Asian call via `bs_call_formula` at the effective
   vol. Unblocked by the crux; mechanical. *(Owner: next finance session's opening move.)*
2. **Non-degenerate T-forward measure** — the constant-rate ZCB gives `Q^T = Q`; a genuine `Q^T ≠ Q` needs
   a stochastic bond-price *process* as a `Q`-martingale numéraire (bond dynamics absent). Depth item.
3. **Vasicek stochastic-Fubini bridge** — derive `∫₀ᵀ r_s ds = M(T) + σ∫₀ᵀ g dB` (currently the cited
   modelling input), promoting the bond-price derivation from "from-the-Wiener-representation" to
   "from-the-OU-SDE".
4. **Hoist `brownian_start_zero`** — relocate to `WienerIntegralIndicator` (public), the reusable *derived*
   zero-start the repo elsewhere only assumes.

**Evidence/context.** corpus 318; full `lake build` green (8854 jobs); gates 19/19; ledger 318 fresh (the
de-duplication restaled + reverified `mf-vasicek-bond-price`); AxiomAuditGen byte-fresh (all four new
constants axioms-clean `[propext, Classical.choice, Quot.sound]`). Panel over-escalation avoided twice (the
assumed-vs-derived `B_0 = 0`; the 1-consumer `HasLaw.congr` wrapper temptation).

## 2026-07-03 — corpus 312 — SDE strong-solution uniqueness: the L²-energy Grönwall keystone (#19)

**Scope**: `Foundations/SDEUniqueness.lean` (new). Executes backlog item 4 of the numéraire review (the
standing SDE #19). Reviewed self-critically against the green `lake build` (8841 jobs,
`REAL_BUILD_EXIT=0`), the pinned Mathlib Grönwall API
(`eq_zero_of_abs_deriv_le_mul_abs_self_of_eq_zero_right`), and the repo's own Itô isometry
(`itoProcessCLM_norm_sq`) — not by a sycophantic panel. Two Explore scouts mapped the pin *before* any
Lean was written; the scout confirming **no integral-form Grönwall exists at the pin** is why the
reusable integral form was *built* from the differential one via the FTC primitive.

**Per-lens read (exemplar → next upgrade):**
- **First principles** — *exemplar*: uniqueness is the classical `L²`-energy argument from the ground up
  — `E t ≤ K·∫₀ᵗE` assembled from `(a+b)²≤2a²+2b²`, Cauchy–Schwarz in time, Lipschitz, and Tonelli, then
  closed by Grönwall; the **drift** bound is *derived* (`drift_energy_le`), not assumed. *Next*: derive
  the diffusion isometry bound too, by instantiating `Iσ` with the codebase Itô operator (needs the
  E↔pathwise per-`t` bridge — the same open infrastructure that blocks pathwise existence).
- **Architectural ingenuity** — *exemplar*: the reusable split — a probability-free integral Grönwall
  (`gronwall_zero_of_le_const_mul_integral`, built from Mathlib's differential form), a clean
  energy-method core (`sde_pathwise_uniqueness`), and the structure `IsL2SolutionPair` bundling the
  regularity so the headline theorem stays one hypothesis. *Next*: trim the 11-field structure —
  `stateSqIntervalInt`/`stateSqTimeInt` are Fubini-derivable from `stateSqProdInt`.
- **Concept clarity / idiomatic register** — *exemplar*: "translate to the structure fields" realized as
  its honest meaning — uniqueness becomes a **theorem, not an assumed field**; the prior `reduced_core`
  read the conclusion off a `uniqueness` field by projection (zero derivation). The `isometry` field is
  labeled the sole assumed property of `Iσ` and cited to the proven isometry.
- **Zero slop** — the integral Grönwall does real work (FTC primitive + differential Grönwall), not a
  wrapper; a non-vacuity guard (the zero solution) certifies the field bundle is satisfiable. Green,
  sorry-free, warning-free; axiom-clean `[propext, Classical.choice, Quot.sound]`.

**Upgrades executed this session:** (1) `gronwall_zero_of_le_const_mul_integral` — a reusable
integral-form Grönwall (Mathlib carries only the differential form at this pin); (2) `drift_energy_le` —
the drift energy bound *derived* from Lipschitz `μ` (Cauchy–Schwarz in time + Tonelli), so the drift is
proven, not assumed; (3) `sde_pathwise_uniqueness` — the energy-method Grönwall core; (4)
`IsL2SolutionPair` + `.uniqueness` — the honest field-translation, uniqueness as a derived theorem, with
`sc-thm-8.2.5` flipped **`reduced_core` → `full`**; (5) whole-repo reconcile
(README / coverage / roadmap / AxiomAudit / AxiomAuditGen / ledger 312/0/0).

**Second-pass adversarial audit (same session, two critics + maintainer adjudication):** the panel found
exactly the defects worth acting on, each verified against code before execution: (6)
`sq_integral_le_measureReal_mul` was near-verbatim **duplicated** between `SDEUniqueness` and
`DriftProcessPredictable` (the latter carrying a dead `hf2`) — extracted once to the Mathlib-only leaf
`Foundations/FiniteMeasureCauchySchwarz.lean`, `public import`ed from both, ~30 duplicated lines + the dead
hypothesis removed; (7) `IsL2SolutionPair` trimmed **11 → 9 fields** — `stateSqIntervalInt` /
`stateSqTimeInt` are Fubini consequences of `stateSqProdInt` (`Integrable.prod_left_ae` /
`integral_prod_right`), now derived inside `drift_energy_le`; (8) two `nlinarith` discharges replaced by
their named certificates (`sq_eq_zero_iff` for `a²=0⇒a=0`; explicit monotonicity + `linarith` for the
Grönwall-constant bound). **Adjudicated down**: the panel's docstring "self-advocacy" flag was only
partly actioned (one redundant restatement trimmed) — the honest-scope notes are the repo's honesty
instrument, not slop; and the `Ici 0` continuity hypothesis of the Grönwall lemma was kept (restricting to
`Icc 0 b` trades a cleaner statement for FTC right-endpoint friction — a borderline call the panel itself
declined to insist on).

**A note on the discipline (honest register):** flipping `sc-thm-8.2.5` to `full` was gated on a real
scope decision — the drift is *concrete*, so it **must** be derived (else the "full" claim is a cheat);
the diffusion `Iσ` is *opaque*, so its isometry **must** stay a labeled hypothesis (a proven property of
the Itô integral). Deriving the drift cost a 4-field regularity bundle. That asymmetry is the honest one
(concrete ⇒ derive; abstract-but-proven ⇒ cite), not a shortcut — and it is why this is the uniqueness
*half* only, existence staying the separately-banked conditional-`E` Picard result.

**Ranked backlog (value-aligned):**
1. **The E↔pathwise per-`t` bridge** — the single piece of open infrastructure blocking *both* pathwise
   SDE existence (`sc-thm-8.2.5` existence half) and a concrete, isometry-derived (hypothesis-free) `Iσ`:
   a continuous-modification value identity for *general* `E`-elements (present only definitionally on
   simple processes today). The genuine multi-session mountain.
2. The *continuous* numéraire-portfolio benchmark (Long/Platen) — carried from the prior review.
3. Relate `numeraireDensity` to `Measure.rnDeriv` (carried).

*(The prior "trim `IsL2SolutionPair`" backlog item was executed this session — see the second-pass audit
above; the CS-lemma duplication it surfaced was also fixed.)*

## 2026-07-03 — corpus 312 — The change of numéraire: the full IV↔I seam (backbone + both directions)

**Scope**: `Foundations/Numeraire.lean` (new) + `BlackScholes/StockNumeraire` + `BlackScholes/ExchangeOption`
+ `Performance/KellyNumeraire.lean` (new). Reviewed self-critically against the green `lake build` + the
pinned Mathlib change-of-measure API (the `ChangeOfMeasure` engine's
`setIntegral_withDensity_eq_setIntegral_toReal_smul` idiom), not by a sycophantic panel. **This entry
covers the full day's arc**: the backbone was built first, then — executing this same review's ranked
backlog items 1 and 2 in-session — the two seam directions were added.

**Per-lens read (exemplar → next upgrade):**
- **Coherence (Mathlib/Degenne)** — *exemplar*: `changeOfNumeraire` consumes `integral_withDensity_eq_integral_toReal_smul` directly rather than re-deriving transport; the density idiom `ENNReal.ofReal ∘ (real)` + `toReal_ofReal` matches the repo's own `ChangeOfMeasure` engine. *Next*: state the density as an `rnDeriv` / relate to `Measure.rnDeriv` so it plugs into Mathlib's Radon–Nikodym API.
- **Architectural ingenuity** — *exemplar (the session's #1 upgrade)*: the theorem is a **backbone that is consumed**, not an orphan — `stockNumeraireMeasure_eq_numeraireMeasure` proves the hand-rolled BS stock measure *is* the abstract instance, so `Φ(d₁) = Q^(S)(S_T>K)` now stands on the general law. This is the anti-orphan discipline (a Foundations result with a live pricing consumer on day one). *Next*: wire `ExchangeOption` (S²-numéraire) and `GarmanNormalForm` (forward/annuity) as the two further instances — they currently re-derive the change by hand.
- **First principles** — *exemplar*: the proof is the one-line cancellation of `N_T`, with the *no-integrability-needed* observation made explicit (it is a measure-transport identity, true for every claim). *Next*: derive the numéraire-portfolio ⟷ EMM identity from first principles (the deep seam, below).
- **Zero slop** — no wrapper: the abstract theorem does real work (density construction + cancellation) and generalizes three hand-rolled instances. Green, sorry-free, warning-free; axiom-clean `[propext, Classical.choice, Quot.sound]`.

**Upgrades executed this session:** (1) the abstract `changeOfNumeraire` backbone + probability-measure companion; (2) **wired** it into `StockNumeraire` (a consumed backbone); (3) **backlog item 2 (partial)** — `ExchangeOption.exchangeOption_numeraire_price` makes Margrabe's `S²`-numéraire valuation a genuine `changeOfNumeraire` instance; on inspection **Garman is closed-form algebra with no measure**, so it is honestly *not* wireable and none was faked; (4) **backlog item 1** — `Performance/KellyNumeraire.kellyNumeraire_isRiskNeutral` delivers the numéraire-portfolio ⟹ EMM direction in the discrete Kelly market (the `p`-independence of the GOP-deflated probabilities *is* the Kelly FOC); (5) honest scope framing in every doc (discrete Kelly shadow; continuous Long/Platen still open).

**A note on the discipline (lens 2 + zero-slop):** backlog item 2 was stated this morning as "wire `ExchangeOption` **and** `GarmanNormalForm` as instances." Executing it revealed the premise was half-wrong — only `ExchangeOption` has a measure to wire; `Garman` is post-integration closed form. The honest outcome (one real instance + a documented non-instance) beats forcing a wrapper to hit a self-set target. The backlog is a hypothesis generator, not a checklist to satisfy at the cost of honesty.

**Ranked backlog (value-aligned):**
1. **The *continuous* numéraire-portfolio benchmark** (Long/Platen): deflated prices are `P`-martingales, EMM density `∝ 1/N*`, for a continuous market. Needs a state-price-density / market model absent from the Itô tower — the multi-session mountain behind the discrete Kelly result now delivered.
2. A forward-measure (zero-coupon-bond numéraire) instance in `FixedIncome`, under which forward rates are martingales — the natural third `numeraireMeasure` instance after stock and `S²`.
3. Relate `numeraireDensity` to `Measure.rnDeriv` so the backbone plugs into Mathlib's Radon–Nikodym API (lens-1 coherence upgrade).
4. SDE #19 (the `sc-thm-8.2.5` ℝ-time translation + Grönwall) remains the standing formalization-axis backlog item.

## 2026-07-02 — corpus 309 — SDE Picard: 3-agent values AUDIT + relocation upgrades

**Panel**: three agents — (coherence + idiomatic), (slop + first principles + architecture), (clarity +
inspired + elegant) — on `SDEExistence.lean` (the delivered Picard construction). Each verified findings
against the pinned Mathlib source + the sibling files; cross-checked against the maintainer's own
verification. The panel was genuinely **split** on the operator-bound relocation (agent 1 ranked it low,
agent 2 `[now]`) — resolved by a *verified* fact: the drift CLM's docstring advertised a bound it did not
witness (see below). Verdict: coherence / slop / clarity ceilings already **HIGH** — no in-session slop to
repair (the file is a thin, honestly-derived wiring layer). The upgrades are architecture/placement + clarity.

**Executed this session (all full-build-green, 0-sorry, 8838 jobs).**
1. **Relocated `driftProcessAssembled_norm_le`** → `DriftProcessPredictable` (beside the CLM). Closes a
   VERIFIED broken docstring promise: the drift CLM docstring (`:49`, `:415`) advertised "bounded
   (`‖·‖ ≤ T‖·‖`), all for free" with **no witnessing lemma in the file** — now witnessed and exported.
2. **Relocated `itoProcessAssembled_norm_le`** → `ItoProcessPredictable` (beside its energy identity
   `itoProcessAssembled_norm_sq`), + the `ItoIntegralProcessIsometry` import + a docstring line. `SDEExistence`
   is now pure wiring.
3. **Clarity**: fixed the module docstring's loose "both as operators" — the drift is a genuine CLM
   `E →L E`, the Itô term is element-valued `E → E` (a continuous modification, not a CLM), which is *why* the
   contraction uses `map_sub` for the drift but `itoProcessAssembled_sub` for the Itô term. Surfaced the
   **T-vs-√T asymmetry** where the reader meets it (Cauchy–Schwarz spends time inside each drift slice → full
   `T`; the Itô isometry is flat in `t` → only `√T` survives the outer integral). Folded `lipschitz_sub_const`
   into the decl list.

**Lens reads (exemplar → next upgrade).**
- *Coherence (high)*: consumes `LipschitzWith.compLp` / `norm_compLp_sub_le`, `LinearMap.norm_extendOfNorm_apply_le`,
  `ContractingWith.fixedPoint`, `integral_mono_of_nonneg`, `setIntegral_le_integral` directly. Panel confirmed
  `lipschitz_sub_const` is NOT a re-derivation (no `LipschitzWith.sub_const` at the pin).
- *First principles / elegant (exemplar)*: the `T`/`√T` asymmetry is the a priori SDE estimate made
  structural — each operator bound *derived* from its energy identity, not assumed.

**Ranked backlog (deferred).**
1. **`itoProcessAssembledCLM` via `extendOfNorm`** — retire the ~110 hand-proven `itoProcessAssembled_add`/`_sub`
   lines (`ItoProcessPredictable:215-324`) and let the contraction use `map_sub` uniformly. Deferred:
   `itoProcessAssembled` is deliberately the pathwise-continuous modification for future SDE-path-continuity; a
   CLM's representative need not be that modification (needs an a.e.-agreement lemma). The deepest upgrade.
2. **`timeMeasure_T_real_univ` helper** (in `ItoIntegralCLM`, beside `timeMeasure_T`) — the 7-lemma total-mass
   `rw` chain is verified-triplicated across the Foundations cluster; collapse each site to one rewrite.
3. **`lipComp`'s `L` → implicit** (consistency with `lipComp_sub_norm_le`); the stronger `opNorm_extendOfNorm_le`
   form of the drift bound; `set δb/δσ` in `picardMap_contraction` (low value — the verbosity is honest).
4. **#19** — the `ℝ≥0`↔`ℝ`-time translation to flip `sc-thm-8.2.5` + a Bielecki all-`T` extension (the mountain).

**Evidence/context.** corpus 309; full `lake build` green (8838 jobs) after the relocations; AxiomAuditGen
byte-unchanged (relocation touched no corpus-cited pin); ledger re-verified (1 restaled entry, the sole
transitive importer).

## 2026-07-02 — corpus 308 — SDE existence: the Picard fixed point in `E` (#16–#18)

**Executed this session.** `MathFin/Foundations/SDEExistence.lean` (new, 210 lines, 0-sorry, in the umbrella,
full-build-green 8838 jobs) — the Picard construction for `dX = b(X)dt + σ(X)dB` as a self-map of the
predictable `L²` space `E`, through to the **unique fixed point**: `lipComp` (coefficient composition
`f∘X ∈ E`), `picardMap` (Φ:E→E), the two operator bounds `driftProcessAssembled_norm_le` (`≤T‖·‖`) /
`itoProcessAssembled_norm_le` (`≤√T‖·‖`), `picardMap_contraction` (`‖ΦX−ΦY‖ ≤ (T·L_b+√T·L_σ)‖X−Y‖`), and
`picardMap_exists_unique_fixedPoint` (`∃!`, via `ContractingWith.fixedPoint`). Consumes #14/#15's assembled
operators. The mathematical core of Theorem 8.2.5 — existence **and** uniqueness — is proved.

**Panel**: maintainer self-review (built inline on the warm daemon; each lemma green before the next).

**Lens reads (exemplar → next upgrade).**
- *Mathlib/Degenne coherence (strong)*: no re-derivation — consumes `LipschitzWith.compLp` / `norm_compLp_sub_le`,
  `LinearMap.norm_extendOfNorm_apply_le` (the extendOfNorm operator-norm), `integral_mono_of_nonneg` (dominated
  form, avoids proving LHS integrability), `setIntegral_le_integral`, and `ContractingWith.fixedPoint` directly.
- *Beautiful / first principles (exemplar)*: the estimate's `T·L_b + √T·L_σ` asymmetry is the classical SDE a
  priori bound made structural — the drift contributes the operator norm `T` (Cauchy–Schwarz `∫₀ᵗ`), the Itô term
  `√T` (the isometry's `[0,t]`-energy `≤` full energy). Each bound is *derived* from its energy identity.
- *Zero slop / honesty (holding)*: proofs are certificate-shaped; the result is **stated conditional on
  `T·L_b+√T·L_σ < 1`** (small-horizon) and the module docstring says so plainly — no overclaim as the
  unconditional theorem, and `sc-thm-8.2.5` is left `reduced_core` (not faked).
- *Architecture (one relocation)*: `driftProcessAssembled_norm_le` / `itoProcessAssembled_norm_le` are natural
  companions of their assembled defs — they belong in `DriftProcessPredictable` / `ItoProcessPredictable` (the
  drift keystone's docstring already advertises `‖·‖≤T‖·‖` without a witnessing lemma; relocating closes that gap).

**Ranked backlog (carried + new).**
1. **#19 — the `ℝ≥0`↔`ℝ`-time translation** to `sc-thm-8.2.5` (still `reduced_core`): realize the `E`-fixed-point as a
   pointwise `X : ℝ→Ω→ℝ`, match the Bochner drift to `intervalIntegral ∫ s in 0..t` a.e., instantiate the opaque
   `Iσ` as the real Itô term, prove the per-`t`-a.e. equation + Grönwall uniqueness. The real remaining mountain.
2. **All-`T` extension** — a Bielecki exp-weighted norm on `E` to drop the `< 1` smallness condition (the benchmark
   quantifies all `t ≥ 0`).
3. **Relocate the two operator bounds** into their home files (architecture lens above).
4. **#20 wiring** — benchmark entry + AxiomAudit pins (`picardMap_contraction`, `picardMap_exists_unique_fixedPoint`)
   + AxiomAuditGen + ledger + coverage/docs, at delivery.

**Evidence/context.** corpus **308 unchanged** (a `MathFin/` build — no benchmark entries added); ledger **fresh
308/0/0** (imported by no benchmark snippet); full `lake build` green (8838 jobs), SDEExistence 0-warning 0-sorry.
Committed + pushed `e949194..6521a2d`.

## 2026-07-02 — corpus 308 — SDE-existence keystone II: the drift assembled into `E` (values-upgrade pass)

**Executed this session.** A three-agent upgrade pass on the drift keystone
`Foundations/DriftProcessPredictable` (`driftProcessAssembled : E →L E`, the drift term of the Picard
iterate as a bounded operator on the predictable `L²` space; landed `403b6f2`→`0a1a707`, lake-verified).
Six in-session upgrades, all daemon-green (success, zero warnings, zero sorries; 431 lines):
1. *coherence rename* `driftProcessLp` → `driftSimpleProcessLp` (+ `_norm_le`) — it takes a `SimpleProcess`,
   so it now parallels the Itô sibling `itoSimpleProcessLp`/`_norm_le` exactly (file-local, no external refs);
2. *slop* — the triplicated `IsFiniteMeasure (timeMeasure.restrict (Ioc a b))` `haveI` (lines 138/239/264)
   folded into one file-local `instance isFiniteMeasure_timeMeasure_restrict_Ioc`; the three sites now
   resolve it automatically;
3. *concept clarity* — the module docstring rewritten to actually map the file: it had stopped at Part 1
   (predictability) and never named the keystone (the honest-integral bridge, `driftSimpleProcessLp_norm_le`,
   the `driftProcessAssembled` CLM); now a `Part 1 / Part 2` structure lists every deliverable;
4. *inspired core, surfaced* — the header now states the elegant contrast where the reader meets it: the drift
   carries **no randomness in its time-regularity**, so there is **no exceptional null set** and Degenne's
   `…of_leftContinuous` applies to the *raw* `natFiltration` — vs. the Itô side, which applies it
   per-elementary-process to dodge the augmented-filtration friction;
5. *idiomatic register* — `push Not` → `rw [not_le]` (matching the file's other branch); `Finsupp.sum`-unfold
   cleaned to `simp only [driftSimpleProcess, Finsupp.sum]` where the binder blocks `rw`, and dropped entirely
   in `_stronglyAdapted` where the closing `exact` unifies by defeq;
6. *clarity* — a one-line gloss on `driftSimpleProcess` explaining the `((min · t : ℝ≥0) : ℝ)` double coercion
   (the clamp is taken in `ℝ≥0` to line up with `timeMeasure_Ioc_inter`'s endpoints in the bridge).

**Panel**: three agents — (coherence + idiomatic), (slop + first principles + architecture),
(clarity + inspired + elegant). Findings cross-verified against the code before acting (per the
subagents-over-escalate discipline): the sum-unfold fix corrected a reviewer's `rw` suggestion — `rw` cannot
rewrite under the `fun t =>` binder, `simp only` can; and the `_stronglyAdapted` unfold was shown *unnecessary*
(the `exact` closes by defeq), removed rather than kept.

**Lens reads (exemplar → next upgrade).**
- *Coherence (strong)*: no lemma re-proves upstream — the file consumes `isStronglyPredictable_of_leftContinuous`,
  `StronglyMeasurable.limUnder`, `LinearMap.extendOfNorm`, `integral_mul_le_Lp_mul_Lq_of_nonneg`,
  `Finsupp.sum_add_index'` directly and reuses the repo's `simpleAssembly_T` / `memLp_uncurry_trim_T` /
  `lp_two_norm_sq`. **Next:** factor the shared `‖toLp g‖² = ∫ (uncurry g)² ∂prod` computation (inlined here as
  `hnorm` and again in `itoProcessAssembled_norm_sq`) into one lemma both keystones consume.
- *Architectural ingenuity (strong, one open fork)*: the CLM-via-`extendOfNorm` route is cleaner than the Itô
  side's element-valued `toLp` with hand-proven `_add`/`_sub`/`_norm_sq` — linearity, boundedness, and
  predictability all fall out of `E`-membership. **The fork:** `driftContinuousMod` (Part 1) is an *orphan* —
  the CLM never routes through it, and unlike the Itô sibling's `itoContinuousMod_modification` there is no
  bridge tying the abstract CLM output to that pathwise realization. Now documented as a parity / future-use
  track rather than deleted (orphan-reflection rule); the delete-vs-bridge call belongs to #18/#19.
- *Zero slop (holding)*: the one Cauchy–Schwarz helper `sq_integral_le_measureReal_mul` is honestly the
  canonical Hölder (`g = 1`), not a re-proof (confirmed no direct Bochner-`∫` Mathlib lemma exists); its
  rpow-squaring tail is the only ceremony. Remaining duplication is measure-finiteness / `toReal` plumbing.
- *Concept clarity (upgraded this session)*: header now maps the whole file and states the inspired point where
  the reader arrives, closing the "header describes only Part 1" gap all three reviewers flagged.

**Ranked backlog (carried + new).**
1. **The Picard assembly (#16–#20 — the delivery, not a nit)**: `Φ = η + driftProcessAssembled(b∘X) +
   itoProcessAssembled(σ∘X)`; Bielecki-weighted contraction; `ContractingWith.fixedPoint`; Grönwall
   uniqueness; translate to `sc-thm-8.2.5` (still `reduced_core`) and retire the opaque `Iσ`.
2. **`driftContinuousMod` fork resolution** — delete (YAGNI; the CLM route supersedes) *or* earn it with the
   `driftProcessAssembled φ =ᵐ uncurry (driftContinuousMod φ)` bridge; decide when #18/#19 fix whether the
   fixed point's a.s.-path-continuity needs a pathwise drift realization.
3. **Repo-wide plumbing factor** (deferred: touching `ItoIntegralL2` restales the corpus, so batch on a
   GitHub-runner ledger sweep): promote the `IsFiniteMeasure (timeMeasure.restrict (Ioc a b))` instance and add
   a `timeMeasureReal_Ioc : (timeMeasure (Ioc a b)).toReal = b − a` helper into `ItoIntegralL2`, killing ~6
   in-repo copies each; plus the shared `‖toLp g‖²` lemma (from the coherence lens above).
4. **Micro, on next touch**: slim `sq_integral_le_measureReal_mul`'s rpow tail (try `Real.rpow_two` + `sq_abs`);
   unify `driftSimpleProcess_add`/`_smul` onto the closed `Finsupp.sum` form (`_smul` currently detours through
   the integral bridge).

**Evidence/context.** corpus **308 unchanged** (a `MathFin/` upgrade pass — no benchmark entries added, so the
cadence gate is untouched); ledger **fresh 308/0/0** (the file is imported by no benchmark snippet, so the edit
stales nothing); `DriftProcessPredictable.lean` daemon-green. These upgrades are a follow-on to the pushed
keystone (`8660775..0a1a707`), to be committed on top.

## 2026-06-30 — corpus 308 — Phase 2: Girsanov, the EMM as an explicit change of measure

**Executed this session.** The continuous-time EMM is now *constructed*, not assumed:
`Foundations/Girsanov.bs_discounted_isQMartingale` (the Black–Scholes risk-neutral measure as a Girsanov
density tilt, constant θ; the discounted stock a `Q`-martingale on `[0,T]`) standing on a reusable
abstract engine `Foundations/ChangeOfMeasure.changeOfMeasure_setIntegral_eq` (the Bayes change of
measure: `Z` and `Z·D` `P`-martingales ⟹ `D` a `Q`-martingale). Two new `full` entries; retires the Wald
shortcut of `discountedGBM_isMartingale`.

**Lens reads (exemplar → next upgrade).**
- *Architectural ingenuity* (strong): the deep content is a **general** engine (any density `Z`), with
  Black–Scholes as one instance — so it already covers the constant-θ case and will consume the adapted-θ
  Doléans–Dade exponential *unchanged* once the Itô tower exposes it. The abstraction is the reuse, not
  decoration. **Next:** wire a *second* consumer (e.g. a numéraire change) so the engine's generality is
  visible in the corpus, not just latent.
- *First principles* (strong): no black-box Girsanov — the change of measure is a Bayes pull-out plus a
  martingale set-integral, and the one estimate (mixed-time integrability) is an explicit AM–GM bound,
  not a `positivity`/`fun_prop` incantation.
- *Zero slop / honesty* (holding): the spike proved general adapted θ is **out of reach** in the tower
  (no Itô for `F(∫θ dB)`; QV only in expectation), and the result is scoped and documented as such — no
  overclaim that `gir-thm-9.1.8` (the distributional Girsanov) is done. **Next:** the distributional
  statement is the honest headline once an adapted-integrand Itô formula lands.

**Ranked backlog (carried + new).** (1) adapted-integrand Itô / pathwise QV of `∫θ dB` — unblocks general
Girsanov + `gir-thm-9.1.8` (Itô-tower depth; re-scout upstream Degenne first); (2) superhedging
strong-duality equality — finite-dim Farkas (#39); (3) the numéraire (IV↔I) — a natural *second* consumer
of the change-of-measure engine; (4) the Gaussian CVaR robust form.

## 2026-06-29 — corpus 306 — Phase 1: the convex-duality unification (FTAP = coherent-risk, one Hahn–Banach root)

**Upgrade executed (the headline).** The architecture doc's **#1 unification** — the I↔IV convex-duality
bridge — is now *realized in Lean*, not latent. The shared geometric root lives in `Foundations/ConvexDuality`
(the cone↔simplex separation `exists_pos_separating_of_cone_disjoint_simplex` + its point↔cone companion
`exists_separating_of_not_mem_cone`, sharing two named atoms `functional_eq_sum_single` /
`functional_nonneg_on_cone`), and four consumers now *stand on it*:
- **pricing**: the FTAP kernel `exists_pos_dual_of_disjoint_stdSimplex` is **re-derived** from the root (a
  subspace = two-sided cone), so "the separating hyperplane is the EMM" is load-bearing, not annotation;
- **risk**: the coherent-risk ADEH representation `coherentRisk_isLUB` (a coherent ρ = sup of expected loss
  over its representing measures), closedness **derived** from the four axioms, not assumed;
- **concrete**: `worstCase_isLUB` (worst-case loss = sup over the whole probability simplex);
- **superhedging**: the `emm_le_superReplication` bound (EMM price ≤ super-replication cost).
**Proved: the FTAP and the coherent-risk representation are the same Hahn–Banach theorem** — the two
most-disconnected towers (pricing ↔ risk) are now one. Four new `full` corpus entries (302→306); axioms-clean.

**Method (a lens-4 / infra note).** Every proof was **spike-validated by the maintainer on the warm daemon
first**, then handed to a transcription subagent under a two-stage (implementer → reviewer) gate. Result:
6 tasks, zero proof rework, every per-task review clean. The novel kernels (the point-from-cone primitive,
the full ADEH `IsLUB` with its `q*`-normalization) were the maintainer's to find; the subagents assembled and
wired. Subagent-driven development adapted to research-grade Lean.

**Per-lens gradient (exemplar → next upgrade).**
- *Inspired math / first principles*: exemplar = the ADEH representation from four axioms + one separation
  primitive (closedness derived). Upgrade = the superhedging **strong** duality (the root-using ≤ direction).
- *Architectural ingenuity / concept clarity*: exemplar = `ConvexDuality` naming the two atoms both separation
  theorems consume — the unification made structural. Upgrade = a capstone enumerating the instances in one place.
- *Coherence*: exemplar = the in-place re-derivation of the FTAP kernel (one proof, no primed duplicate).
- *Zero slop*: the env-linter is restored to a **blocking** per-push gate (build.yml), green via a
  `scripts/nolints.json` baseline that catches *new* findings.

**Refreshed ranked backlog (a future session's opening move).**
1. **Superhedging strong duality** (`superhedge = sup_{EMM}`) — blocked on a finite-dim **Farkas /
   polyhedral-cone closedness** (Mathlib gap at this pin; `PointedCone.isClosed_dual` covers only *dual* cones).
   The genuine root-using direction; highest-value backlog item.
2. **Girsanov (I↔II)** — the next bridge; derive the continuous EMM from the Itô tower (Phase 2).
3. **The lint baseline's 28 grandfathered findings** — 4 genuine dead `_hBmeas` args (drop with the Phase-2
   bundled-`IsBrownianMotion` refactor), 16 deliberate naming (`_T` / `Has…_state`), 8 internal-helper docstrings.
4. **Gaussian CVaR robust form** + **numéraire (IV↔I)** — the continuous-instance and portfolio seams.

**Evidence/context.** corpus 302→306 (4 new `full`), ledger fresh, `lake build` green, AxiomAudit `#guard_msgs`
pins all four new headline theorems to `[propext, Classical.choice, Quot.sound]`. **CI fix embedded in Phase 1**:
the env-linter had been silently breaking `main`'s build (lean-action auto-runs `lake lint` when a `lintDriver`
is configured, and the linter exits 1 on findings) — restored to a green blocking per-push gate via the
`scripts/nolints.json` baseline; `lint.yml` (workflow_dispatch) stays the on-demand inventory.

## 2026-06-29 — corpus 302 — WHOLE-REPO values-upgrade review (program-quality deep dive; first under the upgrade model)

**Scope**: the entire library at corpus 302 (~41.9k lines, 212 modules, 267 full / 18 library_wrapper /
17 reduced_core), commissioned as a standalone session: *given the drastic growth, is the program still
coherent, or sliding toward a low-quality dump — and what are the next upgrades that keep it climbing?*
Deep dive on the eight lenses **individually and as a set**, plus an infrastructure-modernity assessment.
Read each lens as a **gradient**, not a threshold.

**Method**: a three-agent read-only panel (Itô-tower coherence / pricing + reduced_core honesty /
adversarial whole-repo slop sweep), then **maintainer adjudication** against the settled wrapper doctrine,
`grep`-confirmed usage, and mechanical sweeps (`sorry`/`axiom`/`native_decide`/`maxHeartbeats` counts, the
module import graph, orphan cross-reference).

**Baseline / evidence (the floor the upgrades build from — context, not a grade).**
- Mechanical floor clean: 0 `sorry`/`admit` in source (7 hits are comment prose), 0 `axiom` decls (1 grep
  hit is a comment word), 0 `native_decide`, 0 `maxHeartbeats`, 0 true orphans (the 5 import-graph leaves
  — `AxiomAudit`, `AxiomAuditGen`, `Blueprint`, `Blueprint/Export`, `Examples` — are deliberate
  `globs := .andSubmodules` harnesses). `autoImplicit false`; `@[expose] public section` gate-enforced.
  19/19 pytest, ledger 302/302. Lean's default build-time linters run green.
- **The panel's "BLOCKING slop" escalations mostly DISSOLVED on adjudication**, which is the reassuring
  signal: `Phi_def := rfl` is used 4× as a `rw` handle (idiomatic, not bookkeeping); the survival `rfl`
  is a *declared* cross-domain coherence bridge ("**not** new finance"); the `GreekSigns` delta one-liners
  complete a documented catalogue; the four `_pos := Real.exp_pos _` are domain positivity API over
  `noncomputable def`s; `ItoLemma` is consumed by `GBMLogMoments`/`PDEFromIto`; the strong/weak Itô pair
  is both load-bearing. Each flag violated one lens *in isolation* but satisfied the lens **system**. The
  pricing agent's opposite failure (all-green sycophancy) was equally discounted. Net: the discipline is
  holding — this is the *baseline*, not an end state.

**Per-lens: exemplar (the bar to propagate) → next upgrade (the gradient).**
1. **Inspired math** — exemplar: the Summit-C localization (`ito_formula_unrestricted`, a genuine
   `IsLocalMartingale`). *Upgrade*: the general **adapted-coefficient** (random-integrand) Itô formula —
   the open frontier that retires the last "bounded / exp-growth" caveat.
2. **Mathlib/Degenne coherence** — exemplar: `VasicekSDEGaussian` consuming the Wiener-integral tower.
   *Upgrade*: make the two-tower bridge **plural** — route a second pricing family (a barrier/lookback, or
   a CIR/Heston short rate) through the Itô tower, so the bridge is structural rather than exemplary.
3. **Zero slop** — exemplar: the certificate-shaped `nlinarith` convention. *Upgrade* **[EXECUTED]**: wire
   the env-linter (`lake lint` → Batteries `runLinter`, advisory CI) so `unusedArguments` /
   `unusedHavesSuffices` / `synTaut` mechanize this lens instead of human eyes. *Next*: triage its first
   inventory into fixes + a `nolints.json` baseline.
4. **Architectural ingenuity** — exemplar: hoisting `StandardNormal` out of pricing to fix a layering
   inversion. *Upgrade* **[EXECUTED, this review]**: the review model itself — from pass/fail to an
   upgrade engine. *Next structural*: the Itô-tower naming layer (`_T`/`_Infinite`/`_TD`) is debt; do it as
   a deliberate tower-consolidation (a rename restales the whole ledger, so batch it with real work).
5. **First principles** — exemplar: the reduced_core honesty taxonomy + the definitional-`rfl` tripwire.
   The seven sampled reduced_core entries (SDE existence, Lévy, Girsanov, martingale representation,
   Novikov, strong Markov, 2D Itô) are honest specification-level encodings. *Upgrade*: promote one
   reduced_core sub-core (e.g. Lévy or martingale representation) from spec-encoding to a *derived*
   statement.
6. **Idiomatic register** — exemplar **[NEW, this session]**: consuming Batteries' `runLinter` via
   `lintDriver` rather than re-implementing it. *Upgrade*: from the env-linter inventory, fix or `nolint`
   each `simpNF` / `defLemma` / `dupNamespace` finding.
7. **Concept clarity** — exemplar: the `GreekSigns` table + the honest verification-vs-derivation
   docstrings. *Upgrade*: rename the two stale "deferred" doc filenames to their CLOSED status; let
   `docBlame` surface public decls missing docstrings and fill the load-bearing ones.
8. **Beautiful math** — exemplar: the heat-kernel-carries-the-BS-PDE route; the time-clamp
   drift-adaptedness argument. *Upgrade*: an "elegant proofs" tour in `Examples.lean` that *propagates*
   the obviously-right-once-seen arguments — beauty is also raised by being shown.

**The lenses AS A SET (the meta-ask).** Three bands: **honesty** (3, 5, 7 — largely machine-enforceable;
the env-linter extends lens-3's reach), **taste** (1, 4, 8 — irreducible human/agent judgment, what the
review cadence protects), **coherence** (2, 6 — semi-mechanizable). The built-in tensions are *resolved
doctrinally*, which is why the panel's surface findings dissolved: lens-2 *no thin wrappers* vs lens-7
*name the concept* → the wrapper taxonomy; lens-8 *minimal* vs lens-3 *no opaque discharge* → the
certificate-shaped `nlinarith`; lens-1/4 *earn-its-place / right-generality* vs over-engineering → *every
headline theorem has a consumer*. The upgrade model makes each lens **point somewhere** instead of
settling at a checkmark.

**Upgrades EXECUTED this session.**
- *(honesty machinery — lens 3/7)* Fixed the values-freshness gate's stale anchor: `REVIEW_HEADER_RE`
  required a `commit <sha>` the 7 newest entries had dropped, so it tracked corpus 292 (gap 10) while real
  reviews sat at 302. Loosened to parse `date … corpus N`; now anchors to 302 (gap 0). A freshness gate
  reading the wrong line is the one place slop had reached the dump-prevention machinery itself.
- *(lens 3 + 6)* Wired the advisory env-linter — lakefile `lintDriver := "batteries/runLinter"` +
  `lintDriverArgs := #["MathFin"]`, and `.github/workflows/lint.yml` (`workflow_dispatch`, advisory).
- *(lens 4 — the review itself)* Reframed this protocol from pass/fail verdict to value-aligned upgrade
  engine (this entry, and the doctrine + Protocol above).

**Ranked upgrade backlog (next moves, highest leverage first).**
1. **Triage the env-linter's first CI inventory** — fix genuine dead-args (e.g. confirm/clear
   `bsV_gamma_pos`'s `_hK`), `nolint` the deliberate conventions into `scripts/nolints.json`, then promote
   `lint.yml` to PR-advisory (`continue-on-error`).
2. **General adapted-coefficient Itô formula** (lens 1) — the standing open frontier.
3. **Second two-tower bridge** to a new pricing family (lens 2).
4. **Itô-tower naming-consolidation** pass, batched with structural work (lens 4/6).
5. **Promote one reduced_core sub-core** from spec-encoding to derived (lens 5).
6. **Rename the stale "deferred" docs**; fill load-bearing `docBlame` gaps (lens 7).

This review records a **direction, not a grade**. The discipline is intact across both towers; the work is
to keep climbing, not to certify "OK."

## 2026-06-29 — corpus 302 — Summit C in Degenne's `IsLocalMartingale` typeclass (the wrapper completed)

**Scope**: `Foundations/ItoFormulaUnrestrictedLocMart.lean` (new — `driftPrimitive_stronglyMeasurable`
[the drift primitive `D_t = ∫₀ᵗ drift` is `𝓕_t`-measurable via time-clamping + Carathéodory +
`StronglyMeasurable.integral_prod_right`], `residual_stronglyMeasurable` [`M` adapted], and
`ito_formula_unrestricted` [the genuine `IsLocalMartingale M`]), the docstring updates to
`ItoFormulaUnrestricted.lean` (the wrapper is no longer "deferred"), and corpus entry
`sc-ito-formula-unrestricted-islocalmartingale` (`full`).

**Panel**: two independent reviewers across the eight lenses.

**Verdict: 8/8 PASS** — no blocking findings.

- **The headline question — is `IsLocalMartingale M` genuine or overclaimed?** Both reviewers traced
  the `IsLocalMartingale → Locally → ∃ τ, IsLocalizingSequence ∧ ∀ N, p(stopped)` unfolding and
  confirmed the proof discharges it honestly: the localizer is the **real** exit-time sequence
  `σ_N = min(τ_N, N)` (not the trivial const-`⊤`), the reference martingale `Z` is the genuine
  stopped truncated martingale, the target `Y`'s martingale identity is transferred via
  `condExp_congr_ae` + `Z`'s identity + the all-time agreement `indistinguishable_on_stochInterval`,
  and adaptedness is real (`residual_stronglyMeasurable`). No `sorry`/cheat; axioms-clean
  `[propext, Classical.choice, Quot.sound]` (confirmed pinned).
- **Math / coherence / ingenuity / first principles**: the time-clamp drift-adaptedness argument
  (`min s t ≤ t` ⇒ each slice `𝓕_t`-measurable; Carathéodory joint measurability; `integral_prod_right`)
  is correct; the `letI : MeasurableSpace Ω := natFiltration hBmeas t` sub-σ-algebra switch is sound
  and well-commented (slice facts proved with `mΩ` ambient, then the product/integral lemmas
  re-pointed); consumes the right Mathlib/Degenne lemmas (`stronglyMeasurable_uncurry_of_continuous_of_stronglyMeasurable`,
  `Martingale.stoppedProcess_indicator`, `StronglyAdapted.stoppedProcess_indicator`, `isStable_isCadlag`,
  `stoppedProcess_eq_of_le/ge`) without reproving; the `untopA` `WithTop`/`ℝ≥0` boundary handling is
  necessary friction, not a workaround.
- **Slop / idiom / clarity / beauty**: all three lemmas load-bearing, no unused hypotheses, idiomatic
  combinators, the Itô identity discharged "by construction" (`simp only [hM]; ring`), the martingale
  transfer a clean symmetric `=ᵐ` calc. Two tiny dedup observations (the `IsCadlag`-from-continuous
  constructor appears twice; `M`'s definition/continuity is re-derived because the upstream
  `ito_formula_unrestricted_local` packages `M` existentially) — both non-blocking, the latter forced
  by the existential seam.
- **One stale-language nit (fixed before commit)**: the Strategy *intro* in `ItoFormulaUnrestricted.lean`
  still said the typeclass packaging "is deferred", contradicting the (already-updated) bullet that
  says it is complete. Reworded to point at `ito_formula_unrestricted`.

**Net**: Summit C is now complete in **both** the explicit local-martingale form
(`ito_formula_unrestricted_local`) and Degenne's `IsLocalMartingale` typeclass
(`ito_formula_unrestricted`). The deferred piece is genuinely done; no overclaiming remains.

## 2026-06-29 — corpus 301 — Summit C: the unrestricted-`C³` Itô formula via stopping-time localization (explicit local-martingale form)

**Scope**: `Foundations/ItoFormulaUnrestricted.lean` (new — the double cutoff `fTrunc N` with its
six chain-rule `HasDerivAt` lemmas + constant bounds on the compact square + two joint-continuity
facts; `continuous_timeMeasure_primitive`; `abs_le_N_of_le_exitTime`; `sigmaSeq` /
`isLocalizingSequence_sigma`; the cut-inactivity helpers; `ito_formula_unrestricted_local`; and the
indistinguishability crux `indistinguishable_on_stochInterval`), the refactor of
`ItoIntegralProcessLocalMartingaleInfinite.lean` (exposing the global `Martingale` via
`exists_continuous_martingale_modification_infinite`, with the local-martingale corollary derived
from it), and corpus entry `sc-ito-formula-unrestricted-local` (`full`).

**Panel**: two independent reviewers across the eight lenses.

**Verdict: 8/8 PASS** after one blocking fix.

- **Blocking finding (fixed before commit)**: *both* reviewers independently flagged the module-header
  "Strategy" docstring's "Assembly" stage as an **overclaim** — it described the
  `stoppedProcess_indicator → Locally → IsLocalMartingale` typeclass machinery as if realized in the
  file ("…i.e. `IsLocalMartingale M`"), when the shipped theorem delivers the **explicit** local-martingale
  form (localizing sequence + per-`N` continuous true martingales `Mₙ` agreeing with `M` on
  `{t ≤ σ_N}`). Every other honesty surface (theorem name `ito_formula_unrestricted_local`, theorem
  docstring, `AxiomAudit` prose, corpus `formalization_scope`) was already scrupulously honest. The
  header was rewritten to describe the explicit form and to mark the typeclass wrapper as **deferred**
  (staged by `indistinguishable_on_stochInterval`, blocked only on drift-integral adaptedness).
- **Inspired math / coherence / ingenuity / first principles**: both reviewers verified the chain rule
  for all six truncated partials, the compact-square bounds, the exit-time confinement (closed-exterior
  + boundary left-continuity), the drift collapse, and the indistinguishability lemma — no errors. The
  "time cut is essential" reasoning (a general `C³` `f` has `t`-derivatives unbounded over `t ∈ ℝ`, so
  the localizer is capped at `N`) is correct and subtle. Consumes `ito_formula_td_process`, the newly
  exposed global martingale, `Set.EqOn.of_subset_closure`/`closure_Iio'` without reproving; the
  infinite-file refactor is clean. The explicit-residual `M` design (Itô identity by construction,
  continuity free) is elegant.
- **Zero slop / idiom / clarity / beauty**: no dead code, no unused hypotheses (all six `HasDerivAt`
  + seven continuities consumed), idiomatic `HasDerivAt`/`Continuous` combinators, sensible naming.
  `indistinguishable_on_stochInterval` is unused by the shipped theorem but justified under the
  orphan/future-use doctrine (the documented foundation of the deferred wrapper) — its docstring was
  augmented to say so. `continuous_timeMeasure_primitive` is genuinely new (no duplicate).

**Honesty note**: the delivered result is the continuous-local-martingale property in *explicit form*
— the full mathematical content of Summit C. The Degenne-`IsLocalMartingale`-typeclass packaging is
*deferred* (open frontier), blocked only on the parametrized-integral adaptedness of `M`; this is
recorded consistently across the file, `AxiomAudit`, the corpus scope, `docs/coverage.md`, and
`docs/roadmap.md`. No overclaiming remains.

## 2026-06-28 — corpus 300 — Brownian exit times: the first localizing sequence

**Scope**: `Foundations/ExitTime.lean` (new — `exitTime`, `exists_rat_time_below`,
`exitTime_le_iff`, `exists_le_abs_eq_iInter_iUnion`, `isStoppingTime_exitTime`,
`exitTime_mono`/`exitTime_monotone`, `exitTime_tendsto_top`, capstone
`isLocalizingSequence_exitTime`); umbrella import; curated `AxiomAudit` pins
(`isStoppingTime_exitTime`, `isLocalizingSequence_exitTime`) + regenerated `AxiomAuditGen`.
Entry `sc-exit-times-localizing-sequence` (`full`). Two-agent panel
(inspired / coherence / architecture / first-principles ; zero-slop / idiom / clarity / beauty).

| lens | verdict |
| --- | --- |
| inspired math quality | PASS |
| Mathlib / Degenne coherence | PASS |
| zero slop | PASS |
| architectural ingenuity | PASS |
| first principles | PASS |
| idiomatic register | PASS |
| concept clarity | PASS |
| beautiful, elegant math | PASS |

**Blocking findings**: none.

**Checks that mattered**: the closed-exterior design is load-bearing, not laziness — the panel
verified `IsClosed.csInf_mem` is the pivot (the `sInf` of the closed hit-set is *attained*), so
`{τ_N ≤ i}` is genuinely the attained-`sInf` event, measurable in `𝓕_i` **without** right-continuity;
the open-exterior `{N < |x|}` route would only characterize `{τ_N < i} ∈ 𝓕_{i⁺}` (Blumenthal), which
the raw Brownian filtration does not provide. The from-scratch `exitTime_le_iff` is necessary, not a
reproval: Mathlib's `hittingAfter_le_iff` needs `[WellFoundedLT ι]`, which `ℝ≥0` lacks. The module
**consumes** the right Mathlib lemmas (`hittingAfter`, `NNReal.lt_iff_exists_rat_btwn`,
`IsCompact.exists_isMaxOn`, `WithTop.tendsto_nhds_top_iff`, `Filtration.mono`,
`measurable_eval_natFiltration`) — nothing reproved; the backward measurability direction is a
compact-max (`IsCompact.exists_isMaxOn`), not a Bolzano–Weierstrass subsequence. Automation is
targeted (`linarith`/`positivity`/one `simpa`), no `simp`/`grind` obfuscation; no
`sorry`/`admit`/`native_decide`/uncertificated `nlinarith`. Corpus entry honest: `full` re-export,
no overclaiming — the unrestricted-`C²` Itô formula it enables is named as the open Summit-C
frontier, not claimed. Axioms-clean (`[propext, Classical.choice, Quot.sound]`), confirmed by the
`#print axioms` guards in the 8813-job green build.

**Recorded actions**: none blocking. Next session — Summit C Stages 2–4: the time+space truncation
of a general `C³` `f` (via `SmoothTrunc.cut` in **both** arguments → `ito_formula_td_process`), then
the `Locally` / `Martingale.stoppedProcess_indicator` assembly stopping the truncated martingales at
these exit times.

## 2026-06-28 — corpus 299 — Itô's lemma as a process (semimartingale decomposition)

**Scope**: `Foundations/ItoFormulaProcess.lean` (new — `ito_formula_td_process`,
`exists_fullHorizon_extension`); the witness-exposure strengthening of
`ItoIntegralRiemannBridgeTD.itoIntegralCLM_T_of_bdd_cont_td`; the `_explicit` core +
thin wrapper refactor of `ItoFormulaTD.ito_formula_td_L2_bddDeriv`; the extraction of
`itoProcessCLM_terminal_eq` into `ItoIntegralProcessGeneral`. Entry `sc-ito-formula-td-process`
(`full`). Two-agent panel (coherence + architecture + first-principles; zero-slop + idiom +
clarity + beauty/inspired).

| lens | verdict |
| --- | --- |
| inspired math quality | PASS |
| Mathlib / Degenne coherence | PASS |
| zero slop | PASS |
| architectural ingenuity | PASS |
| first principles | PASS |
| idiomatic register | PASS |
| concept clarity | PASS |
| beautiful, elegant math | PASS |

**Blocking findings**: none.

**Checks that mattered**: the "no Markov property, no PDE" claim is literally true — the
import closure is `ItoFormulaTD` + `ItoIntegralProcessLocalMartingaleInfinite` only, no
Feynman–Kac/heat-kernel/Markov module is reachable; the stochastic term is built analytically
through the Riemann↔CLM bridge, the continuity/local-martingale structure through the existing
`[0,∞)` tower (Degenne maximal inequality + Borel–Cantelli), *not* a semigroup. The crux
`M_t =ᵐ itoProcessL2Inf t F` is genuinely derived (terminal-explicit at horizon `t` →
witness restriction `restrictToBand t F = gfxₜ` → horizon consistency), nothing circular. The
witness-exposure is a **one-conjunct** strengthening returning the bridge's already-built `toLp`
witness (`MemLp.coeFn_toLp _`), not a second copy of the bridge — the minimality is the tell of
the right abstraction. Both the `_explicit`/wrapper split and the `itoProcessCLM_terminal_eq`
extraction are pure dedups (verified against the diffs: zero proof duplication; both have two real
consumers). The full `C^{1,2}`-with-bounds package is genuinely needed (forwarded to the terminal
formula's 2D Itô–Taylor remainder), not vestigial. Scope honest: bounded-derivative base, general
**adapted** coefficients named as the open frontier. Axioms-clean
(`[propext, Classical.choice, Quot.sound]`).

**Recorded actions**:
1. *(done in this commit)* cleared the panel's three cosmetic nits — dropped the unused
   `with hm`/`with hh` bindings on two `set`s, tightened the `exists_fullHorizon_extension`
   docstring (`restrictToBand T F =ᵐ g` is a stated consequence, not the returned conjunct),
   restored the trailing newline on `benchmarks/stochastic_calculus.json`.

## 2026-06-28 — corpus 298 — the Itô formula reaches a general (constant-coefficient) Itô process

**Scope.** New `Foundations/ItoFormulaItoProcess.lean` (`ito_formula_itoProcess`: the Itô formula
`f(X_T) − f(X₀) =ᵐ itoIntegralCLM_T gfx + ∫₀ᵀ (f'(X)·b + ½f''(X)·σ²) ds` for `X_t = X₀ + b·t + σ B_t`
and a general `C³` exponential-growth `f`); the coherence refactor lifting three `SmoothTrunc`
lemmas (`cut_eq_id_of_abs_le`, `cutD1_eq_one_of_abs_lt`, `phi'_eq_one_of_lt`) into
`ItoFormulaLocalized.lean` (with `cut_eventually_id` refactored to consume the first); and the
**re-derivation of `ito_formula_gbm` as the `f = S₀·exp` specialization** of the new general
theorem. Corpus entry `sc-ito-formula-ito-process` (`full`, axioms-clean
`[propext, Classical.choice, Quot.sound]`).

**Panel.** Two independent reviewers, eight lenses.

| lens | verdict |
|---|---|
| inspired math | PASS |
| Mathlib/Degenne coherence | PASS |
| zero slop | PASS |
| architectural ingenuity | PASS |
| first principles | PASS |
| idiomatic register | PASS |
| concept clarity | PASS |
| beautiful, elegant math | PASS |

**Blocking findings**: none. The panel verified the new theorem is a genuine generalization (not a
parallel rebuild) — it instantiates the shared `ito_formula_td_localized` exactly as GBM does, with
the *right new abstraction* (`hfbd` over an arbitrary exp-growth `h ∘ affine`, then `hbound` for the
coefficient), no dead `have`s (the GBM review's dead `hM0` is not repeated), the two-term `f_tt`
bound handled cleanly, and the constant-coefficient scope stated honestly (adapted coefficients named
as the open frontier). The refactor is behavior-preserving.

**Top recommendation, executed in-session.** The panel flagged one substantive coherence debt the new
theorem *created*: `ito_formula_gbm` was now a ~130-line near-clone of its own generalization. Per the
repo's anti-parallel-rebuild and cleanup-pass values, this was fixed before close — `ito_formula_gbm`
is re-derived as the `f = S₀·exp`, `X₀ = 0`, `b = m−σ²/2` specialization (`obtain` + `simp [zero_add]`
+ `ring`, ~15 lines), deleting ~130 lines of duplicated bound/derivative apparatus and establishing
the clean hierarchy `ItoFormulaLocalized → ItoFormulaItoProcess → ItoFormulaGBM`.
`discountedGBM_eq_itoIntegral` still consumes `ito_formula_gbm` unchanged.

**Verdict: PASS.** Zero blocking findings; the one coherence debt is paid. corpus 298, axioms-clean.

## 2026-06-28 — corpus 297 — the Itô tower reaches pricing: GBM decomposed by the Itô integral

**Scope.** New proof content in `Foundations/ItoFormulaGBM.lean`: `ito_formula_gbm` (the GBM
Itô decomposition `Ŝ(T) − Ŝ(0) =ᵐ itoIntegralCLM_T gfx + ∫₀ᵀ m·Ŝ ds` via time-localization),
`discountedGBM_eq_itoIntegral` (the `m=0` pure-Itô-integral specialization), and the plateau-slope
lemma `SmoothTrunc.phi'_eq_one_of_lt`. Corpus entries `sc-ito-formula-gbm`, `sc-discounted-gbm-ito`
(both `full`, axioms-clean `[propext, Classical.choice, Quot.sound]`).

**Panel.** Two independent reviewers, four lenses each.

| lens | verdict |
|---|---|
| inspired math | PASS |
| Mathlib/Degenne coherence | PASS |
| zero slop | PASS (after fix) |
| architectural ingenuity | PASS |
| first principles | PASS |
| idiomatic register | PASS |
| concept clarity | PASS |
| beautiful, elegant math | PASS |

**Blocking findings**: one, **fixed before this verdict** — a dead `have hM0 : 0 ≤ S.M₀` (never
referenced; the value bound `hDbd` needs only `abs_nonneg`/`cut_bdd`) was deleted. Also applied a
clean non-blocking dedup: the GBM-value joint continuity, copy-pasted across the three partial
continuity arguments, is now factored into a single `hScont` (each partial is `(const)·Ŝ`).

**Checks that mattered.** (1) This is the **first pricing-ward consumer of the analytic Itô
tower** — closing the standing two-tower disconnect on the Itô side: GBM is now decomposed by the
*genuine* `itoIntegralCLM_T`, not the algebraic `ItoLemma`/`PDEFromIto` tower or the Wald
exponential. (2) The route is the *classic* one and the right idea, not a hack: the GBM value is
`t`-exponential (`exp(a·t)`, `a=m−σ²/2`), which fails the localized formula's `t`-uniform
exp-in-`x` growth, so the formula is applied to the **time-localized** exponent
`S₀ exp(a·φₙ(t)+σx)` (`φₙ=cut`, `n=⌈T⌉₊`) — identity on `[0,T]`, globally bounded off it — and the
cutoff is *invisible in the statement*, eliminated at `T`, `0`, and a.e. `s≤T` by
`hcut_id`/`hcutD1_one`. (3) The `m·Ŝ` drift is *derived*: on `[0,T]` `φₙ=id`, `φₙ'=1`, so the
localization drift `(m−σ²/2)·Ŝ` plus the Itô correction `½σ²·Ŝ` collapse to `m·Ŝ` by `ring`; the
`m=0` corollary shows the cancellation that makes the discounted increment a pure Itô integral.
(4) Coherence: every derivative is a real `HasDerivAt` combinator, every bound a `cutDi_bdd`, every
continuity a `continuous_cut(D1)` — nothing reproved; the only new fact, `phi'_eq_one_of_lt`, is
the minimal honest addition (`at_zero₁` gives unit slope only at `0`; the plateau needs it on all
`|y|<1`, from `id_near` + `HasDerivAt.unique`). The `hbound`/`hDbd`/`hlinx` helpers factor the
common "coef ≤ Cs, ×Ŝ ⇒ ≤ C·exp" / value-bound / clean-`x`-derivative patterns at the right
register.

**Recorded follow-up (non-blocking).** Both reviewers noted `hcut_id`/`hcutD1_one` duplicate the
core of `SmoothTrunc.cut_eventually_id`; extracting them as `SmoothTrunc.cut_eq_id_of_abs_le` /
`cutD1_eq_one_of_abs_lt` in `ItoFormulaLocalized.lean` (and relocating `phi'_eq_one_of_lt` beside
the other `SmoothTrunc` lemmas) would dedup the shared `rw [cut, id_near]; field_simp`. Deferred to
avoid a full rebuild of the localized file and its dependents for a cosmetic coherence gain.

**Verdict: PASS.** Zero blocking findings outstanding; corpus 297, axioms-clean.

## 2026-06-28 — working tree (uncommitted) — corpus 295 — localized (exponential-growth) time-dependent Itô formula: the rung-3 unlock to GBM

**Scope.** New proof content in `Foundations/ItoFormulaLocalized.lean` (`SmoothTrunc`,
`abs_le_of_expGrowth_deriv`, `fCut`/`cutoff_bddDeriv`, `pathIntegral_expGrowth_memLp`,
`boundary_tendsto_L2`, `drift_tendsto_L2`, headline `ito_formula_td_localized`),
`Foundations/BrownianExpMoment.lean` (Brownian marginal exponential moments), and the
strict generalization+exposure of `WeightedQuadraticVariation.tendsto_riemann_continuous`
(global → local `[0,T]` bound) and `measurable_pathIntegral` (drop the uniform bound). Corpus
entry `sc-ito-formula-localized` (`full`, axioms-clean `[propext, Classical.choice, Quot.sound]`).

**Panel.** Two independent reviewers, four lenses each.

| lens | verdict |
|---|---|
| inspired math | PASS |
| Mathlib/Degenne coherence | PASS |
| zero slop | PASS-WITH-NOTES |
| architectural ingenuity | PASS |
| first principles | PASS |
| idiomatic register | PASS |
| concept clarity | PASS |
| beautiful, elegant math | PASS-WITH-NOTES |

**Blocking findings**: none.

**Checks that mattered.** (1) The localization recovers the limit integrand by the Itô
**isometry** (two-way: forward to bound `aₙ`, backward to make `(gfxₙ)` Cauchy) +
completeness + CLM continuity — never an explicit trim-L² realization of `s ↦ f_x(s,B_s)`;
the elegant route. (2) `pathIntegral_expGrowth_memLp` gets its L² bound by Fatou over
left-endpoint Riemann sums + discrete Cauchy–Schwarz × the per-marginal exponential moment —
**no Tonelli, no joint measurability** — which is strictly more than `memLp_pathIntegral_process`
and the honest way to avoid the Carathéodory wall the rest of the tower carefully sidesteps.
(3) The result is *derived*, not assumed: `boundary_tendsto_L2`/`drift_tendsto_L2` target the
**true** `f` (boundary `f(T,B_T)−f(0,B_0)`, drift `f_t+½f_xx`), and the conclusion is the
genuine Itô identity. (4) The single extra cost vs the bounded engine — joint continuity of
`f_t` — is disclosed honestly in the file/headline/corpus docs: the per-variable `HasDerivAt`
hyps give only *separate* differentiability, and exp-growth (unlike a global derivative bound,
which feeds `continuous_uncurry_of_bdd_partials`) does not supply joint continuity. (5)
Consumes the right Mathlib/Degenne machinery throughout (`ContDiffBump` antiderivative,
Gaussian MGF, `Convex.norm_image_sub_le_of_norm_hasDerivWithin_le`,
`Finset.sum_mul_sq_le_sq_mul_sq`, `lintegral_liminf_le`, the existing `itoIntegralCLM_T_norm`
isometry and `tendsto_norm_toLp_sub'` bridge); the WQV change is backward-compatible (the
in-file callers still compile) and genuinely needed by the new lemma.

**Recorded actions.**
1. *(done in this review)* removed dead code the panel found — an unused `have h1` (drift
   integrand bound, `nlinarith` re-derives it) and two unused `hM1 : 0 ≤ S.M₁` (only `M₁²`,
   structurally nonneg, is ever used).
2. *(done in this review)* replaced two trivial-monotonicity `nlinarith`s in `cutD2_bdd`/
   `cutD3_bdd` with the named `le_mul_of_one_le_right`; fixed two deprecated
   `integrable_finset_sum`/`integral_finset_sum` → `…finsetSum`.
3. *(nit, accepted)* `SmoothTrunc.cont₁/cont₂` are derivable from the `hasDeriv` fields; kept
   as a convenience (consumed in four places). `pathIntegral_expGrowth_memLp`'s `0 ≤ K`
   precondition is unused by the proof (K² absorbs the sign) but kept as honest API for the
   bound constant.
4. *(nit, open)* the "reaches GBM/Black–Scholes" applicability claim has no consumer wiring it
   to a pricing module yet — tracked on the roadmap open frontier (the Itô formula against an
   Itô process `∫ f'(X) dX`).



The first time the deep analytic Itô tower feeds a pricing module at the
*integral-law* level (not the drift-algebra level). Two new files:
`MathFin/Foundations/WienerIntegralGaussian.lean` proves the distributional
fact the isometry construction left open — a deterministic-integrand Wiener
integral is Gaussian, `μ.map (wienerIntegralLp B hB T f) = gaussianReal 0 ‖f‖²`
(`wienerIntegralLp_map_eq_gaussianReal`) — by the characteristic-function
route: simple-process Gaussianity (`IsGaussianProcess.of_isGaussianProcess` on
the scaled-increment family + `HasGaussianLaw.map_eq_gaussianReal`, mean 0 from
`IsPreBrownianReal.integral_eval`, variance the Itô isometry
`wiener_assembly_isometry`), lifted to all `L²` by a `|t|`-Lipschitz
characteristic-function bound (`Real.norm_exp_I_mul_ofReal_sub_one_le` + an
`L¹ ≤ L²` estimate on the probability space) feeding `DenseRange.induction_on`,
then `Measure.ext_of_charFun`. Its consumer
`MathFin/FixedIncome/VasicekSDEGaussian.lean` (`vasicekShortRate_hasLaw_gaussian`)
makes the Vasicek SDE terminal law a *theorem*:
`r_T = mean + σ ∫₀ᵀ e^{−κ(T−s)} dB_s ~ N(vasicekSDEMean, σ²(1−e^{−2κT})/(2κ))` —
variance pinned by the FTC integral `∫₀ᵀ e^{−2κ(T−s)} ds` (`vasicekKernel_integral_sq`,
antiderivative `e^{−2κ(T−s)}/(2κ)`), affine transport via
`gaussianReal_const_mul`/`gaussianReal_const_add`. Retires `VasicekSDE.lean`'s
"stated, not derived". Corpus entries `sc-wiener-integral-gaussian`,
`mf-vasicek-sde-terminal-gaussian` (both `full`); corpus 292 → 294, 257 → 259 full.
lake build 8821 jobs (0 errors, 0 sorries; only Degenne-package `sorry` + benign
unused-section-variable warnings); ledger 294/294 fresh; AxiomAudit +
AxiomAuditGen pin both headlines at `[propext, Classical.choice, Quot.sound]`.

Review panel (focused, the 8 lenses + a dedicated mathematical-honesty pass):
**PASS, no blocking findings.** Honesty pass confirmed: the FTC integral is the
claimed value; `κ > 0` (and the weaker `0 ≤ κ` / `κ ≠ 0` in the helpers) are
genuinely necessary, not vacuous; the charFun density argument is gap-free (no
`convert`/`simp` papering over a step); the scope claim (deterministic integrand)
matches what the theorem delivers. Coherence: consumes the upstream Gaussian /
charFun / affine-map API throughout, reproving nothing. The review's one
non-blocking note — a private `lpTwoNormSq` helper duplicating the (private)
`Lp_real_two_norm_sq` in `WienerIntegralL2.lean` — was **resolved**: the
foundational lemma was de-privatised and is now consumed directly, with the
duplicate deleted (no copy). Honest scope: the *deterministic*-integrand case;
the genuinely-random-integrand localized Itô formula remains the open frontier.

## 2026-06-27 — commit 913f969 — corpus 292 — the [0,∞) unbounded-horizon Itô integral as a continuous local martingale

The `[0,∞)` crown of the continuous-time Itô tower. New files
`MathFin/Foundations/ItoIntegralProcessL2Infinite.lean` (the `L²` process
`itoProcessL2Inf`, the `SimpleProcess` clamp `clampSP` + horizon consistency
`itoProcessL2Inf_eq_itoProcessCLM`) and
`MathFin/Foundations/ItoIntegralProcessLocalMartingaleInfinite.lean` (the per-horizon
gluing + the headline `exists_continuous_localMartingale_modification_infinite`); the
`[0,T]` follow-on (`…LocalMartingaleGeneral.lean`) strengthened to also expose per-horizon
`StronglyMeasurable[augFiltration]`. Corpus entry `sc-ito-infinite-local-martingale`
(`full`); `sc-ito-general-local-martingale` updated to the strengthened conclusion. lake
build 8819 jobs (0 warnings, 0 sorries); ledger 292/292 fresh; AxiomAudit pins the headline
at `[propext, Classical.choice, Quot.sound]`.

Three-agent panel (lenses split 1·2·8 / 3·6·7 / 4·5):

| lens | verdict |
|------|---------|
| inspired math quality | PASS |
| Mathlib / BrownianMotion coherence | PASS |
| zero slop | PASS |
| architectural ingenuity | PASS |
| first principles | PASS |
| idiomatic register | PASS |
| concept clarity | PASS (one note, fixed in this commit) |
| beautiful, elegant math | PASS |

**Blocking findings**: none.

**Checks that mattered**: the result is *not* a degenerate witness —
`itoProcessL2Inf t f = E[∫₀^∞ f dB | 𝓕_t]` is a genuine CLM composition and its martingale
property is the honest conditional-expectation tower (not assumed); the glued process is
`0` only off a co-null set (an honest a.e.-modification, not a cheat trivializing
continuity/martingale); the three conclusions (modification at *every* `t`,
everywhere-continuous on all of `ℝ≥0`, real `IsLocalMartingale`) are each derived, none
degenerate; no hidden hypotheses beyond `IsPreBrownianReal` + measurability + pathwise
continuity of `B`. The `clampSP` `SimpleProcess` truncation genuinely preserves
`𝓕(left-endpoint)`-measurability (drop intervals starting past `T`, clamp surviving right
endpoints — *not* both, which would break it); `clampSP_value_sum` factors the three
agreement statistics into one principled identity rather than triplicated case-work. The
key architectural win — horizon-independent integrand ⇒ *global* martingale ⇒ no clamp in
step 4 (vs. the `min·T` clamp of the `[0,T]` follow-on) — is real and load-bearing. No
reproving of Mathlib/Degenne lemmas; `monoMeasureLp` is a clean upstream candidate (Mathlib
has `MemLp.mono_measure`, no packaged CLM), not wrapper-slop.

**Recorded actions**:
1. *(done in this commit)* the `[0,T]` theorem docstring now enumerates the new 4th
   conjunct `(iv) StronglyMeasurable[augFiltration i]` (panel concept-clarity note).
2. *(nit, accepted)* `isCadlag_of_continuous` is re-derived in the `[0,∞)` file because the
   `[0,T]` copy is `private`; a shared public helper is a fold-in for the next touch.
3. *(nit, open)* `monoMeasureLp` is a genuine Mathlib-upstream candidate; route it through
   the BM-upstream triage when that window opens.

## 2026-06-26 (IV) — the general-integrand Itô process as a continuous local martingale (the IsLocalMartingale follow-on) — corpus 291

New file `MathFin/Foundations/ItoIntegralProcessLocalMartingaleGeneral.lean`
(augmentation core + the assembly) + corpus entry `sc-ito-general-local-martingale`
(`full`). Upgrades the gate (III) to Degenne's local-martingale interface:
`exists_continuous_localMartingale_modification` — an everywhere-continuous process
`X` that is a modification of `itoProcessCLM T t φ` for `t ≤ T`, has continuous paths
for **every** `ω`, and is a genuine `IsLocalMartingale` for the **null-augmented**
Brownian filtration `𝓕ᴮ ⊔ 𝓝`. Degenne's `Martingale.IsLocalMartingale` needs paths
càdlàg for every `ω`, forcing the everywhere-continuous representative; on a null set it
can only be repaired while staying adapted if the filtration carries the null sets —
hence the augmentation, whose cond-expectation invariance (`condExp_sup_nulls`) transfers
the L² martingale property to the repaired process.

**Panel**: three independent agents — (math correctness + first principles
[adversarial]), (Mathlib/Degenne coherence + zero slop + idiomatic register),
(skeptic: honest scope + concept clarity + no-overclaim).

| lens | verdict |
|---|---|
| inspired math quality | PASS |
| Mathlib/BrownianMotion coherence | PASS (blocking finding fixed in this commit) |
| zero slop | PASS |
| architectural ingenuity | PASS |
| first principles | PASS |
| idiomatic register | PASS |
| concept clarity | PASS (notes fixed in this commit) |
| beautiful, elegant math | PASS |

**Blocking findings**: one, **fixed in this commit**. The coherence reviewer caught that
`exists_ae_eq_of_sup_nulls` hand-rolled a `MeasurableSpace M` (sets `=ᵐ` an `m₁`-set) that
**is** Mathlib's `eventuallyMeasurableSpace m₁ (ae μ)` — an anti-wrapper reproof of a named
Mathlib construction. Rewritten to consume `eventuallyMeasurableSpace` +
`le_eventuallyMeasurableSpace` directly (the theorem statement, genuinely new, is unchanged);
`condExp_sup_nulls` and the null-augmented filtration were confirmed genuinely absent upstream
(no Mathlib/Degenne "completed filtration" constructor; BM has only the `IsComplete` predicate).

**Notes addressed** (non-blocking, fixed): the "usual conditions" phrasing overclaimed (the
construction adds the **completeness** half only — null sets — not right-continuity); reworded
across the module/`nullsAlg`/`augFiltration` docstrings + the two benchmark scopes. The theorem
docstring mis-cited `condExp_sup_nulls` for *adaptedness* (adaptedness comes from `G ∈ 𝓝`;
`condExp_sup_nulls` transfers the *martingale* property) — corrected, and the "[0,T]" framing
clarified (the martingale property holds **globally** on `ℝ≥0` via the `min · T` freeze; only
the modification clause is horizon-scoped). Scope "impossible" → "not achievable"; "consumes" →
"is built to consume".

**Checks that mattered**:
- **No mathematical hole** (full adversarial trace of all five concerns). The two cruxes
  (`exists_ae_eq_of_sup_nulls`, `condExp_sup_nulls`) are true and correctly proven; the
  `by_cases i ≤ T` martingale-identity transfer at clamped indices `min i T ≤ min j T` is valid
  in both branches (L² identity for `i ≤ T`; cond-exp of an already-`𝓕_i`-measurable terminal
  value for `T < i`); the `min · T` clamp genuinely yields a **global** martingale without
  needing values past `T` (the standard "freeze a `[0,T]` martingale" device, not degenerate).
- **The `IsLocalMartingale` is genuine, not vacuous**: it is obtained by first proving the
  strictly stronger `Martingale` (everywhere-continuous, frozen past `T`) and downgrading via
  `Martingale.IsLocalMartingale` (Degenne's `Locally.of_prop` with the constant `τ ≡ ⊤`). The
  result therefore *under*-claims relative to what is proved.
- **The null augmentation earns its keep** exactly at adaptedness: the good set `G = Nᶜ` is
  co-null but **not** `natFiltration`-measurable, so `𝓝` is what keeps the everywhere-continuous
  representative adapted (`stronglyMeasurable_of_tendsto` on the pointwise limit of
  `G.indicator`(simple integrals), each `natFiltration`-measurable, `G ∈ 𝓝`).
- **Axioms-clean** `[propext, Classical.choice, Quot.sound]` (AxiomAudit pin); `lake build`
  green (8817 jobs); ledger 291/291 fresh; pytest 19/19.

## 2026-06-26 (III) — continuous modification of the general-integrand Itô process (the gate) — corpus 290

New file `MathFin/Foundations/ItoIntegralProcessContinuousModification.lean`
(13 declarations) + corpus entry `sc-ito-general-continuous-modification`
(`full`). The first pathwise-regularity result for the **general** integrand:
`exists_continuous_modification_itoProcess` — the L²-valued process
`itoProcessCLM T t φ` has a pathwise-continuous modification on `[0,T]`
(modification a.e. at every `t ≤ T` + a.s. continuous paths). The
tower→pricing gate.

**Panel**: three independent agents — (coherence + idiomatic + slop),
(soundness [adversarial] + ingenuity + first principles), (skeptic: integrity
+ honesty + concept clarity).

| lens | verdict |
|---|---|
| inspired math quality | PASS |
| Mathlib/BrownianMotion coherence | PASS |
| zero slop | PASS |
| architectural ingenuity | PASS |
| first principles | PASS |
| idiomatic register | PASS |
| concept clarity | PASS (blocking finding fixed in this commit) |
| beautiful, elegant math | PASS |

**Blocking findings**: one, **fixed in this commit**. All three reviewers
independently flagged the **module docstring** (`:16-17`, `:27-28`) stating the
modification is "packaged as a continuous (hence local) martingale" and "is a
continuous L² martingale — hence an `IsLocalMartingale`" — content the file does
**not** prove (it delivers only the modification + pathwise continuity). The
gating benchmark `formalization_scope` was already honest (defers
`IsLocalMartingale`); only the in-file prose overstated. Reworded to describe the
continuous modification as the *input* the localized calculus will consume, with
the `IsLocalMartingale` packaging an explicit follow-on (it needs paths càdlàg for
every `ω`, hence an augmented filtration / "usual conditions" that `natFiltration`
does not carry — B3 sidesteps this only because the *simple* process is continuous
and adapted for every `ω`).

**Checks that mattered**:
- **No mathematical hole** (full adversarial trace). The constants are exact:
  per-term tail `μ(Aₙ) ≤ εₙ⁻¹·2·2⁻ⁿ = 2·(2/3)ⁿ` (summable), uniform tail
  `dist (fₙ) X ≤ (3/4)ⁿ/(1−3/4) = 4·(3/4)ⁿ` (the `dist_le_of_le_geometric_of_tendsto₀`
  output, no off-by-one). The **two-rate coupling** is the crux and is valid:
  Borel–Cantelli needs `Σ εₙ⁻¹·2⁻ⁿ < ∞`, uniform-Cauchy needs `Σ εₙ < ∞`; with
  `εₙ = (3/4)ⁿ ∈ (½,1)ⁿ` both converge. Index shifts (`summable_nat_add_iff N`,
  `tendsto_add_atTop_nat n`, `hN (k+n)` justified by `N≤n≤k+n`) carry no off-by-one.
- **Coherence**: nothing upstream reproved. Degenne's `maximal_ineq_norm` is
  applied **directly in continuous time** (right-continuity from B3) — better than
  the spec's planned continuous-sup→countable-sup reduction. Non-redundant *and
  stronger*: Degenne's general càdlàg modification (`exists_modification_isCadlag`)
  is `sorry`-backed; the L²+Doob route yields a genuinely **continuous** version.
- **Integrity**: `sorry`-free, axiom-clean. `AxiomAudit.lean` pins
  `itoContinuousMod_modification` / `_continuousOn` / `exists_continuous_modification_itoProcess`
  to exactly `[propext, Classical.choice, Quot.sound]`; the whole 13-lemma chain feeds
  the capstone, so the clean print certifies the chain (including the consumed
  `maximal_ineq_norm`). The `full` claim is honest: the headline is the genuine
  "continuous modification exists" statement (both clauses about the same `X`,
  non-vacuous comparison target), faithfully 1:1 re-exported; the benchmark scope
  correctly discloses the `[0,T]` horizon and defers `[0,∞)` / localized-Itô /
  `IsLocalMartingale`.
- **Elegance win (recorded)**: the implementation uses weak-(1,1) + `L¹ ≤ L²` (one
  monotonicity step, never squares the L² norm) where the spec proposed weak-(2,2)
  with `εₙ = 2^{-n/2}`. Cleaner first-principles math; keep it.

**Recorded actions**:
1. *(done this commit)* docstring honesty fix — the blocking finding above.
2. *(done this commit)* idiom: `field_simp` → explicit `inv_mul_cancel₀ hε.ne'`
   for `ε⁻¹·(ε·x) = x`; `nlinarith [pow_nonneg …]` → `linarith [pow_nonneg …]` (the
   goal `a + a·2⁻¹ ≤ 2a` is linear in the atom `a = (2⁻¹)ⁿ`).
3. *(done this commit)* `omit hB in` on the `itoContinuousMod` def, making its
   non-dependence on the pre-Brownian property explicit (matches the file's `omit`
   discipline; `include` did not force `hB` into the def, but the marker is honest).
4. *(nit, open)* minor duplication: the `Iic T = Icc 0 T` conversion (×2) and the
   `(V−W).val = V.val − W.val := rfl` + `itoSimpleProcess_sub` point-linearity
   (×2). Fold into helpers on next touch; consider relocating `itoSimpleProcess_sub`
   beside `_add`/`_neg` in the B1a module for reuse.
5. *(deferred, scoped)* the `IsLocalMartingale` framing needs augmented-filtration
   ("usual conditions") infrastructure that `natFiltration` lacks — a separate
   deliverable, honestly disclosed in the benchmark scope and the module docstring.

## 2026-06-26 (II) — d-asset one-period FTAP: reduced_core → FULL — corpus 289

**Scope**: dropping the non-redundancy hypothesis from the **d-asset** one-period FTAP, this
session. `Foundations/FTAPOnePeriodVector.lean` was generalised from
`Y : Ω → EuclideanSpace ℝ (Fin d)` to a discounted return valued in any **finite-dimensional**
real inner-product space `F` (the `ℝᵈ` market is the instance `F = EuclideanSpace ℝ (Fin d)`),
and the coercivity/minimiser machinery was rebuilt around the **gains kernel**
`N = gainsKernel = {θ : ⟪θ,Y⟫ = 0 a.e.}`: the softplus potential is constant along `N` and
coercive on `Nᗮ`, so it is minimised over `Nᗮ` and — being `N`-translation-invariant — a
minimiser there is **automatically global** over all of `F`. This discharges the old `hndg`
assumption entirely; the first-order-condition lemma and the whole Esscher/`withDensity` EMM
block are reused verbatim. The corpus entry `mf-ftap-one-period-vector` is now **`full`**
(254 full + 18 wrappers = 272/289 delivery-ready, 17 reduced cores). Library green
(`lake build` 8814 jobs), axioms-clean (`[propext, Classical.choice, Quot.sound]`), ledger
289/289 fresh, pytest 19/19, zero warnings/sorries.

| lens | verdict |
| --- | --- |
| inspired math quality | PASS |
| Mathlib/BrownianMotion coherence | PASS |
| zero slop | PASS |
| architectural ingenuity | PASS |
| first principles | PASS |
| idiomatic register | PASS |
| concept clarity | PASS (after fix) |
| beautiful, elegant math | PASS |

**Panel**: three independent review agents, lenses grouped (1+4+5+8 / 2+3+6 / clarity+faithfulness),
reading the module, the corpus entry, and `coverage.md` read-only against the pinned Mathlib (no Lean
run — the daemon held the local Lean slot). Initial outcome **2 PASS + 1 BLOCK**.

**Honesty — the "full" claim, verified clean**: the headline `ftap_one_period_vector` carries
**only** `Measurable Y` — no integrability, no boundedness, no non-redundancy. `NoArbitrage` is the
genuine textbook NA; `IsEMM` carries true equivalence (`Q ≪ P` **and** `P ≪ Q`), `Integrable Y Q`,
and `∫ Y ∂Q = 0`. The redundant-everything case (`Nᗮ = ⊥ ⟺ Y =ᵐ 0`) is handled explicitly
(`Q = P`); redundant directions are absorbed by the `Nᗮ`-minimisation + `N ⊔ Nᗮ = ⊤` decomposition,
with `N ⊓ Nᗮ = ⊥` (via `inner_right_of_mem_orthogonal`) keeping the `Nᗮ`-coercivity honest.
`FiniteDimensional F` is the d-asset model itself (Föllmer–Schied 1.6), not a narrowing. The panel
confirmed no hidden hypothesis sneaks the restriction back in.

**Coherence / ingenuity**: no reproved lemma — the orthogonal-complement API (`isCompl_orthogonal`,
`sup_orthogonal_of_hasOrthogonalProjection`, `inner_right_of_mem_orthogonal`,
`closed_of_finiteDimensional`, `orthogonal_orthogonal`, `bot_orthogonal_eq_top`), extreme-value,
Fermat, and differentiation-under-the-integral are all consumed upstream. Generalising to abstract
`F` is the **minimal-interface** move (the proof uses only the inner product + finite-dimensionality,
never a coordinate basis), making `ℝᵈ` and even the scalar `ℝ` free instances; the verbatim reuse of
the FOC + `withDensity` block is good factoring.

**Blocking finding (remediated before this verdict)**: the corpus entry's **metadata** prose (`name`
"…Non-Redundant", `description`, and especially `formalization_scope` "…NARROWER… assumes the market
is NON-REDUNDANT… the redundant-asset generalisation… remain out of scope") still described the
pre-upgrade reduced core, flatly contradicting the `full` status flipped one field above — a
restriction-in-disguise surfaced in metadata, exactly what the values gate exists to catch. Plus
`coverage.md` listed the now-closed d-asset case as an open follow-on. All synced to the full theorem.

**Recorded actions**:
1. *(done this verdict)* Corpus `name` / `description` / `formalization_scope` for
   `mf-ftap-one-period-vector` rewritten to the full statement; `coverage.md` live-status +
   open-follow-ons line corrected (only the general-Ω multi-period DMW remains open).
2. *(done this verdict)* `set F`/`F'` in `hasDerivAt_potential_dir` renamed to `Φ`/`Φ'` (they
   shadowed the market type `F`); two unused `set N := … with hN` binders dropped; the scalar sibling
   `FTAPOnePeriod.lean`'s `## Scope` (which still called the d-asset case open) repointed at the
   now-complete `ftap_one_period_vector`.
3. *(done — follow-up commit)* The `isEquivProbMeasure_withDensity` cross-file dedup is landed: new
   shared module `Foundations/EquivMeasure.lean` (a measurable, strictly-positive, normalised density
   → equivalent probability measure: `IsProbabilityMeasure` ∧ `Q ≪ P` ∧ `P ≪ Q`), consumed at all
   **four** sites (the two `FTAPOnePeriodVector` densities + the two scalar `FTAPOnePeriod` densities),
   each `obtain ⟨…⟩ := isEquivProbMeasure_withDensity P … ; rw [← h…def] at …`. Term-preserving
   extraction, net −~40 lines of duplicated ritual; the helper bundles four Mathlib lemmas consumed
   four times (a real abstraction, not a thin wrapper — zero-slop / coherence). lake build 8815 jobs,
   ledger 289/289 fresh, pytest 19/19, axiom-clean.
4. *(noted, kept)* "Esscher" stays the project's chosen label for the softplus/logistic construction
   (the density is the bounded logistic `σ`, not the raw exponential tilt); the body shows `σ`
   explicitly, so no reader is misled.

**The actual crown still open**: the general-Ω **multi-period** DMW (L⁰-cone closedness + measurable
selection), unchanged by this rung.

## 2026-06-26 — commit bc9a258 — corpus 289

**Scope**: the **d-asset** one-period FTAP (Föllmer–Schied Thm 1.6, non-redundant
markets), this session. New proof content: `Foundations/FTAPOnePeriodVector.lean`
(~580 lines) — the vector model (`NoArbitrage`, `IsEMM` over `EuclideanSpace ℝ (Fin d)`),
the forward direction, the **softplus potential** `f(θ)=∫ log(1+exp⟪θ,Y⟫)` with its
logistic derivative, differentiation under the integral (`hasDerivAt_potential_dir`),
coercivity (`exists_pos_lower_bound`), the global minimiser (`exists_global_min_potential`),
the first-order condition (`integral_logistic_smul_eq_zero`), the integrable Esscher-EMM
core, the bounded-density reduction, and the biconditional `ftap_one_period_vector`; one
`reduced_core` corpus entry (`mf-ftap-one-period-vector`). Library green (`lake build`
8814 jobs), axioms-clean (`[propext, Classical.choice, Quot.sound]`), ledger 289/289 fresh,
pytest 19/19.

| lens | verdict |
| --- | --- |
| inspired math quality | PASS |
| Mathlib/BrownianMotion coherence | PASS |
| zero slop | PASS |
| architectural ingenuity | PASS |
| first principles | PASS |
| idiomatic register | PASS |
| concept clarity | PASS |
| beautiful, elegant math | PASS |

**Panel**: three independent review agents, lenses grouped (1+2+8 / 3+4+5 / 6+7), reading
`FTAPOnePeriodVector.lean` read-only against the pinned Mathlib (no Lean run — the daemon
held the local Lean slot).

**Honesty — the headline checks, verified clean**: the backward direction **constructs**
the EMM, never posits it. The Esscher density `z = σ⟪θ₀,Y⟫` is the first-order condition of
a genuine optimisation: the softplus potential is convex and finite on all of `ℝᵈ` (the
`log(1+exp)` tempering avoids the exponential-moment restriction of the classical Esscher
tilt while keeping `σ ∈ (0,1)` for a uniform `L¹` domination), coercivity comes from the
**attained** unit-sphere minimum of `g(θ)=∫⟪θ,Y⟫⁺` (genuinely needing both no-arbitrage —
applied to `−θ` — and non-redundancy), the minimiser exists by compactness, and its FOC
`∫ Y·σ⟪θ₀,Y⟫ = 0` is real differentiation under the integral
(`hasDerivAt_integral_of_dominated_loc_of_deriv_le` + `IsLocalMin.hasDerivAt_eq_zero`,
scalarised per direction then assembled via `inner_self_eq_zero` — strictly less machinery
than a Fréchet-derivative route). Nothing is a definitional `rfl`. Non-redundancy enters
**only** the coercivity step (one `apply hndg`), is honestly the `reduced_core` narrowing,
and is named in the module `## Scope`, the theorem docstring, and the corpus scope.

**Coherence / ingenuity checks**: no reproved lemma — parametric differentiation, Fermat,
extreme-value, Lipschitz, inner/integral, and `withDensity` APIs are all consumed upstream.
`lipschitzWith_integral_inner` is a clean reusable abstraction ("averaging a 1-Lipschitz
function of `⟪θ,Y⟫` is `(∫‖Y‖)`-Lipschitz"), consumed for both the potential and the
positive-gain average so continuity falls out of Lipschitz for free. The integrable-core →
reduction → biconditional layering and the single `d = 0` empty-market split (at the first
point `Nonempty (Fin d)` is needed) are the right shape.

**Blocking findings**: none.

**Recorded actions**:
1. *(done this verdict)* Module `## Scope` now lists **non-redundant** among the
   restrictions and the **redundant** one-period d-asset case (quotient by the gains kernel)
   among the open follow-ups — the panel's one substantive clarity gap (the narrowing was
   stated everywhere except its dedicated Scope block).
2. *(done this verdict)* Intro wording sharpened: `z = σ⟪θ₀,Y⟫` is the unnormalised **weight**;
   its normalisation `z/E[z]` is the EMM density.
3. *(done this verdict)* Dead `with hz` binder dropped (the unused-variable linter does not
   flag `set … with`).
4. *(considered, deferred)* The "equivalent probability measure from a strictly-positive
   normalised density" block (`IsProbabilityMeasure` + `Q≪P` + `P≪Q` via `withDensity`)
   recurs ~3× across this file and the scalar `FTAPOnePeriod.lean`. Both panellists flagged a
   shared `isEquivProbMeasure_withDensity` helper. It is a **cross-file** dedup of ritual (the
   densities — logistic Esscher vs `(1+‖Y‖)⁻¹` tempering — differ), judged a non-blocking
   cleanup-pass opportunity; deferred to a dedicated cross-file pass so the two FTAP files
   move together.
5. *(noted, kept)* Three `classical` (lines 278/393/471) read defensively; standard idiom,
   removability unconfirmed without a compile. Kept.

## 2026-06-25 — commit a5197ee — corpus 288

**Scope**: the general-Ω one-period Fundamental Theorem of Asset Pricing
(Föllmer–Schied Thm 1.55 / one-period Dalang–Morton–Willinger), shipped this session.
New proof content: `Foundations/FTAPOnePeriod.lean` — the scalar L⁰ model
(`NoArbitrage`, `IsEMM` with mutual absolute continuity), the forward direction
`noArbitrage_of_isEMM`, the balancing-density core `exists_isEMM_of_pos_tails`
(EMM `Q = P.withDensity (λ·𝟙_{Y≥0} + μ·𝟙_{Y<0})`, weights solved so `Y` is fair), the
scalar no-arbitrage dichotomy + integrable backward `exists_isEMM_of_noArbitrage_integrable`,
the integrability-dropping reduction `exists_isEMM_of_noArbitrage` (equivalent
`P̃ = P.withDensity (1+|Y|)⁻¹/κ`), and the biconditional
`ftap_one_period : NoArbitrage ↔ ∃ EMM`; one `full` corpus entry
(`mf-ftap-one-period-general`). Library green (`lake build` 8813 jobs), axioms-clean
(`[propext, Classical.choice, Quot.sound]`), ledger 288/288 fresh, pytest 19/19.

| lens | verdict |
| --- | --- |
| inspired math quality | PASS |
| Mathlib/BrownianMotion coherence | PASS |
| zero slop | PASS |
| architectural ingenuity | PASS |
| first principles | PASS |
| idiomatic register | PASS |
| concept clarity | PASS |
| beautiful, elegant math | PASS |

**Panel**: three independent review agents, lenses grouped (1+2+8 / 3+4+5 / 6+7),
reading `FTAPOnePeriod.lean` read-only against the pinned Mathlib (no Lean run — the
daemon held the local Lean slot).

**Honesty — the headline checks, verified clean**: the backward direction genuinely
**constructs** the EMM, never posits it. `exists_isEMM_of_pos_tails` builds
`Q = P.withDensity (ofReal Z)` with `Z = λ·𝟙_{Y≥0} + μ·𝟙_{Y<0}`, the weights **solved**
from the fairness + normalisation 2×2 system (`D = −c·P(s) + a·P(sᶜ)`, `λ = −c/D`,
`μ = a/D`), with `D > 0` proved by a genuine case-split on `P(s)=0`; `∫Z=1` and `∫Z·Y=0`
are then *derived* (`field_simp; ring` bottoming out in the chosen weights, not a
definitional `rfl` — the `test_values.py` rfl-tripwire does not fire). The scalar
dichotomy (`θ=±1` annihilates a one-signed `Y`) upgrades the weak tail inequalities to
strict via `integral_eq_zero_iff_of_nonneg_ae` on the restricted measure — real
measure-theoretic work. Mutual absolute continuity `Q ~ P` is established from the
strictly-positive density on **both** sides (`withDensity_absolutelyContinuous` / `…'`),
never assumed. Scope honest in module docstring + corpus `formalization_scope` +
`coverage.md`: one period, one scalar asset, arbitrary Ω; the general-Ω **multi-period**
DMW (measurable selection) and the d-asset case named as open.

**Coherence / ingenuity checks**: library consumption is clean — no reproved lemma. The
one bespoke helper `hsplit` (`∫ Z·g = λ·∫_s g + μ·∫_sᶜ g`) is the problem-specific
two-region decomposition over `integral_add_compl`, not a re-derivation of additivity.
The elementary Föllmer–Schied route (bounded-density reduction + scalar dichotomy +
balancing `withDensity`) is the inspired choice: it avoids Hahn–Banach / Kreps–Yan
precisely because the one-period scalar case makes the EMM *explicit* — the verified
contrast with the finite-Ω sibling `ftap_discrete`, which *does* route through
`exists_pos_dual_of_disjoint_stdSimplex`. The 5-theorem decomposition cuts at the right
joints: `exists_isEMM_of_pos_tails` is a reusable quantitative core knowing nothing of
no-arbitrage; integrability is dropped in a separate, conceptually-orthogonal reduction
rather than inlined.

**Blocking findings**: none.

**Recorded actions**:
1. *(done this verdict)* Dead `with hsdef` binders removed from both
   `exists_isEMM_of_pos_tails` and `exists_isEMM_of_noArbitrage_integrable`
   (`set s := … with hsdef` where `hsdef` was never referenced — a dead hypothesis, the
   panel's one concrete slop flag).
2. *(done this verdict)* Down-weight renamed `m → μ` (`lam`/`mu` for `λ`/`μ`) so the
   up/down symmetry the docstrings describe is literal in the source — flagged by two
   panellists (idiomatic register + elegant math).
3. *(considered, kept)* The two sign-asymmetric contrapositive tail blocks (`{Y≥0}`
   direct, `{Y<0}` via `−Y`) and the ~6-line `withDensity`-⇒-equivalent-probability
   boilerplate shared by the two existence theorems. Both panellists judged a `wlog` /
   shared `equivProbOfDensity` abstraction below the threshold where factoring pays (the
   sign-flip is genuine math; the boilerplate is over two differently-named densities at
   the only two sites). Kept; revisit if a third site appears.
4. *(nit, kept)* `exists_isEMM_of_noArbitrage`'s docstring states `κ = ∫ w ∈ (0,1]` while
   the proof establishes/uses only `0 < κ` (upper bound true but unused). Kept as honest
   exposition of the object — proving an unused `κ ≤ 1` would itself be slop.

## 2026-06-25 — commit 74e94b6 — corpus 287

**Scope**: the finite-Ω Fundamental Theorem of Asset Pricing (Harrison–Pliska /
finite Dalang–Morton–Willinger), shipped this session to public `main`. New proof
content: `Foundations/ConvexSeparation.lean` (the separating-dual kernel
`exists_pos_dual_of_disjoint_stdSimplex`); `Foundations/FTAPMultiState.lean`
backward direction + biconditional `hasEMM_multi_iff_not_hasArbitrage`;
`Foundations/FTAPDiscrete.lean` (the multi-period model `NoArbitrage`/`IsEMM`, both
directions, `ftap_discrete : NoArbitrage ↔ ∃ EMM`); two `full` corpus entries
(`mf-ftap-discrete-complete`, `mf-ftap-single-period-complete`). Also a build-env fix
(`7b15319`, warm REPL daemon on v4.31 — infra, not proof content). Library green,
axioms-clean, ledger 287/287 fresh, pytest 19/19.

| lens | verdict |
| --- | --- |
| inspired math quality | PASS |
| Mathlib/BrownianMotion coherence | PASS-WITH-NOTES |
| zero slop | PASS-WITH-NOTES |
| architectural ingenuity | PASS |
| first principles | PASS |
| idiomatic register | PASS |
| concept clarity | PASS-WITH-NOTES |
| beautiful, elegant math | PASS-WITH-NOTES |

**Panel**: four independent review agents, lenses paired (3+6 / 2+4 / 5+7 / 1+8),
reading the new files read-only (no Lean run — the daemon held the local Lean slot).

**Honesty — the headline checks, verified clean**: the backward direction genuinely
**constructs** the EMM from no-arbitrage (gains subspace disjoint from the simplex →
`geometric_hahn_banach_compact_closed` → strictly-positive dual → `PMF` measure → the
one-step martingale property via `ae_eq_condExp_of_forall_setIntegral_eq`) — `Q` is
built, never posited. `IsEMM.mart`'s one-step-up-to-`T` form is the **faithful**
finite-horizon object (`S` genuinely need not be a `Q`-martingale past `T`); it is
proved via the textbook set-integral condExp characterisation and consumed
substantively by the forward telescoping, so the biconditional is non-trivial both
ways. The full-support hypothesis `∀ ω, 0 < P {ω}` is standard finite-state hygiene
(makes `~P` ≡ full support and `ᵐ[P]` ≡ pointwise), not a trivialiser, and is not
droppable without a messier theorem. Scope stated honestly in three places (module
docstrings, corpus `formalization_scope`, `coverage.md`) — "finite case of DMW"; the
general-Ω multi-period crown (L⁰-closedness + measurable selection) is named as open.

**Coherence / ingenuity checks**: `martingaleTransform_add`/`_smul` are genuinely new
(Mathlib has only `martingalePart` linearity for the Doob decomposition — a different
object; no `martingaleTransform` upstream). The separating-dual kernel is consumed by
**both** the single-period multi-state and the multi-period scalar backward
directions — genuine reuse at the right altitude. The forward-direction overlap with
`FTAP.emm_implies_no_arbitrage` is **not** a missed factoring: the honest
finite-horizon one-step `IsEMM` is strictly weaker than the all-time `Martingale` the
abstract forward (and `martingaleTransform_isMartingale`) require, so no shared core
is extractable without weakening the theorem — the hand telescoping is forced and
correct. The global-separation architecture is decisively the elegant route for
finite Ω (vs per-atom backward induction + gluing).

**Blocking findings**: none.

**Recorded actions**:
1. *(done this verdict)* Stale public-doc claims corrected — all three **under**-stated
   the work after this session: `README.md` (FTAP line said "multi-state forward" →
   now multi-state biconditional + multi-period finite-Ω biconditional),
   `FTAPMultiState.lean` module header (said "forward direction / backward not attempted
   here" → "both directions"), `FTAPTwoState.lean` cross-ref (mis-cited
   `NoArbitrageDerivations` for the general forward → `FTAPMultiState`).
2. *(done this verdict)* The "full-support ⇒ null set empty" reasoning, written twice in
   `FTAPDiscrete.lean` (`gains_disjoint_stdSimplex` + `exists_isEMM_of_noArbitrage`),
   extracted to one `private lemma eq_empty_of_pos_singleton` consumed at both sites.
3. *(considered, kept)* `FTAPDiscrete.lean`'s file-wide
   `set_option linter.unusedSectionVars false` (the repo's only such suppression; house
   style is `omit … in`). Switching needs **five** `omit` clauses — the two algebraic
   lemmas, the span-induction, and `gains_disjoint`/`noArbitrage_of_isEMM` all use
   heterogeneous subsets of the rich shared `variable` context — noisier than one
   suppression. Kept with an explanatory comment; revisit if the file is split.
4. *(nit, open)* `ConvexSeparation.lean:84–101` hand-rolls "a linear functional equals
   the coordinate-sum of its standard-basis values" + a sign-flip `calc`; correct but
   ~12 lines more verbose than a `Pi.basisFun`/`Finset.sum_pi_single` collapse. Sharpen
   on next touch of the file.

## 2026-06-24 — commit 4e921c4 — corpus 285

**Scope**: the v4.31 toolchain bump + full-library port (branch
`bump-bm-mathlib-4.31`: ~36 MathFin files across the BrownianMotion `d6f23da`
+ Mathlib `v4.31.0` + toolchain `v4.31.0` co-bump) and the lint-cleanup commit
`4e921c4`. Mechanical drift-fixing — no new theorems, no benchmark entries added
(corpus unchanged at 285). Library green (8810 jobs), axiom-clean.

| lens | verdict |
| --- | --- |
| inspired math quality | PASS |
| Mathlib/BrownianMotion coherence | PASS |
| zero slop | PASS |
| architectural ingenuity | PASS |
| first principles | PASS |
| idiomatic register | PASS |
| concept clarity | PASS |
| beautiful, elegant math | PASS-WITH-NOTES |

**Panel**: three independent review agents, lenses split (2+3 / 4+5+6 / 1+7+8),
reading `git diff origin/main...HEAD -- MathFin/` read-only (no Lean run — the
ledger build held the one local Lean slot).

**Statement integrity (the port's #1 risk) — verified clean**: every changed
`theorem`/`lemma`/`def` signature is exactly one of (a) `IsPreBrownian` →
`IsPreBrownianReal` rename, (b) instance binder `[hB]` → explicit `(hB)` +
`include`/`omit hB in` (same hypothesis, v4.31-mandated since it is now a `Prop`),
or (c) a definitionally-equal reformulation (`max (t-s)(s-t)` ↔ `nndist ↑t ↑s`,
`B t - B s` ↔ `fun ω => B t ω - B s ω`). No hypothesis dropped, no conclusion
weakened, no measure/variance changed to a non-equal value. Deprecations migrated
1:1 to the non-deprecated upstream lemma (`measure_sdiff`, `FunLike.coe_*`,
`apply_sup'_eq_sup'_comp`, `zero_le`, unqualified CLM `*_apply`) — consumed, not
wrapped. The cleanup removed only provably-dead tactic arms + a no-op `change` +
unused simp args; no live step lost. Docstrings updated in lockstep (incl. the
`@[blueprint]` spine); exhaustive grep found zero surviving `IsPreBrownian` or
deprecated-name references in changed files.

**Blocking findings**: none.

**Benchmark corpus**: the ledger sweep surfaced that the port had been
library-only — 20 benchmark snippets (the inline re-exports in `benchmarks/*.json`)
still used the v4.30 API. All 20 were ported: explicit `(hB : IsPreBrownianReal …)`
threading with `hB` as the re-exported lemma's first argument, and the BM-API
renames (`IsPreBrownian.isMartingale`→`IsPreBrownianReal.isMartingale`,
`memHolder_mk`/`mk` now on `IsPreBrownianReal`). `bm-prop-5.1.2` was the one that
looked like a removed constructor (`IsGaussianProcess.isPreBrownian_of_covariance`)
but is in fact *absorbed into Mathlib* as `IsGaussianProcess.isPreBrownianReal_of_covariance`
(`Mathlib.Probability.BrownianMotion.Basic`) — same min-covariance characterization,
so it stays a faithful one-line library_wrapper. All **285** ledger entries now
re-verify fresh under the v4.31 pins (`lake env lean` per snippet); pytest 19/19.

**Recorded actions (non-blocking, next-session tidy)**:
1. *(nit)* `Foundations/ItoIntegralBrownian.lean:251` — `riemannFn` `def` sits under
   an active `include hB` with no `omit hB in`, so it carries a vacuous `hB` argument
   (harmless; build green). Inconsistent with the file's own `omit hB in` discipline;
   one-line fix deferred (it touches `riemannFn`'s callers, so out of scope for a
   mid-finalize edit on the memory-constrained box).
2. *(minor)* `BlackScholes/StrikeGreeks.lean:136/141` — `hasDerivAt_bsV_K` declares
   two side conditions for `K·σ·√τ` (`≠ 0` and `0 <`); `field_simp` may not need both.
   No unused-variable warning fired (both are referenced), so it is at most a
   functional redundancy — confirm with a build which (if either) is droppable.
3. *(nit)* the `nndist ↑t ↑s = (t-s)` bridge is hand-inlined ~7× (QuadraticVariationL2,
   BrownianMartingale, ItoFormulaRemainder, WienerIntegral); orientations differ per
   site, but a shared helper would DRY it.
4. *(nit)* the `convert … <;> try rfl` / `<;> first | rfl | ring` module-instance-diamond
   closer idiom is marginally noisier than the pre-bump closers — the honest minimal
   response to the v4.31 elaborator (drives the lone PASS-WITH-NOTES on lens 8), not
   obfuscation. The `StrikeGreeks` rewrite to `congr_deriv` + named value lemmas is a
   net clarity gain.

**Verdict: PASS-WITH-NOTES** — a faithful mechanical port that preserves every
statement and improves coherence (current API) and one proof's legibility; the only
blemishes are cosmetic idiom noise and one vacuous-binder nit, none blocking.

## 2026-06-23 — commit 2e23025 — corpus 285

**Scope**: D1 — covariation of Itô integrals (the bilinear Itô isometry).
`Foundations/ItoIntegralCovariation.lean` + umbrella import, 4 AxiomAudit pins,
benchmark `sc-ito-covariation-bilinear-isometry` (full), roadmap/coverage notes.
The `[0,T]` Itô CLM is bundled as a `LinearIsometry` (`itoIsometry_T`);
polarization (`LinearIsometry.inner_map_map`) gives `⟪∫φ dB, ∫ψ dB⟫ = ⟪φ, ψ⟫`
(`inner_itoIntegralCLM_T`); `L2.inner_def` unfolds the μ-side to the expectation
form `𝔼[(∫φ dB)(∫ψ dB)] = ⟪φ, ψ⟫` (`covariation_itoIntegralCLM_T`); the diagonal
`φ = ψ` recovers the isometry (`variance_itoIntegralCLM_T`).

**Panel**: three agents — (Mathlib/Degenne coherence + idiomatic register + zero
slop), (concept clarity + first principles + honest scope), (inspired/beautiful
math + architectural ingenuity + AxiomAudit honesty floor).

| lens | verdict |
|---|---|
| inspired math quality | PASS |
| Mathlib/BrownianMotion coherence | PASS |
| zero slop | PASS |
| architectural ingenuity | PASS |
| first principles | PASS |
| idiomatic register | PASS |
| concept clarity | PASS |
| beautiful, elegant math | PASS |

**Blocking findings**: none.

**Checks that mattered**: the Mathlib lemmas (`LinearIsometry.inner_map_map`,
`L2.inner_def`, `RCLike.inner_apply`, `conj_trivial`, `real_inner_self_eq_norm_sq`,
`ContinuousLinearMap.coe_coe`) were each cross-checked against ledger-verified
sibling files that use them identically; nothing of B1's isometry is reproved
(the bilinear law is pure polarization of `itoIntegralCLM_T_norm`); the bundled
`LinearIsometry` is novel in the repo (no other `→ₗᵢ[` for the Itô integral) and
is the genuine reusable artifact, not a wrapper-to-inline; `mul_comm` in the
`simpa` is load-bearing, not masking a mismatch (sibling `ItoIntegralL2Dense`
confirms `⟪x,y⟫_ℝ` reduces second-argument-first under this pin); `[IsProbabilityMeasure μ]`
is genuinely required (the CLM needs it; `IsPreBrownian` does not imply it);
`full` status is correct (multi-step composition over a bundled definition, not a
one-line wrapper, not a definitional `rfl`); the RHS is honestly the inner product
`⟪φ, ψ⟫` (the `= ∫ φψ d(trim) = 𝔼∫₀ᵀ φψ ds` chain is a true explanatory gloss, not
a literal Lean claim); the `[0,∞)` analog is honestly deferred; the 4 AxiomAudit
pins are correct and complete at `[propext, Classical.choice, Quot.sound]` (no
`sorry`/`sorryAx`).

**Recorded actions**:
1. *(done in this commit)* docstring polish from panel nits — the predictable
   `trim` measure is described as a `.trim` (not `Measure.restrict`), and the
   `variance_` name is justified in-docstring (the Itô integral is centered, so
   its second moment is its variance).
2. *(open, next session)* **D2** — the general-integrand local martingale — is
   gated on a pathwise continuous-modification of the B1b integral (Doob
   L²-maximal inequality → a.s.-uniform limit of the simple approximants), a
   multi-session build; it is the load-bearing prerequisite for localizing the
   Itô formula (`ito_formula_td_L2_bddDeriv`, presently bounded-derivative only)
   to unbounded/GBM coefficients — the analytic-tower → pricing-tower bridge.
3. *(open)* the `[0,∞)` bilinear analog lands cheaply once a named
   full-trim-measure def is exposed in `ItoIntegralL2Dense.lean`.

## 2026-06-13 — commit 839dd06 — corpus 283

**Scope**: Summit B / B3 — the elementary Itô integral as a continuous local
martingale (the localization entry point). `MathFin/Foundations/ItoIntegralProcessLocalMartingale.lean`
(`itoSimpleProcess_pathContinuous`, `itoSimpleProcess_isLocalMartingale`), corpus
entry `sc-ito-simple-process-local-martingale`.

**Panel**: two agents — (A) slop / coherence / first-principles / idiom, with an
explicit no-sorry-dependency audit; (B) does-it-earn-its-place / continuity-hypothesis
honesty / scope honesty / stale docs.

**Findings & resolution**:
- **BLOCKER (honesty, stale docs)** — `docs/roadmap.md` still read "Next: **B3**"
  as future work, and `docs/coverage.md`'s live-status block was stale (corpus
  280 / 263-ready, pre-B2). Both updated to record B2+B3 as delivered (corpus
  283 / 266-ready); `docs/blueprint.md` frontier note extended with the B3
  localization bridge.
- **MINOR (earns-its-place / clarity)** — the module docstring led with the
  "localization entry point" headline, foregrounding the (trivial) local-martingale
  weakening over the genuine new content. Reordered to lead with the **pathwise
  continuity** as the result and present the local martingale as its consequence
  and the upstream-coherence bridge.

**The earns-its-place judgment (both agents)**: the local-martingale statement is
mathematically a one-line weakening of B1a's true `L²` martingale
(`Martingale.IsLocalMartingale`). It clears the bar because the genuine content is
`itoSimpleProcess_pathContinuous` — the **first sample-path regularity result** in
a tower that was otherwise entirely `L²`/in-measure — and the local-martingale is
the honest, canonical framing that connects the integral to Degenne's localization
machinery (the gateway for SDE/Lévy/Girsanov). **Continuity-hypothesis honesty**:
PASS — taking `∀ ω, Continuous (B · ω)` as a hypothesis is the standard pathwise
setting (`IsPreBrownian` fixes only the finite-dim laws; a continuous version
exists by Kolmogorov–Chentsov), stated honestly in three places; consuming
Degenne's KC construction is infeasible for an arbitrary `IsPreBrownian B`.
**No-sorry audit**: PASS — `#print axioms` is `[propext, Classical.choice,
Quot.sound]`; the `isStable_submartingale` `sorry` in upstream `LocalMartingale.lean`
is provably off the `Martingale.IsLocalMartingale` proof path. **Coherence**: PASS —
pure consumption (B1a + `Martingale.IsLocalMartingale` + `itoSimpleProcess_apply`);
the private `isCadlag_of_continuous` is justified plumbing (no `Continuous → IsCadlag`
exists upstream; `IsCadlag` is Degenne-only). **Scope**: PASS — `full` justified,
no overclaim (simple integrands, continuity assumed).

**Verdict: PASS** (one stale-doc blocker + one docstring minor, both fixed). Build
8726 jobs green, axioms-clean; ledger 283/283 fresh; pytest 19.

## 2026-06-13 — commit 6bd9477 — corpus 282

**Scope**: Summit B / B2 — the unbounded-horizon `[0,∞)` Itô integral as a
continuous linear isometry. `MathFin/Foundations/ItoIntegralL2Dense.lean`
(`itoIntegralL2`, `itoIntegralL2_norm`), corpus entry
`sc-ito-infinite-horizon-isometry`, plus de-privatising
`ItoIntegralCLM.setIntegral_eq_zero_of_orthogonal_pred` for reuse. Closes the
σ-finite density gap recorded in `docs/ito-integral-clm-deferred.md`.

**Panel**: three agents over the eight lenses (slop / idiom / clarity;
coherence / first-principles / architecture; inspired / elegant / honesty).

**Findings & resolution** (all fixed before this verdict):
- **BLOCKER (clarity/honesty)** — `ItoIntegralCLM.lean`'s module docstring still
  declared the unbounded-horizon CLM "left gated … not required by any
  downstream pricing module." Now false on both counts (it is built, and this
  file de-privatises a CLM lemma to serve it). Rewritten to point at
  `ItoIntegralL2Dense` and name the consumed bridges.
- **MINOR (slop/idiom)** — five implementation-detail helpers (`iocSP`,
  `uncurry_iocSP_eq`, `inner_simpleAssembly_iocSP`, `itoOrthRect`,
  `aezeroOfOrth`) leaked into the public namespace, against the repo convention
  (only the density theorem + CLM + isometry are public, as in
  `ItoIntegralCLM`/`WienerIntegralL2`). Marked `private`.
- **MINOR (clarity)** — module doc said B2 "removes the horizon bound from
  `itoIntegralCLM_T`"; it is a sibling CLM reusing that file's density
  machinery, not a direct extension. Reworded.
- **MINOR (honesty, stale docs)** — `docs/coverage.md`, `docs/blueprint.md`,
  `docs/roadmap.md`, and the deferred-doc header still listed the
  infinite-horizon variant as open/future. All updated to record B2 as
  delivered; the deferred doc carries a `CLOSED 2026-06-13` stamp.

**Coherence / first principles / architecture** — PASS, unanimous. Pure
consumption of the finite-horizon layer (the `predictableRect` π-system reused
verbatim, T-independent) + Degenne `SimpleProcess` + Mathlib `extendOfNorm` /
`Lp.ae_eq_zero_of_forall_setIntegral_eq_zero`; nothing of the π-system or the
isometry is reproved. The σ-finite-exhaustion argument (per-frame `g =ᵐ 0` via
the finite-horizon lemma, then a null-cover patch over `{0}×univ`) is sound and
formally tight, and is the right architecture — reduce the σ-finite case to the
already-proven finite case rather than rebuild density from scratch (and it
sidesteps the upstream elementary-set π-system gap the deferred doc anticipated
needing). `full` status justified: a genuine theorem, axioms-clean, AxiomAudit-pinned.

**Verdict: PASS** (one blocker + minors, all fixed). Build 8725 jobs green,
axioms-clean; ledger 282/282 fresh; pytest 19.

## 2026-06-12 — commit 867d265 — corpus 281

**Scope**: the deferred per-`t` Itô isometry, now closed —
`MathFin/Foundations/ItoIntegralProcessIsometry.lean` (`itoProcessCLM_norm_sq`:
`‖(φ●B)_t‖² = ∫_{(0,t]×Ω} φ² d(trimMeasure_T T)` `= ∫₀ᵗ E[φ_s²] ds`, for every
predictable `φ ∈ L²([0,T])` and `t ≤ T`) — plus the de-privatisation of the generic
`lp_two_norm_sq` in `ItoIntegralL2` (reused, not copied) and 1 new `full` corpus entry
`sc-ito-general-time-isometry`. This is the refinement B1b openly deferred (the
band-over-trimmed-measure computation).

**Panel**: 3 independent agents — two splitting the eight lenses
(coherence/slop/idiomatic/first-principles; inspired/architecture/clarity/beauty), one
completeness/faithfulness critic (snippet ⊨ theorem, no circularity, AxiomAudit honesty,
de-dup). Read-only, no Lean.

**Per-lens verdicts — all PASS**:
1. *Inspired math* — the L²-energy law that makes the Itô integral an isometric
   embedding at every `t`, not only the terminal; the load-bearing fact behind
   quadratic-variation / hedging-error analysis in continuous time.
2. *Mathlib/Degenne coherence* — consumes B1a's `itoSimpleProcess_isometry_time`, the
   repo's `integral_rectTerm_mul` / `trimMeasure_T_eq_restrict` / `simpleAssembly_T`, and
   Mathlib's `DenseRange.equalizer` / `integral_trim` / `eLpNorm_indicator_le`. The one
   hand-built object `truncCLM` is justified: Mathlib has only the *constant*-indicator
   `indicatorConstLp` and no `Lp→Lp` restriction CLM (confirmed by loogle search).
3. *Zero slop* — every helper load-bearing; stepping-stones `private`; the generic
   `lp_two_norm_sq` de-duplicated rather than copied (the very concern that triggered
   this round). [fix applied: `integral_rectTerm_mul_band` made `private`.]
4. *Architectural ingenuity* — reduce the per-`t` isometry to a band-restricted *simple*
   isometry, then transfer by density through `truncCLM`; reuses the SAME
   `simpleAssembly_T` dense embedding, so the bridge to B1a is definitional.
5. *First principles* — no circularity (`truncCLM_norm_sq` assumes no isometry; the
   simple case is B1a + Fubini + the pure-ℝ overlap identity), and the statement is the
   genuine isometry — RHS a real integral against the predictable Lebesgue⊗μ measure, not
   `‖x‖²=‖x‖²` in disguise.
6. *Idiomatic register* — `mkContinuous` CLM, `DenseRange.equalizer` + `congrFun`,
   `filter_upwards … rw [show …]`, `omit … in` placement — all match the adjacent
   `ItoIntegralProcessGeneral` / CLM files.
7. *Concept clarity* — docstrings name the key identity and state honest scope. [fixes
   applied: the `truncCLM` docstring no longer flatly calls itself "the orthogonal
   projection" (only norm-`≤1` is formalised) and now states the *squared*-norm isometry;
   the `ItoIntegralProcessGeneral` module docstring updated from "deferred" to "proved in
   the companion module".]
8. *Beautiful, elegant math* — the reconciliation `band_overlap_real` (B1a's
   per-endpoint-`∧t` overlap form = the joint-overlap-`∩(0,t]` form, both measuring
   `(p.1,p.2]∩(q.1,q.2]∩(0,t]`) gets its own named lemma with the "why" in prose.

**Blocking findings**: none (3-agent consensus).

**Recorded actions**:
1. *(done this round)* de-privatised `ItoIntegralL2.lp_two_norm_sq` and deleted the
   temporary in-file copy — the generic `‖g‖² = ∫ g²` now has a single home and three
   consumers across two files.
2. *(done this round)* `integral_rectTerm_mul_band` → `private`; `truncCLM` docstring
   sharpened (orthogonal-projection qualification + squared-norm statement).
3. *(open, non-blocking)* `∫₀ᵗ E[φ_s²] ds` as an *explicit* Lean term (the Fubini split
   of the product integral) is described in prose but not formalised as a standalone
   corollary — a cheap future add if a consumer needs it.

Cold `lake build` 8724 jobs green, axioms-clean; ledger 281/281 fresh; router/values
pytest green.

## 2026-06-12 — commit 5f41a11 — corpus 280

**Scope**: this session's Summit B / B1b deliverable —
`MathFin/Foundations/ItoIntegralProcessGeneral.lean` (the **general-integrand**
Itô integral `(φ●B)_t = ∫₀ᵗ φ dB` for `φ ∈ L2Predictable[0,T]` as a continuous L²
martingale on `[0,T]`: `itoProcessCLM` via `extendOfNorm` along `simpleAssembly_T`,
the definitional bridge to B1a, the key identity `(φ●B)_t = condExpL2 𝓕_t
(∫₀ᵀ φ dB)`, a.e.-adaptedness, the L² martingale property, the contraction
`‖(φ●B)_t‖ ≤ ‖φ‖`, the terminal isometry `‖(φ●B)_T‖ = ‖φ‖`, and L²-continuity) plus
its 3 new `full` corpus entries (`sc-ito-general-martingale` /
`-terminal-isometry` / `-l2-continuity`). The explicit per-t isometry
`E[(φ●B)_t²] = ∫₀ᵗ E[φ²] ds` is deliberately deferred (the band-over-trimmed-measure
computation) — openly flagged.

**Panel**: 3 independent agents, the eight lenses split among them, reading the new
file + its dependencies + the corpus prose (read-only, no Lean).

**Per-lens verdicts — all PASS**:
1. *Inspired math* — the L² Itô integral of a *general* predictable integrand as a
   continuous L² martingale; closes the density gap B1a left (simple integrands
   only). The load-bearing fact behind continuous-time pricing/hedging.
2. *Mathlib/Degenne coherence* — pure consumption: `condExpL2` +
   `MemLp.condExpL2_ae_eq_condExp`, `mem_lpMeas_iff_aestronglyMeasurable`,
   `condExp_condExp_of_le`, `DenseRange.equalizer`, `TendstoUniformly.continuous`,
   `eLpNorm_condExp_le`, plus B1a + `itoIntegralCLM_T`. The consumed surface was
   verified to exist upstream; nothing reproved.
3. *Zero slop* — every declaration load-bearing; the two helpers
   (`condExp_itoSimple_eq`, `itoIntegralCLM_T_simpleAssembly_T`) earn their place
   (no upstream duplicate; each discharges a real `extendOfNorm_eq`/martingale
   obligation, not a thin wrapper).
4. *Architectural ingenuity* — `itoProcessCLM := itoProcessLM.extendOfNorm
   simpleAssembly_T` reuses the exact recipe that builds `itoIntegralCLM_T`, making
   the bridge to B1a definitional (`rfl` after `extendOfNorm_eq`); the key identity
   collapses martingale/adaptedness/contraction/terminal-isometry into corollaries
   of ONE identity; the t-uniform contraction reused for
   continuity-via-`TendstoUniformly`. No simpler architecture found by the panel.
5. *First principles* — derived from B1a's martingale + the condExp tower + the
   terminal isometry + the real `simpleAssembly_T_denseRange`; no hypothesis
   smuggles the conclusion (`hBmeas`, T-boundedness are honest side-conditions).
6. *Idiomatic register* — disciplined `simp only` (always an explicit lemma list),
   `calc`/`filter_upwards`, B1a-consistent naming (`_norm_le`, `_isMartingale`,
   `_eq_condExpL2`, `_l2_continuous`), no hammer/omega/native_decide.
7. *Concept clarity* — statements + per-theorem docstrings model-grade (after the
   blocking fix below).
8. *Beautiful/elegant math* — the key identity is the spine; the five properties
   read off as short corollaries; the `(μ := μ)` ascriptions are load-bearing
   (implicit-`variable` disambiguation), not noise.

**Blocking finding (fixed before this verdict)**:
- The file-level docstring (lines 16-17) overclaimed the **deferred** per-t
  isometry `E[(φ●B)_t²] = ∫₀ᵗ E[φ²] ds` as delivered, contradicting the file's own
  theorems (only the contraction + terminal isometry are proved) and the honest
  corpus prose. **Fixed** in 5f41a11: the header now states the contraction +
  terminal isometry and marks the per-t isometry as the deferred refinement — the
  `.lean` header brought back into sync with the (already-honest) corpus JSON.

**Recorded actions / non-blocking notes**:
1. *(nit, open)* `condExp_itoSimple_eq` overlaps in content with the inline
   `hT'eq`/`hcond` block inside `itoSimpleProcessLp_norm_le` (the same
   B1a-martingale-to-terminal fact, once as an inequality-feeder, once as a
   reusable `=ᵐ`). Defensible (distinct downstream shapes); a future tidy could
   route the bound through the extracted lemma. Cosmetic — next touch of the file.
2. *(scope, accepted)* the per-t isometry is the genuine remaining gap (the file
   proves the L²-energy law only as the one-sided contraction off the horizon,
   exact at the terminal); openly flagged in the header + all 3 corpus scopes. The
   band-over-trimmed-measure computation (a `restrict`∘`trim`∘`prod` rectTerm
   integral mirroring `simpleProcessL2_norm_sq`) is the B1b follow-up / B2.

## 2026-06-10 — commit c288861 — corpus 277

**Scope**: this session's B1a deliverable — `MathFin/Foundations/ItoIntegralProcessMartingale.lean`
(the elementary Itô integral as a *process*: adaptedness, the conditional martingale-difference,
the martingale property, the time-indexed isometry, L²-continuity) plus its 3 new `full` corpus
entries `sc-ito-simple-process-{martingale,isometry,l2-continuity}`. Machine gates green before the
panel (cold build 8709 jobs, pytest 19, ledger 277).
**Panel**: three independent agents — (zero slop + idiomatic register), (Mathlib/Degenne coherence
+ concept clarity), (the four judgment lenses: inspired / architecture / first principles / elegance).

| lens | panel verdict | after fixes |
|---|---|---|
| inspired math quality | PASS | PASS |
| Mathlib/BrownianMotion coherence | PASS-WITH-NOTES | PASS |
| zero slop | PASS-WITH-NOTES | PASS |
| architectural ingenuity | PASS | PASS |
| first principles | PASS | PASS |
| idiomatic register | PASS-WITH-NOTES | PASS |
| concept clarity | PASS-WITH-NOTES | PASS |
| beautiful, elegant math | PASS | PASS |

**Blocking findings**: none.

**The convergent finding (all three reviewers, non-blocking)**: `condExp_adapted_mul_increment` —
the conditional martingale-difference — was framed as "the crux" but `itoSimpleProcess_isMartingale`
does not call it (it applies the same set-integral characterisation directly per `𝓕_s`-set), leaving
the lemma as unconsumed, over-sold public surface. **Resolved by reframing, not refactoring**: the
direct set-integral martingale proof is cleaner than routing through the condExp tower, and the lemma
legitimately *completes the conditional/unconditional API pair* with the public
`integral_adapted_mul_increment` (and is the natural form the gated Girsanov/Lévy/martingale-rep
cluster will consume). Fixed: the module docstring and the lemma's own docstring now state it is the
reusable conditional sibling, with the martingale established directly; the benchmark scope matches.

**Other fixes (minor, this round)**:
- The isometry docstring + benchmark scope implied the proof *delegates* to `itoSimple_sq_integral`;
  reworded to "mirrors" its structure, with the terminal isometry *mathematically recovered* (not a
  proof step) when `t` is past every right endpoint.
- Corpus `sc-ito-simple-process-martingale` called the martingale "the defining property" → "a
  fundamental property" (the L²-limit/isometry construction is the standard "defining" one).
- Documented the deliberate coercion-after-min ascription at the isometry RHS (prevents a future
  "cleanup" that would break the `rect_increment_pairing` match).

**Checks that mattered**: the truncated-isometry "rectangle past `t`" case is genuinely correct
(both the term and the overlap factor vanish — `min(t,·) ≤ t ≤ max(t,·)`), not a fudge; the
√-Hölder continuity bound honestly *bounds* (Cauchy–Schwarz over the finite support + the
single-increment isometry `integral_adapted_sq_mul_increment_sq`) rather than *computes* — no
spurious cross-term claim, and the docstring says so; `clamped_increment_eq`'s `grind` close is over
an exhaustive 16-way `le_total` split; the three `full` re-exports carry genuine proofs (no
rfl-tripwire), axioms-clean.

**Recorded actions (non-blocking, next cleanup pass)**:
1. `memLp_truncated_term` (private, this file) duplicates the per-term case split of
   `ItoIntegralProcess.memLp_itoSimpleProcess`; hoist it public into `ItoIntegralProcess.lean` and
   reimplement the loop body via it (~15 lines, removes the drift).
2. `hVL2` (`∀ p, MemLp (V.value p) 2 μ`) is re-derived identically in the martingale and continuity
   proofs; hoist to one `have`/private lemma.
3. Four `funext ω; by_cases h : ω ∈ s <;> simp [h]` indicator steps have direct Mathlib lemmas
   (`Set.indicator_one_mul` / `_mul_left`); fold on next touch.

## 2026-06-09 (round 6) — WHOLE-REPO values review — corpus 274

**Scope**: at the user's request, a second full-repo panel two days after round 5 — **eight
reviewers, one per lens**, with the round-5-unreviewed delta (`c3a3498`/`d2cb7bd`/`3a25518`/`bde8f24`)
reviewed in full and the whole-repo budget pointed at the **long tail** (Actuarial / DeFi /
Performance / Portfolio / FixedIncome / Futures / Binomial / RiskMeasures + older Foundations),
since the FK/Itô/Merton headliners had four recent reviews. Machine gates green before the panel
(19 pytest, ledger 273/273).

| lens | panel verdict | after fixes |
|---|---|---|
| inspired math quality | BLOCKING (2) | PASS |
| Mathlib/BrownianMotion coherence | PASS-WITH-NOTES | PASS |
| zero slop | PASS-WITH-NOTES | PASS |
| architectural ingenuity | PASS-WITH-NOTES | PASS |
| first principles | BLOCKING (1) | PASS |
| idiomatic register | PASS-WITH-NOTES | PASS |
| concept clarity | BLOCKING (1, same as first-principles') | PASS |
| beautiful, elegant math | PASS-WITH-NOTES | PASS |

**Blocking findings (3, all fixed this round):**

1. **`sc-thm-8.2.5` was uninhabitable** (first principles + concept clarity, found *independently*
   by two reviewers; then machine-confirmed by a daemon-checked refutation
   `SDEExistenceUniqueness → False`). The round-5 follow-up rewrite (`3a25518`) quantified the
   uniqueness candidate's diffusion integral `IσY` freely, so every process discharges the solution
   premise by taking its own residual as the "integral" — the field collapses to "every process
   started at `η` equals `X`", refuted inside any inhabitant by `Y := X + t`. The spec encoded a
   contradiction; `unique_strong_solution` was a theorem about an empty type. **Fix**: an opaque
   integral-**operator** encoding `Iσ : (ℝ → Ω → ℝ) → ℝ → Ω → ℝ`, consumed as `Iσ X` (solution)
   and `Iσ Y` (uniqueness premise) — candidates genuinely pinned to the same equation; the
   uniqueness conclusion scoped to `0 ≤ t` (the synthesizer found the unscoped `∀ t` conclusion
   left candidates free at negative times — a second uninhabitability the panel itself missed);
   a `: Prop` ascription (register corroboration); and an **in-snippet inhabitant `example`**, so
   non-vacuity is machine-guarded permanently. Corollary corrections in `coverage.md`.
2. **`FixedIncome/Vasicek.lean` claimed an unproved limit theorem** ("limiting value `r(∞) = θ`" —
   no `Tendsto` existed in FixedIncome). **Fixed in the strong direction**:
   `vasicekDeterministic_tendsto_mean` added (exponential mean reversion, consuming `hκ` exactly
   as the docstring advertised), making the claim true rather than deleting it.
3. **`Performance/RatiosExtended.lean` claimed an unproved `Var(R_p − R_b)` expansion** for
   `trackingErrorSq`. **Fix**: de-claimed — the def is the model definition, the variance-level
   identity honestly out of scope; `trackingErrorSq_self`'s "decomposition" header retitled.

**Fixed minors (the round's main wave):**

- *PricingKernel recomposed* (3 lenses converged): `statePrices_two_state` is now **defined** as
  `e^{−rT} · emmWeight{Up,Down}` — the Phase-37 weights, newly **named** in `FTAPTwoState` and
  consumed by `emm_of_signs` — and `pricingKernel_two_state` is defined as the two-state
  `statePricePricing` instance, so `_linear`/`_bond`/`_nonneg` genuinely consume `StatePrices`
  and the "via state-price linearity" docstring describes the actual proof (the round-5-era
  "via Greeks" fiction class, eliminated structurally). Phantom Results name fixed; `⟨0, by omega⟩`
  statement literals → vector literals. `FTAPTwoState`'s own Results list had two more phantom
  names (`signs_of_noArbitrage`, `ftap_two_state`) — rewritten with an honest not-formalized note.
- *FTAPMultiState*: misleading "backward direction" title fixed (the file proves the **forward**
  direction); the zero-consumer constructor-adapter `hasEMM_multi_of_candidate` (bold-titled
  "Backward FTAP" over an anonymous-constructor application) deleted; closing `linarith` → the
  pointed `h_sum_pos.ne' h_zero`.
- *VarianceSwapEquivalence*: split `(T ≠ 0) + (0 ≤ T)` merged to the memorable `(hT : 0 < T)`
  (+ snippet); intro-docstring normalization inconsistency fixed.
- *André's reflection principle wired* (the round's inverted-weight repair): `PathReflection.lean`'s
  stale "the hitting-time bijection is downstream work" de-staled (the bijection was *in the file*),
  Results list completed, and the counting form wired as **`mf-reflection-principle-counting`**
  (`Nat.card_congr` over `reflectionPrincipleEquiv_below`) with a curated AxiomAudit pin — the
  library's best long-tail mathematics now has corpus existence.
- *Coherence cites*: `herfindahl_card_inv_le_of_sum_one` now consumes Mathlib's
  `sq_sum_le_card_mul_sum_sq` (was hand-reconstructed; a pre-existing dead `have` went with it);
  `net_premium_principle := (eq_div_iff hA).symm`; `max_sub_max_neg :=
  max_zero_sub_max_neg_zero_eq_self` (kept under its finance name as the file's conceptual pivot,
  with the upstream cite documented).
- *Register*: `annuityDueValue` → `annuityDue_closed_form` (+ snippet); `IsBLPosteriorMean_unique`
  → dot-notation `IsBLPosteriorMean.unique`; CAPM's `a = b ↔ a − b = 0` anti-shape replaced by a
  real `jensenAlpha` def + `jensenAlpha_eq_zero_iff := sub_eq_zero`; DeFi `swap_output_lt_y`
  strengthened from `lt ∨ y = 0` to the honest `0 < y ⟹ lt` (named product certificate);
  `cml_decomposition_unique`'s misnomer resolved by **adding the uniqueness direction**
  (`cml_weight_unique := (eq_div_iff hσ_t).mpr`) so the entry's name became true — the snippet now
  exports recovery ∧ uniqueness.
- *Spectral*: the title promised monotonicity that did not exist — the real `spectralRisk_mono`
  added (the file's first contentful inequality); Results list fixed.
- *Stale-docstring batch*: 8 phantom identifiers fixed across DriftLimit / ForwardRate / CAPM(3) /
  Markowitz / MarkowitzLagrangian / SharpeFOCDerivation (+ American's loose `BinomialModel` ref,
  CAPMEquilibrium cross-ref; the Markowitz bullet also claimed positivity hypotheses the lemma
  does not take).
- *Corpus honesty*: `mf-compound-poisson-mgf` demoted `full` → `reduced_core` (the exp-algebra core
  of the named MGF identity — the taxonomy's own definition; the Kelly-demotion pattern one notch
  above `rfl`, exactly what the judgment layer exists to catch); `mf-credit-spread-time-avg-hazard`
  upgraded honestly (the definitional spread identity now *paired with* the substantive FTC
  recovery `hazard_eq_neg_log_deriv_survival`, both exported, the scope note splitting
  definitional-vs-derived); `gir-thm-9.1.7`'s scope note now states exactly what the L¹-bound
  field does and does not encode (no `θ`, no `B`, not Novikov's condition) + Doléans–Dade spelling;
  10 scope notes' stale "toolchain v4.18.0" → pin-stable wording; `mart-thm-2.6.7`'s pre-strip
  "inlined helper" provenance fixed; `mf-cds-fair-spread` abstract-annuity-factor disclosure.
- *Docs*: `bridges.md` `||`-merged rows 42/40 split (the Phase-40 row had been invisible in
  rendered markdown since 2026-05-30); row 42's wrong "discrete-Lagrangian" gloss and its mention
  of the deleted adapter fixed; the CondExpJensen audit row annotated **DELETED** (it said "NOT
  duplicate" about a file deleted as a duplicate); `ConvexPricingFunctional` got its missing
  catalogue row (53a, recording its layering exception); `blueprint.md`'s prose walk caught up to
  the generated spine (4 sections: FK heat flow, Markov path law, **BS PDE from Feynman–Kac**,
  Merton dominance, + cross-link from the Itô 🚧 section); `roadmap.md`'s same-day-stale "next
  candidates" fixed; `patterns.md` now declares the canonical `exp (-(r * τ))` form for new files;
  `coverage.md` live-status pointer + the 8.2.5 round-6 correction note; **README's Reproducibility
  pins were ALL stale** (toolchain rc1→rc2, Mathlib `f23306…`→`c87cc97…`, BM `16d15e…`→`fa590b1…`)
  — a panel miss caught in the follow-up sweep, fixed.
- *Repo hygiene*: the tracked-but-gitignored `docs/superpowers/specs/…` design spec untracked
  (`git rm --cached`; the dir is deliberately private); `docs/README.md`'s links into that dir
  removed and a `values-review.md` row added.

**Declined / corrected reviewer claims**: lens 3's "tracked stale HF snapshot jsonl" was wrong on
git status — the jsonl is untracked (local-only, no public exposure); the genuinely tracked-but-
ignored file was the reorg spec (fixed above). Elegance refactors of sound, heavily-reviewed proofs
were deferred with sketches recorded rather than churned (below), per the panel's own
keep-deferred recommendations.

**Recorded actions (deferred, owner = next session touching those files):**
1. *(elegance, sketched in the panel reports)* `NewtonConvergence` mirrored case duplication
   (~30 lines) → one `abs_integral_le_sq` helper; `SharpeFOCDerivation`'s 4× spelled-out derivative
   numerator → rewrite-through-factorization (~50→15 lines); `UtilityDerivation` have-pyramid →
   `calc` (+ canonical `ConcaveOn` hypothesis).
2. *(slop, catalogued)* dedup pairs: `ItoIntegralRiemannBridge`/`TD` (accepted-debt class, fold
   with the SimpleProcess/L2Predictable unification); `Immunization`/`ConvexityImmunization`
   shared weighted-exponential-sum `HasDerivAt` skeleton; `integrable_payoff_mul_d{t,x}K` stays
   deferred (fold when the general-`g` FK PDE lands); `MertonClassicDisplay`'s twice-proved
   rate-shift identity → private lemma.
3. *(elegance, assessed and closed)* the exp-sign convention split is **accepted permanently**;
   the canonical form for new files is now in `patterns.md`.
4. *(slop, Lean-gated)* dead `set … with` bindings: the two reviewers' static lists disagree
   (8 vs 7, overlap 4) — itself proof the item needs per-case Lean confirmation; batch into
   sessions already touching those files.
5. *(register, recorded)* `HasEMM_*_state` hybrid casing kept (coherent in-repo family);
   finance-acronym name parts (`_FOC`, `_SML`, `_QV_`) kept; ASCII-vs-unicode subscript census
   recorded; `swap_output_*` family naming; `VasicekSDE`/`MertonAmericanCallTree` `exp_zero`-show
   one-liners; `Phi_neg`'s `Iio_ae_eq_Iic` polish.
6. *(infrastructure, noted)* `AxiomAuditGen` pins only head-position constants of snippet proofs —
   compound proofs (`Nat.card_congr (…)`, anonymous constructors) contribute nothing; the
   reflection keystone is pinned in the **curated** audit instead. Consider a generator extension.
7. *(corpus, judgment note)* the long-tail trivia cluster (`mf-tracking-error-self`,
   `mf-triangle-arbitrage-unique`, `mf-log-forward-bsTerminal`, `mf-sortino-translation`) stays
   honest-but-thin `full`; upgrade toward the real theorems when those files are next touched.

**Positive exemplars recorded by the panel**: `Portfolio/CovariancePSD` (the docstring's story IS
the certificate), `Futures/Black76Greeks` (structural reduction made visible),
`RiskMeasures/RockafellarUryasev` (certificate-first elegance), `RiskMeasures/UtilityDerivation`
(the coherent axioms given content from a primitive), `Foundations/CarrMadan` (the model
upstream-coherence note), `FixedIncome/KMVMerton` (structural-identity honesty),
`pp-prop-3.3.6`'s scope note (the model reduced_core disclosure), and the snippet corpus's
mechanically perfect import discipline (0 blanket-Mathlib violations in 235 MathFin-importing
snippets).

**Verdict**: **PASS after fixes** — all three blockers repaired and machine-verified (the 8.2.5
refutation AND the repaired spec's inhabitant were both daemon-checked; the inhabitant ships
inside the snippet as a permanent non-vacuity guard). Net: corpus 273 → **274**
(+`mf-reflection-principle-counting`), **full 239** (−1 compound-poisson demotion, +1 reflection
wire), wrappers 18, reduced 17, delivery-ready **257**/274. lake build **8708 jobs green**,
MathFin sorry-free, axiom-clean (generated audit regenerated + a new curated pin); ledger
**274/274 fresh**; **19 pytest gates green**. Shipped alongside: the repo-presentation upgrade
(README landmark-results table + how-verification-works section + the stale Reproducibility pins
fixed; GitHub description/topics; docs index repaired).

## 2026-06-08 (round 5) — WHOLE-REPO values review — corpus 270

**Scope**: at the user's request, a full-repo panel (not just the Feynman–Kac keystone) — **six**
reviewers: two deep on the keystone tower, plus one each on `MathFin/Foundations/`, the pricing modules
(`BlackScholes`/`Futures`/`Binomial`/`FixedIncome`/`Portfolio`/`Performance`/`RiskMeasures`/`Actuarial`/`DeFi`),
the benchmark corpus (all 270 entries), and `docs/` + repo-meta.

**Headline**: the library is in **excellent shape**. No forbidden tactics anywhere; no proof smuggling;
no `rfl`/`trivial`-in-disguise `full` entry; every `library_wrapper` is a genuine Mathlib/Degenne
re-export; the `full`/`wrapper`/`reduced` split (236/18/16) is **honest**; coherence with the pinned
Mathlib/Degenne is real (no reproving of pinned lemmas); the Itô-formula ladder and the FK keystone are
principled, not redundant; `RockafellarUryasev`, the BS "magic identity" Greeks, Merton dominance, and the
dividend-Greek reparametrization are genuinely elegant. **The findings are honesty-of-claims drift (stale
docs/docstrings after the keystone landed) + a few pre-existing orphans + minor faithfulness/nits — no
blocking findings.**

**Applied this round** (public-facing honesty, no rebuild): README counts → 270/236/254/16, "What's not
done" corrected (dropped the now-`full` time-dependent Itô; Markov 6→5), the FK→BS-PDE keystone surfaced
in "What's covered"; CITATION.cff 251→254; `sc-thm-9.2.1` scope note (metadata **and** in-snippet)
de-staled — the "~300–500 lines left as upstream work" claim was false (that infra is built and consumed
by `sc-bs-pde-feynman-kac`); coverage.md round record. **PASS 2** (Lean rebuild) then fixed the
keystone-tower docstring drift: `PDEFromFeynmanKac` ("Only step 4 remains" → step 4 is the capstone;
"(until now consumed by nothing)" → load-bearing; wrong `Foundations.` qualifier on opened lemmas; step
numbering) and `FeynmanKacHeatEquation` (three stale "deferred heat-PDE direction" notes — the work is in
the file; the "Main results" block now lists `hasFDerivAt_heatKernel` + the `feynmanU` derivatives/heat
equation; the `heatKernel_t_eq_half_y_y` docstring, which wrongly said "not consumed" when
`feynmanU_heat_equation` consumes it) — all now honest that the keystone is complete and the heat flow
load-bearing.

**Orphans — REFLECTED, kept** (per the user's "always reflect if orphans will be used later", which
flipped a too-aggressive "delete"):
- `hasDerivAt_feynmanU_t` has zero *code* consumers (only docstring mentions) but is **kept public**: it
  is the `∂_t` building block the still-open fully-general-`g` PDE + uniqueness will consume, and it
  completes the natural `∂_t / ∂_x / ∂_xx` heat-flow API triple. Privating it would be wrong.
- The 3 `unfold;ring` lemmas in `PDEFromIto.lean` (`bsItoDrift_eq_itoDrift2D`,
  `bsItoDrift_no_time_eq_itoDrift`, `bs_pde_lhs_eq_drift_minus_rV`) are **kept**: they are the named
  coherence bridges that file exists to state (the bespoke BS drift *is* the general 1D/2D Itô drift
  specialised; the PDE LHS = drift − rV), carrying real conceptual content, and the file's own deferred
  martingale-route continuation (discounted price is a `Q`-martingale ⟹ driftless) consumes them. Not slop.

**Deferred, prioritized** (catalogued so nothing is lost — a clean follow-up cleanup):
- *[Lean, umbrella] Foundations orphan modules* (~700 lines, zero consumers): `VarianceSwapEquivalence`
  (a literal re-export anti-wrapper), `StochasticInterval` (the abandoned upstream-PR body), `PricingKernel`,
  `FTAPMultiState` → wire to a benchmark or delete. (`PricingFromBrownian` is intentional BM-grounding — keep.)
- *[corpus] `sc-thm-8.2.5`* (reduced_core): the SDE structure encodes a Lebesgue `∫σ ds`, not Itô `∫σ dB`
  (the `B` parameter is dead) → use an opaque adapted stochastic-integral field, mirroring `sc-thm-7.5.2`.
  `sc-thm-9.2.1` name/description state the full PDE+uniqueness (disclosed in scope) → optionally narrow.
- *[docs] roadmap.md / bridges.md / blueprint.md*: log the FK round, add the FK→BS-PDE bridge row, and
  regenerate the blueprint spine (tag the keystone `@[blueprint]`); `feynman-kac-growth-deferred.md` add a
  "superseded — a kernel-differentiation FK route landed" note.
- *[style, declined/deferred]*: ~159 `Real.` qualifiers under `open Real` — **declined** (the file
  consistently qualifies; low-value, high-churn, disambiguation-fragile); the `integrable_payoff_mul_d{t,x}K`
  / `curve_*` boilerplate dedup; 8 dead `set … with h…_def` binding names; 9 honestly-labeled re-export
  shim files; DeFi `internalPrice`/`arbitragePresent` + a `Performance/Ratios` docstring word.

**Verdict**: PASS. No blocking findings; the proofs across the whole repo are sound, elegant, and honest.
The remaining work is honesty-drift cleanup + pre-existing orphan housekeeping, fully catalogued above.

**Follow-up execution (2026-06-09)** — the catalogued deferred items above were executed (housekeeping of
panel-vetted "wire or delete" items, no fresh mathematical content, so no new panel):
- *docs*: the FK round logged in `roadmap.md` (new phase), `bridges.md` (the "FK" bridge row), and
  `feynman-kac-growth-deferred.md` (SUPERSEDED banner — its "deferred, not needed ever" kernel-
  differentiation route is exactly what shipped).
- *corpus faithfulness*: `sc-thm-8.2.5` SDE diffusion `∫σ ds` (dead `B`) → opaque adapted Itô integral
  `IσX`, mirroring `sc-thm-7.5.2`. Stays `reduced_core`, now faithful.
- *orphans, reflected per [[feedback_orphan_future_use]]*: `FTAPMultiState` (Phase 42 forward),
  `PricingKernel` (Phase 53 butterfly), and `VarianceSwapEquivalence` (Phase 45 equivalence) **wired** to
  new `full` corpus entries (`mf-ftap-multi-state-forward` / `mf-pricing-kernel-butterfly` /
  `mf-variance-swap-equivalence`); the literal anti-wrapper `varianceSwap_equivalence` removed (subsumed by
  the genuine two-functional theorem). `StochasticInterval` **kept** — Degenne #440 upstream-PR body,
  two-AxiomAudit-anchored, named `ElementaryPredictableSet` gap in the deferred Itô-CLM record.
- *blueprint*: the keystone `bsV_satisfies_bs_pde_via_feynmanKac` + the kernel heat equation
  `feynmanU_heat_equation` are now `@[blueprint]` spine nodes (curated AxiomAudit guards added; spine
  regenerated — the FK tower links into the existing `bsCall` node).

Net: corpus 270 → **273**, full 236 → **239**, delivery-ready **257**/273, 16 reduced. lake build 8708
jobs axiom-clean; AxiomAuditGen 226 guards; ledger 273/273 fresh; 19 gate tests green. Still-open
(unchanged): the fully-general continuous-`g` FK PDE + uniqueness; variable-coefficient FK (local-vol/
Heston) on the general-Itô layer; the Markov renewal/spectral cluster; P1 the CRR→BS error-constant paper.

## 2026-06-08 (round 4) — the keystone complete: BS PDE from Feynman–Kac — corpus 269

**Scope**: step 4 — `bsV_satisfies_bs_pde_via_feynmanKac`: the Black–Scholes PDE
`−∂_τV + ½σ²S²∂_SSV + rS∂_SV − rV = 0` derived *independently* from the Feynman–Kac representation,
closing the two-tower gap. Plus `hasDerivAt_bsV_SS_fk` (Gamma via FK) and the two integrability helpers
(`integrable_payoff_mul_d{t,x}K`). The whole chain — `hasFDerivAt_heatKernel → hasDerivAt_heatKernel_comp
→ hasDerivAt_feynmanU_comp → {Δ,Γ,Θ Greeks} → the PDE` — is now consumed end-to-end; `feynmanU` is
load-bearing for the PDE.

**Panel**: one adversarial reviewer (try-to-refute + no-smuggling audit), synthesised with Opus judgment.
**No blocking findings.** Verified the proof is honest: it genuinely rests on `feynmanU_heat_equation`
(the kernel identity `∂_t K = ½ ∂_xx K`) + the exact drift cancellation (`U_x` coeff
`−(r−σ²/2)−½σ²+r = 0`, `U_xx` coeff `−½σ²+½σ²=0`), with the DCT/uniform-domination content living in the
already-proved `hasDerivAt_feynmanU_comp` — no smuggling.

**Findings applied** (2): dropped an unused `with hc₀`; docstring clarified that the hard
differentiability work is in `feynmanU_comp` and `feynmanU_heat_equation` is only the algebraic kernel
identity. **Declined**: (a) the reviewer's "`hSne` is dead" — false, it is used by the final `field_simp`
to clear the `S`-powers (kept); (b) the reviewer's idiom suggestion `simp only []`→`dsimp only` —
*tried and reverted*: `dsimp only` does **not** beta-reduce the `feynmanU_heat_equation` `h z`-redex here
(it broke the build), so `simp only []` is the correct tactic. **Deferred**: the ~10-line copy-paste
between `integrable_payoff_mul_d{t,x}K` (a future unified skeleton); and **benchmark wiring** — the public
keystone theorem is not yet cited by a corpus entry (the only substantive open item; adding one triggers
an axiom-audit regen + ledger, deferred at this budget) — flagged as the immediate follow-up.

**Verdict**: PASS — the four-step keystone (kernel heat equation → FK price representation → discounted
heat flow → PDE) is complete, sound, axiom-clean. lake build green, 19 pytest, ledger 269/269 fresh.

## 2026-06-08 (round 3) — ∂_τ landed (Theta via Feynman–Kac) — corpus 269

**Scope**: the Black–Scholes `τ`-derivative via Feynman–Kac — the result that defeated several prior
attempts (the uniform domination kept hitting Lean's 200k-heartbeat `nlinarith`/`whnf` wall). The
four-step tower (all green): `hasFDerivAt_heatKernel` (heat kernel jointly Fréchet-differentiable) →
`hasDerivAt_heatKernel_comp` (curve chain rule) → `hasDerivAt_feynmanU_comp` (∂_τ of the FK function) →
`hasDerivAt_bsV_tau_fk` (the price's Theta). The breakthrough: **(1)** isolate the polynomial bracket
bounds (`curve_sq_ratio_le` / `curve_abs_ratio_le`) as standalone lemmas with the moving denominator
replaced by the constant `v₀` — in isolation `nlinarith` elaborates (the inline failure was the
`whnf`/`isDefEq` blow-up on a single mega-constant, not the math); **(2)** dominate by a **sum of two
Gaussian-moment envelopes** (one per kernel-derivative term), never a single mega-constant.

**Panel**: one adversarial reviewer (try-to-refute "net improvement"), synthesised with Opus judgment.

**Findings applied** (2): (a) **[blocking]** the `PDEFromFeynmanKac` module docstring still declared the
`τ`-derivative "deferred … the same nlinarith/heartbeat wall" — now false (`hasDerivAt_bsV_tau_fk` is
proved); rewritten to the honest status (Theta landed, only the step-4 PDE assembly remains); (b)
[minor slop] an unreduced beta-redex `(fun ξ => …) z` in `bsV_tau_fk`'s stated value → `max (e^z−K) 0`.

**Findings accepted / declined**: `hasDerivAt_bsV_tau_fk` is private with no consumer yet — accepted as
an in-progress Greek awaiting the step-4 PDE assembly, exactly as the already-committed
`hasDerivAt_bsV_S_fk` (Delta) was; the `sc-thm-9.2.1` benchmark scope-note overclaim ("~300–500 lines
upstream") is now mildly stale but left untouched (editing a benchmark re-stales the ledger + forces an
axiom-audit regen for a narrative note; flagged for a future benchmark pass). All other lenses PASS
(inspired math, idiomatic register, Mathlib coherence, elegance, concept clarity, architectural
ingenuity — the one genuinely-2D ingredient `hasFDerivAt_heatKernel` makes a single chain rule available).

**Verdict**: PASS. `feynmanU` is now load-bearing for the Black–Scholes time-derivative; the C¹ tower is
fully consumed. Lean: `lake build` green (no MathFin errors), 19 pytest, ledger 269/269 fresh,
axiom-clean. Remaining for the full keystone: `∂_SS` via FK + the PDE-operator assembly (step 4).

## 2026-06-08 (round 2) — parametric unification — corpus 269

**Scope**: the parametric unification of the heat-kernel differentiate-under-the-integral lemmas in
`Foundations/FeynmanKacHeatEquation` — new skeleton `hasDerivAt_integral_mul_kernelFamily` + extracted
`heatKernel_temporal_le` / `sq_sub_div_le` / `integrable_payoff_mul_heatKernel`, with `hasDerivAt_phi`
and `hasDerivAt_feynmanU_{t,x,xx}` refactored to route through it (net ≈ −55 lines); the
`exp_mul_heatKernel` docstring made honest. The timed-out ∂_τ tower (the heat kernel's joint Fréchet
derivative + its curve derivative + `feynmanU_comp`) was *validated* but **removed**: its uniform
domination hits the 200k-heartbeat wall — the same obstacle as the earlier brute force — so it was kept
zero-orphan rather than shipped behind a `maxHeartbeats` discharge (which would itself be slop).

**Panel**: three reviewers — (1) zero-slop / idiomatic register / Mathlib coherence; (2) elegance /
concept clarity / architecture; (3) adversarial abstraction audit (try to refute "net improvement").
**No blocking findings — all three judged it a net improvement.**

**Findings applied** (3): (a) stale cross-ref in `heatKernel_shift_le` (`hasDerivAt_phi` →
`heatKernel_temporal_le`); (b) `integrable_payoff_mul_heatKernel` docstring overclaim ("every
diff-under-integral lemma" → the `_t`/`_x` lemmas, since `_phi` uses the Gaussian-integrability route
and `_xx` a first-derivative integrand); (c) **[adversarial, deepest]** the temporal polynomial-ratio
bound `|w²−s|/(2s²) ≤ 2(w²+3t/2)/t²` was still duplicated verbatim (modulo `y` vs `z−x`) between
`hasDerivAt_phi` and `_t` — extracted as the private `sq_sub_div_le`, so the shared estimate is now
named and the per-lemma dominations are genuinely distinct (making the skeleton docstring's claim true).

**Findings declined** (with reason): "remove the named `hs_pos`" — load-bearing via `positivity`'s
context search, removing it breaks the build; param-lemma arg reorder + skeleton rename — subjective
idiom not worth touching four green call sites; restore "Cameron–Martin" to the `exp_mul_heatKernel`
title — honesty wins (it is the completing-the-square real-analysis identity, *not* the measure change;
the Cameron–Martin/Girsanov connection stays in the body); `_xx`'s interleaved `?_` argument
ergonomics — an honest, accepted cost (its base point is a first-derivative integrand, not a raw
kernel product, so it cannot use `integrable_payoff_mul_heatKernel`).

**Verdict**: PASS. The unification is elegant, fully consumed (4 callers + shared helpers), and reduces
duplication without hiding the genuinely-distinct dominations. Lean: `lake build` green (no MathFin
errors), 19 pytest pass, ledger 269/269 fresh, axiom-clean.

## 2026-06-08 — commit 3beb170 — corpus 269

**Scope**: the Feynman–Kac → BS-PDE *keystone core* — step 1 (kernel-side heat equation
`∂_t U = ½ ∂_xx U` for sub-Gaussian payoffs, in `Foundations/FeynmanKacHeatEquation`: the
completing-the-square mean-shift, the sub-Gaussian envelope, the spatial kernel bound, three
diff-under-integral derivatives, the `feynmanU_heat_equation` identity) + the bridge
`bsV_eq_discount_feynmanU` (bsV = discounted heat flow, making `feynmanU` load-bearing for pricing)
and Delta-via-FK `hasDerivAt_bsV_S_fk` (in `BlackScholes/PDEFromFeynmanKac`). The full `∂_τ`/PDE
assembly is deferred (its brute-force domination is infeasible — see below).
**Panel**: three Sonnet reviewers (coherence+idiomatic · zero-slop+architecture ·
inspired-math+first-principles+clarity+beauty) reading the diff, + Opus synthesis and judgment.

| lens | verdict |
|---|---|
| inspired math quality | PASS |
| Mathlib/BrownianMotion coherence | PASS-WITH-NOTES |
| zero slop | PASS-WITH-NOTES |
| architectural ingenuity | PASS-WITH-NOTES |
| first principles | PASS |
| idiomatic register | PASS-WITH-NOTES |
| concept clarity | PASS-WITH-NOTES |
| beautiful, elegant math | PASS-WITH-NOTES |

**Blocking finding (fixed in this commit's follow-up)**: `PDEFromFeynmanKac` carried ~112 lines of
orphaned, never-consumed `∂_τ` domination scaffolding (`hasDerivAt_kernelCurve`, `heatKernel_curve_le`,
`integrable_tau_bound`) — machinery for a brute-force differentiate-under-the-integral that
heartbeat-times-out and is being abandoned for a leaner route. Removed (recoverable from `3beb170`);
the file now holds only the FK representation, the bridge, and the FK-Delta, with an honest module
docstring.

**Recorded actions (deferred to the next FK round, batched to avoid re-staling the ledger)**:
1. *(top priority — leaner + elegant + architecture; all three panels)* `hasDerivAt_phi`,
   `hasDerivAt_feynmanU_t/_x/_xx` are the same dominated-convergence proof at different parameters;
   unify into ONE parametric `hasDerivAt_feynmanU_param` (≈200 → ≈100 lines).
2. failing 1, extract the verbatim-duplicated `heatKernel_temporal_le`, polynomial-bound, and
   `hFt_int` blocks as shared private helpers (≈35 lines).
3. *(concept clarity)* `exp_mul_heatKernel` docstring over-claims "Cameron–Martin mean shift" — it is
   the completing-the-square identity (the *analytic core* of the shift, not the measure-change
   theorem); retitle honestly.
4. *(idiomatic)* `open Real` is declared but `Real.` is qualified ~200×; drop it.
5. *(architecture)* `callPayoff_continuous`/`le_exp` are call-payoff facts → `BlackScholes/Call.lean`.
6. *(zero slop)* `hasDerivAt_feynmanU_xx`'s closing `linarith [show … ring]` should mirror `_x`'s
   clean `calc … ring`.

**Declined (Sonnet suggestions overruled on the math)**:
- "compose `hasDerivAt_kernelCurve` from the `∂_t` + `∂_y` partials" — wrong: the curve moves both
  kernel arguments, so total = sum-of-partials ONLY under joint differentiability, which the
  partial-`HasDerivAt`s do not provide; the from-scratch differentiation of the explicit kernel is
  the correct route.
- "`heatKernel_shift_le` without variance-widening (same-`t` bound)" — false: `K(t,z−x)/K(t,z−x₀)`
  is unbounded in `z`; widening to `2t` is essential for the domination.

**Verdict**: the keystone core is sound, honest, and largely elegant — the inspired ideas
(kernel-side differentiation, the mean-shift, the heat-equation collapse) are present and correct.
The first-try slop (the duplicated diff-under-integral template; the brute-force `∂_τ` scaffolding) is
the natural debris of a large climb: the scaffolding is removed here, the duplication is scheduled for
a parametric pass.

## 2026-06-07 — commit 321eb4f — corpus 269

**Scope**: commit `321eb4f` — `bsV_eq_feynmanU` (the Feynman–Kac representation of
the Black–Scholes call price) in the new bridge module
`MathFin/BlackScholes/PDEFromFeynmanKac.lean`, plus its umbrella import. This is
step 2 of the Feynman–Kac → BS PDE keystone (which makes the previously
consumer-less `Foundations.FeynmanKacHeatEquation.feynmanU` load-bearing for
pricing); steps 1 (kernel-side heat equation), 3 (change of variables) and 4
(assembly) remain in progress.
**Panel**: three Sonnet agents on the mechanical lenses — (coherence + idiomatic
register), (zero slop + dead-code/forbidden-text), (architecture + first-principles
+ docstring fidelity) — and Opus on the judgment lenses (inspired math, first
principles, concept clarity, beauty).

| lens | verdict |
|---|---|
| inspired math quality | PASS |
| Mathlib/BrownianMotion coherence | PASS-WITH-NOTES |
| zero slop | PASS |
| architectural ingenuity | PASS |
| first principles | PASS |
| idiomatic register | PASS |
| concept clarity | PASS (after the fix below) |
| beautiful, elegant math | PASS |

**Blocking findings**: one, fixed before this verdict. The theorem docstring's
"Proof chain" described a *two-step* route (`feynmanU_eq_integral_of_map` with
`B = id` over `gaussianReal 0 (σ²τ)`, then a **separate** `integral_map` rescale)
that was never written: the actual proof is a *single* `feynmanU_eq_integral_of_map`
with `B = (σ√τ · ·)` over the standard normal, the variance rescale discharged as
its hypothesis `hmap`. The docstring — the concept-clarity instrument — was
rewritten to describe the one-step proof that exists.

**Checks that mattered**: all four hypotheses are consumed (`hS` via
`Real.exp_log` and the `BSCallHyp` constructor; `hK`/`hσ` via `BSCallHyp`; `hτ`
via `Real.sq_sqrt` and `BSCallHyp`) — no dead binders; forbidden-text scan clean
(no `sorry`/`native_decide`/`?`-tactics/etc.); the statement is a genuine identity,
not a disguised `rfl` (the closed-form `bsV` and the integral `feynmanU` are
definitionally distinct) and not vacuous; it consumes the canonical upstream API
(`gaussianReal_map_const_mul`, `feynmanU_eq_integral_of_map`, `bs_call_formula`,
`HasLaw.id`) with no thin wrappers or re-derivations; the NNReal-coercion block and
the two `neg_mul` reconciliations are load-bearing glue, not slop; correct
file/layer (a `BlackScholes/` bridge over the Foundations FK layer) at the right
generality (the concrete call payoff baked in, not over-abstracted).

**Declined reviewer flags** (with reason):
1. *(minor)* "redundant `public import MathFin.BlackScholes.Call`" — declined: this
   file directly consumes `bs_call_formula`/`bsTerminal`/`BSCallHyp`, so the
   explicit import is correct direct-dependency hygiene; the file's transitive-import
   comment scopes only the Mathlib base, not directly-used modules.
2. *(minor)* "`NNReal.coe_mk` is deprecated" — declined: the pinned-Mathlib build is
   warning-clean, so this is the documented public-Mathlib-newer-than-pin artifact
   (the same class as the `abs_sub` false positive in the `14ca008` review).
3. *(nit)* "'until now consumed by nothing' is stale" — declined: "until now
   consumed by nothing, becomes load-bearing" is self-consistent and correct.

**Recorded actions**:
1. *(minor, out of scope — future cleanup)* the exp-sign convention mismatch
   between `Call.lean` (`Real.exp (-r * T)`) and `PDE.lean` (`Real.exp (-(r * τ))`)
   forces two cosmetic `neg_mul` reconciliations in this file; unify the convention
   in a pass over the lower BS modules.

## 2026-06-07 — commit 14ca008 — corpus 269

**Scope**: commit `14ca008` — Summit A′ (the time-dependent Itô formula:
three new Foundations modules + the process-weight generalization of
`WeightedQuadraticVariation`), the Kelly n-period iid model re-promotion,
and the wiring (`sc-thm-7.1.2` + `mf-kelly-n-periods-linearity` → `full`,
AxiomAudit Summit A′ section, blueprint spine node, docs).
**Panel**: three agents — (coherence + idiomatic), (slop + first principles
+ architecture), (clarity + inspired math + beauty).

| lens | verdict |
|---|---|
| inspired math quality | PASS |
| Mathlib/BrownianMotion coherence | PASS-WITH-NOTES |
| zero slop | PASS-WITH-NOTES |
| architectural ingenuity | PASS |
| first principles | PASS |
| idiomatic register | PASS-WITH-NOTES |
| concept clarity | PASS-WITH-NOTES |
| beautiful, elegant math | PASS |

**Blocking findings**: none.

**Checks that mattered**: the boundary-cancellation algebra of the named-limit
core was verified symbolically — the discrete 2D identity makes the unbounded
`f(T,B_T) − f(0,B₀)` cancel, so "the L² estimate only ever sees three
vanishing terms" is literally true, not prose; the Kelly repair is genuine
first principles (`integral_log_kellyReturnMeasure` *computes* the two-point
integral, `kellyGrowth_n_periods` is real linearity of expectation over
`Measure.pi` — no step is `rfl`); a dead-hypothesis sweep over every new
public theorem found every binder consumed (including both joint-continuity
hypotheses of the CLM theorem); every `nlinarith` carries certificate hints
(the `(u+v+w)² ≤ 3(u²+v²+w²)` step via the three cross-difference squares);
no Mathlib lemma yields joint continuity from bounded one-variable partials,
so the corner-split Lipschitz route of `continuous_uncurry_of_bdd_partials`
is canonical, and `tendsto_riemann_L2_process` duplicates no Mathlib
Riemann-DCT result (bespoke `NNReal` `timeMeasure`); the `sc-thm-7.1.2`
snippet matches `ito_formula_td_L2_bddDeriv` hypothesis-for-hypothesis, and
the unbounded-coefficient gap is named everywhere it matters.

**Fixed before this verdict** (triaged minor, fixed in `14ca008`):
1. `integral_increment_sq` duplication — the TDRemainder copy re-derived
   `ItoIsometryAdapted.integral_increment_sq` at the bare `MathFin` namespace
   (a latent ambiguity trap since `ItoFormulaTD` opens that namespace);
   deleted, the call site consumes the existing lemma, the genuinely-new
   `integrable_increment_sq` companion stays.
2. Three dead nonneg `have`s in `tendsto_ito_remainder_td` left by the
   memLp hoist (self-caught pre-panel, confirmed by the panel's sweep).
3. `tendsto_riemann_continuous` had been widened to public with a docstring
   claiming the Itô layers consume it — they consume the L² wrappers;
   reverted to `private` with the honest description.
4. `docs/blueprint.md` BS-PDE section still called `sc-thm-7.1.2` "still
   `reduced_core`"; rewritten to the bounded-regime status (the deferral
   argument stands: the BS value function's Γ is unbounded as `S → 0`).
5. Kelly horizon-binder drift (`T : ℕ` vs the file's new `n : ℕ` register)
   in `kelly_n_periods_deriv_at_kelly` + its benchmark snippet.

**Recorded actions**:
1. *(minor, DONE same day — consolidation follow-up commit)*
   increment-second-moment fact consolidated: `ItoIsometryAdapted` now
   imports `WienerIntegralL2` (acyclic) and `integral_increment_sq` /
   `integral_two_increment` are one-step instances of
   `covariance_increment_aux` (diagonal and shared-start), `hBmeas` dropped
   from both signatures as dead; module docstring's stale "(non-`module`)
   file" re-derivation apology rewritten. The `SimpleProcess`/`L2Predictable`
   unification remains the only deferred item of that paragraph.
2. *(minor, DONE same day — same commit)* the Term-II scaffolding hoist
   completed: private `measurable_pathIntegral` + `abs_pathIntegral_le` are
   the single home of the path-integral measurability/bound, consumed by
   `tendsto_riemann_L2_process`, the new per-`n` companion
   `integrable_riemann_defect_sq`, and `memLp_pathIntegral_process`;
   `tendsto_weighted_qv_process` lost its 19-line duplicate block.
3. *(nit, RESOLVED — no action at this pin)* `abs_sub` is **not** deprecated
   in the pinned Mathlib: it is the live `to_additive` companion of
   `theorem mabs_div` (`Algebra/Order/Group/Abs.lean:81`), and the bridges
   elaborate with zero deprecation warnings. The reviewer's claim was a
   newer-Mathlib artifact — the documented public-loogle-vs-pin caveat.
   Re-check at the next toolchain bump.
4. *(nit, accepted)* `coverage.md`'s "pre-re-audit historical record" line is
   deliberately stale provenance; the panel flagged it, the file already
   frames it as such — no action.
5. *(nit, DONE same day — same commit)* `PoissonCounting`'s two unused-`hr`
   warnings (pre-existing, surfaced by the consolidation rebuild) pruned as
   a dead-positivity cascade: three private Gamma-CDF calculus lemmas
   (`hasDerivAt_gamma_antideriv`, `integral_gammaPDFReal_sub_succ`,
   `integral_gammaPDFReal_one`) never needed `0 < r` — the telescoping
   antiderivative identities are formal algebra; public signatures
   untouched.

## 2026-06-06 — commit f1b0dcd — corpus 269

**Scope**: commits `9db04f8` (Merton dominance + classic display + Markov
path law), `aec693d` (values-gates round), `f1b0dcd` (HF publish CI) — four
new Lean modules, one bridge lemma, the enforcement tooling.
**Panel**: three agents — (coherence + idiomatic), (slop + first principles
+ architecture), (clarity + inspired math + prose honesty).

| lens | verdict |
|---|---|
| inspired math quality | PASS |
| Mathlib/BrownianMotion coherence | PASS |
| zero slop | PASS |
| architectural ingenuity | PASS |
| first principles | PASS |
| idiomatic register | PASS |
| concept clarity | PASS-WITH-NOTES |
| beautiful, elegant math | PASS |

**Blocking findings**: none.

**Checks that mattered**: `bsV_spot_tangent_le` duplicates no Mathlib
support-line lemma (it is the delta-substituted form, needing the
closed-form Greek); the Markov factorization is genuinely derived (base
case computes through `traj_map_frestrictLe` + `partialTraj_self` +
`piUnique`; inductive step through the comp-product marginal recursion —
no step smuggles the conclusion); `mertonCallTerm_eq_bsV`'s trivial proof
is a feature (it validates the definition is the BS value, and two modules
consume it); "jump risk is never free" is an exact gloss of the inequality
under its hypotheses; the classic display matches Merton (1976) eq. (16)
weights/rates/vols precisely; the converse direction of the Markov
characterization is nowhere claimed.

**Recorded actions**:
1. *(done in this commit)* corpus-iteration was triplicated across
   `axiom_audit_gen.py` / `hf_dataset.py` / `ledger.py` — extracted
   `tools/verify/corpus.py`; the two new tools now share it. `ledger.py`
   deliberately untouched (verified load-bearing hashing code) — fold into
   its next structural pass.
2. *(nit, open)* `MertonClassicDisplay.lean` docstring: "absorbs the jump
   factor" is terse about the mechanism (the rate-shift identity supplies
   it two paragraphs later); sharpen on next touch of the file.
3. *(nit, accepted)* the rfl-tripwire's tail regex is documented
   "good enough" in-file; a Lean-aware scanner is not worth its weight while
   the catch rate is this good (1 for 1 on first run).

## 2026-08-07 — corpus 351 — naming the Itô integrand, and a systematic prose-vs-statement audit

Scope: the `#183` chain (`ItoFormulaTD`/`…Localized`/`…ItoProcess`/`…GBM`), the follow-on audit the
user asked for after two prose overstatements turned up in one day, and the `ItoFormulaCLM` /
`ItoIntegralRiemannBridge` work that audit forced. Corpus **351**, unchanged — no entries added,
seven strengthened or corrected. This is a single-reviewer pass, not the three-agent panel; the panel
is still owed at the next proof session (carried from the last round, which owed it too — see the
backlog).

### Upgrades executed

1. **The Itô chain names its integrand** (#183, PR #189). Every rung from `ito_formula_td_L2_bddDeriv`
   to `discountedGBM_eq_itoIntegral` states `gfx =ᵐ [the integrand]`, ending at `σ·Ŝ(·)`.
2. **The `C²` sibling, found by the audit, not by the issue.** `sc-thm-7.1.1` had exactly the same
   defect one tower over: its description wrote `∫₀ᵗ f'(B_s) dB_s` while the statement said `∃ gf'`.
   Fixed by carrying the conjunct through `itoIntegralCLM_T_of_bdd_cont → ito_formula_L2_bddDeriv →
   _mk`. The TD bridge had exposed the identification since it was written; the untimed one never did.
3. **Two forgetful wrappers merged away.** `ito_formula_td_L2_bddDeriv_explicit` + its conjunct-dropping
   wrapper are one theorem now.
4. **`ae_fst_mem_Ioc_trimMeasure_T` existed six times.** One private lemma in `ItoIntegralLocality`,
   four inline `have`s (`ItoIntegralRiemannBridge`, `…TD`, `…Adapted`, `SimpleProcessPartition`), and
   the public one I added *yesterday* in `ItoIntegralCLM` without noticing the other five. All five
   duplicates retired.
5. **Four descriptions corrected** where they claimed the textbook theorem and the entry delivered
   less: `cm-thm-4.3.10` (`L^p` convergence not delivered — a.s. along ℕ plus in-measure in real time
   is), `sc-thm-8.2.5` (uniqueness only, not existence), `sc-thm-7.4.5` (constant `σ`, not `σ(s)`),
   `sc-thm-9.2.1` (the Feynman–Kac identification, not uniqueness of a bounded classical solution).
6. **The gate**: `test_values.py::test_prose_does_not_outrun_statement`, plus the standing first pass
   in this file's protocol and in `CLAUDE.md`.

### The lenses, as gradients

**1 Inspired math.** *Exemplar:* the identification argument. `L²` convergence gives a.e. convergence
only along a subsequence, which reads like a weakness and is exactly enough — and the pointwise input
is not analysis at all, just the observation that the truncation goes inert at each point once
`n ≥ |B|`. The `L²` membership of `f_x(·,B)` then falls *out* of the identification instead of being
its prerequisite. *Upgrade (MED):* `ae_eq_of_tendsto_Lp_of_tendsto` is `private` with one consumer.
The second consumer promotes it; if a third appears it wants a real home and a Mathlib-shaped name.

**2 Coherence.** *The finding, and it is the headline again.* Last round's headline was three general
lemmas stranded in application files. This round: the *same* fact written six times, and I added the
sixth. The last round's own recorded lesson did not prevent it, because nothing looks for duplicates —
I wrote a lemma without grepping for its statement first. *Upgrade (HIGH):* a duplicate-statement
detector. A cheap version — normalise whitespace on each `have h : <prop> := by` and each lemma
conclusion, hash, report collisions across files — would have caught all five. This is the highest-value
item on the backlog because it is the one failure this repo keeps repeating.

**3 Zero slop.** *Exemplar:* `discountedGBM_eq_itoIntegral`'s proof is four lines and every one is the
mathematical step. *Finding, fixed:* the `hsupp` copies were slop by the strict definition —
"duplicated sub-derivations". *Upgrade (LOW):* `ito_formula_itoProcess` now mixes a bulleted goal with
an unbulleted one after `refine ⟨gfx, ?_, ?_⟩`. Idiomatic, but the file would read better with both
bulleted; costs a re-indent, worth folding into the next touch.

**4 Architectural ingenuity.** *Exemplar:* the conjunct rides the existing `∃` rather than spawning a
parallel `_explicit` tower — six statements got stronger and no new names appeared. *Upgrade (MED):*
`ito_formula_expBrownian` is strengthened and has no consumer at all, corpus or library. Keep it (it
is the pedagogical rung), but it is the kind of thing that should be *either* consumed *or* deleted
within a phase or two.

**5 First principles.** *Exemplar:* nothing in the chain is assumed; each rung derives its conjunct
from the rung below, and `cutoff_bddDeriv` derives it from a theorem that already knew it. *Finding,
open:* `sc-thm-9.1.8` is honestly labelled `reduced_core` and its docstring says "specification", but
its hypothesis is a structure (`GirsanovGeneral`) that bundles what the conclusion reads off. That is
the reduced-core shape working as intended and disclosed — but it is worth stating plainly in the
entry that the structure is the hypothesis, since "specification" is doing quiet work.

**6 Idiomatic register.** *Exemplar:* `{mα : MeasurableSpace α}` as a plain implicit, matching
Mathlib's own measure-theory convention — which is *why* our helper composes with a trim measure at
all; instance-implicit would have synthesized `Prod.instMeasurableSpace` and failed. *Upgrade (LOW):*
`ae_fst_mem_Ioc_trimMeasure_T` is a mouthful; a Mathlib reviewer would want
`trimMeasure_T.ae_fst_mem_Ioc` or similar once it has a namespace worth dotting into.

**7 Concept clarity.** *This is the round's weak lens, and the reason the user asked for the audit.*
Six separate places said more than their Lean did. The pattern is not carelessness, it is structural:
prose is written to describe the theorem the author has in mind, and when the statement lands weaker,
nothing re-reads the prose against it. *Upgrade (executed, partial):* the mechanical gate and the
standing first pass. *Upgrade (HIGH, open):* **`description` has two incompatible jobs.** For 36
entries it is the textbook target; for the rest it is the delivered result; nothing marks which, and it
is published in the HF dataset. Either split the field (`textbook_statement` vs `description`) or
require every textbook-framed description to carry its delivered scope inline — the four I corrected
now do, ad hoc. 225 of 351 entries carry no docstring at all, so for those `description` is the *only*
prose and carries the whole weight.

**8 Beautiful math.** *Exemplar:* "the truncation is eventually inert at every point, and an `L²` limit
is an a.e. limit along a subsequence" — two sentences, no estimates, and the theorem falls out.
*Upgrade (MED):* the same eventually-inert observation should retire domination arguments elsewhere in
the localization files; `boundary_tendsto_L2` and `drift_tendsto_L2` still do dominated convergence
where pointwise eventual-constancy may be available.

### Ranked backlog

1. **[HIGH] A duplicate-statement detector** (lens 2). Six copies of one fact, and the round that
   recorded the lesson still produced the sixth. Normalise-and-hash lemma conclusions and `have`
   propositions; report cross-file collisions. Owner: next session's opening move.
2. ~~**[HIGH] Split or discipline `description`**~~ **executed 2026-08-07.** One job: `description`
   states the theorem as the entry proves it. All 36 textbook-framed descriptions read against their
   statements — **15, i.e. 42%, overstated**, including a sign error (`mart-prop-2.5.5`), a stale
   description contradicting its own `full` status (`gir-thm-9.1.8`), a multivariate claim delivered
   in 1-D (`dist-thm-B.1.2-affine`), and `[B,B]_t = t` where the L¹-mean is what holds
   (`sc-thm-6.1.1`). Structural cause found and fixed: `formalization_scope` — the honest per-entry
   disclosure — existed on every entry and was **not** exported while `description` was, so the claim
   shipped and the disclosure stayed home. Both are published now. *Residual (LOW):* nothing
   mechanically checks a description against its statement; that is judgment and stays with the
   standing first pass.
3. **[HIGH, carried] Run the actual three-agent panel.** Two rounds running have deviated — last round
   ran eleven scoped passes, this round is a single reviewer. Both deviations were reasonable and both
   were the same deviation. The next proof session runs the panel or the protocol should be amended to
   say what we actually do.
4. **[MED] #182 — Clark–Ocone**, naming the *representation's* `φ`. #183 named the Itô formula's
   integrand; this is the harder and more valuable half, and it is what "state the delta of a general
   claim" actually needs.
5. **[MED] Audit the remaining 32 textbook-framed descriptions** (lens 7). I checked the five highest-
   risk and corrected four. The rest are unread against their statements.
6. **[MED] Retire dominated convergence where eventual-inertness suffices** (lens 8).
7. *(Carried, unchanged:)* compose the `PricesGainsAtZero` guards (#186); the vector driver (#180);
   the second-FTAP converse (#181); the discrete general-Ω multi-period DMW crown; the 2D covariation
   Itô tower (#48); Girsanov `L²`/Novikov.

### Evidence

Mechanical floor: `lake build MathFin` + `lake lint` green; pytest 6/6 in `test_values.py` including
the new gate, full suite green; ledger re-verified; axiom pins hold; `AxiomAuditGen` byte-fresh at 308
guards.

The new gate was negative-controlled rather than trusted: reverting the three naming conjuncts in a
scratch copy made it fail with exactly those three ids. Its first draft did *not* have that property —
it accepted any `=ᵐ` after the `∃`, including the main identity, and so passed `sc-thm-7.1.1`, the very
entry the audit was chasing. A gate that cannot fail on the defect it was written for is worse than no
gate, because it launders the defect as checked.

**Checks that dissolved**: `gir-pricing-measure-unique` (prose says "uniqueness", statement is
`Q A = μ A` for arbitrary measurable `A` — that *is* the uniqueness); `mf-fixedincome-fra` ("the unique
fixed rate" is delivered by the `↔`); `mf-cash-or-nothing` / `mf-asset-or-nothing` (the "iff" is in the
payoff's definition, not a claimed equivalence); `pp-thm-3.3.5` (same); `sde-picard-existence-uniqueness`
(`∃!` on the Picard fixed point, and the docstring identifies fixed point with solution);
`sc-thm-9.1.8` (the `∃ v` *is* pinned, through a coercion the first regex could not see);
`mart-thm-2.4.6` (Doob `L^p`, description matches).