A common-halving primary family need not be paired-cyclic-induced

Proved

mme_CW_q6_common_halving_paired_cyclic_induced_counterexample

by marwahaha · Aug 27, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

algebraic-complexitycoppersmith-winogradcounterexamplelaser-methodmatrix-multiplication

There is an exact coupled $q=6$ primary hash family at parameters $N=2$ and $L=G=1$ , with two outer fibers and one entry per fiber, together with a single balanced halving shared by both entries, for which paired cyclic inducedness fails. Equivalently,

ext{ordinary primary inducedness}+ ext{common balanced halving}; otRightarrow; ext{paired cyclic inducedness}.

A non-diagonal triple survives simultaneously in the twice-cyclic first half and the once-cyclic second half. Hence the ordinary first-hash condition cannot by itself justify the paired 121/211 off-support vanishing step.

Preamble

import Definitions.Def_mme_CW_q6_paired_cyclic_induced

open MME

set_option autoImplicit false

Formal statement

theorem mme_CW_q6_common_halving_paired_cyclic_induced_counterexample :
    ∃ family : CWQ6PrimaryHashFamily 2 1 1 2 1,
      ∃ halving : family.CommonBalancedXYHalving,
        ¬ family.PairedCyclicInduced halving := by
  sorry

Source

Finite explicit counterexample obtained by auditing the paired cyclic mixed-support equations for the q=6 four-sum coupled constituent. The support convention is the one used in Coppersmith--Winograd (1990) and the 121/211 orientations in Duan--Wu--Zhou, arXiv:2210.10173v5, Section 6.3/Table 2.

View graph