edges_per_face
plain-language theorem explainer
The definition of edges per face in the D-dimensional cube Q_D sets this quantity to 2 raised to (d minus 1). Researchers deriving particle baselines from hypercube combinatorics cite this to fix the quark rung at 4 when D equals 3. The implementation is a direct power expression with no additional lemmas required.
Claim. The number of edges per face of the $D$-dimensional hypercube $Q_D$ equals $2^{D-1}$.
background
In the BaselineDerivation module, baseline rung integers for masses are obtained from the combinatorics of the 3-cube Q_3. The function edges_per_face computes a standard count: each face of Q_D is itself a (D-1)-cube whose edges number 2^{D-1}. This replaces earlier boundary assumptions with derivations from D=3 alone, as listed in the module table for B-12 quark baseline and B-25 color offset.
proof idea
This is a one-line definition that directly encodes the combinatorial formula for edges per face in the D-cube.
why it matters
This definition supplies the common value 4 used by quark_baseline and color_offset, which in turn match the anchor integers r_down and r_up. It fills the B-12 and B-25 slots in the module's derivation table, tracing all mass baselines to the single input D=3 from the eight-tick octave in the forcing chain. No open questions remain for this quantity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.