LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)

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.

Piola divergence and facet-flux identities

Statement

Let $F_{K} (\hat{x}) = A_{K} \hat{x} + b_{K}$ be as in Contravariant Piola map, and let $\hat{v} \in C^{1} (\overline{\hat{K}}; R^{d})$ . Set $v = P_{K} \hat{v}$ . Then

({div}_{x} v) (F_{K} (\hat{x})) = J_{K}^{- 1} {div}_{\hat{x}} \hat{v} (\hat{x}) .

For each facet $\hat{F}$ mapped to $F$ , with the corresponding oriented normals, the integrated flux is preserved:

\int_{F} v \cdot n_{F} d s = \int_{\hat{F}} \hat{v} \cdot {\hat{n}}_{\hat{F}} d \hat{s} .

Facts & Assumptions

Given: An orientation-preserving affine bijection $F_{K}$ with matrix $A_{K}$ , determinant $J_{K} > 0$ , a smooth reference vector field $\hat{v}$ , and its contravariant Piola push-forward.

[F1]

The push-forward is $v (F_{K} (\hat{x})) = J_{K}^{- 1} A_{K} \hat{v} (\hat{x})$ . (Contravariant Piola map)

[F2]

The chain rule for total derivatives states $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ for differentiable maps between finite-dimensional real spaces. (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ )

Proof

1.1F1F2algebra

Write $v_{i} (F_{K} (\hat{x})) = J_{K}^{- 1} \sum_{j} (A_{K})_{i j} {\hat{v}}_{j} (\hat{x})$ . The chain rule [F2] for $F_{K}^{- 1}$ gives $\partial_{x_{i}} = \sum_{k} (A_{K}^{- 1})_{k i} \partial_{{\hat{x}}_{k}}$ ; since $A_{K}$ is constant, summing the derivatives gives $({div}_{x} v) \circ F_{K} = J_{K}^{- 1} \sum_{i, k, j} (A_{K}^{- 1})_{k i} (A_{K})_{i j} \partial_{{\hat{x}}_{k}} {\hat{v}}_{j} = J_{K}^{- 1} \sum_{j} \partial_{{\hat{x}}_{j}} {\hat{v}}_{j} .$ The middle equality uses $A_{K}^{- 1} A_{K} = I$ .

2.1F1F2constructalgebra∎

Choose oriented tangent vectors ${\hat{t}}_{1}, \dots, {\hat{t}}_{d - 1}$ on $\hat{F}$ . Under $F_{K}$ the tangent vectors are $A_{K} {\hat{t}}_{i}$ ; multilinearity of the determinant gives the oriented area-normal transformation $n_{F} d s = cof (A_{K}) {\hat{n}}_{\hat{F}} d \hat{s}$ . Since $A_{K}$ is invertible, $cof (A_{K}) = J_{K} A_{K}^{- T}$ . Therefore the Piola flux element satisfies $v \cdot n_{F} d s = (J_{K}^{- 1} A_{K} \hat{v}) \cdot (J_{K} A_{K}^{- T} {\hat{n}}_{\hat{F}}) d \hat{s} = \hat{v} \cdot {\hat{n}}_{\hat{F}} d \hat{s} .$ Integrating over the corresponding facets proves the flux identity.

Commuting diagram

For smooth fields, the proved identity is represented by

diagram failed to render:
C^1(\overline{\widehat K};\mathbb R^d) \arrow[r,"\operatorname{div}"] \arrow[d,"\mathcal P_K"'] & C(\widehat K) \arrow[d,"J_K^{-1}(\cdot)\circ F_K^{-1}"] \\
C^1(\overline K;\mathbb R^d) \arrow[r,"\operatorname{div}"'] & C(K)

The top and bottom arrows are divergence, the left arrow is the contravariant Piola push-forward, and the right arrow is scalar pull-forward with the Jacobian factor. The proof above establishes the commutation algebraically; the diagram is only a record of the identity.

Depends on

Used by

RT0 facet-flux unisolvence and global H(div) conformity Lemma

Dependency tree · two levels

6 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

Jean-Luc Guermond, MATH 661 Fall 2025, Part III Chapter 14: H(div) finite elements (standard reference, not scraped)
Daniele Boffi, Franco Brezzi and Michel Fortin, Mixed Finite Element Methods and Applications (standard reference, not scraped)