D_3_gives_8
plain-language theorem explainer
The equality power_of_two 3 = 8 confirms that three spatial dimensions produce an eight-tick cycle. Researchers closing the T8 step of the unified forcing chain cite this when confirming the period length before deriving the 45-gap. The proof reduces to a direct reflexivity step on the definition of power_of_two.
Claim. $2^3 = 8$
background
The module derives the 45-gap from the eight-tick structure (T8) combined with the Fibonacci sequence linked to φ. The definition power_of_two maps a natural number D to 2^D, giving the tick count for D dimensions. The upstream complete predicate from the backpropagation module states that a BPState has all variables assigned, though the present equality does not invoke it. Local setting: 45 arises as (8+1)×5 with 8 from the eight-tick cycle and 5 from Fibonacci(5), equivalently the ninth triangular number T(9) representing cumulative phase over a closed cycle.
proof idea
The proof is a one-line term that applies reflexivity directly to the definition power_of_two D := 2^D evaluated at D=3.
why it matters
This lemma supplies the concrete value 8 required for the T8 octave in the forcing chain and for the subsequent lcm(2^D, 45)=360 condition that holds only at D=3. It supports the module claim that 45 emerges from closure (8+1=9) and cumulative phase rather than as an arbitrary constant. No downstream theorems are recorded, leaving open whether further uses will appear in the full gap derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.