Public theorem chain constructs a bounded star-shaped non-disk with C² boundary and a global C² field satisfying normalized Helmholtz and zero full boundary gradient, then derives failure of the Pompeiu property.
Public formal source; execution and statement correspondence are separate checks.
1 cited passage ↓1 problem ↓Record 2938e277969c329caf154e48a3d8823f3635c7f1 ↓
The exact passages cited in OpenMath. Each passage identifies how its wording was recorded.
Public theorem chain constructs a bounded star-shaped non-disk with C² boundary and a global C² field satisfying normalized Helmholtz and zero full boundary gradient, then derives failure of the Pompeiu property.
Passage ID: schiffer-pompeiu:entry:lean:v1
Source item: lean
Source record: schiffer-pompeiu:source: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
C² counterexample theorem reported complete in Lean
The normalized eigenvalue is one; the field is global C² and its full gradient vanishes on the boundary.
Observed Oct 13, 2026
Formal declaration
Star-shaped C² Schiffer counterexample
Scope
The normalized C² formal statement
Source assessment
Proved
Conditional mathematical implication in the cited source
The implication needs its stated boundary regularity and field assumptions. It does not classify every domain failing the Pompeiu property or assert an equivalence for rough domains.
Observed Oct 13, 2026
Source assessment
Proved
C² counterexample theorem reported complete in Lean
The normalized eigenvalue is one; the field is global C² and its full gradient vanishes on the boundary.
Observed Oct 13, 2026
Formal declaration
Star-shaped C² Pompeiu 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.
Connection
The project derives a nonzero test function with vanishing rigid-domain integrals from the normalized Schiffer field using Green’s identity.
History
An infinite family by uniform bifurcation
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: 2938e277969c329caf154e48a3d8823f3635c7f1
SHA-256 for this linked file. A matching checksum identifies the same bytes; it does not assess the mathematics.
02cdbc8f521968df2c2da3c6caad9fc1e93245230efff82ae4509615dc390e96Complete formal proof reported externally
Exact global C² normalized statement. Smoothness, the tenfold analytic frequency interval and every symmetry order are not attributed to this declaration.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Schiffer.Comparator.Schiffer_Star_ShapedCommit 2938e277969c329caf154e48a3d8823f3635c7f1
Complete formal proof reported externally
A continuous nonzero real test function has zero integral over every rigid copy of the formal domain. The simply-connected corollary follows from contractibility.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Schiffer.Comparator.Pompeiu_Star_ShapedCommit 2938e277969c329caf154e48a3d8823f3635c7f1
Recorded authorship
Jaume de Dios Pont · Gonzalo Cao-Labora
Jaume de Dios Pont, Gonzalo Cao-Labora
The repository attributes formalization to OpenAI Codex. Its metadata reports agent review rather than independent human peer review. The formal path and C² scope differ from the later smooth manuscript.
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 star-shaped Schiffer/Pompeiu construction
OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.
Source terms ↗