{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R793",
  "content_hash": null,
  "slug": "tmpc-claim-certified-value",
  "type": "claim",
  "title": "The sharp eigenvalue is certified to ten decimal places",
  "summary": "Exact Taylor bounds place lambda_* in an interval of width 7.189455132656e-10.",
  "relevance": "For The sharp Dirichlet Poincare constant with two moment constraints, record tmpc-claim-certified-value (“The sharp eigenvalue is certified to ten decimal places”) records a bound, answer, status fact, or structural consequence. The record states: Exact Taylor bounds place lambda_* in an interval of width 7.189455132656e-10.",
  "relevance_source": "recorded",
  "body": "Take the rational endpoints\n\\[\nz_-=\\frac{44934094579}{10^{10}},\\qquad\nz_+=\\frac{3510476139}{781250000}.\n\\]\nFor \\(h(z)=\\sin z-z\\cos z\\), Taylor's theorem gives rigorous enclosures by using the sine polynomial through degree 49 with error at most \\(z^{51}/51!\\), and the cosine polynomial through degree 48 with error at most \\(z^{50}/50!\\). Exact rational arithmetic gives\n\\[\nh(z_-)>\\frac3{10^{11}},\\qquad h(z_+)<-\\frac4{10^{11}}.\n\\]\nThe uniqueness proved in the spectral record isolates \\(z_*\\) between these endpoints. Squaring the positive interval and multiplying by four gives\n\\[\n\\frac{2019072855634517187241}{25000000000000000000}\n<\\lambda_*<\n\\frac{12323442722488347321}{152587890625000000}.\n\\]\nIn terminating decimals,\n\\[\n\\boxed{80.76291422538068748964<\\lambda_*<80.76291422609963300291}.\n\\]\nThe exact width is\n\\[\n\\frac{449340945791}{625000000000000000000}\n=0.0000000007189455132656<10^{-8}.\n\\]\nConsequently the best constant \\(C_*=1/\\lambda_*\\) obeys\n\\[\n\\frac{152587890625000000}{12323442722488347321}\n<C_*<\n\\frac{25000000000000000000}{2019072855634517187241},\n\\]\nor approximately \\(0.01238192070682903136<C_*<0.01238192070693925431\\).",
  "status": "established",
  "evidence_grade": "reproduced",
  "scope": {
    "kind": "universal",
    "statement": "the sharp eigenvalue and reciprocal Poincare constant in the stated two-moment problem"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.1112/S0025579314000229",
      "locator": "Exact rational certificate tmpc-artifact-rational-root-certificate, together with tmpc-claim-spectral-reduction"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1112/S0025579314000229",
    "locator": "Exact rational certificate tmpc-artifact-rational-root-certificate, together with tmpc-claim-spectral-reduction"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R794",
      "title": "Parity reduction gives the sharp eigenvalue equation",
      "object_type": "claim",
      "relation": "supports",
      "direction": "incoming"
    },
    {
      "slug": "R791",
      "title": "Exact rational root isolation certificate",
      "object_type": "artifact",
      "relation": "verifies",
      "direction": "incoming"
    },
    {
      "slug": "two-moment-poincare-constant",
      "title": "two moment poincare constant",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}