fFace
plain-language theorem explainer
fFace(n) supplies the multiplicative factor (11/12)^n for optional face corrections inside voxel summations. Researchers expanding sigmaN for QCD or QED approximations cite it when the useFace flag is active. The definition consists of a direct power expression with no lemmas or reductions required.
Claim. $f(n) = (11/12)^n$ for natural number $n$.
background
The VoxelWalks module defines auxiliary scaling functions that combine with sigmaCore inside sigmaN. fFace sits alongside fEye and fHalfVoxel as a conditional multiplier toggled by Boolean flags. The local setting supports the explicit product expansions shown in sigmaN_QED_expand and sigmaN_QCD_expand.
proof idea
The declaration is a direct definition of the power expression; no lemmas or tactics are applied.
why it matters
fFace is referenced by sigmaN and the two expansion lemmas sigmaN_QED_expand and sigmaN_QCD_expand. These lemmas unfold the face term when the flag is set, enabling concrete numerical evaluations of the summation under different approximation choices. It belongs to the discrete auxiliary layer that interfaces with sibling constants such as A2 and phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.