∑math20

Partial differential equations · Result 372

Global uniqueness in smooth isotropic elasticity

1 paperLean

Proves that full static boundary displacement-to-traction data determine both smooth real Lamé moduli on every bounded connected smooth domain in ℝ3, provided μ > 0 and \(3\lambda+2\mu\gt 0\) on the closure. Neither analyticity, proximity to constant coefficients nor prior knowledge near the boundary is required.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of Global Uniqueness for the Smooth Isotropic Elasticity Inverse Problem

Global Uniqueness for the Smooth Isotropic Elasticity Inverse Problem

OpenAI · September 24, 2026

We prove that the full static displacement-to-traction map uniquely determines both real smooth Lamé moduli on every bounded connected smooth domain in ℝ3, provided μ > 0 and \(3\lambda+2\mu\gt 0\) on the closure. This resolves the smooth three-dimensional isotropic elastic Calderón uniqueness problem under these positivity assumptions.

Read PDF Download Source

Cite
@misc{OAI:Global-Uniqueness-for-the-Smooth-Isotropic-Elasticity-Inverse-Problem-September-24-2026,
  author = {{OpenAI}},
  title = {{Global Uniqueness for the Smooth Isotropic Elasticity Inverse Problem}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Global-Uniqueness-for-the-Smooth-Isotropic-Elasticity-Inverse-Problem-September-24-2026/article.pdf}{OAI:Global-Uniqueness-for-the-Smooth-Isotropic-Elasticity-Inverse-Problem-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalization proves global uniqueness in the three-dimensional static isotropic elasticity inverse problem. On a bounded connected smooth domain, let two pairs of smooth real Lamé moduli satisfy \(\mu>0\) and \(3\lambda+2\mu>0\) on the closure. If their full displacement-to-traction maps agree, then both Lamé moduli agree throughout the domain. The selected statement is uniqueness; it does not supply a reconstruction algorithm.

Comparator links

ResultComparator statement
Global uniqueness of smooth isotropic Lamé moduliElasticityUniqueness.lean

Scope note on GitHub →