LemmaStatement: AI-adaptedProof: AI-generatedPipeline-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.

Kernel, range, and mean-zero inverse for the no-flux Laplacian

Statement

Use either connected no-flux realization in No-flux finite-volume and conforming realizations for phase fields. In its finite-volume branch, assume the interior cell graph is connected; in its interval conforming branch, assume $N \geq 1$ . Write ${\overset{ˉ}{u}}_{h} = ⟨ u_{h}, 1 ⟩_{h} / ⟨ 1, 1 ⟩_{h}$ and $X_{h, 0} = {u_{h} : {\overset{ˉ}{u}}_{h} = 0}$ . Then $A_{h}$ is self-adjoint and nonnegative, $\ker A_{h} = span {1}$ , and $ran A_{h} = X_{h, 0}$ . The restriction $A_{h} : X_{h, 0} \to X_{h, 0}$ is positive definite and invertible. Define $A_{h}^{†} u_{h}$ by first projecting $u_{h}$ onto $X_{h, 0}$ and then applying this self-adjoint positive inverse. For each fixed finite mesh there is $C_{h} < \infty$ such that $∥ u_{h} - {\overset{ˉ}{u}}_{h} 1 ∥_{h}^{2} \leq C_{h} ⟨ A_{h} u_{h}, u_{h} ⟩_{h} .$ For a one-cell mesh, $X_{h, 0} = {0}$ and the inequality is vacuous.

Facts & Assumptions

Given: A finite-dimensional real inner-product space and one of the two connected no-flux realizations in the statement.

[F1]

No-flux finite-volume and conforming realizations for phase fields: in the cell branch, $⟨ A_{h} u, v ⟩_{h} = \sum_{F = K ∣ L} T_{F} (u_{K} - u_{L}) (v_{K} - v_{L})$ with $T_{F} > 0$ ; in the interval branch, $⟨ A_{h} u, v ⟩_{h} = \int_{0}^{L} u^{'} v^{'} d x$ on continuous piecewise-affine functions.

[F2]

For a nonempty subset of $R^{n}$ with $n \geq 1$ , compactness, closedness and boundedness, pseudocompactness, and attainment of extrema by every continuous real-valued function are equivalent: every continuous real-valued function on a nonempty compact subset of a finite-dimensional Euclidean space attains its minimum.

Proof

1.1F1givenalgebra

The displayed bilinear form in [F1] is symmetric, so $A_{h}$ is self-adjoint. Its quadratic form is a sum of positive transmissibility-weighted squared jumps in the cell branch and is $\int_{0}^{L} ∣ u_{h}^{'} ∣^{2}$ in the interval branch, so it is nonnegative. If it is zero, every interior jump vanishes in the cell branch, and connectedness makes all cell values equal; in the interval branch the derivative is zero on every segment, and continuity makes the function constant. Conversely, constants have zero quadratic form. Thus $\ker A_{h} = span {1}$ .

2.1step 1.1algebra

Self-adjointness implies $ran A_{h} \subseteq (\ker A_{h})^{⊥}$ : for $z = A_{h} x$ and $c \in \ker A_{h}$ , $⟨ z, c ⟩_{h} = ⟨ x, A_{h} c ⟩_{h} = 0$ . Rank-nullity gives $\dim ran A_{h} = \dim X_{h} - \dim \ker A_{h} = \dim (\ker A_{h})^{⊥}$ , so equality holds. The orthogonal complement of the constants is exactly $X_{h, 0}$ .

3.1step 1.1step 2.1algebra

The restriction of $A_{h}$ to $X_{h, 0}$ maps into $X_{h, 0}$ and has trivial kernel by step 1.1. It is therefore bijective on this finite-dimensional space. Hence each mean-zero source has a unique mean-zero inverse, and projecting an arbitrary source onto $X_{h, 0}$ defines $A_{h}^{†}$ .

4.1F1step 1.1step 3.1algebra

On $X_{h, 0}$ the restriction of $A_{h}$ is self-adjoint positive definite by step 1.1. If $x, y \in X_{h, 0}$ , write $x = A_{h} s$ and $y = A_{h} t$ with $s, t \in X_{h, 0}$ ; then $⟨ A_{h}^{†} x, y ⟩_{h} = ⟨ s, A_{h} t ⟩_{h} = ⟨ A_{h} s, t ⟩_{h} = ⟨ x, A_{h}^{†} y ⟩_{h}$ , so its inverse is self-adjoint. Also, for nonzero $x = A_{h} s$ , $⟨ A_{h}^{†} x, x ⟩_{h} = ⟨ s, A_{h} s ⟩_{h} > 0$ .

5.1F1F2step 1.1algebra∎

If $X_{h, 0} = {0}$ the claimed inequality is immediate. Otherwise its unit sphere is compact and nonempty. The continuous quadratic form $u_{h} \mapsto ⟨ A_{h} u_{h}, u_{h} ⟩_{h}$ attains a minimum there by [F2]. The minimum is positive, since a zero value would put a unit mean-zero vector in the constant kernel from step 1.1. Calling the minimum $λ_{h} > 0$ , homogeneity gives $∥ u_{h} - {\overset{ˉ}{u}}_{h} 1 ∥_{h}^{2} \leq λ_{h}^{- 1} ⟨ A_{h} u_{h}, u_{h} ⟩_{h}$ .

Depends on

Used by

Dependency tree · two levels

11 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

R. Eymard, T. Gallouët, and R. Herbin, Finite Volume Methods, Handbook of Numerical Analysis, Vol. VII, 2000; complete updated author text (standard reference, not scraped)
Jérôme Droniou, Finite volume schemes for diffusion equations: introduction to and review of modern methods, 2014 (standard reference, not scraped)