For p(x)=x^3 on [0,3], the secant endpoints p(3)=27 and p(0)=0 are kernel-reconstructed, not just CAS-asserted

Identifier: F:cas-mvt-secant-endpoints-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/EVT sign-bracket bridges enumerate (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.mvt-certificate-slope-arithmetic-rolle-and-witness-not-claimed-here: this fact states ONLY the two endpoint evaluations p(3)=27 and p(0)=0. It does not reconstruct the division (27-0)/(3-0)=9 that produces the slope, does not reconstruct the Rolle reduction g/g', and does not reconstruct the witness c=sqrt(3) or its Sturm-isolated bracket -- all remain cas-internal, checked only by mvt::verify_mvt_certificate (see F:cas-mvt-cubic-witness-sqrt3's own evidence notes).

Recorded description

For p(x) = x^3 on [0, 3] (the same instance F:cas-mvt-cubic-witness-sqrt3's certificate names, secant slope 9, irrational witness c = sqrt(3)), the two endpoint evaluations p(3) = 27 and p(0) = 0 -- the values axeyum-cas's own MvtCertificate.slope field is computed FROM -- are 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 MvtCertificate: it does not compute the slope (27-0)/(3-0)=9 itself (no Rat division is reconstructed here), it says nothing about Rolle's theorem, the Rolle reduction g(x)=p(x)-p(0)-9x, or the witness c=sqrt(3) and its Sturm-isolated bracket. All of that remains cas-internal, exactly as F:cas-mvt-cubic-witness-sqrt3's own evidence notes already state.

Formal statement

(define-poly p (^ x 3))
(assert (= (poly-eval p 3) 27))
(assert (= (poly-eval p 0) 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-mvt-secant-p-at-b

Kind: kernel-term
Status: checked

Supports: p(3) = 27 for p = x^3, admitted by crate::Kernel::add_declaration as Check.mvt_secant_p_at_b : Eq Rat (Rat.polyEval c 4 (Rat.ofInt 3)) (Rat.ofInt <the arithmetic chain the CAS-derived coefficients reduce to at x=3>), where c is built from the same [0,0,0,1] integer coefficients axeyum-cas's own mvt::polynomial_mvt(x^3, 0, 3) certificate's cert.poly field actually returns (asserted equal in the test, not hand-picked). Unlike the IVT/EVT sign-bracket siblings (which state an inequality and let the numeral live only inside the proof's Nat.le witness), this is an EQUALITY reconstruction: the ascribed type's right-hand side IS the same Rat.ofInt(chain) expression poly_eval_to_of_int's own returned proof already has as its inferred type, so there is no separate def_eq-only ascription step -- the value argument is literally that returned proof, unmodified.

Checker command

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

Evidence notes

The named test builds both endpoint equalities (Check.mvt_secant_p_at_b and Check.mvt_secant_p_at_a) plus a swapped-value negative control in one #[test] fn, so this evidence row and the next one share one checker_command -- separate rows because they support distinct halves of the statement, not distinct commands. cert.poly/a/b are asserted equal to [0,0,0,1]/0/3 BEFORE any kernel-side term is built, and cert.slope is separately asserted equal to 9 as a sanity check on the CAS side (not itself kernel-reconstructed -- see axiom_footprint). Measured wall-clock (this machine, cold cargo-serialized.sh test, single invocation): 6.53s including the one-time Rat prelude build, comparable to the sibling IVT/EVT/extremum bridges.

kernel-reconstructed-mvt-secant-p-at-a

Kind: kernel-term
Status: checked

Supports: p(0) = 0 for p = x^3, admitted by crate::Kernel::add_declaration as Check.mvt_secant_p_at_a : Eq Rat (Rat.polyEval c 4 (Rat.ofInt 0)) (Rat.ofInt <chain>). Also carries the swapped-value negative control: the SAME proof term for p(3)=27, re-ascribed against the FALSE statement p(3)=28, 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_mvt_secant_bridge_tests::tests::mvt_secant_endpoints_kernel_checked -- --exact 2>/dev/null | grep -cE '^test rat_prelude::cas_mvt_secant_bridge_tests::tests::mvt_secant_endpoints_kernel_checked \.\.\. ok$'

Evidence notes

Same single #[test] fn as the p(3) row (both endpoints plus the negative control are asserted together, so the checker_command is identical). Unlike the IVT sign-bracket bridge's negative and positive halves (which need two DIFFERENT closing lemmas, lt_zero_via_true vs zero_lt_via_nat_le, because Rat.lt's two directions reduce differently), both equality rows here use the identical poly_eval_to_of_int engine -- Eq is symmetric in a way Lt is not, so no analogous asymmetry arises.

Provenance

{
  "date": "2026-08-29",
  "established_by": "rat_prelude::cas_mvt_secant_bridge_tests::tests::mvt_secant_endpoints_kernel_checked (crates/axeyum-lean-kernel/src/rat_prelude/cas_mvt_secant_bridge_tests.rs), sized by docs/research/11-design-review/2026-08-28-ivt-evt-pareto-position-measured.md's 'Row 3, followed up' section, which named 28-of-32 cas-certificate facts as the number to move and identified the real-algebraic cluster (which the MVT fact belongs to) as reachable without new kernel machinery for its rational sub-claims",
  "source": "classical Mean Value Theorem via Rolle's theorem, specialized to the concrete cubic p=x^3 on [0,3] -- the same instance F:cas-mvt-cubic-witness-sqrt3's certificate names (mvt::tests::cubic_irrational_witness_x_cubed_on_0_3)",
  "prior_art": [
    {
      "who": "Rolle; Lagrange; Cauchy",
      "what": "Rolle's theorem and its generalization to the Mean Value Theorem for differentiable real functions",
      "year": 1823,
      "where": "classical analysis; this instance is a routine cubic-polynomial application",
      "attribution": "standard textbook attribution; this lane did not consult the primary source"
    }
  ]
}