faceVertexCount_D3
plain-language theorem explainer
faceVertexCount_D3 establishes that each face of the three-dimensional cube has four vertices. Researchers deriving the tau lepton mass correction from cube geometry cite it to fix the discrete measure in the facet term. The proof is a direct computational evaluation of the general face vertex count definition at dimension three.
Claim. In three dimensions, the vertex count of each two-dimensional face of the cube is exactly four.
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 employs the continuous solid angle 4π as measure, with the μ→τ step, which employs the discrete vertex count per face as the analogous measure. The upstream definition states that the face vertex count for dimension D is 2 raised to the power of (D minus 1), counting the vertices of the (D-1)-hypercube that forms each face of the D-cube. The module doc notes that this vertex count serves as the discrete analog of the solid angle.
proof idea
The proof is a term-mode one-line wrapper that applies native_decide directly to the expression obtained from the definition of faceVertexCount at D=3, which reduces to 2^(3-1) and evaluates to 4.
why it matters
It is invoked by D3_has_2D_faces to confirm the two-dimensional structure of faces at D=3 and by discreteMeasure_eq_4 to equate the discrete measure to 4. This anchors the facet-mediated correction Δ = F/V in the first-principles derivation of Δ(D) = D/2 for the μ→τ lepton generation step, supporting the framework assignment of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.