Metadata

slug: cui-mehta-mousavi-nezhadi-2020-chsh-group-decomposition
bibkey: cuimehtamousavinezhadi2020chsh
doi: 10.22331/q-2020-10-21-346
url: https://arxiv.org/abs/1911.01593
triage: theorem
motivation_gids:
  - D5/S3/Quantum/Algebra/GeneralizedCHSHGroupDecomposition.result

A product decomposition of the generalized CHSH groups

Problem

Cui, Mehta, Mousavi and Nezhadi, A generalization of CHSH and the algebraic structure of optimal strategies, Quantum 4, 346 (2020), arXiv:1911.01593v5, Section 1.4 (Further work), item 2, ask:

In Section 5, we give efficient explicit presentations for G_n and its multiplication table. Can we go further and characterize these groups in terms of direct and semidirect products of small well-known groups? The first few cases are as follows

For every natural $n \geq 2$ , the answer is

$G_{n} ≅ (C_{2 n} \times C_{2}^{n - 2}) ⋊_{α_{n}} C_{n} .$

The group $G_{n}$ has the source’s Section 5 presentation on $P_{0}, P_{1}, J$ : the relators are $P_{0}^{n}, P_{1}^{n}, J^{n}, [J, P_{0}], [J, P_{1}]$ and $J^{i} (P_{0}^{i} P_{1}^{- i})^{2}$ for $1 \leq i \leq ⌊ n /2 ⌋$ .

Statement echo

Source clause	Lean counterpart	Fidelity
The Section 5 presentation	`P0`, `P1`, `J`, `rels`, `G`	The relators are words equal to the identity; the negative exponent uses the integer cast of the natural index.
Every $n \geq 2$	`claim` quantifies over natural `n` with `2 ≤ n`	No further assumption on $n$ .
Small cyclic factors	`L` is `Multiplicative (ZMod (2*n))` times the functions from `Fin (n-2)` to `Multiplicative (ZMod 2)`	The independent involutions have zero-based indices.
An explicit semidirect product	`alpha` and the `MulEquiv` in `claim`	The action is the binding action in the definition comment on #16204.
A product characterization	`result : claim`	An actual multiplicative equivalence, rather than an order comparison.

The binding comment fixes cyclicHom, s, t, liftL, ts, u, e, step, stepAut and alpha. Here t n i represents the source’s $t_{i + 1}$ , and u n k uses one-based indices. In particular, $u_{n - 1} = s^{n} \prod_{i = 1}^{n - 2} t_{i}$ , while $u_{k} = 1$ outside the indicated range. For $n = 2$ , $u_{1} = s^{2}$ . The action below two is trivial; the claim has no conclusion for those values.

Motivation

The settling declaration is D5/S3/Quantum/Algebra/GeneralizedCHSHGroupDecomposition.result. It supplies a uniform structural answer to the source’s further-work question. The source’s Theorem 5.7 identifies the presented group with its observable matrix group; the new equivalence characterizes the presented group using cyclic and elementary abelian factors.

The literature locator and quoted presentation are in the Library note. The external question is preregistered in #16204; there is no digestion atom.

Gap

The source gives four small cases and the order formula, without the displayed all- $n$ product decomposition. The kernel-checked equivalence closes this structural question for $n \geq 2$ . Simplification for odd $n$ and explicit correspondences to the source’s even small-case decompositions remain open here.

Route

Write $L_{n} = C_{2 n} \times C_{2}^{n - 2}$ , with generator $s$ of the first factor and independent involutions $t_{1}, \dots, t_{n - 2}$ . Set $t_{n - 1} = s^{n} \prod t_{i}$ , $e_{k} = s t_{k}$ and $e_{0} = e_{n} = s$ . The cyclic generator acts by $s \mapsto e_{1}$ and $t_{i} \mapsto e_{i + 1} e_{1}^{- 1}$ . The orbit calculation shows that this automorphism has period dividing $n$ .

The forward map sends $P_{0}$ to the outer cyclic generator, $P_{1}$ to $s$ times that generator, and $J$ to $s^{2}$ . In the presented group, the elements $δ_{i} = P_{0}^{i} P_{1}^{- i}$ commute. Their subgroup supports the inverse map from $L_{n}$ . Compatibility with conjugation by $P_{0}$ extends it to the semidirect product. The two composites fix the generators, yielding the multiplicative equivalence.

Falsifier

A mismatch of the source relators or the binding action would invalidate the interpretation of the settlement. The exact Lean conclusion is the preregistered claim, and the action data are fixed by the linked definition comment. A numerical order match alone does not prove this conclusion.

Evidence

Kernel-checked. D5.S3.Quantum.Algebra.GeneralizedCHSHGroupDecomposition.result proves claim. Its axiom closure is contained in {propext, Classical.choice, Quot.sound}. The private helper identities named below belong to the same compiled module; they are supporting proof steps, not additional public settlements.

Computed. The experiment is the pinned experiment directory. Run python3 check.py in that directory. Exit code: 0; result: ALL_OK. The SHA-256 of check.py is be0fdfe9abe9f800c0805d4b40c48fd5c8dd96abd75ec3f12b8642d9d3b384b1. The exact tested scope is $n = 2, \dots, 9$ . The matrix-group orders are respectively $8, 36, 128, 400, 1152, 3136, 8192, 20736$ . Within that scope the program verifies the factor-coordinate bijection, the dependent-involution identity, the conjugation formulas and the trivial intersection with the shift subgroup. It does not compute the odd- $n$ simplified decomposition or explicit isomorphisms to the authors’ $G_{4}, G_{6}$ forms.

