ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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 constraints on a sphere-plane circle, where one multiplier solution is only a local maximum

Example

Let $G (x, y, z) = (x^{2} + y^{2} + z^{2}, z)$ , let $c = (2, 1)$ , and let $M = G^{- 1} (c)$ , the unit circle in the plane $z = 1$ . The derivative $D G$ is surjective at every point of $M$ , so the two-constraint multiplier rule applies there, and its equation $\nabla f = D G^{T} λ$ for the objective $f (x, y, z) = x y + x z + y z$ has exactly four solutions on $M$ : $P_{1} = (\frac{1}{\sqrt{2}}, \frac{1}{\sqrt{2}}, 1), P_{2} = (0, - 1, 1), P_{3} = (- 1, 0, 1), P_{4} = (- \frac{1}{\sqrt{2}}, - \frac{1}{\sqrt{2}}, 1) .$

On $M$ the objective has maximum $\frac{1}{2} + \sqrt{2}$ , attained only at $P_{1}$ , and minimum $- 1$ , attained exactly at $P_{2}$ and $P_{3}$ . The fourth solution has $f (P_{4}) = \frac{1}{2} - \sqrt{2}$ , which is neither of those values, and it is nevertheless a strict local maximum of $f$ on $M$ : $f (p) < f (P_{4})$ for every $p \in M$ with $0 < ∥ p - P_{4} ∥_{2} < \sqrt{2 - \sqrt{2}}$ .

So the multiplier equation does not, by itself, separate a global extremum from a merely local one. Every one of its solutions here is a local extremum of $f$ on $M$ , and three of the four are global; deciding which is which took a separate argument.

Facts & Assumptions

Given: The maps $f (x, y, z) = x y + x z + y z$ and $G (x, y, z) = (x^{2} + y^{2} + z^{2}, z)$ on $R^{3}$ , the value $c = (2, 1)$ , and $M = G^{- 1} (c)$ . Extrema on $M$ are constrained extrema, comparing $f$ only at points of $M$ : a point $a \in M$ is a local extremum of $f$ on $M$ when for some $r > 0$ either $f (p) \leq f (a)$ for every $p \in M$ with $∥ p - a ∥_{2} < r$ , or $f (p) \geq f (a)$ for every such $p$ ; it is a strict local maximum of $f$ on $M$ when for some $r > 0$ , $f (p) < f (a)$ for every $p \in M$ with $0 < ∥ p - a ∥_{2} < r$ . This is the sense of "local maximum or minimum of $f$ subject to $G (x) = c$ " in [L3]; [L4] is the unconstrained notion, comparing $f$ at every nearby point of the open set on which it is defined.

[L1]

A polynomial in one real variable is differentiable with the derivative computed by the power, sum and product rules, so each partial derivative of $f$ and of the components of $G$ is again a polynomial and hence continuous; a map whose partial derivatives exist near a point and are continuous there is totally differentiable there, with derivative the Jacobian matrix (For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative, The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case).

[L2]

A $C^{1}$ map is a submersion at a point when its derivative there is surjective, and a matrix has rank at least $r$ exactly when some $r$ -rowed minor is nonzero (Submersions and immersions between Euclidean open sets, A matrix has rank at least $r$ exactly when it has a nonzero $r$ -rowed minor).

[L3]

If $a$ is a local maximum or minimum of a $C^{1}$ objective $f$ subject to $G (x) = c$ with $G$ of class $C^{1}$ , and $D G (a)$ is surjective, then there is a unique $λ$ with $\nabla f (a) = D G (a)^{T} λ$ ; the condition is necessary and not sufficient (Lagrange multipliers for a regular vector-valued level-set constraint).

[L4]

