Q3_vertices
plain-language theorem explainer
The declaration fixes the vertex count of the three-cube Q₃ at eight. Workers deriving the recognition length λ_rec from curvature balance cite this value to close the Gauss-Bonnet step in the non-circular chain. The assignment is a direct numerical constant that aligns with the eight-tick octave of the forcing chain.
Claim. The three-dimensional cube $Q_3$ has eight vertices.
background
The LambdaRecDerivation module constructs a non-circular derivation of the recognition length λ_rec. It starts from the normalized bit cost of one and equates it to the curvature cost 2λ² obtained from the Gauss-Bonnet theorem applied to Q₃. The vertex count enters as the multiplier that distributes the total curvature 4π over the cube's geometry, consistent with the eight-tick period in the unified forcing chain. Upstream results from SpectralEmergence and CubeSpectrum confirm that the hyperoctahedral group order for D=3 yields eight vertices, matching the combinatorial count 2^3.
proof idea
The definition directly assigns the natural number eight, matching the combinatorial expression 2^3 for the three-cube vertices. It functions as a one-line wrapper that supplies the constant to downstream structures such as GDerivationChain.
why it matters
This constant supplies the vertex count required by the GDerivationChain certificate, which links Q₃ geometry to the unique λ_rec root and the consequent definition of Newton's constant G. It instantiates the eight-tick octave (T7) and the spatial dimension D=3 from the forcing chain. The value propagates into kappa_normalized and the total curvature identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.