pith. machine review for the scientific record. sign in
theorem other other high

sixtyfour_identities

show as:
view Lean formalization →

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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  97theorem sixtyfour_identities : 64 = 8 * 8 ∧ 64 = 2^6 := by decide

proof body

  98

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.