For $U \subseteq R^{m}$ open, $a \in U$ and $f : U \to R$ , the point $a$ is a local minimum when some Euclidean neighbourhood $V$ of $a$ satisfies $f (a) \leq f (x)$ for every $x \in U \cap V$ , and a strict local minimum when the inequality is strict for $x \neq a$ ; local and strict local maxima reverse these inequalities (Local and strict local extrema for scalar fields on Euclidean open sets). The Euclidean norm is $∥ x ∥_{2} = (\sum_{k < n} ∣ x_{k} ∣^{2})^{1 / 2}$ (The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ ).

Verification

technique · direct

1.1

By [L1], $f$ and $G$ are $C^{1}$ , with $\nabla f (x, y, z) = (y + z, x + z, x + y)$ and with the two rows of $J G (x, y, z)$ equal to $(2 x, 2 y, 2 z)$ and $(0, 0, 1)$ .

givenL1

1.2

A point lies in $M$ exactly when $z = 1$ and $x^{2} + y^{2} = 1$ . Writing $s = x + y$ on $M$ gives $s^{2} = x^{2} + y^{2} + 2 x y = 1 + 2 x y$ , so $x y = (s^{2} - 1) / 2$ and $f = x y + z (x + y) = (s^{2} + 2 s - 1) / 2$ ; moreover $2 x y \leq x^{2} + y^{2} = 1$ because $(x - y)^{2} \geq 0$ , so $s^{2} \leq 2$ and $- \sqrt{2} \leq s \leq \sqrt{2}$ .

givenalgebra

1.3

For $p = (x, y, 1) \in M$ and $P_{4} = (- \frac{1}{\sqrt{2}}, - \frac{1}{\sqrt{2}}, 1)$ , expanding gives $∥ p - P_{4} ∥_{2}^{2} = (x + \frac{1}{\sqrt{2}})^{2} + (y + \frac{1}{\sqrt{2}})^{2} = (x^{2} + y^{2}) + \sqrt{2} (x + y) + 1 = 2 + \sqrt{2} s$ . So on $M$ the distance to $P_{4}$ determines $s$ and increases with it.

givenL4algebra

2.1

At a point of $M$ the two-rowed minor of $J G$ from columns $1, 3$ is $2 x$ and the minor from columns $2, 3$ is $2 y$ , and $x^{2} + y^{2} = 1$ forces $(x, y) \neq (0, 0)$ , so one of them is nonzero and $J G$ has rank $2$ . By [L2], $D G$ is surjective at every point of $M$ .

step 1.1step 1.2L2algebra

2.2

By step 1.2, on $M$ the value of $f$ at a point with $x + y = s$ is $(s^{2} + 2 s - 1) / 2$ , and $\frac{s^{2} + 2 s - 1}{2} - (- 1) = \frac{(s + 1)^{2}}{2} \geq 0$ with equality exactly when $s = - 1$ , while $\frac{(\sqrt{2})^{2} + 2 \sqrt{2} - 1}{2} - \frac{s^{2} + 2 s - 1}{2} = \frac{(\sqrt{2} - s) (\sqrt{2} + s + 2)}{2} \geq 0$ for $- \sqrt{2} \leq s \leq \sqrt{2}$ , with equality exactly when $s = \sqrt{2}$ . Hence $f \geq - 1$ on $M$ , with equality exactly at the points where $s = - 1$ , and $f \leq \frac{1}{2} + \sqrt{2}$ on $M$ , with equality exactly at the points where $s = \sqrt{2}$ .

step 1.2algebra

2.3

By step 1.2 and step 1.3, a point of $M$ with $0 < ∥ p - P_{4} ∥_{2} < \sqrt{2 - \sqrt{2}}$ has $0 < 2 + \sqrt{2} s < 2 - \sqrt{2}$ , that is $- \sqrt{2} < s < - 1$ ; and $\frac{s^{2} + 2 s - 1}{2} - \frac{(- \sqrt{2})^{2} + 2 (- \sqrt{2}) - 1}{2} = \frac{(s + \sqrt{2}) (s + 2 - \sqrt{2})}{2} < 0$ there, because $s + \sqrt{2} > 0$ while $s + 2 - \sqrt{2} < 1 - \sqrt{2} < 0$ .

