fEye
plain-language theorem explainer
fEye supplies the eye factor (1/2)^n for natural n inside the sigmaN assembly for voxel walks. Researchers expanding sigmaN for A2_QED or A2_QCD cite it when the useEye flag is active. The declaration is a direct real-valued power with no lemmas or steps.
Claim. $f(n) = (1/2)^n$ for $n$ a natural number, serving as the eye multiplier in the sigmaN product.
background
The VoxelWalks module assembles sigmaN from a sigmaCore base multiplied by three optional real factors controlled by boolean flags: fEye, fHalfVoxel, and fFace. These factors encode geometric contributions from eye, half-voxel, and face elements in discrete walks. The module imports only Mathlib and defines all three as functions from natural numbers to reals; no prior lemmas are required.
proof idea
Direct definition that equates the function to the real power expression (1/2)^n with no tactics, reductions, or referenced lemmas.
why it matters
fEye is invoked inside sigmaN and therefore appears in the downstream lemmas sigmaN_QED_expand and sigmaN_QCD_expand, which unfold the product for the respective A2 values. It supplies the damping term that completes the explicit sigmaN expressions used in Recognition Science voxel calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.