ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10

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.

A conformal metric on the plane

Example

For $g = e^{2 u} (d x^{2} + d y^{2})$ on $R^{2}$ , ${grad}_{g} f = e^{- 2 u} (f_{x} \partial_{x} + f_{y} \partial_{y})$ and $μ_{g} = e^{2 u} ∣ d x d y ∣$ .

Facts & Assumptions

Given: $u, f \in C^{\infty} (R^{2})$ .

[F1]

Conformal equivalence of riemannian metrics: Two Riemannian metrics are conformally equivalent if $\tilde{g} = e^{2 u} g$ for a smooth real function $u$ on $M$ . The positive smooth factor preserves the metric condition of def-riemannian-metric-and-riemannian-manifold. Equivalently $\tilde{g} = f g$ for smooth $f > 0$ , since $u = \frac{1}{2} \log f$ . Reflexivity uses $u = 0$ , reversal uses $- u$ , and composing rescalings adds their functions.

[F2]

Riemannian gradient: For a smooth real function $f$ , its Riemannian gradient is ${grad}_{g} f = (d f)^{♯}$ . prop-exterior-derivative-of-a-function-is-its-differential identifies $d f (X) = X f$ . The smooth bundle isomorphism in thm-the-musical-maps-are-smooth-inverse-bundle-isomorphisms therefore makes the gradient a smooth vector field. In coordinates $({grad}_{g} f)^{i} = \sum_{j} g^{i j} \partial_{j} f$ . Constants, and all functions in dimension zero, have zero gradient.

[F3]

Riemannian volume density: The Riemannian volume density is $μ_{g} = \sqrt{\det G_{x}} ∣ d x^{1} \dots d x^{n} ∣$ in coordinates. The matrix is that of prop-coordinate-criterion-for-a-riemannian-metric, so its determinant is positive and smooth. The density frames and their absolute-Jacobian law are def-density-bundle-and-smooth-density. In dimension zero take the empty determinant to be one, giving weight one at every point, independently of orientation. The compatibility of these local formulas is proved in lem-the-riemannian-volume-density-is-coordinate-independent.

Verification

technique · direct

1.1F1given

The factor $e^{2 u}$ is smooth and strictly positive. The matrix is $G = e^{2 u} I_{2}$ , its inverse is $e^{- 2 u} I_{2}$ , and $v^{T} G v = e^{2 u} (v_{x}^{2} + v_{y}^{2}) > 0$ for $v \neq 0$ , so this is the stated conformal metric.

2.1F2F3step 1.1

Put $Y = e^{- 2 u} (f_{x} \partial_{x} + f_{y} \partial_{y})$ . For every $V = a \partial_{x} + b \partial_{y}$ , $g (Y, V) = f_{x} a + f_{y} b = d f (V)$ , so $Y$ is the gradient. Since $\det G = e^{4 u}$ , its positive square root is $e^{2 u}$ , giving the asserted density.

3.1step 2.1∎

For the explicit instance $u (x, y) = x$ and $f (x, y) = y$ , these formulas yield $g = e^{2 x} (d x^{2} + d y^{2})$ , ${grad}_{g} y = e^{- 2 x} \partial_{y}$ , and $μ_{g} = e^{2 x} ∣ d x d y ∣$ . At $(0, 0)$ the gradient is $\partial_{y}$ and the density coefficient is $1$ .

Source locator

Lee, p.328, coordinate metric criterion; p.342, gradient characterization; Proposition 15.31, p.390, coordinate volume coefficient. The conformal instance and its determinant are derived above.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

John M. Lee, Introduction to Smooth Manifolds, second edition (standard reference, not scraped)