Remark 5: the residue map is a surjective ring homomorphism

Open

QAlgorithms.Papers.Independent.Intakethird100.P85.residue_ringHom

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $\rho:\mathbb Z[\omega]\to\mathbb Z_2[\omega]$ reduce the four omega-power coefficients modulo $2$ . The target multiplication is reduction modulo $\omega^4+1$ . For cyclotomic integers $s,t$ ,

\rho(0)=0,\quad\rho(1)=1,\quad\rho(s+t)=\rho(s)+\rho(t),\quad \rho(st)=\rho(s)\rho(t).

Every residue has a preimage in $\mathbb Z[\omega]$ . Thus the coefficient residue map is a surjective ring homomorphism. This justifies residue arithmetic in denominator reduction.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P85

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P85

open scoped Classical BigOperators

open QAlgorithms

open QAlgorithms.Papers.Independent.Gap48.P10
  (InZomega InDomega Residue bits residue residueMultiply Reducible)

open QAlgorithms.Papers.Independent.Support21.P13
  (synthesisRing integralRing coordinateValue HTLetter htWordMatrix EntriesInRing cliffordTLibrary)

local notation "omega" => QAlgorithms.gateT true true

local notation "sqrtTwo" => ((Real.sqrt 2 : ℝ) : ℂ)

/-- Remark 5, PDF p.2: rho is a surjective ring homomorphism with quotient multiplication. -/
theorem residue_ringHom :
    residue 0 = bits 0 ∧ residue 1 = bits 1 ∧
    (∀ t s : ℂ, InZomega t → InZomega s → residue (t + s) = residue t + residue s) ∧
    (∀ t s : ℂ, InZomega t → InZomega s →
      residue (t * s) = residueMultiply (residue t) (residue s)) ∧
    (∀ x : Residue, ∃ t : ℂ, InZomega t ∧ residue t = x) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P85

end

Source

Exact synthesis of multiqubit Clifford+T circuits, arXiv:1212.0506v3, PDF p. 2, Remark 5: the residue map is a surjective ring homomorphism

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $\omega=e^{i\pi/4}$ and $\mathcal O=\{a_0\omega^3+a_1\omega^2+a_2\omega+a_3:a_0,a_1,a_2,a_3\in\mathbb Z\}$ . Define $\operatorname{res}(t)\in(\mathbb Z/2\mathbb Z)^4$ by choosing such an integer coefficient tuple when $t\in\mathcal O$ and reducing its entries modulo $2$ , and by the zero tuple when $t\notin\mathcal O$ ; define $b(n)_i=\lfloor n/2^{3-i}\rfloor\bmod2$ for $i=0,1,2,3$ , and define

(x\star y)_l=\sum_{\substack{0\le i,j<4\\i+j\equiv l+3\pmod4}}x_i y_j.

Then $\operatorname{res}(0)=b(0)=(0,0,0,0)$ , $\operatorname{res}(1)=b(1)=(0,0,0,1)$ , and for every $t,s\in\mathcal O$ ,

\operatorname{res}(t+s)=\operatorname{res}(t)+\operatorname{res}(s), \qquad \operatorname{res}(ts)=\operatorname{res}(t)\star\operatorname{res}(s),

where addition is coordinatewise modulo $2$ ; moreover, every tuple $x\in(\mathbb Z/2\mathbb Z)^4$ equals $\operatorname{res}(t)$ for some $t\in\mathcal O$ . The addition and multiplication identities are asserted only for inputs in $\mathcal O$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph