Norm base change to the Eisenstein field and quadratic L-function factorization

Let $q\ge 1$ and let $\chi$ be a complex Dirichlet character modulo $q$, extended by zero on non-units. Let $K=\mathbb Q(\zeta_3)$, let $\mathcal O$ be its ring of integers, and let $\chi_{-3}$ be the quadratic character modulo $3$. Write $\widetilde\chi$ for the product of $\chi$ and $\chi_{-3}$ after both characters are extended to the common modulus $3q$.

There exists a finite-order Hecke character $\eta$ in the mission's theta-continued Hecke family whose element coefficients are induced by the ideal norm:

The same character $\eta$ satisfies, for every complex $s\notin\{0,1\}$,

This is the norm base-change factorization used to transfer a zero-free region from the Hecke family to Dirichlet L-functions. The statement applies to primitive and imprimitive Dirichlet characters and retains their zero-on-nonunit conventions.

Formalization Note The existential witness is the character constructed as HeckeDirichlet.character in the upstream source. The factor ShortDraftHeckeBridge.baseChangeChar is the existing published definition of $\widetilde\chi$. The exclusion of both $0$ and $1$ follows the upstream LFunction_eq_dirichlet_product theorem and avoids assigned values of the continuations at exceptional points. This full Euler-factor identity is the form proved in the Lean source; the paper's equation (11.2) presents the corresponding identity after deleting primes dividing $3q$.