We study the Banach dual of the one-parameter stochastic integral δL (u) = ∫₀T uₜ dLₜ for a symmetric γ-stable Lévy process with γ ∈ (1, 2). The natural integrand exponent is p ∈ (1, γ): the small-jump integrability ∫|z|ᵖ ν_γ (dz) 1} − E#|ΔLₛ| > 1 — lie in ker (DL) yet are detected by the standard add-a-point operator. The obstruction is a property of the one-parameter integral, not a feature of jump processes themselves. The factorization (Theorem A) holds on the closed proper subspace im (δL) ⊊ Lᵖ₀ (Ω) and characterizes precisely which functionals admit one-parameter representation. Theorem B (product rule with Leibniz defect) is a standalone duality identity: its proof uses only the definition of DL, the Lévy-Itô formula, and Hölder's inequality, and it does not invoke (H3) or the factorization machinery. Theorem C — the strongest technical result — identifies ker (DL) and the annihilator of im (δL) via Lq-Lᵖ truncation in the jump variable, showing the annihilator is infinite-dimensional even within the first chaos. The framework has been formally verified in the Lean 4 proof assistant (2, 439 lines, zero sorry, zero axioms) using Mathlib. To our knowledge, this is the first formalization of the operator-covariant derivative framework with its representability obstruction in any proof assistant. The formalization includes proved Poisson mean and variance identities, a constructed compound Poisson path, a compensated-integral interface with derived Banach-side consequences, a concrete first-chaos orthogonality model, and the full abstract theorem pipeline — all machine-checked from clearly isolated stochastic-analysis assumptions.
Ramiro Fontes (Sun,) studied this question.