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.

Benchmarks, prior shift, and solver admissibility — Examples and Counterexamples

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

None yet.

4 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedverified 2026-10-22 (gpt-6.1-sol)Open item page →

First-Born optical scattering benchmark

Example

In the implemented first-Born optical-scattering benchmark, the unknown is a real $128 \times 128$ array $z$ of cellwise permittivity contrasts, each equal to the object's permittivity minus the background permittivity. For each transmitter $j \in {1, \dots, 20}$ , $u_{i n}^{(j)}$ is its fixed incident illumination field, and $H_{m, r}$ is the fixed Green response from cell $r$ to receiver $m$ . The released forward implementation reports measurements

$y_{j, m} = Δ x Δ y \sum_{r} z_{r} \overline{u_{i n}^{(j)} (r)} H_{m, r} + e_{j, m},$

where $m$ indexes receivers, $r$ indexes grid cells, $Δ x = Δ y = 18 c m / 128$ are the grid spacings, and $e$ is additive Gaussian measurement noise with reported level $σ_{y} = 10^{- 4}$ . Thus the implemented map is real-linear in $z$ . The reported physical field is $18 c m \times 18 c m$ , the wavelength is $0.84 c m$ , the background permittivity is $1$ , and the receiver count is $360$ , $180$ , or $60$ . The paper reports $10,000$ training images of HL60-cell permittivity, $10$ validation images, and $100$ test images; it curates the test samples so their cosine similarities to training images are below $0.6$ , where cosine similarity of nonzero image arrays $a, b$ is $⟨ a, b ⟩ / (∥ a ∥_{2} ∥ b ∥_{2})$ . The paper's Appendix B.1 also prints a contrast-dependent total-field formula; this example follows the fixed-incident-field implementation and does not infer linearity from that printed formula.

Example references

A benchmark fixes its data law, forward solver, metric, and compute budget

InverseBench findings and the paper/implementation notation discrepancy

Zheng et al., InverseBench, §4.1 and Appendix B.1

InverseBench inverse_scatter.py, pinned implementation

Facts & Assumptions

Given: The real contrast grid, fixed incident fields and sensor Green coefficients, the finite grid and data split stated in the Example, and the released implementation's fixed-incident-field forward routine.

[F1]

Benchmark risk, compute budgets, and uncertainty records: a benchmark instance declares its truth/target spaces, forward observation model, noise, metric, and evaluation protocol.

[F2]

Scope of InverseBench findings: the paper/code discrepancy is resolved for this example by following the implementation, which passes a fixed incident field and builds the linear matrix from that field.

[A1]

For an explicit conditional finite-data benchmark, supply the actual nonempty training, validation, and test lists of the stated sizes, including realized observations, target images, operator metadata, and valid discrete forward values. Let $X = U = C$ be the finite set of labelled cases, with its full power-set sigma-algebra; labels distinguish repeated images. Let $Q = R^{128^{2}}$ with Euclidean distance and Borel sets, and let $Y$ be the finite-dimensional observation-and-operator-metadata space with Borel sets. For case $i$ , set $q (i) = a_{i}$ (its target image), $F (i) = f_{i}$ (its discrete noiseless forward data), and $K (\cdot ∣ i) = δ_{y_{i}}$ (its recorded data, with the same metadata). Thus $K$ describes replay conditional on these realized lists, not fresh Gaussian noise. Set $P_{t e s t} = N^{- 1} \sum_{i \in T} δ_{(y_{i}, a_{i})}$ , where $T$ is the test index set and $N = 100$ ; use the analogous uniform empirical validation law. Take $P_{t r a i n}$ to be the point mass at the entire supplied fitting record, including training/tuning lists and seeds. This conditional specialization supplies laws, not just sample counts, and is not a reconstruction of the paper's full evaluation protocol.

[A2]

