Remark 20: The Gross Code Definition

Statement

The Gross code is a [[144, 12, 12]] BB code with parameters ℓ = 12, m = 6.

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

Logical operators use polynomials f, g, h in F₂[x,y]/(x¹² - 1, y⁶ - 1). The logical X̄_α = X(αf, 0) has weight 12 and acts only on L qubits.

Main Results

• grossA, grossB: the polynomials A and B
• grossCode: the Gross code as a valid stabilizer code
• grossF, grossG, grossH: the logical operator polynomials
• logicalXBar, logicalXBar': the logical X operators
• logicalZBar, logicalZBar': the logical Z operators
• grossCode_numQubits: the code has n = 144 physical qubits
• grossCode_numChecks: the code has 144 checks
• logicalXBar_weight: X̄_α has weight 12
• logicalXBar_pure_X: X̄_α is pure X-type
• logicalXBar_acts_only_on_L: X̄_α acts only on L qubits
• logicalXBar_inCentralizer: X̄_α is in the centralizer (a logical operator candidate)
• logicalXBar_tanner_expansion_insufficient: key property about limited Tanner expansion

The Gross code parameters

@[reducible, inline]

abbrev BivariateBicycle.GrossCode.ℓ : ℕ

ℓ = 12 for the Gross code.

Equations

• BivariateBicycle.GrossCode.ℓ = 12

@[reducible, inline]

abbrev BivariateBicycle.GrossCode.m : ℕ

m = 6 for the Gross code.

Equations

• BivariateBicycle.GrossCode.m = 6

@[reducible, inline]

abbrev BivariateBicycle.GrossCode.GrossMonomial : Type

The monomial group for the Gross code: Z₁₂ × Z₆.

Equations

• BivariateBicycle.GrossCode.GrossMonomial = BivariateBicycle.BBMonomial BivariateBicycle.GrossCode.ℓ BivariateBicycle.GrossCode.m

@[reducible, inline]

abbrev BivariateBicycle.GrossCode.GrossAlgebra : Type

The group algebra for the Gross code: F₂[x,y]/(x¹² - 1, y⁶ - 1).

Equations

• BivariateBicycle.GrossCode.GrossAlgebra = BivariateBicycle.BBGroupAlgebra BivariateBicycle.GrossCode.ℓ BivariateBicycle.GrossCode.m

@[reducible, inline]

abbrev BivariateBicycle.GrossCode.GrossQubit : Type

The qubit type for the Gross code.

Equations

• BivariateBicycle.GrossCode.GrossQubit = BivariateBicycle.BBQubit BivariateBicycle.GrossCode.ℓ BivariateBicycle.GrossCode.m

Polynomial definitions

def BivariateBicycle.GrossCode.grossA : GrossAlgebra

A = x³ + y² + y in F₂[x,y]/(x¹² - 1, y⁶ - 1).

Equations

• BivariateBicycle.GrossCode.grossA = BivariateBicycle.bbMonomial 3 0 + BivariateBicycle.bbMonomial 0 2 + BivariateBicycle.bbMonomial 0 1

def BivariateBicycle.GrossCode.grossB : GrossAlgebra

B = y³ + x² + x in F₂[x,y]/(x¹² - 1, y⁶ - 1).

Equations

• BivariateBicycle.GrossCode.grossB = BivariateBicycle.bbMonomial 0 3 + BivariateBicycle.bbMonomial 2 0 + BivariateBicycle.bbMonomial 1 0

Check commutation

theorem BivariateBicycle.GrossCode.grossChecks_XZ_commute (α β : GrossMonomial) : (bbCheckX grossA grossB α).PauliCommute (bbCheckZ grossA grossB β)

theorem BivariateBicycle.GrossCode.grossChecks_commute (i j : BBCheckIndex ℓ m) : (bbCheck grossA grossB i).PauliCommute (bbCheck grossA grossB j)

The Gross code as a stabilizer code

noncomputable def BivariateBicycle.GrossCode.grossCode : StabilizerCode GrossQubit

The Gross code as a valid stabilizer code, constructed directly.

Equations

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

theorem BivariateBicycle.GrossCode.grossCode_numQubits : grossCode.numQubits = 144

The Gross code has 144 = 2 × 12 × 6 physical qubits.

theorem BivariateBicycle.GrossCode.grossCode_numChecks : grossCode.numChecks = 144

The Gross code has 144 = 2 × 12 × 6 checks.

Logical operator polynomials

def BivariateBicycle.GrossCode.grossF : GrossAlgebra

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.

def BivariateBicycle.GrossCode.grossG : GrossAlgebra

g = x + x²y + (1+x)y² + x²y³ + y⁴

Equations

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

def BivariateBicycle.GrossCode.grossH : GrossAlgebra

h = 1 + (1+x)y + y² + (1+x)y³

Equations

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

Logical X operators

def BivariateBicycle.GrossCode.logicalXBar (α : GrossMonomial) : PauliOp GrossQubit

