sigmaCore_n0
plain-language theorem explainer
The lemma establishes that sigmaCore evaluates to exactly one half at n=0 for arbitrary real a2. It supplies the base case for inductive constructions over the step index in voxel-walk recursions. The proof is a one-line wrapper that unfolds the definition and lets simp reduce the zero-exponent case arising from natural-number subtraction.
Claim. For any real number $a_2$, the function defined by $3^n a_2^n / [2(1-2a_2)^{2n-1}]$ (with the exponent formed by truncated natural-number subtraction) satisfies $n=0$ case equals $1/2$.
background
The VoxelWalks module introduces sigmaCore via the explicit ratio num/den, where num is $3^n a_2^n$ and den is $2(1-2a_2)^{2n-1}$. Because the exponent is computed in the naturals, the subtraction $2n-1$ yields 0 when n=0, so the power becomes 1 and the whole expression collapses to 1/2 independently of a2. This base case sits inside the module's treatment of discrete walks on a voxel lattice, consistent with Recognition Science's use of self-similar fixed points and the eight-tick octave.
proof idea
The proof is a one-line wrapper that unfolds sigmaCore and applies simp. The simplifier reduces the n=0 instance because the natural-number exponent 2*0-1 becomes 0, the power is 1, and the ratio is immediately 1/2.
why it matters
This lemma closes the n=0 base of the sigmaCore definition, which is the building block for the sigmaN and sigmaN_QED_expand constructions listed among the module siblings. It therefore anchors the initial step of any recursion that appears in voxel-walk calculations within the Recognition Science forcing chain (T0-T8) and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.