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

Monolithic backward Euler transmission energy identity

Statement

Assume the finite-dimensional diffusion-transmission model of Finite-dimensional backward-Euler diffusion transmission model. Let $V : = {(v_{1}, v_{2}) \in X_{1} \oplus X_{2} : γ_{1} v_{1} = γ_{2} v_{2}}$ be the common-trace space, take $u^{n} \in V$ , and let $F_{i}^{n + 1} \in X_{i}$ . In the block notation of the definition, set the local right-hand side to $g_{i} : = Δ t^{- 1} M_{i} u_{i}^{n} + F_{i}^{n + 1}$ ; assemble the local equations with common trace and the outward algebraic fluxes $q_{i}$ from that definition. There is a unique $u^{n + 1} \in V$ satisfying

$\sum_{i = 1}^{2} (⟨ M_{i} \frac{u_{i}^{n + 1} - u_{i}^{n}}{Δ t}, v_{i} ⟩ + ⟨ A_{i} u_{i}^{n + 1}, v_{i} ⟩) = \sum_{i = 1}^{2} ⟨ F_{i}^{n + 1}, v_{i} ⟩ (v \in V) .$

It obeys the exact identity

$\frac{1}{2} (∥ u^{n + 1} ∥_{M}^{2} - ∥ u^{n} ∥_{M}^{2} + ∥ u^{n + 1} - u^{n} ∥_{M}^{2}) + Δ t ∥ u^{n + 1} ∥_{A}^{2} = Δ t \sum_{i = 1}^{2} ⟨ F_{i}^{n + 1}, u_{i}^{n + 1} ⟩,$

where $∥ v ∥_{M}^{2} : = \sum_{i} ⟨ M_{i} v_{i}, v_{i} ⟩$ and $∥ v ∥_{A}^{2} : = \sum_{i} ⟨ A_{i} v_{i}, v_{i} ⟩$ . In the unforced case the monolithic backward-Euler energy is nonincreasing.

Facts & Assumptions

Given: The finite-dimensional spaces, positive-definite mass and diffusion operators, common trace map, outward flux convention, and monolithic flux balance of Finite-dimensional backward-Euler diffusion transmission model.

[F1]

Finite-dimensional backward-Euler diffusion transmission model: $M_{i}$ and $A_{i}$ are self-adjoint positive definite, local fluxes use the outward sign, and monolithic traces and fluxes satisfy $λ_{1} = λ_{2}$ and $q_{1} + q_{2} = 0$ .

Proof

1.1givenF1algebra

The interior rows of the two local blocks give their backward-Euler subdomain equations; after eliminating those rows, the common trace row is $q_{1} + q_{2} = 0$ by the definition in [F1]. For a common trace $λ$ , the paired interface work is therefore $⟨ q_{1}, λ ⟩ + ⟨ q_{2}, λ ⟩ = ⟨ q_{1} + q_{2}, λ ⟩ = 0$ ; this cancellation uses the shared trace and outward-flux sign convention.

1.2givenF1algebra

On $V$ , the assembled bilinear form associated with $Δ t^{- 1} M_{i} + A_{i}$ is positive definite: for $v \in V ∖ {0}$ , at least one $v_{i} \neq 0$ , and every corresponding summand $Δ t^{- 1} ⟨ M_{i} v_{i}, v_{i} ⟩ + ⟨ A_{i} v_{i}, v_{i} ⟩$ is positive. Hence the finite-dimensional restricted operator has zero kernel and is invertible, so the variational step has a unique solution. Test the monolithic equation with $v = u^{n + 1}$ and multiply by $Δ t$ . For each $i$ , self-adjointness gives $2 ⟨ M_{i} (u_{i}^{n + 1} - u_{i}^{n}), u_{i}^{n + 1} ⟩ = ∥ u_{i}^{n + 1} ∥_{M_{i}}^{2} - ∥ u_{i}^{n} ∥_{M_{i}}^{2} + ∥ u_{i}^{n + 1} - u_{i}^{n} ∥_{M_{i}}^{2}$ . Summing this identity and retaining $Δ t \sum_{i} ⟨ A_{i} u_{i}^{n + 1}, u_{i}^{n + 1} ⟩$ yields the stated equality.

2.1step 1.2algebra∎

If $F_{i}^{n + 1} = 0$ for both subdomains, the right-hand side is zero and both the time-jump term and diffusion term on the left are nonnegative. Therefore $∥ u^{n + 1} ∥_{M}^{2} \leq ∥ u^{n} ∥_{M}^{2}$ .

Depends on

Finite-dimensional backward-Euler diffusion transmission model

Used by

A two-domain heat trace balances outward fluxes Example

Dependency tree · one level

1 result 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)