Pipeline-generated

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.

✓ 3 results · all verified · 2 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

ALE, interfaces and partitioned multiphysics coupling — Examples

1 · Prerequisites

2 · Summary

Worked ALE and interface cases

These examples instantiate the two separate branches on ale-interface-and-partitioned-multiphysics-discretization. Each calculation is finite and exact; none asserts a general nonlinear fluid-structure result.

Moving mesh

An expanding cell preserves a constant state uses two periodic cells. Their initial widths are both one; a single interior face moves right by $0.01$ , so the cell Jacobians become $1.01$ and $0.99$ . The upwind ALE flux changes each extensive cell value by exactly the corresponding geometric volume change, leaving the constant state and total mass unchanged.

Diffusion interface

A two-domain heat trace balances outward fluxes constructs two positive-definite backward-Euler blocks whose scalar Schur operators are $S_{1} = 2$ and $S_{2} = 1$ . It computes the common trace, the equal-and-opposite outward fluxes, and both passes of the Robin-Robin iteration needed to certify the trace tolerance.

Added mass

A toy sequential coupling can amplify velocity error sets $m_{s} = 1$ and $m_{f} = 2$ in the specifically defined scalar recurrence. It shows the increment doubles in magnitude at each pass, which demonstrates instability of that recurrence only.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

A toy sequential coupling can amplify velocity error

Statement

In the scalar recurrence of Scalar added-mass staggered recurrence, set $m_{s} = 1$ , $m_{f} = 2$ , and choose $δ v_{0} \neq 0$ . Then $δ v_{n} = (- 2)^{n} δ v_{0}$ , so the increments grow geometrically in magnitude.

Facts & Assumptions

Given: The recurrence $m_{s} δ v_{n + 1} = - m_{f} δ v_{n}$ from Scalar added-mass staggered recurrence, with $m_{s} = 1$ , $m_{f} = 2$ , and $δ v_{0} \neq 0$ .

[F1]

Scalar added-mass staggered recurrence: for $m_{s}, m_{f} > 0$ , $m_{s} δ v_{n + 1} = - m_{f} δ v_{n}$ .

Verification

1.1givenF1algebra

Dividing [F1] by $m_{s} = 1$ gives $δ v_{n + 1} = - 2 δ v_{n}$ .

2.1step 1.1algebrainduction

Induction yields $δ v_{n} = (- 2)^{n} δ v_{0}$ : it holds at $n = 0$ , and multiplying the formula at $n$ by $- 2$ gives it at $n + 1$ .

3.1givenF1step 2.1algebra∎

Since $∣ δ v_{0} ∣ > 0$ , $∣ δ v_{n} ∣ = 2^{n} ∣ δ v_{0} ∣$ and $∣ δ v_{n + 1} ∣ = 2 ∣ δ v_{n} ∣ > ∣ δ v_{n} ∣$ . If instead $δ v_{0} = 0$ , step 2.1 gives zero increments throughout, so the nonzero hypothesis is needed for growth. Thus this specified recurrence is unstable in the stated scalar sense; no broader FSI claim follows.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

An expanding cell preserves a constant state

Statement

On a two-cell periodic grid take $Δ ξ = 1$ , $Δ t = 0.1$ , period $L = 2$ , initial faces $x_{1 / 2} = 0$ , $x_{3 / 2} = 1$ , $x_{5 / 2} = 2$ , physical speed $a = 0$ , and periodic face velocities $w_{1 / 2} = 0$ , $w_{3 / 2} = 0.1$ , $w_{5 / 2} = 0$ . If both initial cell averages equal $U \in R$ , the successful ALE upwind step has Jacobians $1.01$ and $0.99$ , preserves both averages at $U$ , and conserves total mass $2 U$ .

Facts & Assumptions

Given: The grid, time step, face velocities, physical speed, and constant initial average in the Statement.

[F1]

Periodic one-dimensional moving grid: $J_{i}^{n} = (x_{i + 1 / 2}^{n} - x_{i - 1 / 2}^{n}) / Δ ξ$ , the face update is $x_{i + 1 / 2}^{n + 1} = x_{i + 1 / 2}^{n} + Δ t w_{i + 1 / 2}^{n}$ , and $c_{i + 1 / 2} = a - w_{i + 1 / 2}$ .

[F2]

Conservative upwind ALE finite-volume step: after checking $J_{i}^{n + 1} > 0$ , the algorithm uses ${\hat{F}}_{i + 1 / 2} = c_{i + 1 / 2}^{+} {\overset{ˉ}{u}}_{i} + c_{i + 1 / 2}^{-} {\overset{ˉ}{u}}_{i + 1}$ and $J_{i}^{n + 1} {\overset{ˉ}{u}}_{i}^{n + 1} = J_{i}^{n} {\overset{ˉ}{u}}_{i}^{n} - (Δ t / Δ ξ) ({\hat{F}}_{i + 1 / 2} - {\hat{F}}_{i - 1 / 2})$ .

[F3]

The upwind ALE step conserves mass and preserves constants: a successful periodic upwind ALE step preserves mass and every constant input state.

Verification

1.1givenF1F2algebra

