The sign bracket of x^3-2 on (1,2) is kernel-reconstructed, not just CAS-internal

Identifier: F:cas-ivt-sign-bracket-cbrt2-kernel-checked
Proof route: cas-certificate
External status: proved
Axiom footprint: cas.route-label-reserves-axiom-free-tally-to-kernel-lean: this fact's OWN evidence is a kernel-reconstructed Kernel::add_declaration acceptance over Rat.polyEval whose proof consults no Axiom/Opaque/Quotient declaration (every constant it calls -- Rat.pow_zero/pow_succ, Rat.ofInt_add/ofInt_mul, Nat.le.refl/le.step, Int.lt's own definitional negSucc/ofNat case, True.intro -- traces to rat_prelude/int_prelude/nat_prelude, all measured axiom-free by rat_prelude_is_axiom_free), but ADR-0601 SS2's classify_cas_certificate_fact / AXIOM_FREE_CAPABLE reserves the headline axiom-free TALLY to proof_route kernel-lean alone, so an empty array here would be read by scripts/validate-facts.py as a claim this route cannot support even though the underlying kernel derivation genuinely has no axioms., cas.ivt-certificate-root-containment-and-sturm-count-not-claimed-here: this fact states ONLY the sign bracket (item 1 of the three-part IvtCertificate in F:cas-ivt-cbrt2-in-1-2's notes) -- root containment (item 2, exact division of p by cert.root's minimal polynomial) and the Sturm uniqueness count (item 3) are NOT reconstructed by this fact's evidence and remain cas-internal, checked only by real_algebraic::verify_ivt_certificate.

Recorded description

For p(x) = x^3 - 2: p(1) < 0 and 0 < p(2), reconstructed through crate::Kernel::add_declaration over Rat.polyEval rather than trusted from axeyum-cas's own normal form. This is a SIBLING fact to F:cas-ivt-cbrt2-in-1-2, not a replacement for it -- it deliberately claims LESS than that fact's full IvtCertificate: it says nothing about the named root cbrt(2), nothing about that root's minimal polynomial dividing p by exact division, and nothing about the Sturm count establishing p has EXACTLY ONE real root in (1,2). Those three remain cas-internal, checked only by axeyum-cas's own verify_ivt_certificate (see F:cas-ivt-cbrt2-in-1-2's own evidence and notes) -- reconstructing the root-containment division and the Sturm sign-variation count through this kernel is future work, sized in this fact's notes. What IS newly true here: the exact sign bracket that IVT's classical hypothesis needs is no longer merely CAS-internal -- an independent, axiom-free kernel proof exists for it, over the SAME certificate (same p, same bracket (1,2)) F:cas-ivt-cbrt2-in-1-2 names.

Formal statement

(define-poly p (- (^ x 3) 2))
(assert (< (poly-eval p 1) 0))
(assert (> (poly-eval p 2) 0))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

kernel-reconstructed-ivt-sign-bracket-cbrt2-lower

Kind: kernel-term
Status: checked

Supports: p(1) < 0 for p = x^3-2, admitted by crate::Kernel::add_declaration over a Rat.polyEval-stated theorem built from a translated axeyum-cas IvtCertificate; paired with a negative control (the same proof term rejected against the swapped-sign statement 0 < p(1))

Checker command

cargo test -p axeyum-lean-kernel --lib rat_prelude::cas_ivt_bridge_tests::tests::ivt_sign_bracket_cbrt2_kernel_checked -- --exact 2>/dev/null | grep -cE '^test rat_prelude::cas_ivt_bridge_tests::tests::ivt_sign_bracket_cbrt2_kernel_checked \.\.\. ok$'

Evidence notes

The named test builds BOTH sign-bracket halves (Check.ivt_sign_bracket_cbrt2_lower : Rat.lt (Rat.polyEval c 4 (Rat.ofInt 1)) Rat.zero, and Check.ivt_sign_bracket_cbrt2_upper : Rat.lt Rat.zero (Rat.polyEval c 4 (Rat.ofInt 2))) plus the paired negative control (Check.ivt_sign_bracket_cbrt2_wrong: the p(1)<0 proof term ascribed against 0<p(1), asserted REJECTED via admitted_wrong.is_err()). c is built by n_term_polynomial from the SAME [-2,0,0,1] integer coefficients axeyum-cas's real_algebraic::polynomial_ivt(x^3-2, 1, 2) actually returns (translated by sign_bracket_to_int, asserted equal in the test) -- not hand-picked. Mutation-tested in an isolated snapshot (scripts/lane-snapshot.sh): (1) corrupting the CAS input polynomial to x^3+2 makes polynomial_ivt itself decline (no sign change on (1,2)), failing the test at the .expect(); (2) corrupting ONLY the kernel-side Nat.le bound the upper-bracket proof is built against (6 -> 8, a wrong-but-plausible 'safe slack' value) makes Kernel::add_declaration reject with TypeMismatch, failing the test -- confirming the KERNEL check itself, not merely the CAS input, is load-bearing. An unmutated control run in the same snapshot passed both times. Measured wall-clock (this machine, cold `cargo-serialized.sh test`, single invocation via --exact): ~8.4s including the one-time Rat prelude build (~5.3s of that, measured separately via rat_prelude::rat_prelude_tests::rat_prelude_is_axiom_free run alone) -- so the bridge construction itself costs roughly 3s at this degree-3 instance. See F:cas-ivt-degree4-sign-bracket-kernel-checked-cost-curve in this fact's sibling test (ivt_sign_bracket_degree_four_kernel_checked, same file) for the one-degree-higher data point (~4.1s bridge cost, ~9.4s total).

kernel-reconstructed-ivt-sign-bracket-cbrt2-upper

Kind: kernel-term
Status: checked

Supports: 0 < p(2) for p = x^3-2, admitted by crate::Kernel::add_declaration over a Rat.polyEval-stated theorem; the companion half of the same certificate's sign bracket

Checker command

cargo test -p axeyum-lean-kernel --lib rat_prelude::cas_ivt_bridge_tests::tests::ivt_sign_bracket_cbrt2_kernel_checked -- --exact 2>/dev/null | grep -cE '^test rat_prelude::cas_ivt_bridge_tests::tests::ivt_sign_bracket_cbrt2_kernel_checked \.\.\. ok$'

Evidence notes

Same single test as the lower-bracket row (both halves are asserted in one #[test] fn, so the checker_command is identical -- this is a separate evidence row because it supports a distinct half of the statement, not a distinct command). Rat.lt (ofInt m) Rat.zero and Rat.lt Rat.zero (ofInt n) are NOT symmetric to reconstruct: the negative half reduces (Int.lt's own negSucc/ofNat definitional case) to True unconditionally, while the positive half reduces to a genuine Nat.le obligation that must be supplied -- see the module's own doc comment (crates/axeyum-lean-kernel/src/rat_prelude/cas_ivt_bridge_tests.rs, `zero_lt_via_nat_le` and `lt_zero_via_true`) for why these needed two different closing lemmas rather than one shared one.

Provenance

{
  "date": "2026-08-27",
  "established_by": "rat_prelude::cas_ivt_bridge_tests (crates/axeyum-lean-kernel/src/rat_prelude/cas_ivt_bridge_tests.rs), bridge-ivt lane, per this session's ADR-0601 SS2 kernel-reconstructed-row task",
  "source": "classical intermediate value theorem's sign-change hypothesis, specialized to p(x)=x^3-2 on (1,2) -- the exact instance F:cas-ivt-cbrt2-in-1-2 already names, reconstructed one level deeper (through Kernel::add_declaration rather than axeyum-cas's own verify_ivt_certificate alone)",
  "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"
    }
  ]
}