slug: miska-ulas-2022-sigma-three-conjecture-4-8
bibkey: miskaulas2022sigma
doi: 10.1142/S1793042124500635
url: https://arxiv.org/abs/2203.03942v1
triage: theorem
motivation_gids:
  - D5/S3/Arith/MiskaUlasSigmaThreeBound.result

Refutation of Miska–Ulas Conjecture 4.8

Problem

Miska and Ulas, On the Diophantine equation σ₂(X̄ₙ) = σₙ(X̄ₙ), arXiv:2203.03942v1, page 16, Conjecture 4.8 states:

Let n ∈ N≥4 and suppose that m ∈ N satisfies m = σ_3(X_n) = σ_n(X_n). Then m ≤ (1/12)(3021n⁶ − 77575n⁵ + 920361n⁴ − 6235705n³ + 24764202n² − 53664304n + 48986640) and x_n ≤ (1/12)(27n⁴ − 190n³ + 471n² − 500n + 216).

Write $Q(n)$ and $D(n)$ for the two bounds, respectively. The source defines ${\sigma }_j$ as the elementary symmetric sum of products over $j$ distinct increasing indices, and a solution as a nondecreasing tuple of positive integers. The target is the conjunction as printed in version 1. Preregistration: #19678.

Statement echo

The rational casts preserve the integer inequalities and interpret the source’s factor $1/12$ exactly. The index proof follows from $n\ge 4$ and adds no mathematical hypothesis.

Motivation

For $k=n-4$, set $c=3\left(\genfrac{}{}{0ex}{}{k}{2}\right)+8k+7=(k+2)(3k+7)/2$ and $Y=(1^k,2,k+3,c)$. Let $d={\sigma }_3(Y)$ and append $d$ to obtain $X_n$. The product $P=2(k+3)c$ satisfies ${\sigma }_2(Y)+1=P$. Hence ${\sigma }_3(X_n)=d+d{\sigma }_2(Y)=dP={\sigma }_n(X_n)$. The family preserves positivity and order and violates the first proposed bound for every $n\ge 11$.

Gap

The universal coordinate bound $x_n\le D(n)$ remains open: the displayed family attains equality. A degree-seven or larger replacement bound for all solutions is also open. The journal publication metadata is verified, but its full text and whether it retains Conjecture 4.8 are unverified. No publication-priority claim is made.

Route

The settling module imports D5.S3.Combinatorics.Graph.MultipartiteCHS.Extremal and pinned Mathlib. D5.S3.Combinatorics.Graph.MultipartiteCHS.Extremal.esymm_cons supplies the adjoining-entry elementary-symmetric identity, and MvPolynomial.aeval_esymm_eq_multiset_esymm supplies the symmetric-sum correspondence. Multiset expansion, binomial coefficient identities, and polynomial normalization give the family, its domain conditions and its factored gap. The public theorem specializes the private family at $k=7$ and contradicts the first conjunct of claim.

The form is deposit-uncovered (no atom), settling D5/S3/Arith/MiskaUlasSigmaThreeBound.result. The module’s admission basis is open-problem-resolution (#19678; Refuted); every delivered declaration has proof_shape: bind-only and escape_witness: none. Its direct frozen D5 dependency is D5/S3/Combinatorics/Graph/MultipartiteCHS/Extremal, specifically D5.S3.Combinatorics.Graph.MultipartiteCHS.Extremal.esymm_cons. Private helpers are consumed within the settlement. Their compiled dependency map supplies the named consumers; no independent general-content result is asserted.

Falsifier

A proof of the printed universal conjunction would apply to the positive nondecreasing tuple at $n=11$ and force $40766040\le 40732020$, contradicting result. The refutation concerns the quoted conjunction, not the universal truth or falsity of its second conjunct.

Evidence

• Kernel evidence: D5/S3/Arith/MiskaUlasSigmaThreeBound.lean, public claim and result; the private family, xvals_domain, xvals_solution, product_gap, product_exceeds, and dval_cast supply the internal argument.
• Canonical mirror: Blueprint/D5/S3/Arith/MiskaUlasSigmaThreeBound.scribe.cs; its result has one Refuted resolution claim for this dossier.
• Source: Library/ArithUnits/miskaulas2022sigma.md.
• The public result is the designated refutation result (basis=refutes) and is exempt from four-slot escape registration (CLAUDE.md §3.9). The newly public D5.S3.Combinatorics.Graph.MultipartiteCHS.Extremal.esymm_cons has an unfinished four-slot escape audit: its source-family reconstruction and enrolled readout remain unsupplied under issue #20171.
• Experiment: exact family checks. Command: python3 /Users/auric/trureturing-experiments/docs/reports/miska-ulas-2022-sigma-three-conjecture-4-8/check.py, whose bytes match that pinned commit; exit 0. Script SHA-256: dfcb47cf22e6f66796b5d520e24886ec6331a4b6ad39cea6770419bbc0791d81. Exact tested scope: every integer $4\le n\le 200$. The checks establish tuple length, positivity, order, ${\sigma }_3={\sigma }_n$, $x_n=D(n)$, the factored gap, and strict excess exactly for $n\ge 11$ within that finite range.

Triage

What the settlement shows

The factored gap is $$m_n-Q(n)=\frac{27}{4}\prod _{j=4}^{10}(n-j).$$ Its seven factors show positivity for $n\ge 11$ and vanishing at the seven distinct integers $4,\dots ,10$. Since $m_n=2(n-1)cD(n)$ has degree seven with leading coefficient $27/4$, while $Q$ has degree at most six, $Q$ is the unique degree-at-most-six interpolant of this family’s values at those seven points. This algebraic explanation does not identify the authors’ numerical search range or their method of choosing $Q$. The family is compatible with a sharp universal second bound, whose proof remains open.

Declaration judgement

Every definition and theorem has proof_shape: bind-only; no same-delivery content declaration or escape witness occurs. The public judgement is:

The helper map is the inversion of the elaborated proof-term constants. Every private helper has a live consumer and remains bind-only; no helper is used as an independent admission witness. The newly public owner helper is consumed by defect_one, dval_expand, and appended_solution and is the audit target in #20171. The module admission basis is open-problem-resolution (#19678; Refuted). This classification reports normalization and consumed helper applications; it does not weaken the settlement of the externally named conjecture.

ASSUMED-UNVERIFIED

Literature completeness and continued prior-art openness are ASSUMED-UNVERIFIED. The source screen recorded in #19678 covers arXiv’s version record, title/identifier/author searches, indexed later works and the formal-conjectures archive; it found no matching settlement in that searched scope. The journal PDF was inaccessible, and exhaustive later-literature coverage and publication priority are unverified. The result refutes the quoted version-1 statement. Finite experiment checks do not by themselves establish any uniform unbounded conclusion.