vertices_are_anchors
plain-language theorem explainer
In three dimensions the number of vertices per two-dimensional face equals four, matching the power-of-two lattice anchor count. Researchers deriving the muon-to-tau mass step cite this to fix the discrete measure in the facet correction. The proof is a direct reflexivity on the definition of the vertex counting function.
Claim. In three spatial dimensions the number of vertices per two-dimensional face equals $2^{3-1}$.
background
The module derives the dimension-dependent correction Δ(D) = D/2 from cube geometry without calibration to observed masses. In this setting the facet-mediated correction for the μ→τ step uses facet count F = 2D together with the discrete measure given by vertices per facet. The vertex count functions as the discrete analog of the solid angle that appears in the electron-to-muon step via the continuous 4π factor.
proof idea
The proof is a one-line reflexivity that confirms the equality holds by the definition of faceVertexCount in the three-dimensional cubic lattice.
why it matters
This declaration anchors the discrete measure inside the tau lepton generation step, realizing the module goal of forcing Δ(3) = 3/2 from geometry alone. It supplies the concrete lattice count that converts facet number into the correction term Δ = F / V_facet and thereby closes the first-principles derivation of lepton mass ratios. The result sits downstream of the Normalization axiom and the active-edge count A, and it directly supports the Recognition Science claim that vertex count supplies the discrete counterpart to solid angle at D = 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.