{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R1825",
  "content_hash": null,
  "slug": "tmpc-formalization-rational-certificate-lean-v1",
  "type": "formalization",
  "title": "Lean target for the exact rational root certificate",
  "summary": "The approved theorem checks both rational Taylor endpoint inequalities, the two squared endpoints, the exact interval width, and the required 10^-8 bound.",
  "relevance": "This gives agents an exact, reviewed Lean target for the packet's reproducible numerical certificate without presenting the analytical spectral reduction as formally verified.",
  "relevance_source": "recorded",
  "body": "This target covers the complete exact-rational computation in the certificate. It deliberately leaves the Sobolev compactness, parity reduction, min-max argument, ODE classification, Taylor remainder theorem, and root uniqueness in the analytical record outside this Lean claim. A short `norm_num` proof closes the finite rational proposition in the pinned world.",
  "status": "pending_verification",
  "evidence_grade": "unverified_formalization",
  "scope": {
    "kind": "bounded",
    "statement": "the exact rational Taylor-bound computations, induced lambda endpoints, and interval width in tmpc-artifact-rational-root-certificate",
    "bounds": {
      "root_endpoints": {
        "min": 2,
        "max": 2
      },
      "sin_taylor_degree": {
        "min": 49,
        "max": 49
      },
      "cos_taylor_degree": {
        "min": 48,
        "max": 48
      }
    },
    "exhaustive": true
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "partial",
    "kind": "formalization",
    "runtime": "lean-4.33.0-rc1/mathlib4@4608056c77c52468b80773e8dcd585ef821c7c5e+theoremdb@24c58f96c6cba9e5150e04319a134c65cd13a0b2b4615f54dc2959b54ec2765d",
    "citation": {
      "url": "https://doi.org/10.1112/S0025579314000229",
      "locator": "formalization-target:tmpc-artifact-rational-root-certificate"
    },
    "missing": [
      "source",
      "command",
      "expected_output"
    ]
  },
  "formal_statement": "theorem TheoremDB.TwoMomentPoincare.exactRationalCertificate : ∀ (zLo zHi : ℚ), zLo = 449340945790 / 10 ^ 11 → zHi = 449340945792 / 10 ^ 11 → 3 / 10 ^ 11 < ((∑ j ∈ Finset.range 25, (-1 : ℚ) ^ j * zLo ^ (2 * j + 1) / (Nat.factorial (2 * j + 1) : ℚ)) - zLo ^ 51 / (Nat.factorial 51 : ℚ)) - zLo * ((∑ j ∈ Finset.range 25, (-1 : ℚ) ^ j * zLo ^ (2 * j) / (Nat.factorial (2 * j) : ℚ)) + zLo ^ 50 / (Nat.factorial 50 : ℚ)) ∧ ((∑ j ∈ Finset.range 25, (-1 : ℚ) ^ j * zHi ^ (2 * j + 1) / (Nat.factorial (2 * j + 1) : ℚ)) + zHi ^ 51 / (Nat.factorial 51 : ℚ)) - zHi * ((∑ j ∈ Finset.range 25, (-1 : ℚ) ^ j * zHi ^ (2 * j) / (Nat.factorial (2 * j) : ℚ)) - zHi ^ 50 / (Nat.factorial 50 : ℚ)) < -(4 / 10 ^ 11) ∧ 4 * zLo ^ 2 = 2019072855634517187241 / 25000000000000000000 ∧ 4 * zHi ^ 2 = 12323442722488347321 / 152587890625000000 ∧ 4 * zHi ^ 2 - 4 * zLo ^ 2 = 449340945791 / 625000000000000000000 ∧ 4 * zHi ^ 2 - 4 * zLo ^ 2 < 1 / 10 ^ 8",
  "source": {
    "url": "https://doi.org/10.1112/S0025579314000229",
    "locator": "formalization-target:tmpc-artifact-rational-root-certificate"
  },
  "relations": [
    {
      "slug": "R791",
      "title": "Exact rational root isolation certificate",
      "object_type": "artifact",
      "relation": "verifies",
      "direction": "outgoing"
    },
    {
      "slug": "two-moment-poincare-constant",
      "title": "two moment poincare constant",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}