Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Anisotropic gauge and unresolved uniqueness — Examples and Counterexamples

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

None yet.

4 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-adaptedverified 2026-10-22 (gpt-6.1-sol)Open item page →

A nontrivial boundary-fixing radial gauge on the ball

Example

Assume the Axiom of Choice and let $n \geq 3$ . On the unit ball $B^{n} = {x \in R^{n} : ∣ x ∣ < 1}$ take the constant matrix conductivity $γ (x) = I_{n}$ , the $n \times n$ identity matrix. For $0 < ε < 1 / 2$ , define $F_{ε} : \overline{B^{n}} \to \overline{B^{n}}$ by $F_{ε} (x) = (1 + ε (1 - ∣ x ∣^{2})) x$ and define ${\tilde{γ}}_{ε} = (F_{ε})_{*} γ$ by the anisotropic conductivity pushforward formula. For $η = γ$ or ${\tilde{γ}}_{ε}$ , let $Λ_{η}$ be the weak energy map on $B_{B^{n}} = H^{1} (B^{n}) / H_{0}^{1} (B^{n})$ given by $⟨ Λ_{η} f, h ⟩ = \int_{B^{n}} η \nabla u_{η, f} \cdot \nabla V_{h} d x$ , where $u_{η, f}$ is the unique weak solution with boundary class $f$ and $V_{h}$ is any representative of $h$ . Then $F_{ε}$ is a smooth diffeomorphism that fixes $\partial B^{n}$ pointwise, ${\tilde{γ}}_{ε}$ is smooth and uniformly positive definite, and ${\tilde{γ}}_{ε} \equiv̸ I_{n}$ ; nevertheless $Λ_{{\tilde{γ}}_{ε}} = Λ_{I_{n}}$ .

Example references

Anisotropic conductivity and weak DN map

Boundary-fixing diffeomorphism invariance

Salo, §1, pp. 170–171

Daudé, Kamran, and Nicoleau, §1, equation (1.6)

Facts & Assumptions

Given: The Axiom of Choice; an integer $n \geq 3$ ; the unit ball $B^{n}$ ; the identity matrix conductivity $I_{n}$ ; and $0 < ε < 1 / 2$ .

[A1]

The Axiom of Choice, as assumed by the local anisotropic DN map and gauge theorem. (The Axiom of Choice)

[F1]

If $F$ is a smooth boundary-fixing diffeomorphism and $γ$ is a smooth uniformly positive-definite symmetric conductivity, then $(F_{*} γ) (x) = D F (y) γ (y) D F (y)^{T} / ∣ \det D F (y) ∣$ for $y = F^{- 1} (x)$ is smooth uniformly positive definite and $Λ_{F_{*} γ} = Λ_{γ}$ . (A boundary-fixing diffeomorphism preserves the anisotropic DN map, Statement)

[F2]

The weak DN map is the energy form on $B_{Ω} = H^{1} (Ω) / H_{0}^{1} (Ω)$ , defined using the unique weak solution and any $H^{1}$ representative of the second boundary datum. (Anisotropic conductivity and weak Dirichlet-to-Neumann map, Definition)

Verification

1.1givenalgebra

Write $R_{ε} (r) = r (1 + ε (1 - r^{2}))$ for $0 \leq r \leq 1$ . Then $R_{ε} (0) = 0$ , $R_{ε} (1) = 1$ , and $R_{ε}^{'} (r) = 1 + ε - 3 ε r^{2} \geq 1 - 2 ε > 0$ . Thus $R_{ε}$ is a strictly increasing bijection of $[0, 1]$ to itself; $F_{ε}$ preserves each radial ray, is bijective on the ball, and fixes the boundary pointwise.

2.1givenstep 1.1algebra

At the origin $D F_{ε} (0) = (1 + ε) I_{n}$ and $J_{F_{ε}} (0) = (1 + ε)^{n} > 0$ . At $r > 0$ the radial derivative is $R_{ε}^{'} (r) > 0$ and each tangential eigenvalue is $R_{ε} (r) / r = 1 + ε (1 - r^{2}) > 0$ . By continuity, $R_{ε}^{'}$ stays positive on $[0, 1 + δ]$ for some $δ > 0$ . The same radial formula extends $F_{ε}$ to a smooth diffeomorphism from the ball of radius $1 + δ$ onto its image, which contains a neighborhood of $\overline{B^{n}}$ ; its inverse is smooth there. Thus the inverse is smooth through the boundary and the differential is nonsingular on the closed ball.

3.1F1givenstep 2.1algebra

Since $F_{ε} (0) = 0$ , the pushforward formula in [F1] gives ${\tilde{γ}}_{ε} (0) = D F_{ε} (0) D F_{ε} (0)^{T} / J_{F_{ε}} (0) = (1 + ε)^{2 - n} I_{n}$ . Because $n \geq 3$ and $ε > 0$ , this differs from $I_{n}$ , so the pushed-forward conductivity is nontrivial.

4.1A1F1F2step 1.1step 2.1step 3.1algebra∎

The hypotheses of [F1] hold for $γ = I_{n}$ and $F_{ε}$ , so $Λ_{{\tilde{γ}}_{ε}} = Λ_{I_{n}}$ . The example therefore exhibits a distinct smooth anisotropic conductivity with exactly the same boundary energy map, caused by the stated boundary-fixing change of variables.