Chirality of the cubic enantiomorphic space-group pair

Proved

LeanEval.Geometry.SpaceGroupsProblem.SpaceGroupCatalog.spaceGroupCatalog_chiral_cubic

by Gabewhigham · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

crystallographydiscrete-geometrygroup-theory

Throughout, $E=\mathbb R^3$ , $G_1,\dots,G_{230}$ are the groups of the explicit catalogue spaceGroupCatalog (the group $G_n$ realises the space-group type with ITA number $n$ , and the second member of each enantiomorphic pair is the image of the first under the point inversion $x\mapsto -x$ ; see the definition SpaceGroupCatalog), and $G\sim_+G'$ means that some invertible affine map $\varphi$ of $E$ with $\det\varphi_{\mathrm{lin}}>0$ satisfies $\varphi G\varphi^{-1}=G'$ (AffOPEquivalent).

For the enantiomorphic pair $(n,n')=(212,213)$ ( $P4_{3}32$ / $P4_{1}32$ ),

G_n\not\sim_+G_{n'}.

(In Lean the catalogue is indexed from $0$ , so $G_n$ is spaceGroupCatalog (n-1).) These are the cubic cases of the statement that the eleven enantiomorphic pairs of space-group types are chiral, i.e. that the members of a pair are mirror images of each other but are not related by any orientation-preserving affine map.

Preamble

import Mathlib
import Definitions.Def_LeanEval_SpaceGroups_Definitions
import Definitions.Def_SpaceGroupCatalog

Formal statement

namespace LeanEval
namespace Geometry
namespace SpaceGroupsProblem
namespace SpaceGroupCatalog

theorem spaceGroupCatalog_chiral_cubic :
    ¬ AffOPEquivalent (spaceGroupCatalog 211) (spaceGroupCatalog 212) := by
  sorry

end SpaceGroupCatalog
end SpaceGroupsProblem
end Geometry
end LeanEval

Source

International Tables for Crystallography, Vol. A (T. Hahn, ed.), Section 1.4 and Table 1.4.1 (the 11 enantiomorphic pairs of space-group types); classification due to E. S. Fedorov (1891) and A. Schoenflies (1891).

View graph