Extreme Value Theorem for p(x)=x^3-6x on [-3,2]: axeyum-cas names the interior argmax -sqrt(2) exactly

Identifier: F:cas-extremum-irrational-argmax
Proof route: cas-certificate
External status: proved
Axiom footprint: cas.exact-rational-polynomial-normal-form, cas.sturm-sequence-real-root-isolation-and-counting, cas.completeness-argument-every-real-root-of-p-prime-is-isolated-not-merely-some, cas.extremum-certificate-not-kernel-reconstructed

Recorded description

For the polynomial p(x) = x^3 - 6x on the closed interval [-3, 2], the classical Extreme Value Theorem asserts p attains a global maximum somewhere on the interval. axeyum-cas's extremum::polynomial_extremum route does not merely assert this: it differentiates p exactly (p' = 3x^2 - 6), isolates EVERY real root of p' via Sturm-certified root isolation, filters to the roots strictly inside (-3, 2), and compares p's exact value at those interior critical points against both endpoints -- naming the maximizer exactly. Here the maximizer is the irrational critical point c = -sqrt(2) (minimal polynomial x^2 - 2, degree 2, genuinely irrational: no rational value), with maximum value 4*sqrt(2), bracketed exactly as strictly between 5 and 6 (no floating point). extremum::verify_extremum_certificate then independently re-derives the certificate: it re-isolates p''s roots from scratch and confirms the recomputed interior candidate SET matches the certificate's critical_points in size (catching a dropped candidate, not merely a wrong one -- this is what makes the completeness claim, not just the individual comparison, falsifiable), confirms each candidate's bracket genuinely isolates one root via a fresh Sturm count, and confirms the argmax is self-consistent with the recomputed candidate values. It accepts: Some(true).

Formal statement

(define-poly p (- (^ x 3) (* 6 x)))
(assert (exists ((c Real))
  (and (<= -3 c) (<= c 2)
       (forall ((z Real)) (=> (and (<= -3 z) (<= z 2)) (<= (poly-eval p z) (poly-eval p c)))))))
; the certificate additionally names c = -sqrt(2) exactly (minimal polynomial x^2 - 2)
; as the unique interior argmax, rather than merely asserting existence.

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

cas-internal-extremum-irrational-argmax

Kind: witness-replay
Status: checked

Supports: the EVT certificate (differentiate p, isolate every real root of p' strictly interior to (a,b), compare against both endpoints, name the maximizer c = -sqrt(2) exactly) is independently re-derived and accepted by a checker (verify_extremum_certificate) that shares no code with the search that produced it (polynomial_extremum)

Checker command

cargo test -p axeyum-cas --lib extremum::tests::irrational_argmax -- --exact 2>/dev/null | grep -cE '^test extremum::tests::irrational_argmax \.\.\. ok$'

Evidence notes

THIS EVIDENCE IS cas-internal, NOT kernel-reconstructed (ADR-0601 SS2): the checker_command only ever names the axeyum-cas package (never axeyum-lean-kernel), so scripts/validate-facts.py's classify_cas_certificate_checker classifies this fact's evidence as cas-internal. verify_extremum_certificate is independently re-derived and is itself mutation-tested in the same module (verify_rejects_corrupted_polynomial_coefficient, verify_rejects_corrupted_derivative, verify_rejects_a_swapped_critical_point, verify_rejects_a_corrupted_bracket, verify_rejects_a_dropped_candidate, verify_rejects_a_fabricated_extra_candidate, verify_rejects_a_duplicated_candidate, verify_rejects_wrong_argmax_self_consistency -- 8 dedicated adversarial fixtures), but NO Kernel::add_declaration term exists for this claim and none is claimed here. This is genuinely NOT the same theorem as crates/axeyum-lean-kernel/src/creal/extreme_value.rs (which proves EVT's ATTAINMENT is constructively UNAVAILABLE for an arbitrary uniformly continuous function -- a refutation of the general case) or crates/axeyum-lean-kernel/src/creal/fermat.rs (Fermat's interior-extremum theorem, which takes a maximizer as a HYPOTHESIS rather than producing one): those are row 1/2 kernel-side results about the GENERAL uniformly-continuous case per extremum.rs's own module doc, and this fact is row 3, the decidable POLYNOMIAL fragment. Neither kernel file reconstructs this certificate's specific claim (that THIS polynomial's maximizer on THIS interval is exactly -sqrt(2)), and no bridge between them exists. The test asserts p := x^3-6x (poly_from([0,-6,0,1])), cert := polynomial_extremum(p, -3, 2).unwrap(), verify_extremum_certificate(&cert) == Some(true), cert.argmax == Critical(0), cert.critical_points[0].rational_value() == None (irrational), cert.critical_points[0].degree() == 2, and 5 < cert.max_value < 6 via exact algebraic comparison.

Provenance

{
  "date": "2026-08-27",
  "established_by": "axeyum-cas extremum::polynomial_extremum / extremum::verify_extremum_certificate (crates/axeyum-cas/src/extremum.rs, landed per ADR-0603 row 3)",
  "source": "classical Extreme Value Theorem plus Fermat's interior-extremum theorem (for locating the maximizer among finitely many candidates), specialized to an exact rational polynomial with an irrational argmax; the concrete instance (p = x^3-6x, interval [-3,2]) is the existing unit test extremum::tests::irrational_argmax, read directly from crates/axeyum-cas/src/extremum.rs rather than hand-transcribed.",
  "prior_art": [
    {
      "who": "Weierstrass (extreme value theorem); Fermat (interior-extremum condition)",
      "what": "the extreme value theorem for continuous real functions on a compact interval, combined with the vanishing-derivative necessary condition at an interior extremum",
      "year": 1860,
      "where": "classical analysis; this instance is a routine cubic-polynomial application",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}