Recognition and Eutaxy Testing of Bacher Matrices

Research-attempt provenance

Definitions and mathematical statement

Shared notation.

Standard number systems are denoted by $\mathbb N,\mathbb Z,\mathbb Q,\mathbb R,\mathbb C$; index ranges, computational models and specialized notation follow the cited problem source and the definitions below.

For a positive-definite form $Q(x)=x^TAx$ on $\mathbb R^n$, $S(Q)$ contains the nonzero integer vectors minimizing $Q$. A form is well rounded when $S(Q)$ spans $\mathbb R^n$. With the minimum fixed, the cell $C_S$ consists of forms having precisely $S$ as their minimal-vector set; classes are taken up to integral invertible changes of basis. Its Bacher matrix is $\sum_{x\in S}xx^T$. Weak eutaxy means $A^{-1}=\sum_{x\in S}\lambda_xxx^T$ for real coefficients $\lambda_x$, while eutaxy requires strictly positive coefficients.

Statement recorded in the supplied source.

Given an integral matrix $A$, decide whether it is the Bacher matrix of an equivalence class of forms and construct an associated class when one exists. Also give a fast algorithm that decides from a Bacher matrix whether its equivalence class contains a weakly eutactic form. [S2]

Scope qualification.

These definitions are the original report's fixed-minimum, well-rounded conventions. The source does not quantify the requested fast running time.

Source status.

The supplied catalogue labels this record open. Its source-status metadata was checked against the supplied snapshot on 2026-10-11. This import does not independently establish current open status or mathematical correctness. The catalogue literature assessment is dated 2026-08-21.

Short English statement

Recognize matrices encoding these quadratic-form cells, reconstruct a cell class, and test whether it contains a weakly eutactic form.

Sources

• S1 Ulam AI and the UnsolvedMath Contributors, UnsolvedMath: A Curated Collection of Open Mathematics Problems, record 30000162 (OWR-782-003). Catalogue curation and metadata: CC BY 4.0. The supplied source question is retained; definitions and the English summary are editorial additions. https://huggingface.co/datasets/ulamai/UnsolvedMath.
• S2 Gitter und Anwendungen $2005$, Oberwolfach Reports, DOI 10.4171/owr/2005/01, pp. 5--67 https://doi.org/10.4171/owr/2005/01.
• S3 primary OWR paper text https://ems.press/content/serial-article-files/45975?nt=1.
• S4 Original Oberwolfach Report 1/2005, Jacques Martinet with Anne-Marie Berge, pp. 24--25 https://ems.press/content/serial-article-files/45975. Underlying Oberwolfach Reports material retains its source-specific licence, including CC BY-SA 4.0 where applicable; see THIRD_PARTY_NOTICES.md.

Preparation and review.

Original question attributed to the cited source and UnsolvedMath contributors. Codex (GPT-6; exact serving revision not exposed) assisted with definitions, English summaries, source inspection and formatting. No new human mathematical authorship or independent proof verification is asserted. Canonical ID 30000162 and source code OWR-782-003 checked against the complete supplied registry and existing repository statements; known flagged repetitions and obvious identical conjectures excluded. Full mathematical-equivalence/literature review has not been performed. Statement preparation and final review followed contribution prompts C and D; automated checks verify structure and identity, not open status.

Literature and context check

The primary report, printed pages 24--25, fixes the minimum and restricts to well-rounded forms. Its three questions ask for recognition, construction, and a fast weak-eutaxy test. The following supplies a finite recognition/construction procedure in these conventions, with no useful running-time bound and no novelty claim. It also checks one weak-eutaxy special case. This does not answer the combined algorithmic target, and no general fast test is obtained. The report's assertions about uniqueness of weakly eutactic forms are context only; the proof below does not use them.

Research attempt: Finite recognition by an explicit lattice cutoff

A finite list of possible minimal sets

