AI 中文总结
该研究分析ℓ^p及其直和有限维子空间的Plücker坐标性质，证明相关子流形的结构，给出分层结果，且核心理论已在Lean~4中形式验证。
AI 中文摘要
ℓ^p的n维子空间具有以ℕ的n元子集为索引的Plücker坐标。我们证明这些坐标属于ℓ^{p⟨n⟩}——指数保持不变——当0<p≤2时，其多重线性范数恰好为1；当p>2时，最优常数大于1，且其确定包含Hadamard最大行列式问题。一个重构引理表明，ℓ^{p⟨n⟩}中二次Plücker关系的每个非零解都可分解为具有ℓ^p框架的形式；因此Gr_n(ℓ^p)是ℙ(ℓ^{p⟨n⟩})中的闭Banach-解析子流形，仅由Plücker关系单独截出，无辅助可和性条件且无需极化。对于混合直和⊕ℓ^{p_i}，外幂按n的分次分级；该分级的支撑是由子空间与部分和的相交模式确定的广义permutohedron的格点集，此分层对等距群是典范的，但对GL群并非如此，每个层都存在管状邻域，其法坐标恰好是在该层上消失的Plücker块。我们记录了已证明和猜想的内容；该理论的有限性和单空间核心，包括Cauchy–Binet和Hadamard不等式的完整证明，已在Lean~4中得到形式验证。
英文摘要
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.
Comments14 pages
