Plücker coordinates of finite-dimensional subspaces of $\ell^p$ and its direct sums: summability, reconstruction, stratification
David Victor Feldman
math.FA
Aug 2, 2026 · v1
TL;DR
The finitary single-space core, including Cauchy–Binet and Hadamard's inequality, is formally verified in Lean 4.
Abstract
An $n$-dimensional subspace of $\ell^p$ has Plücker coordinates indexed by the $n$-element subsets of $\N$. We show these coordinates lie in $\ell^p\In{n}$ — the exponent is preserved — with multilinear norm exactly $1$ for $0<p\le 2$; for $p>2$ the sharp constant exceeds $1$ and its determination contains the Hadamard maximal determinant problem. A reconstruction lemma shows every nonzero solution of the quadratic Plücker relations in $\ell^p\In{n}$ is decomposable with frame in $\ell^p$; consequently $\Gr_n(\ell^p)$ is a closed Banach-analytic submanifold of $\mathbb{P}\big(\ell^p\In{n}\big)$ cut out by the Plücker relations alone, with no auxiliary summability condition and no polarization. For mixed sums $\bigoplus \ell^{p_i}$ the exterior power is graded by compositions of $n$; the support of the grading is the lattice-point set of a generalized permutohedron determined by the intersection pattern of the subspace with partial sums, this stratification is canonical for the isometry group though not for $\GL$, and each stratum admits a tubular neighborhood whose normal coordinates are precisely the Plücker blocks vanishing on it. We record what is proved and what is conjectured; the finitary and single-space core of the theory, including full proofs of Cauchy–Binet and Hadamard's inequality, has been formally verified in Lean 4.
Problem
Determine where the Plücker coordinates of an n-dimensional subspace of ℓ^p live, with sharp summability constants and exponents, and characterize the resulting Grassmannian as a Banach-analytic manifold.
Approach
Coordinates p_I are defined as n×n minors of a frame. The paper proves the exponent p is preserved via tensor-product arguments, with sharp constants obtained from Hölder, p-subadditivity, Cauchy–Binet, Hadamard's inequality, and multilinear interpolation. A reconstruction lemma shows nonzero solutions of the quadratic Plücker relations are decomposable, giving closedness and manifold structure, extended to mixed direct sums with a grading by compositions and metric stratification. The finitary single-space core, including Cauchy–Binet and Hadamard's inequality, is formally verified in Lean 4.
Results
The coordinates lie in ℓ^p with multilinear norm exactly 1 for 0<p≤2; for p>2 the sharp constant exceeds 1 and encodes the Hadamard maximal determinant problem. Gr_n(ℓ^p) is a closed Banach-analytic submanifold cut out by the Plücker relations alone, and for mixed sums the grading support is the lattice-point set of a generalized permutohedron.