For p(x)=x^3-6x on [-3,2], the maximum is interior -- kernel-reconstructed, not just CAS-asserted

Identifier: F:cas-evt-endpoint-exclusion-cubic-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, built from the same rat_prelude/int_prelude/nat_prelude constants the IVT sign-bracket bridge (F:cas-ivt-sign-bracket-cbrt2-kernel-checked) enumerates (all measured axiom-free), but ADR-0601 SS2's 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., cas.extremum-certificate-root-differentiation-and-sturm-count-not-claimed-here: this fact states ONLY that x=-1 beats both endpoints. It does not reconstruct p' = 3x^2-6, does not reconstruct that -sqrt(2) is a root of p', and does not reconstruct the Sturm count establishing completeness of critical_points -- all remain cas-internal, checked only by extremum::verify_extremum_certificate (see F:cas-extremum-irrational-argmax's own evidence notes).

Recorded description

For p(x) = x^3 - 6x on [-3, 2] (the same instance F:cas-extremum-irrational-argmax's certificate names, with irrational argmax -sqrt(2) and value 4*sqrt(2)), the interior point x = -1 strictly beats BOTH endpoints: p(-1) = 5 > p(-3) = -9 and p(-1) = 5 > p(2) = -4. So the classical Extreme Value Theorem's maximum on this interval cannot be attained at either endpoint -- reconstructed through crate::Kernel::add_declaration over Rat.polyEval, not merely asserted by axeyum-cas's own normal form. This is deliberately WEAKER than the full ExtremumCertificate: it does not claim x=-1 IS the argmax (it is not; -sqrt(2) is), only that an interior point beats both endpoints, which is exactly the content the classical EVT statement needs at the 'is the maximum interior' step. Root differentiation (p' = 3x^2-6), the irrationality of -sqrt(2) as a critical point, and the Sturm count establishing completeness of critical_points all remain cas-internal, exactly as F:cas-extremum-irrational-argmax's own evidence notes already state.

Formal statement

(define-poly p (- (^ x 3) (* 6 x)))
(assert (> (poly-eval p -1) (poly-eval p -3)))
(assert (> (poly-eval p -1) (poly-eval p 2)))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

kernel-reconstructed-evt-endpoint-exclusion-lower-leg

Kind: kernel-term
Status: checked

Supports: p(-1) > p(-3) for p = x^3-6x, admitted by crate::Kernel::add_declaration as Check.evt_endpoint_exclusion_lower_leg : Rat.lt Rat.zero (Rat.polyEval q 4 (Rat.ofInt -1)), where q = p - p(-3) (coefficients [9,-6,0,1]) built from the same [0,-6,0,1] integer coefficients the CAS's own extremum::polynomial_extremum(x^3-6x, -3, 2) certificate returns, from a Nat.le 1 14 witness -- 14 being the EXACT value the fully reduced polynomial computes to

Checker command

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

Evidence notes

MUTATION-VERIFIED by this lane before registering: changing ONLY the kernel-side bound for this leg from the exact 14 to a wrong-but-plausible 16 (Nat.le 1 16 is itself a true proposition, just not the one the reduced term inhabits) made Kernel::add_declaration reject with TypeMismatch { expected: ExprId(1579401), got: ExprId(1579415) } and the test FAIL; reverted, it passes again. So the kernel term asserts what the CAS-derived arithmetic actually computed (p(-1)-p(-3) = 14), not merely something well-typed. The mutation and revert were both made and confirmed inside this lane's own worktree; git status was confirmed clean afterward.

kernel-reconstructed-evt-endpoint-exclusion-upper-leg

Kind: kernel-term
Status: checked

Supports: p(-1) > p(2) for p = x^3-6x, admitted by crate::Kernel::add_declaration as Check.evt_endpoint_exclusion_upper_leg : Rat.lt Rat.zero (Rat.polyEval r 4 (Rat.ofInt -1)), where r = p - p(2) (coefficients [4,-6,0,1]), from a Nat.le 1 9 witness -- 9 being the EXACT value the fully reduced polynomial computes to. Also carries the swapped-statement negative control: the SAME proof term for the lower leg, re-ascribed against the FALSE statement q(-1) < 0, is confirmed REJECTED by Kernel::add_declaration -- exercising the kernel's own type check rather than asking any decision procedure to accept a falsehood.

Checker command

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

Evidence notes

Same single #[test] fn as the lower-leg row (both legs plus the negative control are asserted in one test, so the checker_command is identical -- a separate evidence row because it supports a distinct half of the statement plus the non-vacuity control, not a distinct command). Unlike F:cas-ivt-degree4-sign-bracket-kernel-checked-cost-curve (which its own notes flag as lacking a negative control), this test DOES carry one: q(-1) < 0 is false (q(-1)=14>0), and the true proof of 0<q(-1) is confirmed rejected when ascribed against it.

Provenance

{
  "date": "2026-08-28",
  "established_by": "rat_prelude::cas_evt_bridge_tests::tests::evt_endpoint_exclusion_kernel_checked (crates/axeyum-lean-kernel/src/rat_prelude/cas_evt_bridge_tests.rs), authored by the evt-endpoint lane, sized by docs/research/11-design-review/2026-08-28-ivt-evt-pareto-position-measured.md and docs/plan/status/223-cas-reconstruct.md's 'next lane' item 1 as needing no new kernel machinery beyond what the IVT sign-bracket bridge already built and kernel-checked",
  "source": "classical Extreme Value Theorem (attainment) combined with Fermat's interior-extremum condition (the maximizer, if not at an endpoint, must be a critical point), specialized to the concrete cubic p=x^3-6x on [-3,2] -- the same instance F:cas-extremum-irrational-argmax's certificate names (extremum::tests::irrational_argmax)",
  "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"
    }
  ]
}