The logical X operator X̄_α = X(αf, 0) for α ∈ M.

Equations

• BivariateBicycle.GrossCode.logicalXBar α = BivariateBicycle.pauliXBB (BivariateBicycle.bbShift α BivariateBicycle.GrossCode.grossF) 0

def BivariateBicycle.GrossCode.logicalXBar' (β : GrossMonomial) : PauliOp GrossQubit

The logical X' operator X̄'_β = X(βg, βh) for β ∈ M.

Equations

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

Logical Z operators

def BivariateBicycle.GrossCode.logicalZBar (β : GrossMonomial) : PauliOp GrossQubit

The logical Z operator Z̄_β = Z(βh^T, βg^T) for β ∈ M.

Equations

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

def BivariateBicycle.GrossCode.logicalZBar' (α : GrossMonomial) : PauliOp GrossQubit

The logical Z' operator Z̄'_α = Z(0, αf^T) for α ∈ M.

Equations

• BivariateBicycle.GrossCode.logicalZBar' α = BivariateBicycle.pauliZBB 0 (BivariateBicycle.bbShift α (BivariateBicycle.bbTranspose BivariateBicycle.GrossCode.grossF))

Properties of X̄_α

theorem BivariateBicycle.GrossCode.logicalXBar_pure_X (α : GrossMonomial) : (logicalXBar α).zVec = 0

X̄_α is pure X-type: it has no Z-support.

theorem BivariateBicycle.GrossCode.logicalXBar'_pure_X (β : GrossMonomial) : (logicalXBar' β).zVec = 0

X̄'_β is pure X-type: it has no Z-support.

theorem BivariateBicycle.GrossCode.logicalZBar_pure_Z (β : GrossMonomial) : (logicalZBar β).xVec = 0

Z̄_β is pure Z-type: it has no X-support.

theorem BivariateBicycle.GrossCode.logicalZBar'_pure_Z (α : GrossMonomial) : (logicalZBar' α).xVec = 0

Z̄'_α is pure Z-type: it has no X-support.

theorem BivariateBicycle.GrossCode.logicalXBar_acts_only_on_L (α δ : GrossMonomial) : (logicalXBar α).xVec (Sum.inr δ) = 0

X̄_α acts only on L qubits: xVec on R qubits is zero.

theorem BivariateBicycle.GrossCode.logicalZBar'_acts_only_on_R (α γ : GrossMonomial) : (logicalZBar' α).zVec (Sum.inl γ) = 0

Z̄'_α acts only on R qubits: zVec on L qubits is zero.

Support and weight

theorem BivariateBicycle.GrossCode.grossF_weight_eq_12 : {γ : GrossMonomial | grossF γ ≠ 0}.card = 12

The polynomial f has weight 12 (12 nonzero coefficients).

theorem BivariateBicycle.GrossCode.grossA_support_card : {γ : GrossMonomial | grossA γ ≠ 0}.card = 3

A has 3 nonzero coefficients.

theorem BivariateBicycle.GrossCode.grossB_support_card : {γ : GrossMonomial | grossB γ ≠ 0}.card = 3

B has 3 nonzero coefficients.

Shift-invariance of support cardinality

theorem BivariateBicycle.GrossCode.logicalXBar_weight (α : GrossMonomial) : (logicalXBar α).weight = 12

X̄_α has weight 12.

Self-inverse properties

theorem BivariateBicycle.GrossCode.logicalXBar_mul_self (α : GrossMonomial) : logicalXBar α * logicalXBar α = 1

X̄_α is self-inverse.

theorem BivariateBicycle.GrossCode.logicalXBar'_mul_self (β : GrossMonomial) : logicalXBar' β * logicalXBar' β = 1

X̄'_β is self-inverse.

theorem BivariateBicycle.GrossCode.logicalZBar_mul_self (β : GrossMonomial) : logicalZBar β * logicalZBar β = 1

Z̄_β is self-inverse.

theorem BivariateBicycle.GrossCode.logicalZBar'_mul_self (α : GrossMonomial) : logicalZBar' α * logicalZBar' α = 1

Z̄'_α is self-inverse.

Kernel conditions via native_decide

Commutation of logical operators with checks

theorem BivariateBicycle.GrossCode.logicalXBar_commute_xCheck (α β : GrossMonomial) : (logicalXBar α).PauliCommute (bbCheckX grossA grossB β)

X̄_α commutes with all X checks (both pure X-type).

theorem BivariateBicycle.GrossCode.logicalXBar_commute_zCheck (α β : GrossMonomial) : (logicalXBar α).PauliCommute (bbCheckZ grossA grossB β)

X̄_α commutes with all Z checks.

theorem BivariateBicycle.GrossCode.logicalXBar_commute_allChecks (α : GrossMonomial) (i : BBCheckIndex ℓ m) : (logicalXBar α).PauliCommute (bbCheck grossA grossB i)

X̄_α commutes with all checks of the Gross code.

