The public theorem produces one analytic tenfold domain, its classical field, Pompeiu failure and the exact published frequency interval with no remaining numerical hypotheses.
Public formal source; execution and statement correspondence are separate checks.
1 cited passage ↓1 problem ↓Record 2fb3f2ecafd3233dbca390d73e764fe6e04a9c7d ↓
The exact passages cited in OpenMath. Each passage identifies how its wording was recorded.
The public theorem produces one analytic tenfold domain, its classical field, Pompeiu failure and the exact published frequency interval with no remaining numerical hypotheses.
Passage ID: schiffer-pompeiu:entry:computer-lean:v1
Source item: computer-lean
Source record: schiffer-pompeiu:source:computer-lean:v1
Explicit citations in versioned problem publications. A citation records a use; it does not confer proof or independent verification.
Problem publication v7
Source assessment
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 date Sep 12, 2026 · Observed Oct 13, 2026
Formal declaration
Analytic tenfold Schiffer and Pompeiu counterexample
Scope
An analytic tenfold counterexample
Research activity
Compare the two evidence routes
The analytic witness has frozen numerical input data and a certificate; the bifurcation construction has a separate C² formal theorem.
Neither external project has been executed by OpenMath.
History
The analytic certificate receives a public Lean replay
Question
Schiffer and Pompeiu conjectures
Further reading
Inspect the formal statement, assumptions and reported checks.
Linked manuscripts, code and data. External proof reports, statement correspondence and OpenMath execution are separate checks.
Formal code
No OpenMath execution recorded
Exact source inspected; OpenMath has not executed this formal proof project.
Resource revision: 2fb3f2ecafd3233dbca390d73e764fe6e04a9c7d
SHA-256 for this linked file. A matching checksum identifies the same bytes; it does not assess the mathematics.
f14c1f0df5e92636dfe42cd78674f23cf0fa2f1ab221fcfaba6bc1ce38ed611aComplete 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
PompeiuSchiffer.Numerics.UnconditionalCounterexamples.exists_common_domainCommit 2fb3f2ecafd3233dbca390d73e764fe6e04a9c7d
Recorded authorship
Matthew J. Colbrook · George Stepaniants
Matthew J. Colbrook, George Stepaniants
No specific AI contribution is attributed by this source record.
OpenMath source records preserve exact citations. Observation dates order these records; they do not establish the latest upstream paper or proof.
Lean proof of the analytic tenfold construction
OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.
Source terms ↗