Def_14: Gross Code

Statement

The Gross code is a specific [[144, 12, 12]] Bivariate Bicycle code, so named because a 'gross' is a dozen dozens (144).

Parameters: ℓ = 12, m = 6, giving n = 2 · 12 · 6 = 144 qubits.

Polynomials: A = x³ + y² + y, B = y³ + x² + x

Logical operators: A convenient basis of logical operators uses the polynomials: f = 1 + x + x² + x³ + x⁶ + x⁷ + x⁸ + x⁹ + (x + x⁵ + x⁷ + x¹¹)y³ g = x + x²y + (1 + x)y² + x²y³ + y⁴ h = 1 + (1 + x)y + y² + (1 + x)y³

Then for any monomials α, β ∈ M:

• X̄_α = X(αf, 0) are X-type logical operators of weight 12
• X̄'_β = X(βg, βh) are X-type logical operators
• Z̄_β = Z(βh^T, βg^T) are Z-type logical operators
• Z̄'_α = Z(0, αf^T) are Z-type logical operators

Main Definitions

• GrossCode : The Gross code as a BivariateBicycleCode with ℓ = 12, m = 6
• GrossCode.polyF : Polynomial f for X-type logical operators
• GrossCode.polyG : Polynomial g for X-type logical operators
• GrossCode.polyH : Polynomial h for X-type logical operators
• GrossCode.logicalX : X̄_α = X(αf, 0)
• GrossCode.logicalXPrime : X̄'_β = X(βg, βh)
• GrossCode.logicalZ : Z̄_β = Z(βh^T, βg^T)
• GrossCode.logicalZPrime : Z̄'_α = Z(0, αf^T)

Corollaries

• GrossCode.numQubits_eq : The number of physical qubits is 144
• GrossCode.ell_val : ℓ = 12
• GrossCode.m_val : m = 6

Section 1: Parameters

The Gross code has ℓ = 12, m = 6.

@[reducible, inline]

abbrev QEC1.GrossCode.ell : ℕ

The ℓ parameter of the Gross code.

Equations

• QEC1.GrossCode.ell = 12

@[reducible, inline]

abbrev QEC1.GrossCode.m_param : ℕ

The m parameter of the Gross code.

Equations

• QEC1.GrossCode.m_param = 6

instance QEC1.GrossCode.instNeZeroNatEll : NeZero ell

instance QEC1.GrossCode.instNeZeroNatM_param : NeZero m_param

@[reducible, inline]

abbrev QEC1.GrossCode.GM : Type

The monomial set for the Gross code.

Equations

• QEC1.GrossCode.GM = QEC1.BivariateBicycle.M QEC1.GrossCode.ell QEC1.GrossCode.m_param

@[reducible, inline]

abbrev QEC1.GrossCode.GGroupAlg : Type

The group algebra for the Gross code.

Equations

• QEC1.GrossCode.GGroupAlg = QEC1.BivariateBicycle.GroupAlg QEC1.GrossCode.ell QEC1.GrossCode.m_param

Section 2: Convenience for building polynomials

We use the monomial function from the BB code definitions.

noncomputable def QEC1.GrossCode.mon (a : ZMod ell) (b : ZMod m_param) : GGroupAlg

Shorthand for monomials x^a y^b in the Gross code group algebra.

Equations

• QEC1.GrossCode.mon a b = QEC1.BivariateBicycle.monomial QEC1.GrossCode.ell QEC1.GrossCode.m_param a b

Section 3: The polynomials A and B

A = x³ + y² + y B = y³ + x² + x

noncomputable def QEC1.GrossCode.polyA : GGroupAlg

Polynomial A = x³ + y² + y for the Gross code.

Equations

• QEC1.GrossCode.polyA = QEC1.GrossCode.mon 3 0 + QEC1.GrossCode.mon 0 2 + QEC1.GrossCode.mon 0 1

noncomputable def QEC1.GrossCode.polyB : GGroupAlg

Polynomial B = y³ + x² + x for the Gross code.

Equations

• QEC1.GrossCode.polyB = QEC1.GrossCode.mon 0 3 + QEC1.GrossCode.mon 2 0 + QEC1.GrossCode.mon 1 0

Section 4: The Gross Code

The Gross code is a BB code with the above parameters and polynomials.

noncomputable def QEC1.GrossCode.grossCode : BivariateBicycle.BivariateBicycleCode ell m_param

The Gross code: a [[144, 12, 12]] Bivariate Bicycle code.