step 1.2step 1.3algebra

3.1

On $M$ , $s = \sqrt{2}$ forces $2 x y = s^{2} - 1 = 1 = x^{2} + y^{2}$ , hence $(x - y)^{2} = 0$ and $x = y = \frac{1}{\sqrt{2}}$ ; and $s = - 1$ forces $2 x y = s^{2} - 1 = 0$ , hence ${x, y} = {0, - 1}$ . Both loci are therefore nonempty, so by step 2.2 the bounds are attained: the maximum of $f$ on $M$ is $\frac{1}{2} + \sqrt{2}$ , only at $P_{1} = (\frac{1}{\sqrt{2}}, \frac{1}{\sqrt{2}}, 1)$ , and the minimum is $- 1$ , exactly at $P_{2} = (0, - 1, 1)$ and $P_{3} = (- 1, 0, 1)$ .

step 1.2step 2.2algebra

3.2

By step 2.1 and [L3], every local extremum of $f$ on $M$ satisfies $\nabla f = D G^{T} λ$ for a unique $λ = (λ_{1}, λ_{2})$ ; by step 1.1 this reads $y + 1 = 2 λ_{1} x$ , $x + 1 = 2 λ_{1} y$ and $x + y = 2 λ_{1} + λ_{2}$ , the last of which only determines $λ_{2}$ . Subtracting the second equation from the first gives $(y - x) (1 + 2 λ_{1}) = 0$ .

givenstep 1.1step 2.1L3algebra

3.3

By step 1.2 and step 2.3, $f (P_{4}) = \frac{(- \sqrt{2})^{2} + 2 (- \sqrt{2}) - 1}{2} = \frac{1}{2} - \sqrt{2}$ , and $f (p) < f (P_{4})$ for every $p \in M$ with $0 < ∥ p - P_{4} ∥_{2} < \sqrt{2 - \sqrt{2}}$ . So $P_{4}$ is a strict local maximum of $f$ on $M$ , with $r = \sqrt{2 - \sqrt{2}}$ .

givenstep 1.2step 2.3L4algebra

4.1

If $y = x$ , then $x^{2} + y^{2} = 1$ gives $x = y = \pm \frac{1}{\sqrt{2}}$ and $s = \pm \sqrt{2}$ , so the point is $P_{1}$ or $P_{4}$ , and both satisfy the equations of step 3.2 with $λ_{1} = (x + 1) / (2 x)$ , which is defined because $x \neq 0$ . If instead $λ_{1} = - \frac{1}{2}$ , the first equation gives $x + y = - 1$ , so $s = - 1$ , and by step 3.1 the points are $P_{2}$ and $P_{3}$ , which satisfy all three equations with $λ_{1} = - \frac{1}{2}$ . The two cases cannot both hold, since $x = y$ and $x + y = - 1$ give $x^{2} + y^{2} = \frac{1}{2} \neq 1$ . So $P_{1}, P_{2}, P_{3}, P_{4}$ are exactly the solutions of the multiplier equation on $M$ .

step 1.2step 3.1step 3.2algebra

5.1

By step 3.1 the maximum and the minimum of $f$ on $M$ are attained at $P_{1}$ , $P_{2}$ and $P_{3}$ , each of which is among the four solutions of step 4.1, as [L3] requires. By step 3.3 the remaining solution $P_{4}$ is a strict local maximum whose value $\frac{1}{2} - \sqrt{2}$ is neither the maximum nor the minimum, because $- 1 < \frac{1}{2} - \sqrt{2} < \frac{1}{2} + \sqrt{2}$ follows from $1 < \sqrt{2} < \frac{3}{2}$ . So the multiplier equation is satisfied at a point that is a local but not a global extremum, and satisfying it does not decide which.

step 3.1step 3.3step 4.1L3algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

64 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

University of Toronto MAT237 notes, Section 2.8, Example 5 (standard reference, not scraped)