Supply each candidate's complete fitting/tuning procedure and deployed measurable rule $g : Y \to Q$ , with all seeds fixed. Fix the loss $ℓ (a, b) = ∥ a - b ∥_{2}^{2}$ and a radius $r > 0$ before testing. The uncertainty diagnostic is empirical coverage $N^{- 1} \sum_{i \in T} 1 {∥ g (y_{i}) - a_{i} ∥_{2} \leq r}$ , targeting coverage of the balls of radius $r$ centered at $g (y)$ under $P_{t e s t}$ . Evaluate every test case once and average its loss. Before fitting or evaluation, supply finite upper bounds for every applicable forward, adjoint, gradient, ODE-evaluation, iteration/sampling, and runtime count, marking inapplicable entries as not applicable, together with hardware, precision, software/model versions, seeds, tuning data, and stopping tolerances. A procedure must return within these bounds or record failure; its deployed rule returns the zero image on failure. Retain that case in both aggregates and report every status and realized count. These supplied procedures and budget records are parameters of this mathematical specialization; the coverage statistic is not a reported InverseBench calibration result.

Verification

1.1givenalgebra

For each fixed pair $(j, m)$ , all coefficients multiplying $z_{r}$ in the displayed finite sum are fixed independently of $z$ . Therefore the signal part is a real-linear function of the real vector $z$ ; adding the specified noise yields the stated measurement model.

1.2A1F1

On the finite labelled truth space in [A1], the target and discrete forward maps are measurable. For each case $i$ , $K (\cdot ∣ i) = δ_{y_{i}}$ is a probability measure, and $i \mapsto K (B ∣ i)$ is measurable for every Borel observation set $B$ . The declared empirical test/validation laws and point-mass fitting law therefore supply the probability fields of [F1]. Conditioning on a realized noisy list does not identify its replay kernel with the original Gaussian acquisition law.

2.1A1A2F1F2∎

The squared loss and radius-ball membership event in [A2] are product-measurable, and integration against the empirical test law gives exactly the specified average loss and coverage. The supplied procedures, budget records, and failure convention complete the remaining fields of [F1]. Cosine similarity only curates the data; it is not this evaluation loss. The implemented real-linear model and the source/code qualification in [F2] remain unchanged, and no calibration theorem is inferred.

ExampleConstruction: AI-generatedVerification: AI-generatedverified 2026-10-22 (gpt-6.1-sol)Open item page →

Multi-coil MRI benchmark

Example

In the InverseBench multi-coil knee MRI case, a complex image $z \in C^{n}$ with $n = 320^{2}$ produces one k-space data vector per receiver coil:

$y_{j} = P F S_{j} z + n_{j} \in C^{m}, j = 1, \dots, J .$

Here $J$ is the number of coils, $S_{j}$ is multiplication by the sensitivity map of coil $j$ , estimated for each slice using ESPIRiT as implemented in SigPy, $F$ is the discrete Fourier transform, k-space is the Fourier-coefficient data space, $P \in {0, 1}^{m \times n}$ selects the acquired k-space entries, and $n_{j}$ is the raw measurement noise in that coil. With these operators fixed, the measurement map is linear in $z$ ; the paper does not assume Gaussian noise for the raw-data benchmark. Its fastMRI knee split contains $25,012$ training images, $6$ hyperparameter-search images, and $94$ test images, preprocessed to $320 \times 320$ . For the reported metrics in Tables 4 and 5, the reference ground-truth image is the magnitude image of the minimum-variance unbiased estimator (MVUE); these magnitude-MVUE images are also used as training ground truths for Residual UNet and E2E-VarNet. The reported test metrics include peak signal-to-noise ratio (PSNR), structural similarity index measure (SSIM), and data misfit.

Example references

A benchmark declares its noise, metric, and test population

Empirical findings remain confined to the named InverseBench tasks

Zheng et al., InverseBench, §4.1, Appendix B.2, and Table 4

Facts & Assumptions

Given: The finite complex image space, per-slice ESPIRiT-estimated coil sensitivity maps, the fixed Fourier/subsampling operators, raw coil measurement vectors, the magnitude-MVUE ground-truth convention for the reported metrics, and the train/search/test split stated in the Example.

[F1]

Benchmark risk, compute budgets, and uncertainty records: a benchmark fixes its observation model, noise description, loss/metric, evaluation law, and tuning protocol.

[F2]

Scope of InverseBench findings: the empirical MRI results are for the specified multi-coil knee data and test split, not a theorem for other image populations.

[A1]

