Proved
Analytic tenfold witness certified by the authors ↗
The spectral frequency k lies between 31.967007261 and 31.967007293.
Source dated Aug 3, 2026 · Observed Oct 13, 2026
Theorem · version 2
An analytic tenfold counterexample
Statement
There exist a bounded simply connected non-disk Ω with real-analytic Jordan boundary and tenfold symmetry, a nonconstant classical real u and such that in Ω, u = 1 and on ∂Ω.
Assumptions
- Planar domain; real-analytic boundary.
- The exact construction and certified bounds of Colbrook–Stepaniants.
Scope
The narrow k interval belongs to the numerical certificate. The corresponding eigenvalue is k², not k.
- Geometry
- Simply connected non-disk; tenfold symmetry
- Boundary / field
- Real-analytic Jordan boundary; classical real field
- Numerical input
- k ∈ (31.967007261,31.967007293); eigenvalue λ = k²
- Evidence scope
- Numerical certificate and separately linked complete formal proof; the latter uses coarser exact bounds at the same dyadic centre
Evidence
Source reports
Proved
Analytic tenfold theorem reported complete in Lean ↗
The project records a Lean build on 9 September and a Comparator replay on 12 September. These are external reports, not OpenMath executions.
Source dated Sep 12, 2026 · Observed Oct 13, 2026
Formal proofs
Analytic tenfold Schiffer and Pompeiu counterexample ↗
Complete formal proof reported externally
The full statement includes real-analytic Jordan boundary, tenfold dihedral symmetry, the published frequency interval, a real analytic classical Schiffer field and Pompeiu failure. The formal proof checks its own coarser exact numerical bounds using the same dyadic centre as the interval certificate.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Declaration & revision
PompeiuSchiffer.Numerics.UnconditionalCounterexamples.exists_common_domainCommit 2fb3f2ecafd3233dbca390d73e764fe6e04a9c7d
Connections
In this problem · publication v6 · Selected context
Schiffer and Pompeiu conjectures →
Counterexample · Proved
Relationship not independently reviewed. This concerns its use in this problem.
In this problem · publication v7
Schiffer and Pompeiu conjectures →
Counterexample · Proved
Relationship not independently reviewed. This concerns its use in this problem.
Sources
A computer-assisted counterexample to the planar Pompeiu and Schiffer conjectures →
- Main theorem, computational certificate appendix and AI declaration → · Original passage ↗
Recorded wording
Constructs a non-disk simply connected domain with real-analytic Jordan boundary and tenfold symmetry, using certified numerical estimates.
paraphrase · OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.
Matthew J. Colbrook · George Stepaniants · Preprint · Publication date Aug 3, 2026
Revision & attribution
Source revision: 2026-08-03. Observed Oct 13, 2026.
The paper credits GPT-5.5 Codex for debugging early computational code, checked line by line by the authors. The authors own the mathematical argument and certificate.
Lean proof of the analytic tenfold construction →
- PompeiuSchiffer.Numerics.UnconditionalCounterexamples.exists_common_domain; Comparator definitions and verification record → · Original passage ↗
Recorded wording
The public theorem produces one analytic tenfold domain, its classical field, Pompeiu failure and the exact published frequency interval with no remaining numerical hypotheses.
paraphrase · OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.
Matthew J. Colbrook · George Stepaniants · Project documentation
Public formal source; execution and statement correspondence are separate checks.
Lean proof of the analytic tenfold construction — pinned source ↗No OpenMath execution recorded
Exact source inspected; OpenMath has not executed this formal proof project.
Revision & attribution
Source revision: 2fb3f2ecafd3233dbca390d73e764fe6e04a9c7d. Observed Oct 13, 2026.
No specific AI contribution is attributed by this source record.
Lean proof of the analytic tenfold construction — pinned source: 2fb3f2ecafd3233dbca390d73e764fe6e04a9c7d.
Numerical certificate and reproduction report →
- REPRODUCTION_REPORT.md; validation archive; Zenodo DOI 10.5281/zenodo.21765287 → · Original passage ↗
Recorded wording
The exact dyadic input centre, interval audits, tail bounds and standalone checker support the computer-assisted witness.
paraphrase · OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.
Matthew J. Colbrook · George Stepaniants · Project documentation
Frozen numerical certificate archive ↗No OpenMath execution recorded
Revision & attribution
Source revision: 2fb3f2ecafd3233dbca390d73e764fe6e04a9c7d. Observed Oct 13, 2026.
No specific AI contribution is attributed by this source record.
Frozen numerical certificate archive: 2fb3f2ecafd3233dbca390d73e764fe6e04a9c7d. Source reports rigorous interval and exact rational verification. OpenMath has not run the certificate or reproduced its numerical audits.
History
Statement versions
Statement versions and problem publication versions are separate. A new publication can update context or sources while retaining the same statement.
Assessment history · 2
Assessments retained in these publication records. Earlier statement versions retain their own source histories.
Proved
Analytic tenfold theorem reported complete in Lean ↗
The project records a Lean build on 9 September and a Comparator replay on 12 September. These are external reports, not OpenMath executions.
Source dated Sep 12, 2026 · Observed Oct 13, 2026 · Source passage →
Proved
Analytic tenfold witness certified by the authors ↗
The spectral frequency k lies between 31.967007261 and 31.967007293.
Source dated Aug 3, 2026 · Observed Oct 13, 2026 · Source passage →
Record details
- Claim ID
- claim-schiffer-analytic-tenfold-witness
- Statement version
- 2
- SHA-256
- 2b48ed0b43ddba91e6a9ecb85361b8ba71104fdffec887610cbe1f3fcc94b3ab