axis_perm_count_D3
plain-language theorem explainer
The theorem fixes the order of axis permutations in three dimensions at exactly six. Gauge-symmetry derivations from cube automorphisms cite it to set the S3 factor inside the hyperoctahedral group B3. The proof is a one-line native decision that evaluates the factorial definition directly.
Claim. The number of permutations of three coordinate axes equals six, i.e., $3! = 6$.
background
The GaugeFromCube module decomposes the automorphism group B3 of the 3-cube Q3 as (Z/2Z)^3 ⋊ S3 with |B3| = 48. Layer 1 isolates the S3 factor of axis permutations, which acts on the three face-pairs and supplies the Weyl group for the SU(3) color sector. The sibling definition axis_perm_count D returns Nat.factorial D, so the present theorem simply specializes this to D = 3.
proof idea
The proof is a one-line wrapper that applies native_decide to the equality axis_perm_count 3 = 6, which reduces at once to the built-in evaluation of 3!.
why it matters
The result pins the order of the S3 factor that the module identifies with the Weyl group of SU(3). It completes the Layer-1 count inside the three-layer decomposition of B3 and thereby supplies the numerical input for the gauge-group extraction stated in the module header. No downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.