For an explicit conditional finite-data benchmark, supply the actual nonempty training, validation, and test lists of the stated sizes, including realized observations, target images, operator metadata, and valid discrete forward values. Let $X = U = C$ be the finite set of labelled cases, with its full power-set sigma-algebra; labels distinguish repeated images. Let $Q = R^{320^{2}}$ with Euclidean distance and Borel sets, and let $Y$ be the observation-and-operator-metadata space, a finite disjoint union of finite-dimensional Borel spaces if coil counts or data shapes vary; include each case's coil sensitivities and mask in its observation metadata. For case $i$ , set $q (i) = a_{i}$ (its magnitude-MVUE reference image), $F (i) = f_{i}$ (its discrete noiseless forward data), and $K (\cdot ∣ i) = δ_{y_{i}}$ (its recorded data, with the same metadata). For the coil data, the conditional residual law is the point mass at the recorded residual $y_{i}^{d a t a} - f_{i}^{d a t a}$ ; it is not asserted Gaussian, independent of the state, or a law for unobserved acquisitions. Thus $K$ describes replay conditional on these realized lists, not a physical law for repeated MRI acquisitions. Set $P_{t e s t} = N^{- 1} \sum_{i \in T} δ_{(y_{i}, a_{i})}$ , where $T$ is the test index set and $N = 94$ ; use the analogous uniform empirical validation law. Take $P_{t r a i n}$ to be the point mass at the entire supplied fitting record, including training/tuning lists and seeds. This conditional specialization supplies laws, not just sample counts, and is not a reconstruction of the paper's full evaluation protocol.

[A2]

Verification

1.1givenalgebra

With $P$ , $F$ , and each $S_{j}$ fixed, $P F S_{j}$ is a linear map on $C^{n}$ ; therefore the displayed observation equation is a linear multi-coil measurement model for each $j$ .

1.2A1F1

For each labelled case in [A1], $K (\cdot ∣ i) = δ_{y_{i}}$ is a probability measure. Every function on the finite truth space is measurable, including $i \mapsto K (B ∣ i)$ for each Borel observation set $B$ . Thus this is an explicitly specified probability kernel, and $q$ , $F$ , and the empirical test/validation and point-mass fitting laws are measurable or probability-valued as required by [F1]. This conditional construction uses recorded raw data and makes no inference of a physical noise law from the term "raw noise."

2.1A1A2F1F2∎

The squared loss and ball-membership event in [A2] are product-measurable for the magnitude-image targets and measurable deployed rule. Their empirical-law integrals equal the declared averages, including fallback outputs. The procedures, budgets, metadata, and retained statuses in [A2] complete this finite-data instance of [F1]. The paper's PSNR/SSIM/data-misfit reports retain their original meaning and scope in [F2]; the chosen squared-error and coverage protocol is an explicit specialization, not a claim that the paper specified this diagnostic or a physical observation kernel.

ExampleConstruction: AI-generatedVerification: AI-generatedverified 2026-10-22 (gpt-6.1-sol)Open item page →

Black-hole VLBI benchmark

Example

In the InverseBench black-hole-imaging case, very-long-baseline interferometry correlates telescope electric-field signals to produce complex visibilities of a nonnegative source-brightness image $z (ρ, δ)$ on angular coordinates $(ρ, δ)$ . For a telescope pair $(a, b)$ at time $t$ , the ideal visibility is the corresponding Fourier sample

$I_{a, b}^{t} (z) = \iint z (ρ, δ) e^{- 2 π i (u_{a, b}^{t} ρ + v_{a, b}^{t} δ)} d ρ d δ,$

where $(u_{a, b}^{t}, v_{a, b}^{t})$ is the projected baseline. The observed visibility is

$V_{a, b}^{t} = g_{a}^{t} g_{b}^{t} e^{- i (ϕ_{a}^{t} - ϕ_{b}^{t})} I_{a, b}^{t} (z) + η_{a, b}^{t},$

