Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

Convex scaling preserves the cell mean and positive-margin node states

Statement

Fix γ>1, ε>0, a finite nonempty node set J, positive weights wj summing to one, and candidate states Vj∈R3 with mean Vˉ=∑jwjVj∈Kγ,ε. Apply the maximal convex scaling limiter of Maximal convex scaling toward an admissible cell mean with K=Kγ,ε. Its output is well-defined, every limited node lies in Kγ,ε, and the weighted cell mean remains Vˉ. Hence every limited node has positive density and positive pressure. If the unscaled nodes already lie in Kγ,ε, the maximal parameter is θ∗=1. In particular, if smooth target states stay a distance at least δ>0 from R3∖Kγ,ε 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 Kγ,ε, and the maximal scaling procedure. Prove existence, conservation, nodewise admissibility, and the strict-margin accuracy implication.

[F1]

Maximal convex scaling toward an admissible cell mean: the limiter selects the largest θ∈[0,1] such that Vˉ+θ(Vj−Vˉ)∈K for all nodes.

[F2]

Positive-margin admissible states for ideal-gas Euler: Kγ,ε imposes ρ≥ε and E−m2/(2ρ)≥ε.

Proof

1.1givenF1F3algebra

The feasible parameter set S={θ∈[0,1]:Vˉ+θ(Vj−Vˉ)∈Kγ,ε for every j} contains 0. Each node map is continuous and Kγ,ε is closed by [F3], so each inverse image is closed; the finite intersection S is closed in compact [0,1]. Thus S is nonempty compact and has a maximum θ∗. By its definition, every limited node lies in Kγ,ε.

2.1givenF1F2step 1.1algebra

Using ∑jwj=1 and ∑jwjVj=Vˉ, the limited weighted mean is ∑jwj(Vˉ+θ∗(Vj−Vˉ))=Vˉ+θ∗(Vˉ−Vˉ)=Vˉ. By [F2], each limited node has density at least ε>0 and pressure at least (γ−1)ε>0.

3.1givenF1F3step 2.1algebra∎

If every original Vj∈Kγ,ε, then 1∈S, so θ∗=1. If a target state has distance at least δ from the complement and the candidate differs from it by less than δ, the candidate belongs to Kγ,ε; applying this at every node makes 1 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