Proved
Conditional mathematical implication in the cited source ↗
Observed Oct 13, 2026
Theorem · version 1
From boundary data to vanishing domain averages
Statement
For any bounded planar domain Ω with C² boundary, if a global C² real field u satisfies −Δu = u in Ω, u = 1 and ∇u = 0 on ∂Ω, then there exists a continuous real f, not identically zero, with integral zero over every rigid-motion image of Ω.
Assumptions
- C² boundary in the defining-function sense of the cited formal source.
- Planar Lebesgue integration and all affine isometries; the global C² field satisfies the normalized equation.
Scope
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.
Evidence
Source reports
Connections
In this problem · publication v4 · Selected context
Schiffer and Pompeiu conjectures →
Conditional implication · Proved
Relationship not independently reviewed. This concerns its use in this problem.
In this problem · publication v7
Schiffer and Pompeiu conjectures →
Conditional implication · Proved
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
Conditional mathematical implication in the cited source ↗
Observed Oct 13, 2026 · Source passage →
Record details
- Claim ID
- claim-schiffer-pompeiu-consequence
- Statement version
- 1
- SHA-256
- e0f1d36fbc5a6a3a6ea7a212a7e795ed2ce12bb8ccaf74d7389599321c7b8a89