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.

Schur residual controls trace and reconstruction energy error

Statement

Let $S : = S_{1} + S_{2}$ , let $λ_{*}$ solve $S λ_{*} = f_{1} + f_{2}$ , and let $\tilde{λ} \in Λ$ have residual $ρ : = S \tilde{λ} - (f_{1} + f_{2})$ . All trace-vector and operator norms below are induced by the given real inner product on $Λ$ . Then

$∥ \tilde{λ} - λ_{*} ∥ \leq ∥ S^{- 1} ∥ ∥ ρ ∥ .$

If each subdomain state is reconstructed by solving its interior equations at the supplied trace, define the product backward-Euler energy norm by $∥ (z_{1}, z_{2}) ∥_{B_{1} \oplus B_{2}}^{2} : = ⟨ B_{1} z_{1}, z_{1} ⟩ + ⟨ B_{2} z_{2}, z_{2} ⟩$ for $z_{i} \in X_{i}$ . Then

$∥ \tilde{u} - u_{*} ∥_{B_{1} \oplus B_{2}} \leq \sqrt{∥ S^{- 1} ∥} ∥ ρ ∥ .$

Facts & Assumptions

Given: The positive-definite subdomain blocks and Schur complements of Finite-dimensional backward-Euler diffusion transmission model, their energy-minimization property, and the unique monolithic trace $λ_{*}$ .

[F1]

Finite-dimensional backward-Euler diffusion transmission model: $S_{i}$ is the Schur complement of the positive-definite local block $B_{i}$ , and the monolithic trace solves $(S_{1} + S_{2}) λ_{*} = f_{1} + f_{2}$ .

[F2]

The diffusion Schur complement is positive and minimizes energy: for a fixed trace error $z$ , its minimum local $B_{i}$ energy is $⟨ S_{i} z, z ⟩$ .

Proof

1.1givenF1algebra

Set $e : = \tilde{λ} - λ_{*}$ . By [F1], $ρ = S e$ . Since $S$ is positive definite, $e = S^{- 1} ρ$ ; the operator-norm inequality gives $∥ e ∥ \leq ∥ S^{- 1} ∥ ∥ ρ ∥$ .

2.1F1F2step 1.1algebra

The reconstructed state difference on subdomain $i$ has trace $e$ . By [F2], its squared minimum $B_{i}$ energy is $⟨ S_{i} e, e ⟩$ . Adding the two subdomains gives $∥ \tilde{u} - u_{*} ∥_{B_{1} \oplus B_{2}}^{2} = ⟨ S e, e ⟩ = ⟨ ρ, S^{- 1} ρ ⟩$ .

3.1step 2.1algebra∎

Cauchy–Schwarz and the operator norm yield $⟨ ρ, S^{- 1} ρ ⟩ \leq ∥ S^{- 1} ∥ ∥ ρ ∥^{2}$ . Take nonnegative square roots to obtain the stated energy bound.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · one level

2 results within one dependency step 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

Emil Engström and Eskil Hansen, Time-dependent Steklov–Poincaré operators and space-time Robin–Robin decomposition for the heat equation (2022) (standard reference, not scraped)
Martina Maria Joosten, Aspects of interface modelling in fluid-structure interaction problems, PhD thesis, Swansea University (2011) (standard reference, not scraped)