two_cube_powerset_256
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of any concrete A satisfying HasTwoCubeCount.
- Does not handle infinite types or types lacking decidable equality.
- Does not enumerate the 256 subsets explicitly.
- Does not connect the count to mass formulas or J-cost.
formal statement (Lean)
76theorem two_cube_powerset_256
77 {A : Type} [Fintype A] [DecidableEq A] (hA : HasTwoCubeCount A) :
78 Fintype.card (Finset A) = 256 := by
proof body
Term-mode proof.
79 rw [Fintype.card_finset, hA]; decide
80
81/-- DFT modes and Q₃ vertices are equinumerous. -/