47 Thm 12: Encoding Rate (Circle Case)
Let \(H\) be a finite group with \(\operatorname {DecidableEq}\) instance, let \(X\) be a graph with \(H\)-action, let \(\Lambda \) be an \(H\)-invariant cell labeling of \(X\) of width \(s\), let \(\ell \in \mathbb {N}\) with \(\ell \neq 0\) and \(H \curvearrowright \operatorname {Fin}(\ell )\). Assume \(\ell \) is odd (i.e., \(\ell \equiv 1 \pmod{2}\)) and \(|H|\) is odd. Then the horizontal homology of the balanced product Tanner cycle code has the same \(\mathbb {F}_2\)-dimension as the quotient Tanner code homology:
By the linear equivalence \(\iota \colon H_1(C(X/H,\Lambda )) \xrightarrow {\; \simeq \; } H_1^h\) constructed in IotaPiMaps.iotaEquiv, which is a \(\mathbb {F}_2\)-linear isomorphism under the assumptions that \(\ell \) is odd and \(|H|\) is odd, linear equivalences preserve \(\operatorname {finrank}\). Applying LinearEquiv.finrank_eq to this isomorphism and taking the symmetric equality, we obtain the desired dimension equality.
The premises of encodingRateCircle are satisfiable: there exist a finite group \(H\), a graph with \(H\)-action \(X\), an \(H\)-invariant cell labeling \(\Lambda \), a positive natural number \(\ell \) with an \(H\)-action on \(\operatorname {Fin}(\ell )\), a compatible cycle action, \(\ell \) odd, and \(|H|\) odd, such that \(\top \) holds.
We apply IotaPiMaps.piMap_comp_iotaMap_satisfiable, which provides a witness tuple \(\langle H, \text{hG}, \text{hF}, \text{hD}, X, s, \Lambda , \ell , \text{hNZ}, \text{hMA}, h\Lambda , \text{hcompat}, -, h_{\ell \text{\_ odd}}, \text{hodd}, -\rangle \). Decomposing this existential, we extract all required components and assemble the existential for the satisfiability statement, concluding with trivial.