Write the input matrix as $B$, reserving $Q$ for a symmetric form matrix. Reject $B$ unless it is symmetric positive definite and entrywise even. These are necessary because a spanning antipodal set gives \[ B=2\sum_{v\in T}vv^T, \] where $T$ contains one vector from each antipodal pair. Every minimal integer vector is primitive: if $v=ku$ with integer $|k|\geq2$, then $Q[u]=Q[v]/k^2<Q[v]$. Moreover $2v_i^2\leq B_{ii}$. Thus enumerate the finite primitive integer vectors satisfying these coordinate bounds and choose the representative whose first nonzero coordinate is positive. Enumerate all subsets $T$ of this list, retaining exactly those with $2\sum_{v\in T}vv^T=B$. Their sets $S=T\cup(-T)$ span because $B$ is positive definite. The empty or nonspanning cases have therefore already been rejected. All matrix tests can be performed with rational arithmetic; for example exact symmetric elimination tests positivity.

An explicit finite substitute for all lattice inequalities

Fix one candidate $S$ and choose $n$ independent vectors $v_1,\ldots,v_n$ from it. Let $V$ have these columns and put \[ L=n\lVert V^{-1}\rVert_F^2,\qquad K\in\mathbb N,\quad K^2\geq16n\max(1,L),\qquad \delta=\frac1{4K^{2n}}. \] Choose an integer $R$ with \[ R\geq2K^n,\qquad R\geq2\max_{v\in S}\lVert v\rVert_2. \] Consider the finite linear system in the symmetric entries of $Q$: \[ Q[v]=1\ (v\in S),\qquad Q[w]>1\quad(w\in\mathbb Z^n\setminus S, 0<\lVert w\rVert_2\leq R). \tag{1} \] We prove that $1$ is equivalent to positive definiteness with precisely $S$ as the set of minimum-one vectors. Necessity is immediate. For sufficiency, initially do not assume $Q$ is positive definite.

All nonzero $v_i\pm v_j$ lie in the tested ball, and their quadratic values are at least one. Hence $C=V^TQV$ has diagonal entries one and $|C_{ij}|\leq1/2$ for $i\ne j$, since $Q[v_i\pm v_j]=2\pm2C_{ij}$. For every real $z$, \[ |z^TCz|\leq\left(\sum_i|z_i|\right)^2\leq n\lVert z\rVert_2^2. \] It follows, by substituting $z=V^{-1}u$, that $|u^TQu|\leq L\lVert u\rVert_2^2$. In particular the absolute values of all eigenvalues of $Q$ are at most $L$.

Suppose the least eigenvalue $\lambda$ were less than $\delta$, and let $v$ be a corresponding unit eigenvector. Partition $[0,1)^n$ into $K^n$ half-open cubes of side $1/K$. Two of the $K^n+1$ fractional-part vectors of $jv$, $0\leq j\leq K^n$, lie in the same cube. Subtraction gives an integer $1\leq q\leq K^n$ and $w\in\mathbb Z^n$ with $w=qv+e$ and \[ \lVert e\rVert_2\leq\sqrt n/K\leq1/4. \] Thus $w\ne0$ and $\lVert w\rVert_2\leq K^n+1/4\leq R$. Decompose $e=(v\cdot e)v+e_\perp$. Orthogonality to an eigenvector removes the cross term, including when $\lambda$ is negative: \[ Q[w]=\lambda(q+v\cdot e)^2+Q[e_\perp] \leq\delta(K^n+1/4)^2+Ln/K^2 \leq\frac{25}{64}+\frac1{16}<1. \] Here $K^n\geq1$ gives $(1+1/(4K^n))^2/4\leq25/64$. This contradicts the tested inequality, also if $w\in S$, where equality to one was required. Consequently $Q\succeq\delta I$. Finally every untested integer vector has norm greater than $R\geq2K^n$, and therefore $Q[w]\geq\delta\lVert w\rVert_2^2>1$. This proves sufficiency and rules out a hidden boundary at infinity.

Deciding and constructing a form

System $1$ has rational coefficients with both equalities and strict inequalities. It can be decided and, if feasible, solved over the rationals by finite elimination. To see this without assuming a strict-feasibility oracle, replace equalities by two non-strict inequalities. On eliminating a variable, its inequalities give finitely many lower and upper bounds. Require every lower bound to be at most every upper bound, using a strict comparison whenever either original bound was strict. Bounds independent of that variable are retained. If one side has no bounds there is no pair constraint. These comparisons are again rational linear inequalities, after multiplication by the fixed positive denominators coming from the eliminated coefficients. Repetition ends with comparisons between constants. Back substitution chooses a rational between the finite rational endpoints; a closed singleton is allowed, an excluded endpoint is not, and an unbounded side permits a sufficiently large rational. This proves correctness and rational constructibility of the finite procedure. It terminates for each candidate $S$, and supplies $Q$ and the cell description by its exact minimal set whenever recognition succeeds. It does not need the report's separate theorem that a Bacher matrix characterizes an equivalence class.