The moved faces are $0$ , $1.01$ , and $2$ . Hence the two updated Jacobians are $1.01$ and $0.99$ , both positive, so [F2] returns success and performs the state update.

1.2givenF1F2algebra

The relative speeds at these faces are $0$ , $- 0.1$ , and $0$ , so the fluxes are $0$ , $- 0.1 U$ , and $0$ . Formula [F2] gives $J_{1}^{n + 1} {\overset{ˉ}{u}}_{1}^{n + 1} = U - 0.1 (- 0.1 U) = 1.01 U$ and $J_{2}^{n + 1} {\overset{ˉ}{u}}_{2}^{n + 1} = U - 0.1 (0.1 U) = 0.99 U$ . Dividing by the positive Jacobians gives both updated averages equal to $U$ .

2.1F1F3step 1.2algebra∎

The new total mass is $1.01 U + 0.99 U = 2 U$ , equal to the old mass $U + U$ . This is the finite instance of [F3].

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

A two-domain heat trace balances outward fluxes

Statement

Take a one-dimensional trace space $Λ = R$ , two interior spaces $I_{i} = R$ , $Δ t = 2$ , $M_{1} = M_{2} = I_{2}$ , $A_{1} = diag (1 / 2, 3 / 2)$ , and $A_{2} = diag (1 / 2, 1 / 2)$ , with the second coordinate as trace. Let the condensed loads be $f_{1} = 1$ , $f_{2} = 5$ . The monolithic trace is $2$ and the outward fluxes are $3$ and $- 3$ . With $α = 1$ , $r_{1}^{0} = 2$ , tolerance $0.1$ , and budget $M = 2$ , the Robin–Robin algorithm returns the certified trace $2$ on its second pass.

Facts & Assumptions

Given: The finite-dimensional local blocks, trace coordinates, condensed loads, Robin parameter, incoming datum, tolerance, and pass budget in the Statement.

[F1]

Finite-dimensional backward-Euler diffusion transmission model: $B_{i} = Δ t^{- 1} M_{i} + A_{i}$ , $q_{i} = S_{i} λ_{i} - f_{i}$ , and the monolithic trace solves $(S_{1} + S_{2}) λ = f_{1} + f_{2}$ .

[F2]

The diffusion Schur complement is positive and minimizes energy: each positive-definite local block has a positive-definite Schur complement.

[F3]

Monolithic backward Euler transmission energy identity: when traces match and outward fluxes balance, paired interface work cancels in the monolithic energy identity.

[F4]

Finite-budget Robin-Robin transmission iteration: each pass performs the two Robin solves and exchanges and stops only when the stated residual test passes.

[F5]

Robin-Robin iteration contracts to the monolithic trace: a passing stop test certifies trace error at most $ε$ relative to the monolithic trace.

Verification

1.1givenF1F2algebra

The local backward-Euler blocks are $B_{1} = diag (1, 2)$ and $B_{2} = diag (1, 1)$ , which are positive definite. With zero off-diagonal blocks between the interior and trace coordinates, their Schur operators are $S_{1} = 2$ and $S_{2} = 1$ , so [F2] applies.

1.2F1F4algebra

On pass one, $λ_{1}^{1} = (2 + 1) / 3 = 1$ , $r_{2}^{1} = (1 - 2) 1 + 1 = 0$ , $λ_{2}^{1} = (0 + 5) / 2 = 2.5$ , and $r_{1}^{1} = (1 - 1) 2.5 + 5 = 5$ . Here $q_{1} = ∣ (1 - 2) / (1 + 2) ∣ = 1 / 3$ , $q_{2} = 0$ , and the stop threshold is $0.1 / (1 / 3) = 0.3$ ; the incoming-data change is $∣ 5 - 2 ∣ = 3$ , so the algorithm does not stop.

2.1F1F3step 1.1algebra

The monolithic scalar equation is $3 λ = 6$ , hence $λ_{*} = 2$ . Its fluxes are $q_{1} = 2 (2) - 1 = 3$ and $q_{2} = 1 (2) - 5 = - 3$ , so they balance and the interface work $λ_{*} (q_{1} + q_{2})$ vanishes as in [F3].

3.1F4F5step 1.2step 2.1algebra∎

On pass two, $λ_{1}^{2} = (5 + 1) / 3 = 2$ , $r_{2}^{2} = (1 - 2) 2 + 1 = - 1$ , $λ_{2}^{2} = (- 1 + 5) / 2 = 2$ , and $r_{1}^{2} = (1 - 1) 2 + 5 = 5$ . The incoming-data change is $0 \leq 0.3$ , so [F4] returns converged with trace $2$ ; [F5] certifies its error is at most $0.1$ relative to $λ_{*} = 2$ from step 2.1.

ALE, interfaces and partitioned multiphysics coupling — Examples

1 · Prerequisites

2 · Summary

Worked ALE and interface cases

Moving mesh

Diffusion interface

Added mass

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

A toy sequential coupling can amplify velocity error

Statement

Facts & Assumptions

Verification

An expanding cell preserves a constant state

Statement

Facts & Assumptions

Verification

A two-domain heat trace balances outward fluxes

Statement

Facts & Assumptions

Verification

Sources