where $g_{a}^{t}, g_{b}^{t}$ are telescope amplitude gains, $ϕ_{a}^{t}, ϕ_{b}^{t}$ are phase errors, and $η_{a, b}^{t}$ is additive Gaussian thermal noise. For an oriented telescope triangle $(a, b, c)$ , the closure phase is $\arg (V_{a, b}^{t} V_{b, c}^{t} V_{c, a}^{t})$ ; when a stored visibility has the opposite baseline orientation, the implementation uses its complex conjugate. For the ordered quadrangle $(a, b, c, d)$ returned by the implementation's closure-amplitude routine, the log closure amplitude is $\log ⁣ (∣ V_{a, b}^{t} ∣ ∣ V_{c, d}^{t} ∣ / (∣ V_{a, d}^{t} ∣ ∣ V_{b, c}^{t} ∣))$ . The closure phase is defined only when its triangle product is nonzero, and a log closure amplitude is defined only when all four relevant visibility amplitudes are nonzero. No value is assigned by these formulas at an undefined zero visibility; this domain restriction does not assert an implementation masking or rejection rule. The benchmark also uses total flux $\iint z (ρ, δ) d ρ d δ$ . These derived data are nonlinear functions of the visibilities, so their noise is not additive. The training images are $50,000$ simulated general-relativistic magnetohydrodynamic images resized to $64 \times 64$ . Because those images are not public, the paper generates $5$ validation and $100$ test images from a pretrained diffusion model. The sparse, nonconvex closure-data model has multiple solutions compatible with the observations; the reported tests do not make a general uniqueness or posterior-calibration claim.

Example references

A benchmark declares its observation model, metric, test law, and uncertainty diagnostic

The reported scope and empirical limitations of InverseBench

Zheng et al., InverseBench, §§3 and 4.1, Appendix B.3

InverseBench blackhole.py, pinned implementation

Facts & Assumptions

Given: A nonnegative image, telescope pairs and projected baselines, the complex visibility and gain/noise model, closure-data transformations on their stated nonzero-visibility domains, and the data-generation split stated in the Example.

[F1]

Benchmark risk, compute budgets, and uncertainty records: a benchmark instance fixes its forward/observation model, noise description, metric, and evaluation population.

[F2]

Scope of InverseBench findings: the black-hole results are empirical for the paper's selected image/data setup and do not imply a general ranking or calibration result.

[A1]

For an explicit conditional finite-data benchmark, supply the actual nonempty training, validation, and test lists of the stated sizes, including realized observations, target images, operator metadata, and valid discrete forward values. All closure values in these lists must satisfy the stated nonzero-visibility restrictions. Let $X = U = C$ be the finite set of labelled cases, with its full power-set sigma-algebra; labels distinguish repeated images. Let $Q = R^{64^{2}}$ with Euclidean distance and Borel sets, and let $Y$ be the finite-dimensional observation-and-operator-metadata space with Borel sets. For case $i$ , set $q (i) = a_{i}$ (its target image), $F (i) = f_{i}$ (its discrete noiseless forward data), and $K (\cdot ∣ i) = δ_{y_{i}}$ (its recorded data, with the same metadata). Thus $K$ describes replay conditional on these realized lists, not fresh telescope noise. Set $P_{t e s t} = N^{- 1} \sum_{i \in T} δ_{(y_{i}, a_{i})}$ , where $T$ is the test index set and $N = 100$ ; use the analogous uniform empirical validation law. Take $P_{t r a i n}$ to be the point mass at the entire supplied fitting record, including training/tuning lists and seeds. This conditional specialization supplies laws, not just sample counts, and is not a reconstruction of the paper's full evaluation protocol.

[A2]

Supply each candidate's complete fitting/tuning procedure and deployed measurable rule $g : Y \to Q$ , with all seeds fixed. Fix the loss $ℓ (a, b) = ∥ a - b ∥_{2}^{2}$ and a radius $r > 0$ before testing. The uncertainty diagnostic is empirical coverage $N^{- 1} \sum_{i \in T} 1 {∥ g (y_{i}) - a_{i} ∥_{2} \leq r}$ , targeting coverage of the balls of radius $r$ centered at $g (y)$ under $P_{t e s t}$ . Evaluate every test case once and average its loss; no shift alignment is used in this chosen squared-error score. Before fitting or evaluation, supply finite upper bounds for every applicable forward, adjoint, gradient, ODE-evaluation, iteration/sampling, and runtime count, marking inapplicable entries as not applicable, together with hardware, precision, software/model versions, seeds, tuning data, and stopping tolerances. A procedure must return within these bounds or record failure; its deployed rule returns the zero image on failure. Retain that case in both aggregates and report every status and realized count. These supplied procedures and budget records are parameters of this mathematical specialization; the coverage statistic is not a reported InverseBench calibration result.

