Metadata
slug: kenins-kiselev-2026-wronskian-perfect-lonely-algebra
bibkey: keninskiselev2026wronskianalgebras
doi: 10.48550/arXiv.2605.27305
url: https://arxiv.org/abs/2605.27305v2
triage: theorem
motivation_gids:
- D5/S3/HomologicalAlgebra/WronskianPerfectLonelyAlgebra.result
Perfect homogeneous Wronskian extensions exist exactly at order one
Problem
Markuss G. Ķēniņš and Arthemy V. Kiselev, Explicit class of finite-dimensional polynomial algebras with Wronskians over as -ary Lie brackets: beyond , arXiv:2605.27305v2 (2026), subsection (Im)perfect N-ary SH-Lie polynomial algebras, Open problem open:perfect-algebras. The following is the verbatim TeX paragraph at line 1259 of FinDim220526v2.tex (md5 777135f176c9db701f21e5554216fb33):
Let the base dimension and differential order be arbitrary. Put the complete generalised Wronskian as the \nobreakdash-ary bracket, , on the \nobreakdash-ary SH-Lie polynomial algebra . Does there exist an homogeneous polynomial of degree such that the \nobreakdash-ary SH-Lie polynomial subalgebra is \emph{perfect} w.r.t\ the Wronskian, i.e.\ ?
The source macros are retained in the quotation: \Bone is the identity operator, \bx denotes , \wedges denotes , \EuA denotes , and \Span denotes linear span. The source takes or and writes for polynomials of degree at most (TeX lines 538–542 and 613–623).
Issue #22115 fixes the statement over a characteristic-zero field . Put
Here is ordinary iterated partial differentiation, without divided-power normalization. The settled statement is: for every characteristic-zero field , every and every ,
This classification is proved.
Motivation
The source’s research problem concerns perfect finite-dimensional polynomial algebras with the complete Wronskian as bracket (TeX lines 525–527). Perfectness requires regeneration of the entire vector space by bracket values, in addition to closure. Over the source fields or , the source’s main theorem 1 establishes closure of for every , and homogeneous of degree (lines 1187–1192). The open problem asks which parameter pairs also permit perfectness. The settlement gives the exact order restriction throughout the requested range .
Gap
Issue #22115 records the bounded literature check:
- The orchestrator (Claude Code, Opus) checked the v2 TeX question and searched for complete Wronskian brackets, perfectness and homogeneous top-degree polynomials; the reported hits were the source and arXiv:2510.02145.
- The same report checks the abstract of the authors’ follow-up arXiv:2607.26039v2, which concerns degree growth under iterated brackets and does not mention perfect lonely algebras.
- The codex-cli search report identified in the issue attributes zero citing works to OpenAlex, no settlement to arXiv:2510.02145v1 or arXiv:2610.08636v1, and no match to formal-conjectures. MathDB returned HTTP 403.
- The preregistration reports no earlier repository issue title, module, Library note or dossier for arXiv:2605.27305.
not-found-in-searched-scope. These search reports do not establish exhaustive novelty or priority.
Route
All lemma names below belong to D5.S3.HomologicalAlgebra.WronskianPerfectLonelyAlgebra; the proof helpers are private.
- Reduce to omission brackets. Over any field , for arbitrary natural and arbitrary polynomial ,
lonely_eq_spanidentifies with the span of and the monomials for . For any with every ,bracket_mem_span_basisexpands into brackets of this generating family. For every selection ,bracket_mem_span_omissionsplaces its generator bracket in the span of the brackets omitting one generator. Repetitions give equal columns and zero determinant; injective selections differ from one omission bracket by a column-permutation sign. Neither lemma requires to be nonzero or homogeneous. - Separate homogeneous degrees. Over any field , for arbitrary natural , functions and satisfying that each is homogeneous of degree ,
wronskian_homogeneousmakes homogeneous of degree , with truncated natural subtraction. This allows a zero bracket and does not assert nonvanishing or exact total degree. Over any field and arbitrary natural , if is homogeneous of degree ,omittedBracket_homogeneousmakes the bracket omitting homogeneous of degree zero, and the bracket omitting homogeneous of degree . - Obstruct higher orders. Over any field, for arbitrary natural and , homogeneous of degree , and with all arguments in ,
projected_bracket_boundputs the degree- component of in the span of the brackets omitting . Over a characteristic-zero field, for , and every homogeneous of degree ,upper_order_obstructionconcludes . Its dimension contradiction uses the pure powers and : these are distinct, linearly independent degree- monomials in , whereas the projected bracket span has at most generators. The proof establishes finite-dimensionality of that span before using its dimension. Nonzeroness of is not a hypothesis of the obstruction. - Construct at order one. Over any field , for arbitrary natural and homogeneous quadratic ,
first_order_evaluationsgives . Replacing the constant column by gives ; replacing the column by gives . These replacements retain their original column positions. Euler’s quadratic identity supplies the determinant calculation. Over a characteristic-zero field with ,quadratic_constructiontakes , uses and invertibility of to obtain every generator from brackets, and also puts every bracket in . It supplies a nonzero homogeneous quadratic with . Finally, over a characteristic-zero field with and ,resultcombines this construction withupper_order_obstructionto proveclaim.
Falsifier
A statement about a different differential operator or a weaker notion of perfectness would not settle the source’s question. The module uses:
I d k, all differential multi-indices of total order at most , each once;pderivMulti, ordinary repeated partial derivatives in coordinate order, andwronskian, their determinant on all arguments;lonely, the submodule sum ;perfect, the equality , which includes both closure under brackets and generation by their values.
For nonzero homogeneous of degree , the sum defining lonely is direct because its other summand has degree at most . Indexing arguments by rather than only changes their order, hence at most the sign of a bracket and not its span. Factorial-normalized monomials appearing elsewhere in the source change the generating basis by nonzero scalars over a characteristic-zero field; the differential operators themselves are not divided by factorials.
The claim excludes , even though Lean’s homogeneous predicate includes the zero polynomial. Its quantifiers require , and characteristic zero. It asserts existence at order one, not perfectness for every quadratic. The module does not separately formalize the SH-Lie identities of the ambient Wronskian algebra.
Evidence
The canonical source is D5/S3/HomologicalAlgebra/WronskianPerfectLonelyAlgebra.lean (622 lines).
- Proof. It proves
result : claim. - Axioms. It uses only the standard axioms
propext,Classical.choiceandQuot.sound; nosorry,native_decide, or new axiom.
Frozen state: Golden/Frozen/state/D5/S3/HomologicalAlgebra/WronskianPerfectLonelyAlgebra.lean.json, statement sha256:f5460286f014eb9743ef7e91a871cf267d8f0a47c5d6d08d4227d1879082fddd.
Declaration statements:
result:sha256:c8924cc4055629e4033f1a9cf9945703d77b8a6e1b45645a6099dfd613d8d7aa;claim:sha256:b5a7734b29a11de2eed3edb8590a1df2bdd97236409f6c222c6ba8a45b9a33d5.
Triage
Tier 1: an explicit open problem in a 2026 preprint, preregistered in issue #22115 before any Lean.
theorem; resolution proved.
The module is admitted under the open-problem-resolution basis of CLAUDE.md §3.2; the per-declaration proof shapes are listed in the delivery PR. There is no digestion atom.
What the settlement shows
Proved by result: for every characteristic-zero field , every and every , a nonzero homogeneous polynomial of degree whose complete-Wronskian bracket values on span exactly that subspace exists if and only if .
Argued, not formalized.
- Size of the higher-order deficit. For a characteristic-zero field, , and homogeneous of degree ,
projected_bracket_bound, applied to arguments in , bounds each projected bracket by the span of omission brackets. Linearity of the homogeneous projection extends this bound to the entire projected bracket span. The degree- homogeneous space has the monomial basis of size . Subtracting dimensions therefore gives a deficit of at least in that component. This quantitative codimension statement is not an additional conclusion ofresult. - Which quadratics work. For a characteristic-zero field, and a nonzero homogeneous quadratic ,
first_order_evaluations, together withbracket_mem_span_basisfor arguments in andbracket_mem_span_omissionsfor their generator selections, gives . Every listed generator is an actual bracket value, and every bracket is in their span. The constant, linear and quadratic homogeneous components are independent, so exactly when the partial derivatives span all linear forms. Writing with its symmetric Hessian , the gradient is ; the condition is . Thus the remaining coefficient question at order one is a nondegeneracy condition. For example, has no derivative generating when . This criterion is an ordinary linear-algebra argument, not a separate compiled declaration. - A relaxed field hypothesis for the construction. For any field with and , is homogeneous of degree two and nonzero because the coefficient of is one. Its derivatives are , so
first_order_evaluationsapplied to this homogeneous quadratic gives as bracket values. They generate because is invertible. For arguments in ,bracket_mem_span_basisandbracket_mem_span_omissionsapplied to the generator selections put every bracket in their span. This extends the order-one construction as an argument;resultretains characteristic zero. No classification in positive characteristic is asserted here. - Sharpness and remaining scope. Within the formal range , , the transition at is exact. For a characteristic-zero field, , and homogeneous of degree ,
upper_order_obstructionuses two distinct coordinates to obtain its extra mixed monomial. It does not supply a conclusion for , missing lower-degree generators, or extensions with several independent top-degree generators. - Effect on the source. The explicit cross-references to
open:perfect-algebrasoccur in the problem and its following Comment (TeX lines 1258–1277). For the source fields or , and ,resultmakes that Comment’s generation requirement unattainable for every nonzero homogeneous of degree . For those fields, and , the quadratic criterion above answers the corresponding coefficient question. The source’s main theorem 1, over those same fields and for every , and homogeneous of degree , concerns closure, so the negative perfectness conclusion at higher orders does not contradict it. The later questionopen:existence-if-dropped-consistencyand conjectureconj:non-existence-of-inconsistent(lines 1669–1677) concern algebras with gaps in the lower-degree generators and remain outside this settlement.
ASSUMED-UNVERIFIED
The bounded literature check in #22115 does not establish exhaustive worldwide novelty or priority. Its web-search results, follow-up abstract reading, OpenAlex citation count, negative readings of arXiv:2510.02145v1 and arXiv:2610.08636v1, formal-conjectures search and earlier-repository-record search were not independently reproduced. MathDB’s HTTP 403 supplies no negative literature result. The v2 source question, its notation, the adjacent Comment, the closure theorem statement and the later inconsistent-algebra question were checked directly in the TeX identified above.
The random-polynomial rank readings attributed to the orchestrator (Claude Code, Opus) in #22115 remain unreproduced because the issue supplies neither the sampled coefficients nor a random seed. The codimension estimate, Hessian criterion, relaxed field hypothesis for the construction and discussion of consequences for the paper are argued rather than additional formalized statements. A complete dependency audit of the source’s proofs was not performed. The SH-Lie identities, the source’s general classification of finite-dimensional subalgebras, the dimension-one cases, order zero and positive-characteristic classification are not established by result.