Take the rational endpoints \[ z_-=\frac{44934094579}{10^{10}},\qquad z_+=\frac{3510476139}{781250000}. \] For \(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 \[ h(z_-)>\frac3{10^{11}},\qquad h(z_+)<-\frac4{10^{11}}. \] The uniqueness proved in the spectral record isolates \(z_*\) between these endpoints. Squaring the positive interval and multiplying by four gives \[ \frac{2019072855634517187241}{25000000000000000000} <\lambda_*< \frac{12323442722488347321}{152587890625000000}. \] In terminating decimals, \[ \boxed{80.76291422538068748964<\lambda_*<80.76291422609963300291}. \] The exact width is \[ \frac{449340945791}{625000000000000000000} =0.0000000007189455132656<10^{-8}. \] Consequently the best constant \(C_*=1/\lambda_*\) obeys \[ \frac{152587890625000000}{12323442722488347321} <C_*< \frac{25000000000000000000}{2019072855634517187241}, \] or approximately \(0.01238192070682903136<C_*<0.01238192070693925431\).

Put \(t=x-\tfrac12\) and \[ V=\left\{f\in H_0^1(0,1):\langle f,1\rangle=\langle f,t\rangle=0\right\}. \] This 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: \[ -f''=\lambda f+a+bt,\qquad f(-\tfrac12)=f(\tfrac12)=0. \]

Reflection 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 \[ f_e(t)=A\bigl(\cos(kt)-\cos z\bigr). \] Its mean vanishes exactly when \[ E(z):=\sin z-z\cos z=0. \] In the odd sector the mean is automatic, and the corresponding form is \[ f_o(t)=A\bigl(\sin(kt)-2t\sin z\bigr). \] The remaining moment vanishes exactly when \[ O(z):=(z^2-3)\sin z+3z\cos z=0. \]

The 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)\).

The 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 \[ \lambda_*=4z_*^2. \] The 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, \[ f_*(x)=\cos\bigl(2z_*(x-\tfrac12)\bigr)-\cos z_*. \] It 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\).

Kuznetsov and Nazarov survey sharp Poincare, Steklov, and related constants, including the classical interval inequalities with endpoint conditions. Xu, Liu, and Lu treat sharp Wirtinger constants on \([0,1]\) for endpoint interpolation conditions and reduce the \(L^2\) constant to an eigenvalue problem for an integral operator. Bartier, Blanchet, Dolbeault, and Escobedo prove an improved Gaussian Poincare inequality under orthogonality to low-degree Hermite polynomials; they explicitly interpret those conditions as moment conditions.

Focused searches combined `Poincare`, `Wirtinger`, `Dirichlet`, `moment constraints`, `orthogonality to polynomials`, and the two characteristic equations in this record. They found no primary source stating this exact pair of integral constraints, the factorization into \(E\) and \(O\), or the certified value above. The novelty claim remains unverified.

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.

All assertions use integers and `Fraction`. Decimal arithmetic is confined to display strings. The sine enclosure is its degree-49 Taylor polynomial plus or minus \(z^{51}/51!\); the cosine enclosure is its degree-48 polynomial plus or minus \(z^{50}/50!\). Substitution into \(h(z)=\sin z-z\cos z\) is outward rounded with exact fractions.

The canonical JSON output, without a trailing line feed, has SHA-256 digest `af00f1c39a3363414eb35d1d91973da3257ab6293b6006c00814e9e9ff4c34ef`. It records signs `[1,-1]`, the exact root interval, the exact lambda interval, and its width.