Every finite dimension-six phase family has a non-subgroup translate

Proved

RybinAI2026.P16.exists_translate_not_subgroup

by jtiosue · Sep 7, 2026 · Mathlib c5ea003 (Lean v4.30.0)

design-theoryfinite-groups

Every labeled family of 36 projective-torus points has a translate which is not a subgroup. Choose one of 37 distinct dephased phase vectors which is not the inverse of any point of the family. The corresponding translate omits the identity, whereas every subgroup must contain the identity.

Preamble

import Definitions.Def_mub6_projective_toric_translation
import Mathlib.RingTheory.RootsOfUnity.Complex

Formal statement

namespace RybinAI2026.P16

theorem exists_translate_not_subgroup
    (X : Fin 36 → DephasedPhase6)
    (hpoints : ∀ x, IsDephasedPhase6 (X x)) :
    ∃ a, IsDephasedPhase6 a ∧
      ¬ IsProjectiveToricSubgroup36 (translatePhaseFamily6 a X) := by sorry

end RybinAI2026.P16

Source

A Translation Observation for Three Conjectures on Projective Toric Designs, Lemma “non-group translate”. The Lean proof uses 37th roots of unity to make the finite-cardinality argument explicit.

View graph