ohGroupOrder_eq_6_times_8
plain-language theorem explainer
The theorem states that the order of the Oh group equals 48, which is identical to 6 multiplied by 2 to the third power. Materials scientists applying Recognition Science to crystal symmetries would cite this to confirm the canonical cubic group order matches the eight-atom Q3 sublattice size. The proof is a one-line computational decision that directly evaluates the numerical identity.
Claim. The octahedral group Oh has order 48, equivalently expressed as $6$ times $2$ raised to the power $3$.
background
In the Recognition Science treatment of materials, five canonical classes (metals, ceramics, polymers, composites, semiconductors) correspond to configuration dimension D = 5. Crystal symmetries map to Q3 sublattices with 8 atoms, matching 2^D for D = 3 spatial dimensions. The Oh group serves as the canonical cubic symmetry group whose order is set to 48, aligning with the eight-tick octave structure of period 2^3 from the forcing chain T7.
proof idea
The proof is a one-line wrapper that applies the decide tactic to verify the numerical equality directly from the upstream definition of ohGroupOrder as 48.
why it matters
This equality is used by the materialsScienceCert definition to certify the five material classes and Oh group order. It fills a computational step linking to framework landmarks T7 (eight-tick octave) and T8 (D = 3), where 2^3 gives the atom count per sublattice. No open questions are touched; the result closes the numerical identity without new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.