cube_faces
plain-language theorem explainer
cube_faces supplies the face count of a D-dimensional cube through a piecewise match on D that returns 6 for D=3. Researchers deriving the PMNS mixing angles from Recognition Science cite it to fix the atmospheric coefficient at 6α in sin²θ₂₃ = ½ + 6α. The definition proceeds by direct case analysis with hardcoded low-D values and a closed polynomial-exponential expression for D ≥ 4.
Claim. The number of faces F(D) of a D-dimensional cube is given by F(D) = 0 for D ≤ 1, F(2) = 4, F(3) = 6, and F(D) = D(D-1)·2^{D-2} for D ≥ 4.
background
The PMNS Radiative Correction Derivation module obtains the integer coefficients 6, 10, and 3/2 in the mixing-angle predictions from the topology of the 3-cube. A 3-cube has exactly 6 faces; each face stands for a passive mode in the Z-projection, so the atmospheric radiative correction is proportional to this face count and equals 6α. The module states that all such integers derive from the cube topology of the 3D voxel ledger.
proof idea
The definition is supplied directly by pattern matching on the natural number D. Cases for D = 0, 1, 2, 3 return the constants 0, 0, 4, 6. The remaining case D = n+4 returns the expression (n+4)(n+3)·2^{n+2}, which is the standard hypercube face formula rewritten in terms of D.
why it matters
cube_faces feeds the theorem alpha_ingredients_from_D3_cube, which assembles the geometric seed factor, seam numerator, and seam denominator from D=3 cube geometry. It thereby grounds the coefficient 6 that appears in the atmospheric term of the PMNS predictions and aligns with the framework requirement of D = 3 spatial dimensions together with the eight-tick octave. The parent result establishes complete provenance of the magic numbers from the single 3-cube.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.