sigmaCore
plain-language theorem explainer
sigmaCore supplies the base algebraic term 3^n a2^n over 2(1-2a2)^{2n-1} for n-step voxel scaling. It is referenced directly by the sigmaN definition and the QCD and QED expansion lemmas in the VoxelWalks module. The implementation is a direct algebraic definition using let bindings for the numerator and denominator.
Claim. $σ_{core}(n,a_2)=3^n a_2^n / [2(1-2a_2)^{2n-1}]$
background
The VoxelWalks module constructs scaling functions for voxel walks. sigmaCore supplies the central term that sigmaN multiplies by optional factors from fEye, fHalfVoxel, and fFace. Downstream lemmas sigmaN_QCD_expand and sigmaN_QED_expand substitute concrete A2 values and simplify the result after unfolding sigmaN. The module imports Mathlib for real arithmetic, and sigmaCore_n0 records the n=0 base case as 1/2.
proof idea
Direct definition. The body binds the numerator to 3^n * a2^n and the denominator to 2 * (1-2a2)^{2n-1}, then returns their ratio. No lemmas are applied.
why it matters
sigmaCore is the foundation for sigmaN and its QCD/QED expansions, which compute scaling factors in voxel models. These expansions feed into Recognition Science derivations that connect to the phi-ladder and the T7 eight-tick octave. It supplies the concrete algebraic core used when a2 is set to A2_QCD or A2_QED.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.