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.

Stable mixed curl-curl formulation with kernel gauge

Statement

Assume Countable Choice for the graph spaces and real $L^{2}$ product as in Kernel quotient and gauge for discrete curl-curl. Let $V_{h}$ be that finite-dimensional real edge space, $K_{h} = \ker (curl ∣_{V_{h}})$ , and $Z_{h} = V_{h} \cap K_{h}^{⊥}$ . Here $V_{h}^{*} = {Hom}_{R} (V_{h}, R)$ is the algebraic dual of Linear functionals and the algebraic dual $V^{*} = L (V, F)$ . For every $f \in V_{h}^{*}$ there is a unique pair $(u_{h}, p_{h}) \in Z_{h} \times K_{h}$ satisfying $(curl u_{h}, curl v_{h})_{L^{2}} + (p_{h}, v_{h})_{L^{2}} = f (v_{h}) (v_{h} \in V_{h}), (u_{h}, q_{h})_{L^{2}} = 0 (q_{h} \in K_{h}) .$ The gauge multiplier is the $L^{2}$ Riesz representative of $f ∣_{K_{h}}$ . The quotient solution satisfies the exact stability identity $∥ curl u_{h} ∥_{L^{2}} = ∥ f ∣_{Z_{h}} ∥_{(Z_{h}, ∥ curl (\cdot) ∥_{L^{2}})^{*}}, ∥ p_{h} ∥_{L^{2}} = ∥ f ∣_{K_{h}} ∥_{(K_{h}, ∥ \cdot ∥_{L^{2}})^{*}} .$ The constraint form $b (v, q) = (v, q)_{L^{2}}$ has inf-sup constant one when $K_{h} \neq {0}$ , $V_{h}$ has the $H (curl)$ graph norm and $K_{h}$ has the $L^{2}$ norm; if $K_{h} = {0}$ the constraint is vacuous. The curl form is coercive with constant one on $Z_{h}$ in the quotient curl norm. No mesh-uniform estimate in the full graph norm is claimed here.

Facts & Assumptions

Given: The finite-dimensional real space $V_{h}$ , its kernel and orthogonal gauge from Kernel quotient and gauge for discrete curl-curl, and a linear functional $f \in V_{h}^{*}$ .

[A1]

Countable Choice is inherited from the graph-space uniqueness and real $L^{2}$ product interfaces; the finite-dimensional Riesz and orthogonal-decomposition arguments use no stronger choice axiom. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F1]

$K_{h}$ is the curl kernel, $Z_{h} = V_{h} \cap K_{h}^{⊥}$ , and $∥ [v_{h}] ∥_{curl} = ∥ curl v_{h} ∥_{2}$ is the quotient norm. (Kernel quotient and gauge for discrete curl-curl)

[F2]

A finite-dimensional real inner-product space splits as $W \oplus W^{⊥}$ . (For a subspace $W$ of a finite-dimensional inner product space, $V = W \oplus W^{⊥}$ )

[F3]

Every real linear functional on a finite-dimensional real inner-product space is represented uniquely by inner product with a vector. (Finite-dimensional Riesz representation: every functional is uniquely $v \mapsto ⟨ v, w ⟩$ )

[F4]

$V_{h}^{*}$ consists of all real linear functionals on $V_{h}$ . (Linear functionals and the algebraic dual $V^{*} = L (V, F)$ )

Proof

1.1A1F1F3F4givenconstruct

On $Z_{h}$ , the bilinear form $a_{h} (u, v) = (curl u, curl v)_{L^{2}}$ is an inner product: if $a_{h} (u, u) = 0$ , then $u \in K_{h}$ and $u \in K_{h}^{⊥}$ , hence $u = 0$ . The finite-dimensional Riesz theorem [F3] applied to $f ∣_{Z_{h}}$ gives a unique $u_{h} \in Z_{h}$ with $a_{h} (u_{h}, z_{h}) = f (z_{h})$ for every $z_{h} \in Z_{h}$ . Applying [F3] to the $L^{2}$ inner product on the finite-dimensional $K_{h}$ gives a unique $p_{h} \in K_{h}$ with $(p_{h}, q_{h})_{L^{2}} = f (q_{h})$ for all $q_{h} \in K_{h}$ . The zero subspace cases are included in [F3].

2.1A1F1F2step 1.1algebra

Restrict the $L^{2}$ inner product to the finite-dimensional space $V_{h}$ . Its orthogonal complement of $K_{h}$ is $V_{h} \cap K_{h}^{⊥} = Z_{h}$ by [F1], so [F2] gives $V_{h} = Z_{h} \oplus K_{h}$ . Thus each $v_{h}$ has a unique orthogonal decomposition $v_{h} = z_{h} + q_{h}$ . Since $curl q_{h} = 0$ and $(p_{h}, z_{h}) = 0$ , the two identities of step 1.1 give $a_{h} (u_{h}, v_{h}) + (p_{h}, v_{h}) = f (z_{h}) + f (q_{h}) = f (v_{h})$ . Also $u_{h} \in Z_{h}$ gives the gauge equation. Any solution must restrict to the unique Riesz problems on $Z_{h}$ and $K_{h}$ , proving uniqueness.

3.1A1F1F2F3step 1.1step 2.1algebra∎

For any real inner product $c (\cdot, \cdot)$ and any nonzero $w$ , positivity of $c (v - t w, v - t w)$ at $t = c (v, w) / c (w, w)$ gives $∣ c (v, w) ∣^{2} \leq c (v, v) c (w, w)$ ; if $w = 0$ the inequality is immediate. Thus the norm of the functional $z \mapsto c (u, z)$ is at most $∥ u ∥_{c}$ , and when $u \neq 0$ equality is attained at $z = u$ ; when $u = 0$ both sides vanish. Applying this argument to $a_{h}$ and the $L^{2}$ product, together with the Riesz identities of step 1.1, proves both exact dual-norm identities. For the constraint, if $q_{h} \neq 0$ choose $v_{h} = q_{h}$ ; then $curl q_{h} = 0$ , $∥ v_{h} ∥_{H (curl)} = ∥ q_{h} ∥_{2}$ , and $b (v_{h}, q_{h}) = ∥ q_{h} ∥_{2}^{2}$ , so the inf-sup constant is at least one. For the upper bound, the same positive-square argument with the $L^{2}$ inner product gives $∣ b (v_{h}, q_{h}) ∣ \leq ∥ v_{h} ∥_{2} ∥ q_{h} ∥_{2} \leq ∥ v_{h} ∥_{H (curl)} ∥ q_{h} ∥_{2}$ . On $Z_{h}$ , $a_{h} (v_{h}, v_{h}) = ∥ [v_{h}] ∥_{curl}^{}$ , which gives coercivity constant one in the declared quotient norm.

Depends on

Used by

A nodal curl-free mode outside the compatible gradient image Example

Dependency tree · two levels

21 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

Long Chen, Finite Element Methods for Maxwell Equations, complete lecture notes (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)