eight_tick_forces_temporal
plain-language theorem explainer
The theorem confirms that the eight-tick cycle forces the spatial dimension D to obey 2^D = 8. Researchers deriving the curvature correction in the fine-structure constant would cite it to fix the temporal contribution to the five-dimensional configuration space. The proof is a direct computational decision that evaluates the equality once D is set by the forcing chain.
Claim. The spatial dimension $D$ satisfies $2^D = 8$.
background
The module derives the curvature correction term $-103/(102π^5)$ by integrating over a five-dimensional configuration space: three spatial dimensions from the cubic lattice, one temporal dimension from the eight-tick cycle, and one dual-balance dimension from the conservation constraint σ = 0. Each angular integration contributes a factor of π, producing the observed π^5. The eight-tick phase is given by $kπ/4$ for $k=0,…,7$, yielding period $2π$ and cycle length eight. Upstream, Dimension tracks length, time, and mass exponents while the EightTick phase definition supplies the periodic structure used in the temporal count.
proof idea
The proof is a one-line term wrapper that applies native_decide to verify the numerical equality 2^D = 8 for the dimension value fixed by the eight-tick octave.
why it matters
This declaration supplies the temporal dimension required for the five-dimensional integration that produces the π^5 denominator in α^{-1} = 4π·11 - f_gap - 103/(102π^5). It implements the eight-tick octave (T7) and the spatial dimension D = 3 (T8) from the unified forcing chain, directly enabling the curvature-space counting in the module. No downstream theorems are listed, but the result closes the temporal component of the phase-space ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.