{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R554",
  "content_hash": null,
  "slug": "otpc2q-artifact-symbolic-check",
  "type": "artifact",
  "title": "Exact symbolic Peano-kernel check",
  "summary": "SymPy integrates the negative kernel intervals and verifies the radical optimum exactly.",
  "relevance": "For Optimal symmetric three-point quadrature for a bounded second derivative, record otpc2q-artifact-symbolic-check (“Exact symbolic Peano-kernel check”) supplies evidence or a replay used to check the packet. The record states: SymPy integrates the negative kernel intervals and verifies the radical optimum exactly.",
  "relevance_source": "recorded",
  "body": "The replay substitutes \\(a=(1-u^2)/6\\), integrates the two possible negative intervals, differentiates the resulting branches, and checks the minimizing node, sharp constant, and optimal kernel roots with exact arithmetic. Its stable output has SHA-256 digest `e4532299ba7b0a9ad65de1d9c060e8d1f8a8bd81db448521235a9e971da0e692`.",
  "status": "available",
  "evidence_grade": "executable",
  "scope": {
    "kind": "family",
    "statement": "all three Peano-kernel sign regimes, their derivatives, the unique stationary point, and the optimal kernel roots",
    "family": "exact symbolic verification of the one-parameter reduction"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "inline_python_sympy_computation",
    "entrypoint": "join source_lines with newline and run with python3",
    "runtime": "CPython 3.9 or later with SymPy 1.14.0",
    "citation": {
      "url": "https://docs.sympy.org/latest/modules/integrals/integrals.html",
      "locator": "Inline Python and SymPy exact-arithmetic computation executed on 2026-07-24"
    },
    "inline_source": [
      "from hashlib import sha256",
      "import sympy as sp",
      "a,t,u=sp.symbols(\"a t u\")",
      "au=(1-u**2)/6",
      "g=sp.expand(((3*t**2-2*t+2*a)/6).subs(a,au))",
      "S=sp.expand(((-8*a**2+8*a-1)/24).subs(a,au))",
      "rm,rp=(1-u)/3,(1+u)/3",
      "C1=sp.factor(S-4*sp.integrate(g,(t,rm,sp.Rational(1,2))))",
      "C2=sp.factor(S-4*sp.integrate(g,(t,rm,rp)))",
      "assert sp.factor(C1-(1+32*u**3-6*u**4)/648)==0",
      "assert sp.factor(C2-(3-24*u**2+64*u**3-6*u**4)/648)==0",
      "assert sp.factor(sp.diff(C1,u)/sp.diff(au,u)-u*(u-4)/9)==0",
      "assert sp.factor(sp.diff(C2,u)/sp.diff(au,u)-(u**2-8*u+2)/9)==0",
      "us=4-sp.sqrt(14)",
      "astar=sp.simplify(au.subs(u,us))",
      "cstar=sp.expand(C2.subs(u,us))",
      "assert sp.simplify(astar-(8*sp.sqrt(14)-29)/6)==0",
      "assert sp.simplify(cstar-(3355-896*sp.sqrt(14))/648)==0",
      "roots=[sp.simplify(root.subs(u,us)) for root in (rm,rp)]",
      "assert all(sp.simplify(g.subs({u:us,t:root}))==0 for root in roots)",
      "out=\"a_star=(8*sqrt(14)-29)/6\\nC_star=(3355-896*sqrt(14))/648\\nkernel_roots_half=sqrt(14)/3-1,(5-sqrt(14))/3\\n\"",
      "assert sha256(out.encode()).hexdigest()==\"e4532299ba7b0a9ad65de1d9c060e8d1f8a8bd81db448521235a9e971da0e692\"",
      "print(out,end=\"\")"
    ],
    "missing": [
      "command",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://docs.sympy.org/latest/modules/integrals/integrals.html",
    "locator": "Inline Python and SymPy exact-arithmetic computation executed on 2026-07-24"
  },
  "relations": [
    {
      "slug": "R555",
      "title": "The unique optimal node is (8 sqrt(14)-29)/6",
      "object_type": "claim",
      "relation": "evidences",
      "direction": "outgoing"
    },
    {
      "slug": "optimal-three-point-c2-quadrature",
      "title": "optimal three point c2 quadrature",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}