cube_edges_count
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not evaluate for non-positive or non-integer D.
- Does not incorporate defects or J-cost weights on the edges.
- Does not prove the formula from the Recognition forcing chain; it assumes the standard hypercube combinatorics.
Lean usage
def solar_coefficient : ℕ := cube_edges_count 3 - 2formal statement (Lean)
66def cube_edges_count (D : ℕ) : ℕ := D * 2^(D-1)
proof body
Definition body.
67
68/-- Number of faces in a D-cube: F = D(D-1) · 2^(D-2) for D ≥ 2 -/