cube_edges_count
plain-language theorem explainer
The definition supplies the edge count of a D-dimensional hypercube as D times 2 to the power of D minus 1. PMNS mixing-angle derivations cite it to extract the integer 10 for the solar radiative correction from 3-cube topology. The implementation is a direct combinatorial formula with no lemmas or tactics required.
Claim. The number of edges in a $D$-dimensional hypercube is given by $E(D) = D · 2^{D-1}$.
background
The PMNS Radiative Correction Derivation module obtains the integer coefficients 6, 10 and 3/2 for atmospheric, solar and Cabibbo corrections from the topology of the 3D cubic ledger. A 3-cube supplies 12 edges and 6 faces; the solar sector subtracts the two active modes to leave the factor 10. Upstream structures from SpectralEmergence record that the 3D voxel ledger forces exactly three generations and 24 chiral fermions via the relation $D × 2^D$.
proof idea
The declaration is a direct definition that encodes the standard hypercube edge-counting formula.
why it matters
It supplies the edge count required by solar_coefficient and by CorrectionDerivationCert, which certifies that the integers 6, 10 and 3/2 are forced by 3-cube topology rather than free parameters. The construction sits inside the Recognition framework at the point where T8 fixes D = 3 and the eight-tick octave closes the ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.