The One-Parameter Banach Factorization for Stable Lévy Processes: Representability Obstructions and Leibniz Defects

Abstract

We study the Banach dual of the one-parameter stochastic integral δ_L(u) = ∫₀^T u_t dL_t for a symmetric γ-stable Lévy process with γ ∈ (1,2). The natural integrand exponent is p ∈ (1,γ): the small-jump integrability ∫|z|^p ν_γ(dz) < ∞ holds iff p < γ, so this is not an arbitrary L^p but the unique scale dictated by the singularity of the Lévy measure at the origin. On this scale, the operator-covariant derivative D_L := δ_L^* : L^q(Ω) → H_L^* is the Banach dual of the one-parameter integral. Since p < 2, the Riesz identification H_L^* ≅ H_L is unavailable, and the Banach setting is forced. The principal result is structural: D_L is strictly more restricted than the standard Malliavin add-a-point operator D_{t,z}F = F(ω + δ_(t,z)) − F(ω) on Poisson space, which is the dual of the full two-parameter compensated Poisson integral ∫∫ h(s,z) Ñ(ds,dz). By Lévy-Itô, the one-parameter integrand of δ_L has the special form h(s,z) = u(s) · z — linear in z — whereas full martingale representation on Lévy space uses general h(s,z). The representability obstruction quantifies the resulting gap precisely: centered functionals depending nonlinearly on jump sizes — canonically, the centered large-jump count #{|ΔL_s| > 1} − E[#{|ΔL_s| > 1}] — lie in ker(D_L) 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^p_0(Ω) 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 D_L, 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(D_L) and the annihilator of im(δ_L) via L^q-L^p 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.