two_cube_powerset_256
plain-language theorem explainer
Any finite type A satisfying the 2³-count condition has power set cardinality exactly 256. Cross-domain researchers cite this to confirm that the eight-element recognition cube scales uniformly to the Boolean lattice size 2^8. The proof reduces the claim to the hypothesis via a single rewrite then invokes a decision procedure.
Claim. Let $A$ be a finite type with $|A|=8$. Then the cardinality of the power set of $A$ is $256$.
background
HasTwoCubeCount is the predicate that a finite type T satisfies Fintype.card T = 2^3. The module establishes that this count 8 = 2³ = |F₂³| = |Q₃| recurs as the maximal-periodic structure for spatial dimension D = 3 across DFT modes, Pauli elements, 8-tick periods, and zincblende symmetries. Upstream results supply the definition of HasTwoCubeCount itself and the auxiliary A constants that appear in the broader forcing chain.
proof idea
One-line wrapper that rewrites Fintype.card_finset using the HasTwoCubeCount hypothesis then applies the decide tactic to close the equality.
why it matters
The result fills one instance of the module's structural claim that the 2³ cube count is universal for D = 3. It supports the Recognition Science landmarks T7 (eight-tick octave) and T8 (D = 3) by confirming the Boolean algebra size that underlies the listed domains. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.