ExampleConstruction: AI-generatedVerification: 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.

Two Euler quadrature nodes rescaled to a positive margin

Example

With weights $w_{1} = w_{2} = 1 / 2$ , cell mean $\overset{ˉ}{U} = (1, 0, 1)$ , and candidate conserved states $V_{1} = (1, 4, 1)$ and $V_{2} = (1, - 4, 1)$ , apply the limiter to $K_{7 / 5, 1 / 2}$ . It returns $θ_{*} = 1 / 4$ , giving states $(1, 1, 1)$ and $(1, - 1, 1)$ with positive pressure and the original cell mean.

Facts & Assumptions

Given: The weights, mean, nodes, and set $K_{7 / 5, 1 / 2}$ . Compute the maximal scaling and verify the mean and positive margin.

[F1]

Maximal convex scaling toward an admissible cell mean: the limiter chooses the largest $θ \in [0, 1]$ keeping each $\overset{ˉ}{U} + θ (V_{j} - \overset{ˉ}{U})$ in $K$ .

[F2]

Positive-margin admissible states for ideal-gas Euler: $K_{γ, ε}$ requires $ρ \geq ε$ and $E - m^{2} / (2 ρ) \geq ε$ .

[F3]

Admissible states and pressure for one-dimensional ideal-gas Euler: $p = (γ - 1) (E - m^{2} / (2 ρ))$ .

[F4]

Convex scaling preserves the cell mean and positive-margin node states: the maximal scaling exists, preserves the weighted mean, and returns nodes in the positive-margin set.

Verification

1.1givenF2algebra

The weighted mean is $(V_{1} + V_{2}) / 2 = (1, 0, 1)$ . Its density is $1$ and its internal-energy density is $1$ , so it belongs to $K_{7 / 5, 1 / 2}$ by [F2]. The scaled states are $(1, 4 θ, 1)$ and $(1, - 4 θ, 1)$ , each with internal energy $1 - 8 θ^{2}$ . Hence they lie in $K_{7 / 5, 1 / 2}$ exactly when $1 - 8 θ^{2} \geq 1 / 2$ , or $0 \leq θ \leq 1 / 4$ .

2.1givenF1F2F3F4algebra∎

The largest feasible parameter is $θ_{*} = 1 / 4$ by [F1]. The outputs are $(1, 1, 1)$ and $(1, - 1, 1)$ ; each has internal-energy density $1 / 2$ and pressure $(2 / 5) (1 / 2) = 1 / 5 > 0$ by [F3]. Their weighted mean is $(1, 0, 1)$ , also as guaranteed by [F4].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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

X. Zhang and C.-W. Shu, On Positivity-Preserving High Order Discontinuous Galerkin Schemes for Compressible Euler Equations on Rectangular Meshes (standard reference, not scraped)
J.-L. Guermond and B. Popov, Invariant Domains and First-Order Continuous Finite Element Approximation for Hyperbolic Systems (standard reference, not scraped)