ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Subharmonic quartic and harmonic saddle

Example

For $n \geq 2$ , on ${\overline{B}}_{1} (0)$ the function $q (x) = ∣ x ∣^{4}$ is subharmonic and lies below the harmonic function $h \equiv 1$ having the same boundary values. The function $s (x) = x_{1}^{2} - x_{2}^{2}$ is harmonic and has a saddle at the origin, despite $\nabla s (0) = 0$ .

Facts & Assumptions

Given: The objects and hypotheses in the example.

[F1]

Subharmonicity in the classical convention is nonnegativity of the Laplacian. (Subharmonic and superharmonic functions in rn).

[F2]

On bounded nonempty open sets, the classical Laplacian and boundary comparisons imply comparison on the closure. (Comparison principle for classical subharmonic functions).

[F3]

The strong harmonic theorem requires an attained interior global maximum or minimum on a domain. (Strong maximum principle for harmonic functions).

Verification

technique · direct

1.1

Differentiation gives $\partial_{i} q = 4 ∣ x ∣^{2} x_{i}$ and $\partial_{i i} q = 8 x_{i}^{2} + 4 ∣ x ∣^{2}$ , so $Δ q = 4 (n + 2) ∣ x ∣^{2} \geq 0$ . It is subharmonic, with value one on the unit sphere.

F1givenalgebra

2.1

The constant $h = 1$ is harmonic, and $Δ q \geq Δ h$ with equal boundary values. Comparison gives $q \leq h$ on the closed ball, also directly visible from $∣ x ∣ \leq 1$ .

F2step 1.1

3.1

For $s$ , the only nonzero pure second derivatives are $\partial_{11} s = 2$ and $\partial_{22} s = - 2$ , so $Δ s = 0$ and $\nabla s (0) = 0$ . But $s (t e_{1}) = t^{2}$ and $s (t e_{2}) = - t^{2}$ for $0 < ∣ t ∣ < 1$ , proving that zero is neither a local maximum nor a local minimum. There is no interior global extremum to which the strong theorem would apply.

F3algebra∎

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

Hunter, Notes on Partial Differential Equations (standard reference, not scraped)