D3_has_2D_faces
plain-language theorem explainer
At dimension three the vertex count per face equals four. This confirms the two-dimensional character of the facets used in the muon-to-tau generation step. Researchers deriving the discrete correction term in lepton mass ladders would cite the result. The proof is a direct one-line application of the dimension-three specialization of the face-vertex count.
Claim. In three dimensions the number of vertices per two-dimensional face is four: $V_f = 4$.
background
The module derives the dimension-dependent correction Δ(D) = D/2 from cube geometry without calibration to observed masses. It contrasts the e→μ step, which uses the continuous solid angle 4π, with the μ→τ step, which uses the discrete vertex count per facet as the measure. Upstream results supply the vertex count of the D-cube as 2^D and establish that each facet is anchored by 2^{D-1} vertices, making the vertex count the discrete analog of the solid angle.
proof idea
The proof is a one-line wrapper that applies the specialized face-vertex count at D=3.
why it matters
This result supplies the D=3 case required for the facet-mediated correction in the tau step. It supports the geometric analogy in which the contribution per facet is F/V with V=4, feeding the overall derivation of Δ(D)=D/2. The declaration touches the framework landmark that D=3 is forced by the eight-tick octave and closes the discrete/continuous duality for the second lepton generation step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.