Drift term in the Itô-process price: S = S₀ + ∫b ds + (σ●B)

[raphaelrrcoelho]

context

Foundations/MarketCompletenessInPrice.pricePath is driftless by construction, S_t = S₀ + (σ●B)_t — which is what a discounted price is under the reference measure, and is all the pricing-measure argument of PricingMeasureL2Density needs. The module docstring records the absence as a scope decision.

A drift is what the HJM bond dynamics need (#146–#150: dY = (r − α*) dt − σ* dW and dP/P, dZ/Z), and it generalises the phase's price to an honest Itô-process price.

task

Extend pricePath (or add a sibling) to S_t = S₀ + ∫₀ᵗ b ds + (σ●B)_t and define ∫ψ dS := ∫ψ b ds + ∫ψ dM.

The pathwise time-integral object already exists: Foundations/DriftProcessModification.driftContinuousMod, built for the Girsanov track, with driftContinuousMod_eq_setIntegral identifying it with ∫₀ᵘ θ ds. Reuse it rather than building a second one.

what this does NOT need

The martingale results do not extend: with a drift, S is not a martingale and PricingMeasureL2Density does not apply. This issue is about the integral, not about re-running the pricing-measure argument.

acceptance criteria

• ∫ψ dS defined for a drift-plus-diffusion price, with its integrability side conditions stated.
• The driftless case is recovered as b = 0, definitionally or by a one-line lemma.
• Corpus entry + coverage row; axioms-clean; lake build MathFin && lake lint green; ledger fresh.

pointers

Foundations/MarketCompletenessInPrice.lean, Foundations/ItoIntegralAgainstMartingale.lean, Foundations/DriftProcessModification.lean, docs/specs/2026-08-16-ito-chain-rule-design.md §4.4.