A weak-eutaxy boundary case

For $B=2I_n$, the coordinate budgets imply every coordinate occurs with value $\pm1$ in exactly one representative vector. If a vector used distinct coordinates $i,j$, it would contribute a nonzero $ij$ entry with no other representative able to cancel it. Thus $S=\{\pm e_i\}$. The form $Q=I_n$ has exactly this minimum set, and is eutactic with coefficients $1/2$ for all $2n$ vectors. It is the only weakly eutactic form in this cell: the condition $Q^{-1}\in\operatorname{span}\{e_ie_i^T\}$ forces $Q^{-1}$, and hence $Q$, diagonal; its prescribed diagonal values are one. This small exact case does not test general cells efficiently.

Verification and adversarial audit

The cutoff argument explicitly permits negative least eigenvalues before establishing positivity; an orthogonal decomposition avoids an unjustified sign-sensitive cross-term estimate. Integer vectors on the cutoff sphere are included, and the remaining vectors satisfy a strict inequality. Antipodal pairing, primitiveness, positive definiteness of the input, and strict inequalities excluding additional minimum vectors are all essential. For $n=1$ the same argument remains valid; the only well-rounded minimum set is $\{\pm1\}$ and the input is $B=(2)$. No complexity estimate polynomial in the input length follows from enumerating subsets, the radius $R$, or strict linear elimination.

Audit corrections.

Separated finite decidability from the requested fast test; included nonpositive candidate forms in the cutoff audit and credited the parent model's mathematical correction.

External computation.

None; symbolic arguments and boundary checks only.

Scope and remaining gaps

Finite recognition and reconstruction in the stated fixed-minimum conventions are proved above as a known-style exhaustive route; this contribution makes no literature-priority claim. The fast weak-eutaxy part, running-time improvements, and a general practical implementation remain unresolved. The aggregate original question is not marked solved. The parent Codex GPT-6 mathematical audit suggested the orthogonal-eigenvector decomposition used in the cutoff proof, which was checked and incorporated by gpt-6-astra.

Integration review.

Codex (GPT-6; exact serving revision not exposed) reviewed the written arguments and expanded layout and source-reference wrappers. Repository metadata and the production web renderer were checked using Python 3.13 and JavaScript with MathJax 3.2.2. This model-assisted review is not independent human proof verification; no PDF compilation or formal proof checking is asserted.

Completion Estimate

COMPLETION: 0% The calculations below the preserved source statement investigate a concrete route, but establish no substantiated new progress toward the entire original target. Known special cases and failed sufficient conditions are not credited as a solution.

References

The original source references and catalogue attribution are preserved in the Sources section above. The following URLs were actually consulted for this attempt; retention of an additional original reference does not claim fresh consultation of it.

• https://ems.press/content/serial-article-files/45975 (consulted 2026-10-11).

Model and contributor disclosure

OpenAI gpt-6-astra, requested reasoning configuration ultra, generated this research attempt on 2026-10-11. The exact serving revision is not exposed. Codex GPT-6 performed orchestration, repository-format review, and the mathematical cutoff-proof suggestion expressly credited above; its exact serving revision is also not exposed. The mathematical route, boundary checks and final adversarial self-audit followed contribution prompts A then B in docs/contribution_prompts.md, after reading CONTRIBUTING.md. Python 3.14.2 assembled the standalone documents; any mathematical computation is specified in Verification. No theorem prover was used. No human mathematical authorship, substantial human proof correction, or independent human proof checking is asserted. Model-assisted review, source retrieval, and structural checks do not establish correctness or novelty. Full private reasoning transcripts are unavailable as reproducibility artifacts; the complete arguments, inputs and outcomes actually used are stated here or in the companion batch audit.

Final status

Unresolved as a new research contribution. This is a concrete route investigation, not a claim of new complete resolution or a current-status certification. A known answer reproduced for context does not become a new contribution. The catalogue's source-status label is preserved; this attempt status does not assert that a source-labelled solved question is open.