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
Theorem · version 1
A formal non-disk failing the Pompeiu property
Statement
There exist a nonempty bounded star-shaped planar non-disk Ω with C² boundary and a continuous real f, not identically zero, such that the integral of f over every rigid-motion image of Ω equals zero.
Assumptions
- Planar Lebesgue measure and all affine isometries.
- The star-shaped C² witness provided by the cited formal construction.
Scope
The theorem derives Pompeiu failure from its own Schiffer witness through Green’s identity. It is a related conclusion, not a third geometric construction.
Evidence
Source reports
Formal proofs
Star-shaped C² Pompeiu counterexample ↗
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
Declaration & revision
Schiffer.Comparator.Pompeiu_Star_ShapedCommit 2938e277969c329caf154e48a3d8823f3635c7f1
Connections
In this problem · publication v2 · Selected context
Schiffer and Pompeiu conjectures →
Counterexample · Proved
Related statements
The project derives a nonzero test function with vanishing rigid-domain integrals from the normalized Schiffer field using Green’s identity.
This records the source’s construction-specific implication; it is not an equivalence for arbitrary rough domains.
Details & sources
The normalized C² formal statement →
Proved · version 1
There exist a nonempty bounded star-shaped planar non-disk Ω with C² boundary and a global real C² field u such that in Ω, u = 1 and on ∂Ω.
- C² boundary is specified by a global C² defining function with nonzero gradient on its zero set.
- Star-shaped about the origin; hence the domain is contractible and simply connected.
Scope: The formal comparator uses eigenvalue one after dilation and a vanishing full boundary gradient. It does not claim the analytic frequency interval or the manuscript’s C∞ regularity.
A formal non-disk failing the Pompeiu property →
Proved · version 1
There exist a nonempty bounded star-shaped planar non-disk Ω with C² boundary and a continuous real f, not identically zero, such that the integral of f over every rigid-motion image of Ω equals zero.
- Planar Lebesgue measure and all affine isometries.
- The star-shaped C² witness provided by the cited formal construction.
Scope: The theorem derives Pompeiu failure from its own Schiffer witness through Green’s identity. It is a related conclusion, not a third geometric construction.
Relationship not independently reviewed.
Connection in Schiffer and Pompeiu conjectures →Relationship not independently reviewed. This concerns its use in this problem.
In this problem · publication v7
Schiffer and Pompeiu conjectures →
Counterexample · Proved
Related statements
The project derives a nonzero test function with vanishing rigid-domain integrals from the normalized Schiffer field using Green’s identity.
This records the source’s construction-specific implication; it is not an equivalence for arbitrary rough domains.
Details & sources
The normalized C² formal statement →
Proved · version 2
There exist a nonempty bounded star-shaped planar non-disk Ω with C² boundary and a global real C² field u such that in Ω, u = 1 and on ∂Ω.
- C² boundary is specified by a global C² defining function with nonzero gradient on its zero set.
- Star-shaped about the origin; hence the domain is contractible and simply connected.
Scope: The linked formal statement uses eigenvalue one after dilation and a vanishing full boundary gradient. It does not claim the analytic frequency interval or the manuscript’s C∞ regularity.
A formal non-disk failing the Pompeiu property →
Proved · version 1
There exist a nonempty bounded star-shaped planar non-disk Ω with C² boundary and a continuous real f, not identically zero, such that the integral of f over every rigid-motion image of Ω equals zero.
- Planar Lebesgue measure and all affine isometries.
- The star-shaped C² witness provided by the cited formal construction.
Scope: The theorem derives Pompeiu failure from its own Schiffer witness through Green’s identity. It is a related conclusion, not a third geometric construction.
Relationship not independently reviewed.
Connection in Schiffer and Pompeiu conjectures →Relationship not independently reviewed. This concerns its use in this problem.
Sources
Lean proof of the star-shaped Schiffer/Pompeiu construction →
- Schiffer.Comparator.Schiffer_Star_Shaped and Pompeiu_Star_Shaped; simply-connected corollaries → · Original passage ↗
Recorded wording
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.
paraphrase · OpenMath supplies its own mathematical paraphrases and links; proof text is not republished.
Jaume de Dios Pont · Gonzalo Cao-Labora · Project documentation
Public formal source; execution and statement correspondence are separate checks.
Lean proof of the star-shaped Schiffer/Pompeiu construction — pinned source ↗No OpenMath execution recorded
Exact source inspected; OpenMath has not executed this formal proof project.
Revision & attribution
Source revision: 2938e277969c329caf154e48a3d8823f3635c7f1. Observed Oct 13, 2026.
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.
Lean proof of the star-shaped Schiffer/Pompeiu construction — pinned source: 2938e277969c329caf154e48a3d8823f3635c7f1.
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 · 1
Assessments retained in these publication records. Earlier statement versions retain their own source histories.
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 · Source passage →
Record details
- Claim ID
- claim-pompeiu-star-shaped-c2-witness
- Statement version
- 1
- SHA-256
- 49bc26499451398efb98c20751c2e950cf66ed79774fae8a87d5162e7692f642