Escape audit unfinished. The public audit targets are D5.S3.Quantum.Algebra.GeneralizedCHSHGroupDecomposition.result and the compiler-generated congruence theorems D5.S3.Quantum.Algebra.GeneralizedCHSHGroupDecomposition.cyclicHom.congr_simp and D5.S3.Quantum.Algebra.GeneralizedCHSHGroupDecomposition.stepAut.congr_simp. The latter two are compiler consequences of the definitions, not additional authored mathematical conclusions. There is no delivered Reg mirror or validated registration. #16351 identifies the missing dependent-family reconstruction, exact bridge, enrolled readout, observational-dependence evidence, and variation and sensitivity proofs.

The public cyclic evaluation helper D5.S3.Quantum.Algebra.GeneralizedCHSHGroupDecomposition.cyclicHom_int is consumed by this proof and by the encoder settlement in #19189. Its four-slot audit is unfinished under #19215, which identifies the missing dependent-family realization, reconstruction and equivalence bridges, enrolled readout, variation, sensitivity and observational dependence. No validated registration is claimed for this helper.

Triage

What the settlement shows

Item	Status and evidence
A commuting normal subgroup isomorphic to $L_{n}$ , generated by the images of $P_{0}^{i} P_{1}^{- i}$	Proved. Kernel-checked `delta_commute` and `K_isMulCommutative` establish commutation; `result`, `forward_ks`, `backL_t` and the inverse identities supply the factor identification. Normality and equality with the generated subgroup follow by the prose derivation below.
$s = P_{1} P_{0}^{- 1}$ has order $2 n$ , and $s^{2} = J$	Proved. Kernel-checked `ks_coe`, `ks_square_z`, `backL_s` and `forward_backward` identify the element and its square. Exact order is the prose consequence of the factor identification below; `ks_order` alone states the upper bound.
$t_{n - 1} = s^{n} t_{1} \dots t_{n - 2}$ supplies cyclic wrap-around	Proved, kernel-checked. `u_last`, `prod_e`, `step_e_last`, `step_e` and `step_period` establish the endpoint and period identities used to construct `alpha`.
Odd- $n$ simplification $G_{n} ≅ C_{n} \times (V_{n} ⋊ C_{n})$ , with $V_{n}$ the even-weight subspace of $C_{2}^{n}$	Open. Neither formalized nor computed by the experiment. The source gives $G_{3} ≅ Z_{3} \times A_{4}$ ; no uniform simplified-form settlement is claimed.
Correspondence with the authors’ $G_{4}$ and $G_{6}$ forms	Open for the explicit isomorphisms. Computed only for the orders $128$ and $1152$ in the pinned experiment.
Exact finite readings	Computed for $n = 2, \dots, 9$ by the experiment entry in Evidence; no wider computational scope is claimed.
Literature screen	No all- $n$ product decomposition was found in the screened citing works and later author papers recorded in #16204. Completeness is ASSUMED-UNVERIFIED; the Firecrawl Google Scholar query returned HTTP 402.

For the first item, let $F$ be the forward equivalence used by result, and let $K$ be the subgroup generated by all $δ_{i}$ . Each $F (δ_{i})$ has trivial outer cyclic coordinate, so $F (K)$ lies in the copy of $L_{n}$ . Conversely, ks_coe and forward_ks identify preimages of $s$ and each $e_{i}$ inside $K$ ; backL_t identifies preimages of every independent $t_{i}$ there. These elements generate $L_{n}$ , so $F (K) = L_{n}$ . This copy is the kernel of the projection to $C_{n}$ , hence normal; restricting $F$ gives $K ≅ L_{n}$ . This is a derivation from the constructed maps, not a separate Lean normality declaration.

For the second item, ks_coe at zero identifies $P_{1} P_{0}^{- 1}$ and ks_square_z gives its square $J$ . Under $F$ it is $(1, 1)$ in multiplicative notation in $C_{2 n} \times C_{2}^{n - 2}$ , where the first component is the additive residue $1$ modulo $2 n$ . That residue has exact order $2 n$ , and isomorphisms preserve order. The exact-order assertion here is derived in prose; the module’s private ks_order verifies its $2 n$ -th power is one.

The decisive mechanism is the uniform cyclic orbit together with mutually inverse generator maps. It covers every $n \geq 2$ , including the empty independent-involution factor at $n = 2$ . The source’s presentation and Theorem 5.7 remain applicable; its strategies and order computation require no replacement. The neighbouring odd and even classifications above are additional questions, rather than prerequisites of this equivalence.

ASSUMED-UNVERIFIED

The citation-index and later-author screens are not an exhaustive literature proof. Their producer and scope are recorded in #16204; a Firecrawl Google Scholar query returned HTTP 402. No originality or exhaustive absence claim follows from that screen.

The four-slot escape audit remains unfinished under #16351. Its issue link supplies disclosure, not a registration proof. The uniform odd- $n$ simplification and the explicit $G_{4}, G_{6}$ correspondences are not established by this delivery.

Keyboard shortcuts

trureturing — Discovering truth