Verification

1.1givenalgebra

Substitution of the ideal Fourier visibility into the displayed gain/phase/noise equation gives the paper's complex observation model; on the stated nonzero-visibility domains, applying the displayed argument and log-amplitude functions gives the stated closure data.

1.2A1F1

On the finite labelled truth space in [A1], $q$ and $F$ are measurable and each $K (\cdot ∣ i)$ is a probability measure; for every Borel set $B \subseteq Y$ , $i \mapsto 1_{B} (y_{i})$ is measurable. Thus $K$ is a probability kernel. The empirical test and validation laws and the point-mass fitting law are specified probability measures. They complete the case data with the law fields of [F1]; the split sizes alone do not determine those laws.

2.1A1A2F1F2∎

The squared loss and the ball-membership event in [A2] are product-measurable, since $g$ is measurable and the Euclidean distance is continuous. Their integrals under the empirical test law are exactly the declared finite averages, including the prescribed fallback outputs. Together with the supplied procedures, finite budgets, metadata, and failure records, these instantiate the remaining fields of [F1]. This verifies the conditional specialization, while the source's empirical scope remains [F2]; neither empirical coverage nor the physical observation formulas imply population calibration or uniqueness.

ExampleConstruction: AI-generatedVerification: AI-generatedverified 2026-10-22 (gpt-6.1-sol)Open item page →

Full waveform inversion benchmark

Example

In the InverseBench full-waveform-inversion (FWI) case, the unknown $v (x) > 0$ is the compressional-wave velocity on a two-dimensional physical domain $Ω$ ; its discretization is a $128 \times 128$ velocity map $z$ . For each source signal $q (x, t)$ , the pressure field starts with zero initial pressure and velocity, $u (\cdot, 0) = 0$ and $\partial_{t} u (\cdot, 0) = 0$ on $Ω$ , and solves

$v (x)^{- 2} \partial_{t}^{2} u (x, t) - \nabla^{2} u (x, t) = q (x, t),$

and the observation is the receiver restriction $y = P u$ , where $P$ samples the wavefield at the selected receivers. The benchmark uses a $2.54 k m \times 1.27 k m$ domain, horizontal and vertical grid spacings of $20 m$ and $10 m$ , a $0.001 s$ time step chosen to satisfy the numerical solver's Courant–Friedrichs–Lewy stability condition, a $5 H z$ Ricker source wavelet, and $1 s$ of simulated time. Its top boundary has the natural free-surface condition, while the other boundaries have absorbing conditions of width $80$ grid points. It uses $16$ sources at depth $1270 m$ and $129$ receivers evenly placed near the free surface at depth $10 m$ . The reported observation noise is zero. The CurveFaultB velocity-map split has $50,000$ training maps, one validation map, and ten test maps, resized to $128 \times 128$ . These counts and solver settings define this empirical benchmark instance; they are not existence or convergence claims for full waveform inversion.

Example references

A benchmark declares its solver, noise, test population, and compute protocol

FWI performance and stability observations are empirical

Zheng et al., InverseBench, §3, §4.1, and Appendix B.4

InverseBench acoustic forward implementation, pinned revision

Devito v4.8.12 acoustic solver

Devito v4.8.12 wavefield data initialization

Facts & Assumptions

Given: A positive velocity map, the acoustic pressure-wave equation and source signal with zero initial pressure and velocity, the receiver sampling operator, a free-surface top and absorbing other boundaries of width $80$ grid points, $16$ sources at depth $1270 m$ , $129$ receivers at depth $10 m$ , the stated discrete solver and mesh, and the finite CurveFaultB split.

[F1]

Benchmark risk, compute budgets, and uncertainty records: a benchmark instance includes its forward solver, admissible inputs, noise, compute protocol, and test population.

[F2]

Scope of InverseBench findings: the reported FWI outcomes concern this selected solver, tuning procedure, and test set only.

[A1]

