LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Strictification of a viscosity test function by a quartic perturbation

Statement

Let $U \subseteq R^{m}$ be open, let $v : U \to R$ , let $ϕ \in C^{1} (U)$ , suppose $v - ϕ$ has a local maximum at $z_{0} \in U$ , and fix $r > 0$ with $\overline{B} (z_{0}, r) \subseteq U$ and $v (z) - ϕ (z) \leq v (z_{0}) - ϕ (z_{0})$ for every $z \in \overline{B} (z_{0}, r)$ . For $ε > 0$ define $ϕ_{ε} (z) : = ϕ (z) + ε ∣ z - z_{0} ∣^{4} .$ Then $ϕ_{ε} \in C^{1} (U)$ agrees with $ϕ$ to first order at the contact, $ϕ_{ε} (z_{0}) = ϕ (z_{0}), D ϕ_{ε} (z_{0}) = D ϕ (z_{0}),$ and $v - ϕ_{ε}$ has a strict maximum over $\overline{B} (z_{0}, r)$ at $z_{0}$ : $v (z) - ϕ_{ε} (z) < v (z_{0}) - ϕ_{ε} (z_{0}) for every z \in \overline{B} (z_{0}, r) ∖ {z_{0}} .$ The same statement with $ϕ_{ε} : = ϕ - ε ∣ z - z_{0} ∣^{4}$ strictifies a local minimum contact of a test function, and the first jet at the contact is again unchanged. No choice principle is used.

Facts & Assumptions

Given: An open $U \subseteq R^{m}$ , functions $v : U \to R$ and $ϕ \in C^{1} (U)$ , a point $z_{0} \in U$ , a radius $r > 0$ with $\overline{B} (z_{0}, r) \subseteq U$ and $v (z) - ϕ (z) \leq v (z_{0}) - ϕ (z_{0})$ for all $z \in \overline{B} (z_{0}, r)$ , and for $ε > 0$ the function $ϕ_{ε} (z) = ϕ (z) + ε ∣ z - z_{0} ∣^{4}$ .

[F1]

The map $q (z) : = ∣ z - z_{0} ∣^{4}$ is a polynomial in the coordinates of $z$ , hence of class $C^{1}$ on $R^{m}$ , with $q (z_{0}) = 0$ and $D q (z_{0}) = 0$ ; more precisely $D q (z) = 4 ∣ z - z_{0} ∣^{2} (z - z_{0})$ for every $z$ , the derivative being the total derivative in the sense of The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder and its components the partial derivatives of Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ .

[F2]

If $f, g$ are $C^{1}$ on an open set, then so is $f + g$ , with $D (f + g) = D f + D g$ and $(f + g) (z_{0}) = f (z_{0}) + g (z_{0})$ (The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder, Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ).

Proof

technique · an explicit perturbation whose first jet vanishes at the contact

1.1F1F2algebra

Regularity and first jet. The function $q (z) = ∣ z - z_{0} ∣^{4}$ is a polynomial with $q (z_{0}) = 0$ and $D q (z_{0}) = 0$ by [F1]; adding it to the $C^{1}$ function $ϕ$ with coefficient $ε > 0$ gives $ϕ_{ε} \in C^{1} (U)$ with $ϕ_{ε} (z_{0}) = ϕ (z_{0}) + ε q (z_{0}) = ϕ (z_{0})$ and $D ϕ_{ε} (z_{0}) = D ϕ (z_{0}) + ε D q (z_{0}) = D ϕ (z_{0})$ by [F2].

2.1step 1.1algebra

Strict maximum. Let $z \in \overline{B} (z_{0}, r)$ with $z \neq z_{0}$ . Then $∣ z - z_{0} ∣^{4} > 0$ , and the hypothesised maximum inequality gives $v (z) - ϕ (z) \leq v (z_{0}) - ϕ (z_{0})$ ; subtracting the positive quantity $ε ∣ z - z_{0} ∣^{4}$ from the left-hand side and using $ϕ_{ε} = ϕ + ε ∣ \cdot - z_{0} ∣^{4}$ and $ϕ_{ε} (z_{0}) = ϕ (z_{0})$ , we get $v (z) - ϕ_{ε} (z) \leq v (z_{0}) - ϕ (z_{0}) - ε ∣ z - z_{0} ∣^{4} < v (z_{0}) - ϕ (z_{0}) = v (z_{0}) - ϕ_{ε} (z_{0})$ . Hence $z_{0}$ is the strict maximum of $v - ϕ_{ε}$ over $\overline{B} (z_{0}, r)$ .

3.1step 2.1F1F2algebra

Minimum case. If $v - ϕ$ has a local minimum at $z_{0}$ with $v (z) - ϕ (z) \geq v (z_{0}) - ϕ (z_{0})$ on $\overline{B} (z_{0}, r)$ and $ϕ_{ε}^{-} : = ϕ - ε ∣ z - z_{0} ∣^{4}$ , the same two computations with signs reversed give $ϕ_{ε}^{-} (z_{0}) = ϕ (z_{0})$ , $D ϕ_{ε}^{-} (z_{0}) = D ϕ (z_{0})$ and $v (z) - ϕ_{ε}^{-} (z) > v (z_{0}) - ϕ_{ε}^{-} (z_{0})$ for every $z \in \overline{B} (z_{0}, r) ∖ {z_{0}}$ .

4.1step 1.1step 2.1step 3.1∎

Conclusion. Step 1.1 and step 2.1 give the upper-contact statement, and step 3.1 gives the lower-contact statement; the proof used only the polynomial computation [F1] and additivity [F2], so it selects nothing and uses no choice principle.

Remarks

Why the quartic. The perturbation has value $0$ and gradient $0$ at the contact, so it changes neither the value nor the first jet tested in the viscosity inequalities, while it is strictly positive away from the contact and therefore turns a nonstrict contact into a strict one. This is the device that lets the stability and supremum-envelope arguments localise a maximum on a closed ball without losing the tested jet.
Scope. The statement is pointwise in the ball and does not require $v$ to be semicontinuous, bounded or measurable; the compactness and extreme-value suppliers For $n \geq 1$ , every Euclidean closed ball and every Euclidean sphere of positive radius is compact and Semicontinuous extreme value theorem on compact Euclidean sets are available for applications that patch such a ball maximum into a global one, and they are not needed for the computation above.

Depends on

Used by

Dependency tree · two levels

28 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.