Q3_vertices
plain-language theorem explainer
The 3-cube Q3 has exactly eight vertices, matching the eight ticks in the Gray cycle. Researchers deriving the recognition wavelength from the J_bit = J_curv balance in Planck-scale matching cite this to fix the vertex count for curvature packet distribution. The proof is a direct reflexivity reduction on the general hypercube vertex formula cube_vertices(D) := 2^D evaluated at D = 3.
Claim. The three-dimensional hypercube satisfies $V(Q_3) = 8$.
background
The Planck-Scale Matching module derives lambda_rec from equating bit cost J_bit to curvature cost J_curv(lambda) = 2 lambda^2. This J_curv arises by distributing a ±4 curvature packet over the vertices of Q3 and normalizing via Gauss-Bonnet on the sphere. The upstream definition cube_vertices(D : Nat) := 2^D supplies the vertex count for any dimension; the same function appears in AlphaDerivation. LambdaRecDerivation quotes the doc-comment that Q3 has eight vertices (= eight ticks in the Gray cycle) to normalize total curvature as 4 pi.
proof idea
One-line term proof that applies reflexivity directly to the definition cube_vertices(3) = 2^3, which evaluates to 8.
why it matters
This supplies the first step (Q3_vertices = 8) inside the GDerivationChain structure that reaches G = lambda_rec^2 c^3 / (pi hbar). It instantiates the eight-tick octave (T7) required for the curvature functional in the forcing chain and anchors the lambda_rec ≈ 0.564 l_P result of Conjecture C8. Downstream uses include kappa_normalized and total_curvature_gauss_bonnet in LambdaRecDerivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.