theorem BivariateBicycle.GrossCode.logicalXBar'_commute_xCheck (α β : GrossMonomial) : (logicalXBar' α).PauliCommute (bbCheckX grossA grossB β)

X̄'_β commutes with all X checks (both pure X-type).

theorem BivariateBicycle.GrossCode.logicalXBar'_commute_zCheck (α β : GrossMonomial) : (logicalXBar' α).PauliCommute (bbCheckZ grossA grossB β)

X̄'_β commutes with all Z checks.

theorem BivariateBicycle.GrossCode.logicalXBar'_commute_allChecks (β : GrossMonomial) (i : BBCheckIndex ℓ m) : (logicalXBar' β).PauliCommute (bbCheck grossA grossB i)

X̄'_β commutes with all checks of the Gross code.

Z logical operators commute with checks

theorem BivariateBicycle.GrossCode.logicalZBar_commute_zCheck (α β : GrossMonomial) : (logicalZBar α).PauliCommute (bbCheckZ grossA grossB β)

Z̄_β commutes with all Z checks (both pure Z-type).

theorem BivariateBicycle.GrossCode.logicalZBar_commute_xCheck (α β : GrossMonomial) : (logicalZBar α).PauliCommute (bbCheckX grossA grossB β)

Z̄_β commutes with all X checks.

theorem BivariateBicycle.GrossCode.logicalZBar_commute_allChecks (β : GrossMonomial) (i : BBCheckIndex ℓ m) : (logicalZBar β).PauliCommute (bbCheck grossA grossB i)

Z̄_β commutes with all checks.

theorem BivariateBicycle.GrossCode.logicalZBar'_commute_zCheck (α β : GrossMonomial) : (logicalZBar' α).PauliCommute (bbCheckZ grossA grossB β)

Z̄'_α commutes with all Z checks (both pure Z-type).

theorem BivariateBicycle.GrossCode.logicalZBar'_commute_xCheck (α β : GrossMonomial) : (logicalZBar' α).PauliCommute (bbCheckX grossA grossB β)

Z̄'_α commutes with all X checks.

theorem BivariateBicycle.GrossCode.logicalZBar'_commute_allChecks (α : GrossMonomial) (i : BBCheckIndex ℓ m) : (logicalZBar' α).PauliCommute (bbCheck grossA grossB i)

Z̄'_α commutes with all checks.

Centralizer membership

theorem BivariateBicycle.GrossCode.logicalXBar_inCentralizer (α : GrossMonomial) : grossCode.inCentralizer (logicalXBar α)

X̄_α is in the centralizer of the Gross code.

theorem BivariateBicycle.GrossCode.logicalXBar'_inCentralizer (β : GrossMonomial) : grossCode.inCentralizer (logicalXBar' β)

X̄'_β is in the centralizer of the Gross code.

theorem BivariateBicycle.GrossCode.logicalZBar_inCentralizer (β : GrossMonomial) : grossCode.inCentralizer (logicalZBar β)

Z̄_β is in the centralizer of the Gross code.

theorem BivariateBicycle.GrossCode.logicalZBar'_inCentralizer (α : GrossMonomial) : grossCode.inCentralizer (logicalZBar' α)

Z̄'_α is in the centralizer of the Gross code.

The X̄_α xVec characterization

@[simp]

theorem BivariateBicycle.GrossCode.logicalXBar_xVec_left (α γ : GrossMonomial) : (logicalXBar α).xVec (Sum.inl γ) = grossF (γ - α)

@[simp]

theorem BivariateBicycle.GrossCode.logicalXBar_xVec_right (α δ : GrossMonomial) : (logicalXBar α).xVec (Sum.inr δ) = 0

@[simp]

theorem BivariateBicycle.GrossCode.logicalXBar_zVec (α : GrossMonomial) : (logicalXBar α).zVec = 0

Check weight properties

theorem BivariateBicycle.GrossCode.xCheck_weight (α : GrossMonomial) : (bbCheckX grossA grossB α).weight = 6

Each X check of the Gross code has weight 6.

Key property: insufficient Tanner graph expansion

theorem BivariateBicycle.GrossCode.logicalXBar_tanner_expansion_insufficient (α : GrossMonomial) : (logicalXBar α).weight = 12 ∧ (logicalXBar α).zVec = 0 ∧ (∀ (δ : GrossMonomial), (logicalXBar α).xVec (Sum.inr δ) = 0) ∧ {γ : GrossMonomial | grossA γ ≠ 0}.card = 3

Key property (Remark 20): X̄_α has weight 12, is pure X-type, and acts only on L qubits. Each L qubit participates in at most |supp(A)| = 3 X-type checks, so the Tanner subgraph on X̄_α has limited expansion.

Summary

theorem BivariateBicycle.GrossCode.grossCode_parameters : grossCode.numQubits = 144 ∧ grossCode.numChecks = 144

The Gross code has 144 qubits and 144 checks.