twoCubeUniversalityCert
plain-language theorem explainer
Recognition Science researchers cite this certificate to confirm that DFT modes, Q3 vertices, Pauli elements, and tick phases each realize exactly eight elements under the two-cube count. The structure also records that any two such domains are equicardinal and that their product yields cardinality 64 with the supporting identities 64 = 8*8 and 64 = 2^6. Construction occurs by direct field assignment of the four domain theorems together with the equicardinality and product lemmas.
Claim. A certificate asserting that DFTMode, Q3Vertex, PauliElement, and TickPhase each satisfy the two-cube count predicate, that any two finite types satisfying the predicate are equicardinal, that the cardinality of the product DFTMode × Q3Vertex equals 64, and that 64 equals both 8 × 8 and 2^6.
background
The CrossDomain.TwoCubeUniversality module collects instances of the count 8 = 2^3 across domains as the maximal-periodic structure for spatial dimension D = 3. The predicate HasTwoCubeCount A holds precisely when the finite type A has cardinality 8, as shown by the decide tactics in the upstream theorems dft_has_2cube, q3_has_2cube, pauli_has_2cube, and tick_has_2cube. The structure TwoCubeUniversalityCert bundles these four instances with the equicardinality statement that any two such types have equal cardinality, the product theorem showing 8 × 8 = 64, and the identity 64 = 8 × 8 ∧ 64 = 2^6.
proof idea
The definition constructs the certificate by direct substitution of upstream results into each field of the TwoCubeUniversalityCert structure. It assigns dft_has_2cube to the dft field, q3_has_2cube to the q3 field, pauli_has_2cube to the pauli field, and tick_has_2cube to the tick field. The equicardinality field receives the lambda that invokes two_cube_equicardinal, the pair field receives dft_q3_product, and the identities field receives sixtyfour_identities.
why it matters
This definition serves as the central certificate for the C14 claim that the count 8 = 2^3 appears uniformly across domains as the maximal periodic structure in D = 3. It assembles the individual domain proofs into a single object supporting the Recognition Science eight-tick octave and the derivation of three spatial dimensions. The construction directly documents the cross-domain identity without introducing new axioms or sorries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.