For an explicit conditional finite-data benchmark, supply the actual nonempty training, validation, and test lists of the stated sizes, including realized observations, target images, operator metadata, and valid discrete forward values. Let $X = U = C$ be the finite set of labelled cases, with its full power-set sigma-algebra; labels distinguish repeated images. Let $Q = R^{128^{2}}$ with Euclidean distance and Borel sets, and let $Y$ be the finite-dimensional observation-and-operator-metadata space with Borel sets. For case $i$ , set $q (i) = a_{i}$ (its target image), $F (i) = f_{i}$ (its discrete noiseless forward data), and $K (\cdot ∣ i) = δ_{y_{i}}$ (its recorded data, with the same metadata). Thus $K$ describes replay conditional on these realized lists, not a population of newly sampled velocity fields. Require $y_{i} = f_{i}$ because this case is noise-free; the forward values are outputs of the specified discrete solver on admissible inputs, with its actual settings recorded. Set $P_{t e s t} = N^{- 1} \sum_{i \in T} δ_{(y_{i}, a_{i})}$ , where $T$ is the test index set and $N = 10$ ; use the analogous uniform empirical validation law. Take $P_{t r a i n}$ to be the point mass at the entire supplied fitting record, including training/tuning lists and seeds. This conditional specialization supplies laws, not just sample counts, and is not a reconstruction of the paper's full evaluation protocol.

[A2]

Verification

1.1givenconstruct

With the zero initial data and the stated source, boundary conditions, and solver, the forward call produces the acoustic wavefield; applying the receiver restriction $P$ gives the stated observation, with the velocity map as the parameter being inferred.

1.2A1F1

On the finite labelled truth space of [A1], $q$ and $F$ are measurable. Since $y_{i} = f_{i}$ , the replay kernel $K (\cdot ∣ i) = δ_{F (i)}$ is the noise-free observation kernel for this supplied finite numerical model; its dependence on $i$ is measurable. The empirical test/validation laws and point-mass fitting law specify the population fields of [F1]. The counts fix their list sizes, while the actual supplied lists fix their atoms.

2.1A1A2F1F2∎

The squared loss and radius-ball membership event in [A2] are product-measurable, so the loss and coverage under the empirical test law equal the declared finite averages. With the supplied procedures, finite budgets, solver settings, metadata, and retained failure records, this gives the remaining fields of [F1]. The source experiment remains scoped as in [F2]; this finite-data specialization proves no continuum PDE existence, numerical convergence, population generalization, or posterior-calibration theorem.

ExampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

Two-dimensional Navier–Stokes benchmark

Example

In the InverseBench two-dimensional Navier–Stokes case, the spatial domain is the periodic square $(0, 2 π)^{2}$ (the flat torus). In the physical vorticity model, the periodic velocity $u (x, t) \in R^{2}$ is divergence-free and its scalar curl is $ω = \partial_{1} u_{2} - \partial_{2} u_{1}$ . This curl has zero spatial mean. Taking the spatial mean of $u$ to be zero fixes the constant-velocity ambiguity. For viscosity $ν > 0$ , forcing $f (x) = - 4 \cos (4 x_{2})$ , and compatible initial curl $ω_{0}$ , the physical model is

$\partial_{t} ω + u \cdot \nabla ω = ν Δ ω + f, \nabla \cdot u = 0, ω (\cdot, 0) = ω_{0} .$

The released benchmark uses a finite-grid scalar state denoted $w$ . Its pinned solver computes velocity by Fourier streamfunction derivatives, which select zero spatial mean velocity and ignore the constant Fourier mode of the scalar state. The nonlinear term uses a dealiased state with zero mode removed, while the time-update formula retains the original state's zero mode; the specified forcing also has zero mean. Thus the solver defines a scalar-state extension even when $\overline{w} \neq 0$ . One must not identify such an entire state with the curl of a periodic velocity. In the corresponding continuum mean-split convention, $w = \overline{w} + ω$ , $- Δ ψ = ω$ , and $u = (\partial_{2} ψ, - \partial_{1} ψ)$ ; only $ω = w - \overline{w}$ is the curl, and $\overline{w}$ is a conserved scalar offset. This convention explains the zero-mode distinction; it does not assert that the finite-grid dealiased scheme is an exact continuum solution or that the released dataset has been projected to zero mean.

