[proofplan] We reduce the assertion to the standard construction theorem for Galois representations attached to cohomological Hilbert modular automorphic representations of $GL_2$. Regular algebraicity supplies the cohomological hypothesis, cuspidality supplies the automorphic input, and the coefficient field generated by Hecke eigenvalues supplies the field of definition. The construction theorem gives a continuous semisimple $\lambda$-adic representation and its local-global compatibility at every finite place away from $\ell$ where $\pi$ is unramified; this compatibility is exactly the asserted equality with the Hecke polynomial. [/proofplan] [step:Fix the coefficient field and the places where local compatibility is required] Let $E_\pi \subset \mathbb C$ denote the number field generated by the Hecke eigenvalues of $\pi$ at finite places where $\pi$ is unramified. Let $\lambda$ be a finite place of $E_\pi$ above the rational prime $\ell$, let $E_{\pi,\lambda}$ be the $\lambda$-adic completion of $E_\pi$, and choose a finite extension $K_\lambda/E_{\pi,\lambda}$ over which the representation produced below is defined. For a finite place $v$ of $F$, let $F_v$ be the completion of $F$, let $q_v$ be the cardinality of its residue field, let $\varpi_v \in F_v$ be a uniformizer, and let $\operatorname{Frob}_v \in G_F/I_v$ denote geometric Frobenius, where $I_v \subset G_F$ is the inertia subgroup at $v$. Let $S$ be the finite set consisting of the places $v \mid \ell$ and the finite places where $\pi_v$ is ramified. Let $\omega_\pi$ be the central character of $\pi$. For $v \notin S$, define $a_v(\pi) \in E_\pi$ by the following normalization: if $\alpha_v, \beta_v \in \overline{\mathbb Q}$ are the Satake parameters of the unramified local representation $\pi_v$ under the cohomological normalization used by the Hilbert modular variety construction, then \begin{align*} a_v(\pi) &= \alpha_v + \beta_v, & \alpha_v\beta_v &= \omega_\pi(\varpi_v)q_v. \end{align*} Equivalently, the Hecke polynomial of $\pi_v$ in this proof means \begin{align*} P_v(\pi,X) := 1 - a_v(\pi)X + \omega_\pi(\varpi_v)q_vX^2. \end{align*} [/step] [step:Apply the construction theorem for cohomological Hilbert modular forms] Because $F$ is totally real and $\pi$ is regular algebraic and cuspidal, the archimedean component of $\pi$ has the same infinitesimal character as an algebraic representation of $\operatorname{Res}_{F/\mathbb Q}GL_2$. Let $\mathcal V_\pi$ denote that algebraic coefficient system on the Hilbert modular variety attached to $F$; with this coefficient system, $\pi$ contributes to the cuspidal étale cohomology in the cohomological normalization. We invoke the Carayol-Taylor-Blasius-Rogawski-Wiles construction theorem for cohomological Hilbert modular eigenforms in this normalization: for every finite place $\lambda$ of $E_\pi$ above $\ell$, it produces a finite extension $K_\lambda/E_{\pi,\lambda}$ and a continuous semisimple representation \begin{align*} \rho_{\pi,\lambda}: G_F &\to GL_2(K_\lambda) \end{align*} which is unramified at every finite place $v \nmid \ell$ where $\pi_v$ is unramified and whose unramified local-global compatibility is \begin{align*} \det\left(1 - X\rho_{\pi,\lambda}(\operatorname{Frob}_v)\right) &= 1 - (\alpha_v + \beta_v)X + \alpha_v\beta_v X^2 \end{align*} for the Satake parameters $\alpha_v,\beta_v$ in the normalization fixed above. The hypotheses of this construction theorem are now verified: $F$ is totally real, $\pi$ is cuspidal, and regular algebraicity gives precisely the algebraic coefficient system $\mathcal V_\pi$ needed for cohomological realization on the Hilbert modular variety. Since $S$ consists of the places above $\ell$ and the finite ramified places of $\pi$, the theorem gives existence, continuity, semisimplicity, and unramifiedness outside $S$. [guided] The purpose of this step is not to reprove the construction of $\rho_{\pi,\lambda}$ from the étale cohomology of Hilbert modular varieties, but to invoke the precise deep theorem that performs that construction with the same normalization as the polynomial fixed in the first step. The theorem applies to cohomological cuspidal automorphic representations of $GL_2(\mathbb A_F)$ over a totally real field, with coefficients in the algebraic local system determined by the archimedean infinitesimal character. We verify these inputs. First, $F$ is totally real by hypothesis, so the relevant Shimura varieties are Hilbert modular varieties. Second, $\pi$ is cuspidal by hypothesis, so its finite-slope Hecke eigensystem occurs in cuspidal cohomology rather than only in Eisenstein cohomology. Third, regular algebraicity means that the archimedean component of $\pi$ has the same infinitesimal character as an algebraic representation of $\operatorname{Res}_{F/\mathbb Q}GL_2$. Let $\mathcal V_\pi$ denote the corresponding algebraic coefficient system. With this choice, $\pi$ is cohomological in the normalization used by the Hilbert modular variety construction. The Carayol-Taylor-Blasius-Rogawski-Wiles construction theorem therefore supplies, for the chosen finite place $\lambda$ of $E_\pi$ above $\ell$, a finite coefficient extension $K_\lambda/E_{\pi,\lambda}$ and a continuous semisimple homomorphism \begin{align*} \rho_{\pi,\lambda}: G_F &\to GL_2(K_\lambda). \end{align*} It also states the unramified local compatibility in the following explicit form: if $v \nmid \ell$, if $\pi_v$ is unramified, and if $\alpha_v,\beta_v$ are the Satake parameters in the cohomological normalization fixed above, then $\rho_{\pi,\lambda}$ is unramified at $v$ and \begin{align*} \det\left(1 - X\rho_{\pi,\lambda}(\operatorname{Frob}_v)\right) &= 1 - (\alpha_v + \beta_v)X + \alpha_v\beta_v X^2. \end{align*} Since $S$ was defined to contain exactly the places above $\ell$ together with the ramified finite places of $\pi$, this gives unramifiedness outside $S$ and preserves the normalization needed for the final polynomial identity. [/guided] [/step] [step:Translate local-global compatibility into the Frobenius polynomial identity] Let $v \notin S$. Then $v \nmid \ell$, the local representation $\pi_v$ is unramified, and $\rho_{\pi,\lambda}$ is unramified at $v$, so $\rho_{\pi,\lambda}(\operatorname{Frob}_v)$ is well-defined up to conjugacy in $GL_2(K_\lambda)$. By the local-global compatibility statement just invoked, if $\alpha_v,\beta_v$ are the Satake parameters of $\pi_v$ in the fixed cohomological normalization, then \begin{align*} \det\left(1 - X\rho_{\pi,\lambda}(\operatorname{Frob}_v)\right) &= 1 - (\alpha_v + \beta_v)X + \alpha_v\beta_v X^2. \end{align*} By the definitions made in the first step, \begin{align*} \alpha_v + \beta_v &= a_v(\pi), & \alpha_v\beta_v &= \omega_\pi(\varpi_v)q_v. \end{align*} Substituting these two equalities into the preceding characteristic polynomial gives \begin{align*} \det\left(1 - X\rho_{\pi,\lambda}(\operatorname{Frob}_v)\right) &= 1 - a_v(\pi)X + \omega_\pi(\varpi_v)q_vX^2 = P_v(\pi,X). \end{align*} This is precisely the asserted Frobenius-Hecke compatibility at every finite place $v \nmid \ell$ where $\pi_v$ is unramified. Since only finitely many finite places lie in $S$, the representation is unramified at almost all finite places of $F$. [guided] Now we extract the explicit polynomial identity from local-global compatibility. Fix a finite place $v \notin S$. By the definition of $S$, the place $v$ does not divide $\ell$ and $\pi_v$ is unramified. The construction theorem says that $\rho_{\pi,\lambda}$ is also unramified at $v$, meaning that $\rho_{\pi,\lambda}(\sigma)$ is the identity matrix for every $\sigma \in I_v$. Therefore the conjugacy class of \begin{align*} \rho_{\pi,\lambda}(\operatorname{Frob}_v) \in GL_2(K_\lambda) \end{align*} is defined independently of the chosen lift of geometric Frobenius. Let $\alpha_v,\beta_v \in \overline{\mathbb Q}$ be the Satake parameters of $\pi_v$ in the cohomological normalization fixed in the first step. The local-global compatibility theorem gives \begin{align*} \det\left(1 - X\rho_{\pi,\lambda}(\operatorname{Frob}_v)\right) &= 1 - (\alpha_v + \beta_v)X + \alpha_v\beta_v X^2. \end{align*} The first step defined the Hecke eigenvalue and central-character normalization by \begin{align*} a_v(\pi) &= \alpha_v + \beta_v, & \omega_\pi(\varpi_v)q_v &= \alpha_v\beta_v. \end{align*} Substituting these equalities yields \begin{align*} \det\left(1 - X\rho_{\pi,\lambda}(\operatorname{Frob}_v)\right) &= 1 - a_v(\pi)X + \omega_\pi(\varpi_v)q_vX^2. \end{align*} Because $S$ is finite, the excluded finite places are finite in number, so $\rho_{\pi,\lambda}$ is unramified at almost all finite places of $F$. This proves the existence, continuity, unramifiedness, and Frobenius-Hecke compatibility asserted in the theorem. [/guided] [/step]