CorollaryStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass

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.

Exact-arithmetic CG after grounding or a Neumann gauge

Statement

Use the weighted network data of Finite weighted network diffusion data. The exact-arithmetic conjugate-gradient result CG is the Krylov Galerkin method, and the $m$ th iterate uniquely minimizes the $A$ -norm of the error over $x_{0} + K_{m} (A, r_{0})$ applies to each of the following systems:

$M + τ L_{D}$ for every $τ > 0$ ;
the grounded steady matrix $L_{D}$ if every positive-conductance component containing a free vertex also meets the Dirichlet set $D$ ;
the closed Neumann matrix $L_{C}$ restricted to $K^{⊥}$ , where $K = \ker L_{C}$ , for every compatible right-hand side $b \in K^{⊥}$ .

In case 3 the gauge $u \in K^{⊥}$ gives the unique solution of $L_{C} u = b$ . Here $K^{⊥}$ uses the standard Euclidean inner product $⟨ x, y ⟩ = x^{T} y$ . If a stated unknown space is zero-dimensional, its solver claim is vacuous. These are exact-arithmetic applicability claims only; no finite-precision stability claim is made.

Facts & Assumptions

Given: Positive diagonal masses, nonnegative edge conductances, a finite oriented graph, Dirichlet set $D$ , and the matrices $M, L_{D}, L_{C}$ .

[F1]

$L_{D}$ is symmetric positive semidefinite. Its energy is zero exactly for vectors whose zero extensions are constant on every positive-conductance component, with constant zero on components meeting $D$ ; these are precisely the vectors in $\ker L_{D}$ . In the closed case $D = \emptyset$ , $L_{D} = L_{C}$ and $\ker L_{C}$ consists of all positive-conductance componentwise constants, with no Dirichlet constraint (Finite weighted network diffusion data, Energy, kernel, and weighted mass balance for a finite network).

[F2]

A linear endomorphism of a finite-dimensional vector space with trivial kernel is onto by rank-nullity (Rank-nullity: $\dim_{F} V = nullity T + rank T$ ).

[F3]

For a real symmetric positive-definite system $A x = b$ , the exact-arithmetic CG iterates satisfy the published Krylov Galerkin and energy-minimization theorem (CG is the Krylov Galerkin method, and the $m$ th iterate uniquely minimizes the $A$ -norm of the error over $x_{0} + K_{m} (A, r_{0})$ ).

[F4]

$M$ is diagonal with strictly positive entries (Finite weighted network diffusion data).

[F5]

Every finite-dimensional real inner-product space has an orthonormal basis, including the empty basis in dimension zero (Every finite-dimensional real or complex inner product space has an orthonormal basis).

Proof

technique · positive-definite restriction

Given: The weighted graph matrices and the exact-arithmetic CG interface of [F3].

1.1F1givenalgebra

Under the grounded condition, suppose $x \in R^{I}$ and $x^{T} L_{D} x = 0$ . By [F1], the zero extension of $x$ is constant on each positive-conductance component and zero on each such component meeting $D$ . The grounded condition says every component containing a free vertex meets $D$ , so every free coordinate is zero. Thus $L_{D}$ has trivial kernel; it is symmetric positive semidefinite by [F1], hence positive definite.

1.2F1F2F5givenalgebra

In the closed case, let $K = \ker L_{C}$ . Symmetry implies $L_{C} (K^{⊥}) \subseteq K^{⊥}$ : for $x \in K^{⊥}$ and $k \in K$ , $k^{T} L_{C} x = (L_{C} k)^{T} x = 0$ . If a vector $x \in K^{⊥}$ has $x^{T} L_{C} x = 0$ , [F1] puts $x$ in $K$ ; hence $x = 0$ . Therefore the restriction $L_{C} ∣_{K^{⊥}}$ is positive definite. It has trivial kernel and is an endomorphism of the finite-dimensional space $K^{⊥}$ , so [F2] makes it onto. Thus each $b \in K^{⊥}$ has one gauged solution $u \in K^{⊥}$ . By [F5], an orthonormal basis of $K^{⊥}$ identifies this restriction with a real symmetric positive definite matrix, including the zero-dimensional case.

1.3F1F4givenalgebra

For $τ > 0$ and any nonzero $x$ , [F1] and [F4] give $x^{T} (M + τ L_{D}) x = x^{T} M x + τ x^{T} L_{D} x \geq \sum_{i} m_{i} x_{i}^{2} > 0$ . Thus $M + τ L_{D}$ is positive definite.

2.1F2F3step 1.1step 1.2step 1.3given∎

The grounded matrix from step 1.1, the restricted Neumann matrix in the orthonormal coordinates constructed in the preceding argument, and the shifted mass matrix from step 1.3 are all real symmetric positive definite on their stated spaces. Each therefore has trivial kernel and is onto by [F2] on its finite-dimensional domain, so each right-hand side has a unique solution. Applying [F3] gives the exact-arithmetic CG Krylov Galerkin and energy-minimization conclusions.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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

Fan R. K. Chung, Spectral Graph Theory, Chapter 1: Eigenvalues and the Laplacian of a Graph, CBMS 92 (1997), complete chapter text (standard reference, not scraped)
Jonathan Richard Shewchuk, An Introduction to the Conjugate Gradient Method Without the Agonizing Pain, complete lecture note (standard reference, not scraped)