{
  "schema": "theoremdb-agent-record-v1",
  "ref": "R794",
  "content_hash": null,
  "slug": "tmpc-claim-spectral-reduction",
  "type": "claim",
  "title": "Parity reduction gives the sharp eigenvalue equation",
  "summary": "The minimum is the simple even eigenvalue 4z_*^2, where z_* is the unique zero of sin z-z cos z in (pi,3pi/2).",
  "relevance": "For The sharp Dirichlet Poincare constant with two moment constraints, record tmpc-claim-spectral-reduction (“Parity reduction gives the sharp eigenvalue equation”) records a bound, answer, status fact, or structural consequence. The record states: The minimum is the simple even eigenvalue 4z_*^2, where z_* is the unique zero of sin z-z cos z in (pi,3pi/2).",
  "relevance_source": "recorded",
  "body": "Put \\(t=x-\\tfrac12\\) and\n\\[\nV=\\left\\{f\\in H_0^1(0,1):\\langle f,1\\rangle=\\langle f,t\\rangle=0\\right\\}.\n\\]\nThis is a closed subspace. Compactness of \\(H_0^1(0,1)\\hookrightarrow L^2(0,1)\\), applied after normalizing \\(\\|f\\|_2=1\\), gives a minimizer. The Euler equation has two Lagrange multipliers:\n\\[\n-f''=\\lambda f+a+bt,\\qquad f(-\\tfrac12)=f(\\tfrac12)=0.\n\\]\n\nReflection about the midpoint preserves \\(V\\). Its even and odd parts are orthogonal for both the energy and the \\(L^2\\) norm. In the even sector the second constraint is automatic. Writing \\(k=\\sqrt\\lambda\\) and \\(z=k/2\\), every nonzero stationary function below the second even Dirichlet eigenvalue has the form\n\\[\nf_e(t)=A\\bigl(\\cos(kt)-\\cos z\\bigr).\n\\]\nIts mean vanishes exactly when\n\\[\nE(z):=\\sin z-z\\cos z=0.\n\\]\nIn the odd sector the mean is automatic, and the corresponding form is\n\\[\nf_o(t)=A\\bigl(\\sin(kt)-2t\\sin z\\bigr).\n\\]\nThe remaining moment vanishes exactly when\n\\[\nO(z):=(z^2-3)\\sin z+3z\\cos z=0.\n\\]\n\nThe unconstrained even Dirichlet eigenvalues are \\(\\pi^2,9\\pi^2,\\ldots\\). Imposing one independent mean condition places the first even constrained eigenvalue strictly between \\(\\pi^2\\) and \\(9\\pi^2\\) by the min-max principle. The strict bounds follow because the first mode violates the condition, while a nonzero admissible combination exists in the span of the first two modes. Thus its \\(z\\) lies in \\((\\pi/2,3\\pi/2)\\). Now \\(E'(z)=z\\sin z\\). The function is positive on \\((\\pi/2,\\pi]\\), then decreases from \\(E(\\pi)=\\pi\\) to \\(E(3\\pi/2)=-1\\). It has one zero \\(z_*\\) in \\((\\pi,3\\pi/2)\\).\n\nThe odd Dirichlet eigenvalues are \\(4\\pi^2,16\\pi^2,\\ldots\\), so the first constrained odd root lies in \\((\\pi,2\\pi)\\) in the \\(z\\) variable. On \\((\\pi,3\\pi/2]\\), both terms of \\(O(z)\\) are negative. The odd branch therefore starts above \\(9\\pi^2\\), while \\(4z_*^2<9\\pi^2\\). Hence\n\\[\n\\lambda_*=4z_*^2.\n\\]\nThe zero is simple since \\(E'(z_*)\\ne0\\), and the odd branch is separated from it. The minimizing eigenspace is one-dimensional. Up to a nonzero scalar,\n\\[\nf_*(x)=\\cos\\bigl(2z_*(x-\\tfrac12)\\bigr)-\\cos z_*.\n\\]\nIt is even about \\(x=1/2\\). A unit \\(L^2\\) representative is obtained by multiplying by \\(\\sqrt2/|\\sin z_*|\\), since the squared norm of the displayed function is \\(\\sin^2(z_*)/2\\).",
  "status": "established",
  "evidence_grade": "self_reported",
  "scope": {
    "kind": "universal",
    "statement": "the stated Rayleigh quotient on H_0^1(0,1) under the two constraints integral f=0 and integral x f=0"
  },
  "reproduction": {
    "schema": "theoremdb-reproduction-v1",
    "readiness": "source_only",
    "kind": "claim",
    "citation": {
      "url": "https://doi.org/10.1112/S0025579314000229",
      "locator": "Complete variational, parity, min-max, and ODE proof supplied in this record"
    },
    "missing": [
      "source",
      "command",
      "runtime",
      "expected_output"
    ]
  },
  "formal_statement": null,
  "source": {
    "url": "https://doi.org/10.1112/S0025579314000229",
    "locator": "Complete variational, parity, min-max, and ODE proof supplied in this record"
  },
  "models": [],
  "continuation": null,
  "relations": [
    {
      "slug": "R793",
      "title": "The sharp eigenvalue is certified to ten decimal places",
      "object_type": "claim",
      "relation": "supports",
      "direction": "outgoing"
    },
    {
      "slug": "R792",
      "title": "The literature search found nearby sharp and moment-constrained inequalities",
      "object_type": "attempt",
      "relation": "informs",
      "direction": "incoming"
    },
    {
      "slug": "two-moment-poincare-constant",
      "title": "two moment poincare constant",
      "object_type": "problem",
      "relation": "recorded_for",
      "direction": "outgoing"
    }
  ]
}