Equations

• QEC1.GrossCode.grossCode = { polyA := QEC1.GrossCode.polyA, polyB := QEC1.GrossCode.polyB }

Section 5: Parameter verification

theorem QEC1.GrossCode.numQubits_eq : BivariateBicycle.BivariateBicycleCode.numPhysicalQubits ell m_param = 144

The number of physical qubits in the Gross code is 144.

@[simp]

theorem QEC1.GrossCode.ell_val : ell = 12

ℓ = 12.

@[simp]

theorem QEC1.GrossCode.m_val : m_param = 6

m = 6.

theorem QEC1.GrossCode.numLeftQubits_eq : BivariateBicycle.BivariateBicycleCode.numLeftQubits ell m_param = 72

The number of left qubits is 72.

theorem QEC1.GrossCode.numRightQubits_eq : BivariateBicycle.BivariateBicycleCode.numRightQubits ell m_param = 72

The number of right qubits is 72.

theorem QEC1.GrossCode.numXChecks_eq : BivariateBicycle.BivariateBicycleCode.numXChecks ell m_param = 72

The number of X checks is 72.

theorem QEC1.GrossCode.numZChecks_eq : BivariateBicycle.BivariateBicycleCode.numZChecks ell m_param = 72

The number of Z checks is 72.

theorem QEC1.GrossCode.n_eq_2_ell_m : 2 * ell * m_param = 144

n = 2 · ℓ · m = 2 · 12 · 6 = 144

Section 6: Logical operator polynomials

f = 1 + x + x² + x³ + x⁶ + x⁷ + x⁸ + x⁹ + (x + x⁵ + x⁷ + x¹¹)y³ g = x + x²y + (1 + x)y² + x²y³ + y⁴ h = 1 + (1 + x)y + y² + (1 + x)y³

noncomputable def QEC1.GrossCode.polyF : GGroupAlg

Polynomial f for X-type logical operators. f = 1 + x + x² + x³ + x⁶ + x⁷ + x⁸ + x⁹ + (x + x⁵ + x⁷ + x¹¹)y³

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QEC1.GrossCode.polyG : GGroupAlg

Polynomial g for logical operators. g = x + x²y + (1 + x)y² + x²y³ + y⁴

Equations

• QEC1.GrossCode.polyG = QEC1.GrossCode.mon 1 0 + QEC1.GrossCode.mon 2 1 + QEC1.GrossCode.mon 0 2 + QEC1.GrossCode.mon 1 2 + QEC1.GrossCode.mon 2 3 + QEC1.GrossCode.mon 0 4

noncomputable def QEC1.GrossCode.polyH : GGroupAlg

Polynomial h for logical operators. h = 1 + (1 + x)y + y² + (1 + x)y³

Equations

• QEC1.GrossCode.polyH = QEC1.GrossCode.mon 0 0 + QEC1.GrossCode.mon 0 1 + QEC1.GrossCode.mon 1 1 + QEC1.GrossCode.mon 0 2 + QEC1.GrossCode.mon 0 3 + QEC1.GrossCode.mon 1 3

Section 7: Logical Operators

For any monomials α, β ∈ M:

• X̄_α = X(αf, 0) are X-type logical operators of weight 12
• X̄'_β = X(βg, βh) are X-type logical operators
• Z̄_β = Z(βh^T, βg^T) are Z-type logical operators
• Z̄'_α = Z(0, αf^T) are Z-type logical operators

noncomputable def QEC1.GrossCode.monomialMul (α : GM) (p : GGroupAlg) : GGroupAlg

Multiplication of a monomial by a group algebra element (left multiplication). α · p shifts all monomials in p by α.

Equations

• QEC1.GrossCode.monomialMul α p = Finsupp.mapDomain (fun (x : QEC1.BivariateBicycle.M QEC1.GrossCode.ell QEC1.GrossCode.m_param) => x + α) p

noncomputable def QEC1.GrossCode.logicalX (α : GM) : BivariateBicycle.BivariateBicycleCode.PauliX ell m_param

X̄_α = X(αf, 0): X-type logical operator of weight 12.

Equations

• QEC1.GrossCode.logicalX α = { leftPoly := QEC1.GrossCode.monomialMul α QEC1.GrossCode.polyF, rightPoly := 0 }

noncomputable def QEC1.GrossCode.logicalXPrime (β : GM) : BivariateBicycle.BivariateBicycleCode.PauliX ell m_param

