Theorem 12: Encoding Rate (Circle Case)

The horizontal part of the balanced product Tanner cycle code has dimension equal to the dimension of the quotient Tanner code homology: dim H₁ʰ(C(X,L) ⊗_{ℤ_ℓ} C(C_ℓ)) = dim H₁(C(X/H, L))

This follows from the linear isomorphism ι : H₁(C(X/H, L)) ≃ H₁ʰ constructed in Def_28 (the iotaEquiv), which preserves dimension.

Main Results

• encodingRateCircle — the dimension equality
• encodingRateCircle_satisfiable — witness that the premises are satisfiable

theorem EncodingRateCircle.encodingRateCircle {H : Type} [Group H] [Fintype H] [DecidableEq H] (X : GraphWithGroupAction H) {s : ℕ} (Λ : X.CellLabeling s) (ℓ : ℕ) [NeZero ℓ] [MulAction H (Fin ℓ)] (hΛ : GraphWithGroupAction.IsInvariantLabeling Λ) (hcompat : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (hℓ_odd : ℓ % 2 = 1) (hodd : Odd (Fintype.card H)) : Module.finrank 𝔽₂ (HorizontalVerticalHomologySplitting.H1h X Λ ℓ hΛ hcompat) = Module.finrank 𝔽₂ (IotaPiMaps.quotientTannerHomology X Λ hΛ)

Encoding Rate (Circle Case). The horizontal homology of the balanced product Tanner cycle code has the same dimension as the quotient Tanner code homology: dim H₁ʰ(C(X,L) ⊗_{ℤ_ℓ} C(C_ℓ)) = dim H₁(C(X/H, L))

The proof uses the linear isomorphism iotaEquiv from Def_28, which gives H₁(C(X/H, L)) ≃ₗ[𝔽₂] H₁ʰ. Since linear equivalences preserve finrank, we obtain the dimension equality.

theorem EncodingRateCircle.encodingRateCircle_satisfiable : ∃ (H : Type) (x : Group H) (x_1 : Fintype H) (x_2 : DecidableEq H) (X : GraphWithGroupAction H) (s : ℕ) (Λ : X.CellLabeling s) (ℓ : ℕ) (x_3 : NeZero ℓ) (x_4 : MulAction H (Fin ℓ)) (_ : GraphWithGroupAction.IsInvariantLabeling Λ) (_ : BalancedProductTannerCycleCode.CycleCompatibleAction ℓ) (_ : ℓ % 2 = 1) (_ : Odd (Fintype.card H)), True

Witness: the premises of encodingRateCircle are satisfiable. Follows from piMap_comp_iotaMap_satisfiable in Def_28.