sixtyfour_identities
plain-language theorem explainer
The declaration establishes the arithmetic identities 64 = 8 squared and 64 = 2 to the sixth. Researchers unifying 8-element structures across Recognition Science domains cite it when linking DFT modes, the recognition cube, and Pauli elements under a common cardinality. The proof reduces to a single decide tactic that confirms both equalities by direct computation.
Claim. $64 = 8^2$ and $64 = 2^6$.
background
The module collects instances of the count 8 = 2^3 across Recognition Science domains for spatial dimension D = 3. These include DFT-8 modes for fundamental harmonic decomposition, the Q3 vertex count in the recognition cube, the eight elements of the Pauli group, and the 8-tick fundamental period. The local setting proves that all such structures share the underlying identity of cardinality 2^3.
proof idea
The proof is a one-line wrapper that applies the decide tactic to verify the arithmetic identities directly.
why it matters
This identity anchors the TwoCubeUniversalityCert structure, which certifies HasTwoCubeCount for DFTMode, Q3Vertex, PauliElement, and TickPhase while enforcing equicardinality. It fills the C14 claim by grounding the eight-tick octave and D = 3 in the shared count 64 = 8 * 8 = 2^6. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.