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

Energy-stable semidiscrete P1 evolution on an anchored metric graph

Statement

Assume the Axiom of Choice and Countable Choice. Let a finite metric graph with nonempty edge set have every connected edge component anchored, let $V = V_{D}$ and $H = ⨁_{e \in E} L^{2} (0, ℓ_{e}; R)$ , and let $V_{h}$ be its conforming P1 edge space. Put $L_{Γ} = \sum_{e} ℓ_{e}$ , $α = κ_{\min} / (1 + L_{Γ}^{2})$ , and assume constant diffusivities $0 < κ_{\min} \leq κ_{e} \leq κ_{\max}$ . For $T > 0$ , $f \in L^{2} (0, T; V_{D}^{*})$ , and $u_{h}^{0} \in V_{h}$ , define $a (w, v) = \sum_{e} κ_{e} \int_{0}^{ℓ_{e}} w_{e}^{'} v_{e}^{'} d x_{e}$ . There is a unique $u_{h} \in H^{1} (0, T; V_{h})$ with $u_{h} (0) = u_{h}^{0}$ satisfying, for almost every $t$ ,

$((u_{h})^{'} (t), v_{h})_{H} + a (u_{h} (t), v_{h}) = ⟨ f (t), v_{h} ⟩_{V_{D}^{*}, V_{D}} (v_{h} \in V_{h}) .$

For every $t \in [0, T]$ ,

$∥ u_{h} (t) ∥_{H}^{2} + α \int_{0}^{t} ∥ u_{h} (s) ∥_{V_{D}}^{2} d s \leq ∥ u_{h}^{0} ∥_{H}^{2} + α^{- 1} \int_{0}^{t} ∥ f (s) ∥_{V_{D}^{*}}^{2} d s .$

Here $V_{h}$ is the finite P1 space from Conforming P1 edge mesh on an anchored metric graph. This is a semidiscrete existence and energy statement; it gives no parabolic spatial error rate.

Facts & Assumptions

Given: Full AC and Countable Choice; a finite anchored metric graph; the real spaces $V = V_{D}$ and $H$ ; positive edge diffusivities; a fixed finite P1 edge mesh; a dual load $f$ ; and an initial vector $u_{h}^{0} \in V_{h}$ .

[F1]

The edge-product L2 space is a real Hilbert space under the edge-sum integral inner product, assuming Countable Choice ( $L^{2}$ with the integral pairing is a Hilbert space, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F2]

Each $C_{c}^{\infty} (0, ℓ_{e})$ function belongs to edge $H^{1}$ and has zero endpoint traces, so its extension by zero to the other edges lies in $V_{D}$ . Such functions are dense in $L^{2} (0, ℓ_{e})$ under Countable Choice (Anchored finite metric graph and its H1 energy space, Integer-order Sobolev spaces and their norms, Smooth compactly supported functions of an open set are dense in $L^{2}$ , The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F3]

The anchored graph H1 space is Hilbert and its inclusion in H is continuous, with $∥ v ∥_{H} \leq ∥ v ∥_{V}$ (The anchored metric graph H1 space is a closed Hilbert subspace, Anchored finite metric graph and its H1 energy space).

[F4]

Path Poincare gives $∥ v ∥_{H} \leq L_{Γ} ∥ v^{'} ∥_{H}$ , so the graph diffusion form is bounded by $κ_{\max}$ and coercive with $α = κ_{\min} / (1 + L_{Γ}^{2})$ on V (Path Poincare inequality on an anchored finite metric graph, Bounded, coercive and symmetric sesquilinear forms).

[F5]

If V_h is a finite-dimensional real subspace of an evolution space V continuously embedded in H, and the real form is measurable, bounded and coercive on V_h, then the finite-dimensional parabolic Galerkin ODE has a unique H1-in-time solution and the displayed energy estimate (Finite-dimensional parabolic Galerkin ODEs with measurable coefficients).

[F6]

The edge-product Cauchy–Schwarz inequality controls the diffusion form and its load pairing (Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs).

[F7]

An evolution triple is a real Hilbert space V continuously and densely embedded in a real Hilbert space H, with V* its continuous real dual (Evolution triples and the parabolic energy space).

[F8]

The conforming graph P1 space consists of functions in $V_{D}$ affine on each cell of the specified finite edge mesh (Conforming P1 edge mesh on an anchored metric graph).

[A1]

The graph traces and H1 space inherit the Axiom of Choice from the one-dimensional representative theorem (The Axiom of Choice).

[A2]

Countable Choice is assumed by the edge L2 Hilbert and smooth-density suppliers (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Proof

technique · finite-dimensional parabolic Galerkin ODE

Given: Full AC and Countable Choice, the anchored edge graph, the finite P1 space, the diffusion form, the dual load, and the initial value.

1.1F2F3A2givenchoosealgebra

The canonical inclusion $i : V_{D} \to H$ is continuous because $∥ v ∥_{H} \leq ∥ v ∥_{V_{D}}$ . It is injective because $V_{D}$ consists of Sobolev classes included in the edge-product $L^{2}$ classes. To prove density, fix $g = (g_{e}) \in H$ and $ϵ > 0$ . By [F2] and finite choice, choose for each of the finitely many edges a $ϕ_{e} \in C_{c}^{\infty} (0, ℓ_{e})$ with $∥ g_{e} - ϕ_{e} ∥_{L^{2} (e)} < ϵ / \sqrt{∣ E ∣}$ . The edge-product function $ϕ = (ϕ_{e})$ has zero endpoint traces, hence belongs to $V_{D}$ , and $∥ g - ϕ ∥_{H}^{2} = \sum_{e} ∥ g_{e} - ϕ_{e} ∥_{L^{2} (e)}^{2} < ϵ^{2}$ . Thus the range of i is dense in H.

1.2A1F1F2F3F7F8givenconstruct

By [F1] and [F3], H and V_D are real Hilbert spaces with dense continuous inclusion. With V_D^* as its continuous real dual, these spaces form the evolution triple of Evolution triples and the parabolic energy space. The mesh has finitely many cells, and a P1 function is determined by its finite list of nodal values; the vertex matching and anchor conditions are linear. Therefore V_h is a finite-dimensional subspace of V_D by [F8].

2.1F4F5F6step 1.2given

By [F4] and [F6], the form a is bounded by M=κmax and coercive by α on V_D, hence also on V_h. The restriction F_h(t):=f(t)|{V_h} is a bounded functional and its norm is at most |f(t)|{V^}; restriction is a continuous linear map from V_D^ to V_h^*, so F_h is strongly measurable and square-integrable. Thus all hypotheses of [F5] hold for the evolution triple and finite P1 subspace of step 1.2.

3.1F5step 2.1given∎

Applying [F5] gives the unique semidiscrete solution and its energy estimate for every t in [0,T]. No spatial approximation rate is part of [F5], so none follows here.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

67 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

Mario Arioli and Michele Benzi, A Finite Element Method for Quantum Graphs, Emory CS Technical Report TR-2015-009 (44-page full text) (standard reference, not scraped)
Christian Clason, Introduction to Finite Element Methods, complete lecture notes, Chapter 12 (standard reference, not scraped)
Peter Kuchment, Quantum graphs: an introduction and a brief survey, arXiv:0802.3442 (2008) (standard reference, not scraped)