# Joint metric and connection recovery from one boundary patch

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

- [Nonuniqueness for Bounded Measurable Scalar Conductivities in Three Dimensions](../../preprints/Nonuniqueness-for-Bounded-Measurable-Scalar-Conductivities-in-Three-Dimensions-September-23-2026/paper.pdf)

## Scope

The Calderón inverse problem asks whether boundary measurements determine an interior conductivity. The formalized result gives nonuniqueness for bounded measurable scalar conductivities on the ball $B(0,3)\subset\mathbb R^3$: two uniformly positive conductivities differ on a set of positive volume, equal $1$ near the boundary, and have the same full weak Dirichlet-to-Neumann operator. Weak solutions exist uniquely for every boundary trace.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Scalar conductivity nonuniqueness | [Conductivity.lean](../ComparatorChallenges/Conductivity.lean) |