TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck 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.

Regular decomposition of zero-tangential H(curl) fields

Statement

Assume the Axiom of Choice. Let $Ω \subset R^{3}$ be a nonempty bounded contractible Lipschitz polyhedron with connected boundary. For every $u \in H_{0} (curl; Ω)$ there are $z \in H_{0}^{1} (Ω; R^{3})$ and $p \in H^{1} (Ω)$ such that $u = z + \nabla p, ∥ z ∥_{H^{1} (Ω)} + ∥ p - p_{Ω} ∥_{H^{1} (Ω)} \leq C_{Ω} ∥ u ∥_{H (curl; Ω)} .$ Here $H_{0} (curl)$ is the closure definition of Zero tangential trace H(curl) space, and $p_{Ω} = ∣ Ω ∣^{- 1} \int_{Ω} p$ fixes the additive constant. The constant may depend on the domain but not on a mesh.

Facts & Assumptions

Given: AC and exactly the domain and zero-tangential field of the Statement. The stronger full Dirichlet supplier below applies to this domain without changing its stated hypotheses.

[F1]

A bounded regular decomposition with both summands satisfying full Dirichlet conditions gives $z \in H_{0}^{1} (Ω; R^{3})$ and $q \in H_{0}^{1} (Ω)$ with $u = z + \nabla q$ and $∥ z ∥_{H^{1}} + ∥ q ∥_{H^{1}} \leq C_{Ω} ∥ u ∥_{H (curl)}$ .

Proof

1.1F1construct

Apply [F1] and set $p = q$ . This supplies the required vector and scalar spaces and the identity, with the original domain, topology, and connected-boundary clauses retained. The proof of [F1] uses only a scalar H2 extension and an explicitly proved Fourier split; it imports no H(curl) extension theorem and no smooth-to-weak cohomology identification.

2.1F1step 1.1algebra∎

By Holder, $∣ p_{Ω} ∣ ∣ Ω ∣^{1 / 2} \leq ∥ p ∥_{2}$ , whence $∥ p - p_{Ω} ∥_{H^{1}} \leq 2 ∥ p ∥_{H^{1}}$ . Combine this with [F1] and absorb the numerical factor into $C_{Ω}$ to obtain the asserted estimate. The construction in [F1] fixes $p \in H_{0}^{1}$ ; the present statement only requires $H^{1}$ , so its complete original scalar freedom is retained.

Depends on

Used by

Dependency tree · two levels

10 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

Ralf Hiptmair and Clemens Pechstein, Regular Decompositions of Vector Fields—Continuous, Discrete, and Structure-Preserving (standard reference, not scraped)
Douglas N. Arnold, Richard S. Falk, and Ragnar Winther, Finite element exterior calculus: from Hodge theory to numerical stability (standard reference, not scraped)