The reconstruction target is the supplied dataset field $z = w_{0}$ used as initial state for the inversion solver; the observation is $y = P L (z) + n$ , where $L$ is this numerical scalar-state solution map over the specified inversion horizon $T$ , $P$ samples the final field, and $n$ is Gaussian measurement noise. The dataset-generation horizon is a separate five time units: §4.1 and Appendix B.5 report independent Gaussian seed fields $ξ \sim N (0, (- Δ + 9 I)^{- 4})$ , evolved under the stated forcing for five time units to produce the dataset of nontrivial initial fields. Accordingly, $z$ denotes the evolved field, not a claim that the inversion-input distribution remains Gaussian with the seed covariance. On the full periodic space the reported covariance gives the constant eigenmode variance $9^{- 4} > 0$ ; the paper does not specify a zero-mode projection for the seed law. The scalar-state implementation permits retaining that offset without asserting the incompatible identity $w = \nabla \times u$ for arbitrary seeds.

InverseBench uses a pseudo-spectral solver with adaptive time stepping; the reported setup has a $128 \times 128$ grid, Reynolds number $200$ , $10,000$ training samples, one validation sample, and ten test samples. The paper reports black-box forward access without a closed-form gradient for this implementation; the one-validation/ten-test split is part of this empirical benchmark, not a population-level guarantee.

Example references

The solver, noise, compute budget, and test law are explicit benchmark fields

The Navier–Stokes results are empirical for the reported split

Zheng et al., InverseBench, §3, §4.1, Appendix B.5, Tables 2 and 8

Versioned full-text counterpart, §4.1 and Appendix B.5

Pinned Navier–Stokes scalar-state implementation

Facts & Assumptions

Given: The periodic domain, physical mean-zero-curl convention, forcing $f (x) = - 4 \cos (4 x_{2})$ , the pinned finite-grid scalar-state solver with its streamfunction velocity and retained constant mode, the reported Gaussian seed law and five-time-unit dataset preparation, the supplied evolved inversion input $z = w_{0}$ , final-time sampling map, Gaussian observation noise, and stated finite dataset split.

[F1]

Benchmark risk, compute budgets, and uncertainty records: the benchmark specification includes the forward solver, noise law, compute/interface constraints, and test population.

[F2]

Scope of InverseBench findings: this numerical PDE result uses a validation split of size one and a test split of size ten, so it supports no broad-population performance theorem.

Verification

1.1givenconstruct

The supplied evolved dataset field $z = w_{0}$ is the initial scalar state for the specified numerical map $L$ . Applying its final-time sampling operator $P$ and adding the stated observation noise gives exactly $y = P L (z) + n$ ; the separate five-time-unit seed evolution prepares $z$ and is not the inversion horizon.

2.1F1F2given∎

The stated forcing and seed-to-dataset preparation, grid, pseudo-spectral solver, noise model, and finite data split fill the solver/population fields of [F1]. The empirical scope in [F2] is retained, and no closed-form-gradient or convergence claim is added.

ExampleConstruction: AI-generatedVerification: AI-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)Open item page →

Prior-matched and out-of-distribution cases

Example

For an operational within-source reference, InverseBench trains its multi-coil MRI diffusion prior on $25,012$ fastMRI knee images and evaluates on $94$ held-out images from the same named data collection. This is a dataset-family match, not a claim that the population training and test laws are equal. Its separate out-of-distribution diagnostics change the source: a black-hole-imaging prior is trained on $50,000$ simulated general-relativistic magnetohydrodynamic images, while one stress test uses digit images; in linear inverse scattering, the prior is trained on sources with one through six cells, while the stress test uses nine-cell sources. The paper reports outputs drawn toward black-hole structure in the digit case and more effective recovery when the scattering source is close to the trained prior. These are finite, method- and dataset-specific observations; they provide no risk bound or distribution-shift guarantee.

Example references

Training and test laws are separately specified benchmark fields

Risk depends on the named joint test law

Prior-support mismatch is distinct from operator or noise mismatch

InverseBench prior-shift findings are empirical and task-scoped

Zheng et al., InverseBench, §4.1, §4.3, Figure 5, and Appendix C

Facts & Assumptions

Given: The finite train/test splits, each prior's training-source family, and the paper's selected out-of-distribution stress tests and qualitative observations.

[F1]

Benchmark risk, compute budgets, and uncertainty records: the training and test laws are separate inputs and need not be equal.

[F2]

