x^3-2 has exactly one real root in (1,2), named exactly by the CAS's IVT certificate

Identifier: F:cas-ivt-cbrt2-in-1-2
Proof route: cas-certificate
External status: proved
Axiom footprint: cas.exact-rational-polynomial-normal-form, cas.sturm-sequence-real-root-isolation-and-counting, cas.ivt-certificate-not-kernel-reconstructed

Recorded description

The polynomial p(x) = x^3 - 2 satisfies p(1) < 0 and p(2) > 0, so by the intermediate value theorem it has a real root in the open interval (1,2); that root (cbrt(2) ~ 1.26) is genuinely the ONLY real root of p in (1,2), and axeyum-cas's real_algebraic::polynomial_ivt route names it EXACTLY -- as a minimal polynomial (x^3-2 itself, degree 3, hence irreducible over Q by the rational root theorem) plus a Sturm-isolated bracket contained in (1,2) -- rather than approximating it numerically. real_algebraic::verify_ivt_certificate then independently RE-DERIVES every check the certificate asserts (recomputes the sign bracket from p/1/2, confirms the root's minimal polynomial genuinely divides p by exact division, confirms the isolating interval sits inside (1,2), and RE-COUNTS the Sturm sequence's real-root count on that interval rather than trusting the certificate's own bookkeeping) and accepts it: Some(true).

Formal statement

(define-poly p (- (^ x 3) 2))
(assert (< (poly-eval p 1) 0))
(assert (> (poly-eval p 2) 0))
(assert (exists ((r Real))
  (and (< 1 r) (< r 2) (= (poly-eval p r) 0)
       (forall ((s Real))
         (=> (and (< 1 s) (< s 2) (= (poly-eval p s) 0))
             (= s r))))))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

cas-internal-ivt-cbrt2-in-1-2

Kind: witness-replay
Status: checked

Supports: the IVT certificate (sign bracket, minimal polynomial, isolating interval) is independently re-derived and accepted by a checker (verify_ivt_certificate) that shares no code with the search that produced it (polynomial_ivt)

Checker command

cargo test -p axeyum-cas --lib real_algebraic::tests::ivt_names_the_root_of_a_cubic -- --exact 2>/dev/null | grep -cE '^test real_algebraic::tests::ivt_names_the_root_of_a_cubic \.\.\. 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 -- verified by the CAS's own verify_ivt_certificate (which is independently re-derived from poly/a/b/root alone, and IS mutation-tested -- see verify_rejects_corrupted_interval_endpoint / verify_rejects_corrupted_polynomial_coefficient / verify_rejects_corrupted_bracket_bounds in the same test module), but NOT YET reconstructed through Kernel::add_declaration. The ledger must not let this read as kernel-checked: no Lean/kernel term exists for this claim, and 'checked' in this evidence row's check_status means 'independently re-derived by a second CAS routine', not 'admitted by the trusted kernel gate'. The test asserts p := x^3-2 (poly_from([-2,0,0,1])), cert := polynomial_ivt(p, 1, 2).unwrap(), verify_ivt_certificate(&cert) == Some(true), and cert.root.degree() == 3 (confirming the named root is genuinely irrational -- an irreducible cubic, not a value the rational-root theorem would have found). This is the first cas-certificate fact registered against the kernel-reconstructed/cas-internal split introduced in this validator batch, and it is deliberately chosen to demonstrate the split doing its job: an honest, checked-but-not-kernel-reconstructed result, labeled as such rather than folded into the same 'checked' bucket as a kernel-lean fact.

Provenance

{
  "date": "2026-08-27",
  "established_by": "axeyum-cas real_algebraic::polynomial_ivt / verify_ivt_certificate (crates/axeyum-cas/src/real_algebraic.rs, landed same day per ADR-0601)",
  "source": "classical intermediate value theorem, specialized to an exact rational polynomial with a Sturm-isolated real root; the concrete instance (p = x^3-2, bracket (1,2)) is the existing unit test real_algebraic::tests::ivt_names_the_root_of_a_cubic, read directly from crates/axeyum-cas/src/real_algebraic.rs rather than hand-transcribed.",
  "prior_art": [
    {
      "who": "Bolzano; Cauchy",
      "what": "the intermediate value theorem for continuous real functions",
      "year": 1817,
      "where": "classical analysis; this instance is a routine polynomial application",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}