On the Quartic Invariant of Odd Degree Binary Forms

TL;DR

This paper determines the squarefree part of the scalar factor related to the quartic invariant of odd degree binary forms, generalizing classical identities and employing an AI-assisted proof workflow involving formal verification.

Contribution

It provides a complete characterization of the squarefree part of the scalar factor for the quartic invariant of odd degree binary forms, extending classical identities and illustrating an AI-assisted research methodology.

Findings

The squarefree part equals p when n+2 is a power of an odd prime p, and 1 otherwise.

The valuation properties of the scalar factor are explicitly described for primes p.

The proof integrates explicit coefficient analysis, p-adic deformation, and formal verification in Lean 4.

Abstract

We determine the squarefree part of the scalar factor that arises when the quartic invariant of the generic binary form $F$ of odd degree $2n+1$ is expressed as the discriminant of the unique quadratic covariant $(F,F)_{2n}$. This squarefree part is exactly $p$ when $n+2$ is a power of an odd prime $p$, and $1$ otherwise. Equivalently, for each prime $p$: $v_2(S(n))$ is always even, and for odd $p$, $v_p(S(n))$ is odd if and only if $n+2$ is a power of $p$. This generalizes the classical identity $\operatorname{disc}(H(F))=-3\cdot\operatorname{disc}(F)$ for binary cubics, which dates back to the work of Cayley and Sylvester in the 1850s. The proof, which involves substantial explicit coefficient analysis and $p$-adic deformation arguments, was developed using an AI-assisted research workflow: the author's earlier partial attempts were completed through systematic collaboration with Claude Code (Anthropic) and Codex (OpenAI), and key arithmetic lemmas were formally verified in Lean~4 using Aristotle (Harmonic). We describe this workflow in detail as a case study in AI-assisted mathematical research. We also discuss representation-theoretic, geometric, and arithmetic interpretations of the quadratic covariant.