Inverse reconstruction risk under train and test laws: test risk is computed under the specified joint test law, and no comparison with training risk follows without an additional premise.

[F3]

Operator, noise-law, and prior-support mismatch: prior-support mismatch is a distinct model property and by itself supplies no posterior or risk-robustness theorem.

[F4]

Scope of InverseBench findings: InverseBench's results concern its named data, solver, methods, and tuning protocol.

Verification

1.1F1given

The MRI training and held-out test splits come from the same named fastMRI knee collection, so they provide an operational within-source comparison; [F1] does not identify their underlying probability laws.

2.1F2F3F4given∎

The black-hole digit and nine-cell scattering cases deliberately change the test-source family from the source used to train each prior. The reported output tendencies are finite observations under [F4], and [F2]–[F3] preclude promoting them to a general test-risk or robustness bound.

ExampleConstruction: AI-generatedVerification: AI-generatedverified 2026-10-22 (gpt-6.1-sol)Open item page →

A solver-invalid FWI iterate

Example

Fix an FWI velocity-model solver $S$ with a declared finite admissibility predicate ${adm}_{S} (v)$ that checks that solver's coefficient, boundary, mesh, and time-step conditions, including its solver-specific Courant–Friedrichs–Lewy (CFL) condition. If an optimization method proposes a candidate velocity map $\tilde{v}$ with ${adm}_{S} (\tilde{v}) = f a l s e$ , the benchmark records the call as a solver/admissibility failure; its evaluation protocol specifies whether and how that failed trial contributes to any numerical aggregate. In its FWI DAPS experiment, InverseBench reports that a smaller learning rate gave numerically stable but data-ineffective outputs, while a slightly larger learning rate produced a noisy velocity map that violated the PDE solver's CFL condition and failed. The paper gives no exact violating iterate or universal CFL threshold; this example claims neither.

Example references

Failed solver calls remain visible in benchmark results

An admissibility predicate and CFL condition are solver-specific

The step-size/CFL observation is empirical and task-scoped

Zheng et al., InverseBench, §4.3 and Figure 3

Facts & Assumptions

Given: A chosen FWI solver $S$ , its declared finite admissibility predicate, an optimizer-produced velocity map $\tilde{v}$ , the Boolean result ${adm}_{S} (\tilde{v}) = f a l s e$ , and the qualitative DAPS observation reported in the Example.

[F1]

Benchmark risk, compute budgets, and uncertainty records: a failed solver/admissibility call is recorded with its status and is not silently omitted from results.

[F2]

Finite-element PDE solver admissibility and certificate contract: an admissibility predicate tests the specified model's hypotheses, and any CFL condition is method-specific; the definition supplies no universal threshold.

[F3]

Scope of InverseBench findings: InverseBench reports the FWI step-size/CFL behavior as an empirical observation for its named solver and methods.

Verification

1.1F2given

Since ${adm}_{S} (\tilde{v}) = f a l s e$ , the proposed iterate fails the selected solver's declared admissibility test; it is therefore not an admissible input for that solver call.

1.2F1F2given

By [F1], the benchmark records this call as failure and does not silently omit it. [F1] does not prescribe whether the failed call receives or contributes to a numerical score, so no particular scoring rule is asserted.

2.1F3given∎

The stated smaller-step/larger-step DAPS behavior is the paper's reported FWI observation for its numerical PDE setup, as recorded by [F3]; no inference is made from it to other solvers or parameter ranges.

Benchmarks, prior shift, and solver admissibility — Examples and Counterexamples

2 · Logical flowchart

3 · Definitions, theorems and proofs

4 · Examples, counterexamples and false statements

First-Born optical scattering benchmark

Example

Example references

Facts & Assumptions

Verification

Multi-coil MRI benchmark

Example

Example references

Facts & Assumptions

Verification

Black-hole VLBI benchmark

Example

Example references

Facts & Assumptions

Verification

Full waveform inversion benchmark

Example

Example references

Facts & Assumptions

Verification

Two-dimensional Navier–Stokes benchmark

Example

Example references

Facts & Assumptions

Verification

Prior-matched and out-of-distribution cases

Example

Example references

Facts & Assumptions

Verification

A solver-invalid FWI iterate

Example

Example references

Facts & Assumptions

Verification

Sources