edges_per_face_at_D3
plain-language theorem explainer
The result fixes the number of edges per face of the three-dimensional hypercube at exactly four. Researchers deriving fermion baselines in Recognition Science cite it when anchoring the quark rung and color offset to cube combinatorics. The proof evaluates the closed-form definition of edges per face at D = 3 via a decision procedure.
Claim. For the three-dimensional hypercube, the number of edges per face equals 4.
background
The function that counts edges per face of the D-dimensional hypercube is given by the closed form 2^{D-1}. This module converts several prior boundary assumptions about mass rungs into derived statements by specializing every quantity to the single input D = 3, the spatial dimension fixed by the eight-tick octave. The cube supplies the vertex, edge, face, and passive-edge counts that determine the baseline integers for leptons, quarks, and neutrinos.
proof idea
One-line wrapper that applies native_decide to the definition of edges per face specialized at D = 3.
why it matters
The theorem supplies the concrete value 4 that is invoked by the color-offset equality and the quark-baseline equality. It realizes item B-12 in the module derivation table, tracing the quark baseline directly to cube geometry at D = 3. In the framework it instantiates the spatial dimension fixed by T8 of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.