Metadata
slug: krishna-2022-cstar-higher-order-smale-mean-value
bibkey: krishna2022cstarsmale
doi: 10.48550/arXiv.2206.08154
url: https://arxiv.org/abs/2206.08154v1
triage: theorem
motivation_gids:
- D5/S3/Quantum/Algebra/CStarSmaleHigherOrder.result
The Higher Order C*-algebraic Smale Mean Value Conjecture
Problem
K. Mahesh Krishna, C-algebraic Smale Mean Value Conjecture and Dubinin-Sugawa Dual Mean Value Conjecture*, arXiv:2206.08154v1, Section 2, Conjecture HIGHERMEAN; journal DOI 10.26117/2079-6641-2026-54-2-38-47, Conjecture 2.3, p. 44:
Let be a commutative C*-algebra. Let be a polynomial of degree over , . If is not a critical point of , then there exists a critical point of such that
The binding convention of #14982 uses Polynomial A, iterates of Polynomial.derivative, and CommCStarAlgebra A. The factor index Fin n retains every root with multiplicity. Noncritical means ; the same must satisfy every inequality.
Motivation
The frozen declaration D5/S3/Quantum/Algebra/CStarSmaleHigherOrder.result : ¬ claim refutes the conjecture already in the commutative unital C*-algebra with its supremum norm, at degree three.
Gap
The Tier 1 preregistration #14982 records the source and literature readings: the only arXiv version is v1; the journal retains the named conjecture; the checked later Casas–Alvero, Bieberbach/Corona and non-Archimedean Smale/Dubinin–Sugawa papers do not address this inequality in a product C*-algebra. No MathDB page was located. These are attributed preregistration readings, not-found-in-searched-scope, rather than a claim of worldwide priority.
Route
At , take , , , and the three roots
Their factor product is . Its complete critical set is
with the signs independent. The second coordinate gives , hence . At zero, and , with norms and . For every critical point the term is therefore at least
Falsifier
The public claim preserves the universal source statement. A nonzero first derivative at and failure at for every critical point contradict its existential conclusion. The private critical_set lemma enumerates all four critical points, so the refutation does not rely on selecting only some of them.
Evidence
The Lean module is D5/S3/Quantum/Algebra/CStarSmaleHigherOrder.lean, with public definitions smalePoly and claim and the sole public theorem result. The private lemmas compute the factor polynomial and its derivatives, enumerate the critical points, prove the gap bound and the strict failure. Their live uses culminate in result. The axiom closure of every public declaration is contained in {propext, Classical.choice, Quot.sound}.
The numerical experiment entry is docs/reports/krishna-2022-cstar-higher-order-smale-mean-value/. Command: python3 check.py; exit 0; script SHA-256 66a503c5e957e7d7f9619a59f92cae90311bdb0d6fedc396f20bd7d8e8a74ebe. Tested scope: , , , all four critical points. The readings are , ; the two critical points with first coordinate have gap approximately and term approximately , and the other two have gap and term . The exact minimum is . These numerical readings corroborate the kernel-checked fixed instance.
Triage
Tier 1; resolution Refuted by D5/S3/Quantum/Algebra/CStarSmaleHigherOrder.result. proof_shape: bind-only; escape_witness: none; admission_basis: open-problem-resolution (#14982). Utility: certified-instance, with basis=refutes the module’s claim.
The public result is the designated refutation result (basis=refutes) and is exempt from four-slot escape registration (CLAUDE.md §3.9).
What the settlement shows
- Proved, kernel-checked fixed witness: at , private
critical_setgives second coordinate for every critical point;critical_gapproves . Privatederivative_normandsecond_normgive norms and ; these imply the lower bound , andfailing_termproves the strict failure . The publicresultrefutes the full claim. - Proved in prose, not formalized, family and unboundedness: for every real , the roots and in the first coordinate, paired with in the second, yield . At zero its derivative norms are and . Every critical point still has second coordinate and critical-value gap at least , so the term is at least . Given any finite proposed replacement constant , choosing makes that term exceed at every critical point. No finite constant replaces already at degree three in .
- Proved in prose, mechanism: the supremum norm combines curvature from the first coordinate with an unavoidable critical-value gap from the second. Separate scalar bounds on each coordinate do not control the product of these maxima. The fixed witness proves that this obstruction occurs in an actual common polynomial and every one of its critical points.
- Literature reading, degree two: the source’s Theorem 2.2 (journal p. 44) proves Conjecture 2.3 for degree two. The counterexample has degree three; the degree-two theorem and scalar higher-order theorem retain their stated scopes and are not formalized here.
- Computed readings: the pinned experiment entry and command in Evidence test exactly , , and all four critical points. They give minimum . The uniform family conclusion above is a prose argument, rather than an extension of the numerical tested scope.
- Related literature/delivery: the same paper’s Conjecture DUALSMALE is refuted in the separate delivery #14940; it is a different first-derivative assertion.
- Open: whether additional restrictions on the coordinates of , for example connected , imply this inequality. The disconnected two-point space underlying does not decide the connected case.
- Open: the paper’s CSMALE conjecture, its strong form and its dynamics conjecture. This module supplies no settlement of them.
- Effect on source results: HIGHERMEAN fails at degree three and any unrestricted bound obtained by assuming it lacks that premise. The source’s independently proved degree-two and scalar results are unaffected; no additional source theorem is refuted here.
ASSUMED-UNVERIFIED
Absence of a prior settlement outside the accessible literature scope is unverified. The general family and no-finite-constant conclusion are proved in prose, not Lean. The connected-space case and the other named conjectures remain open. Numerical values are computational corroboration, not additional kernel-checked declarations.