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.
Convex scaling preserves the cell mean and positive-margin node states
Statement
Fix , , a finite nonempty node set , positive weights summing to one, and candidate states with mean . Apply the maximal convex scaling limiter of Maximal convex scaling toward an admissible cell mean with . Its output is well-defined, every limited node lies in , and the weighted cell mean remains . Hence every limited node has positive density and positive pressure. If the unscaled nodes already lie in , the maximal parameter is . In particular, if smooth target states stay a distance at least from and each reconstruction node has error less than , the limiter is inactive and preserves that reconstruction's accuracy. No positivity between finitely many nodes is claimed.
Facts & Assumptions
Given: The finite weighted nodes and admissible mean, the closed convex set , and the maximal scaling procedure. Prove existence, conservation, nodewise admissibility, and the strict-margin accuracy implication.
Maximal convex scaling toward an admissible cell mean: the limiter selects the largest such that for all nodes.
Positive-margin admissible states for ideal-gas Euler: imposes and .
Euler positive states are convex and positive-margin sets are closed convex: is closed and convex.
Proof
The feasible parameter set contains . Each node map is continuous and is closed by [F3], so each inverse image is closed; the finite intersection is closed in compact . Thus is nonempty compact and has a maximum . By its definition, every limited node lies in .
Using and , the limited weighted mean is . By [F2], each limited node has density at least and pressure at least .
If every original , then , so . If a target state has distance at least from the complement and the candidate differs from it by less than , the candidate belongs to ; applying this at every node makes feasible. Thus the limiter leaves all candidates unchanged under the stated strict margin, and their reconstruction error is unchanged. The conclusion concerns only the supplied nodes.
Depends on
Used by
Dependency tree · two levels
5 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)