X̄'_β = X(βg, βh): X-type logical operator.

Equations

• QEC1.GrossCode.logicalXPrime β = { leftPoly := QEC1.GrossCode.monomialMul β QEC1.GrossCode.polyG, rightPoly := QEC1.GrossCode.monomialMul β QEC1.GrossCode.polyH }

noncomputable def QEC1.GrossCode.logicalZ (β : GM) : BivariateBicycle.BivariateBicycleCode.PauliZ ell m_param

Z̄_β = Z(βh^T, βg^T): Z-type logical operator.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def QEC1.GrossCode.logicalZPrime (α : GM) : BivariateBicycle.BivariateBicycleCode.PauliZ ell m_param

Z̄'_α = Z(0, αf^T): Z-type logical operator.

Equations

• One or more equations did not get rendered due to their size.

Section 8: Symmetry

The symmetry in the BB code construction means that if gauging measurements are constructed for X̄_α and X̄'_β, the same Tanner graph connectivity works for Z̄'_α and Z̄_β.

The symmetry arises from the relationship between X and Z logical operators: X̄_α uses (αf, 0) while Z̄'_α uses (0, αf^T), X̄'_β uses (βg, βh) while Z̄_β uses (βh^T, βg^T).

theorem QEC1.GrossCode.logicalZPrime_right_eq_transpose_logicalX_left (α : GM) : (logicalZPrime α).leftPoly = 0 ∧ (logicalX α).rightPoly = 0

The Z̄'_α right polynomial is the transpose of the X̄_α left polynomial.

theorem QEC1.GrossCode.symmetry_X_ZPrime (α : GM) : (logicalX α).leftPoly = monomialMul α polyF ∧ (logicalX α).rightPoly = 0 ∧ (logicalZPrime α).leftPoly = 0 ∧ (logicalZPrime α).rightPoly = monomialMul α (BivariateBicycle.transposeAlg ell m_param polyF)

Structural symmetry: logicalX uses (αf, 0) and logicalZPrime uses (0, αf^T).

theorem QEC1.GrossCode.symmetry_XPrime_Z (β : GM) : (logicalXPrime β).leftPoly = monomialMul β polyG ∧ (logicalXPrime β).rightPoly = monomialMul β polyH ∧ (logicalZ β).leftPoly = monomialMul β (BivariateBicycle.transposeAlg ell m_param polyH) ∧ (logicalZ β).rightPoly = monomialMul β (BivariateBicycle.transposeAlg ell m_param polyG)

Structural symmetry: logicalXPrime uses (βg, βh) and logicalZ uses (βh^T, βg^T).

Section 9: Code parameters record

The Gross code is a [[144, 12, 12]] code. We record the claimed parameters.

structure QEC1.GrossCode.CodeParameters : Type

The code parameters [[n, k, d]] of the Gross code.

• n : ℕ
• k : ℕ
• d : ℕ

def QEC1.GrossCode.grossCodeParams : CodeParameters

The claimed parameters of the Gross code: [[144, 12, 12]].

Equations

• QEC1.GrossCode.grossCodeParams = { n := 144, k := 12, d := 12 }

@[simp]

theorem QEC1.GrossCode.grossCodeParams_n : grossCodeParams.n = 144

@[simp]

theorem QEC1.GrossCode.grossCodeParams_k : grossCodeParams.k = 12

@[simp]

theorem QEC1.GrossCode.grossCodeParams_d : grossCodeParams.d = 12

theorem QEC1.GrossCode.gross_is_dozen_dozens : grossCodeParams.n = 12 * 12

144 = 12 × 12, i.e., a gross is a dozen dozens.

theorem QEC1.GrossCode.numQubits_eq_params : BivariateBicycle.BivariateBicycleCode.numPhysicalQubits ell m_param = grossCodeParams.n

The number of physical qubits matches the code parameter n.

Section 10: Simp lemmas for the Gross code polynomials

@[simp]

theorem QEC1.GrossCode.grossCode_polyA : grossCode.polyA = polyA

@[simp]

theorem QEC1.GrossCode.grossCode_polyB : grossCode.polyB = polyB

@[simp]

theorem QEC1.GrossCode.logicalX_rightPoly (α : GM) : (logicalX α).rightPoly = 0

The logicalX operator has zero right component.

@[simp]

theorem QEC1.GrossCode.logicalZPrime_leftPoly (α : GM) : (logicalZPrime α).leftPoly = 0

The logicalZPrime operator has zero left component.