cube_vertices
plain-language theorem explainer
The type of maps from a 3-element index set into Booleans has cardinality 8, i.e. the 3-cube has 2³ vertices. Holography and alpha-derivation arguments cite this as the discrete count of the forced eight-tick cell in D=3. The proof is a one-line kernel decision of a finite cardinality identity.
Claim. The set of functions $\{0,1,2\}\to\{\mathrm{true},\mathrm{false}\}$ is finite of cardinality $8$. Equivalently, the $3$-dimensional hypercube has $2^3=8$ vertices.
background
In the PixelLocal module the forced discrete substrate in spatial dimension $D=3$ is the $8$-tick cell of the cube $2^3$. Recognition Science forces $D=3$ (T8) and the eight-tick octave (T7), so vertex configurations are Boolean assignments to three axes: each vertex is a map $\mathrm{Fin},3\to\mathrm{Bool}$.
Upstream constants modules already package the same count as a definition $\mathrm{cube_vertices}(D)=2^D$, with the $D=3$ specialization equal to $8$ used for Gray-cycle ticks and discrete Gauss–Bonnet on $\partial Q_3$. This theorem is the fintype form of that identity, proved by pure enumeration rather than by unfolding a power definition.
The local goal is combinatorial: boundary recognition pixels are cube faces (square plaquettes), and the vertex count $8$ anchors sector enumeration and curvature sums without continuum isotropy or Bekenstein–Hawking input.
proof idea
One-line tactic proof: decide closes the goal because both sides are concrete finite-type cardinalities. Lean’s kernel evaluates $\lvert\mathrm{Fin},3\to\mathrm{Bool}\rvert=2^3=8$ by exhaustive computation on a decidable fintype equality; no lemmas are invoked.
why it matters
This is the substrate-native statement that the forced eight-tick cell has eight vertices, matching T7 (eight-tick octave) and T8 ($D=3$). Downstream alpha work uses the count heavily: vertices_at_D3 and discrete Gauss–Bonnet on $Q_3$ rewrite total curvature as $8\times(\pi/2)=4\pi$; solid angle of $\partial Q_3$ is the same product; the curvature $J$-cost sums the quadratic $J$-Hessian coefficient over eight vertex deficits $\delta=\pi/2$ to obtain $\pi^2$.
U1 normalization and gauge-redundancy arguments also consume the cube vertex count when ranking cycles on the forced lattice. In PixelLocal the theorem sits beside the face count and the admissible-sector quotient that realizes the integer $4$ in $a_{\mathrm{pix}}=4\cdot H\cdot\ell_P^2$ as pure plaquette combinatorics. It does not itself link that sector count to the area coefficient; that remains an open panel gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.