physical_eight_tick
plain-language theorem explainer
The declaration confirms that the eight-tick ledger cycle equals eight when the spatial dimension is fixed at three. Researchers closing the Recognition Science derivation of spacetime geometry would cite this equality when linking the topological forcing argument to the octave period. The proof reduces directly to reflexivity on the definition of the eight-tick function evaluated at the physical dimension constant.
Claim. The eight-tick period forced by the physical spatial dimension satisfies $2^D = 8$, where $D$ is the constant three.
background
The Dimension Forcing module shows that spatial dimension is fixed at three by a combination of topological linking and synchronization requirements. EightTickFromDimension is the function that sends a dimension value D to the natural number 2^D, encoding the fundamental period of a simplicial ledger cycle. D_physical is the constant three, declared to be the RS-compatible spatial dimension.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of EightTickFromDimension at D_physical. Because the definition expands directly to 2 raised to the power of the dimension argument and the physical dimension equals three, the equality to eight follows by arithmetic evaluation.
why it matters
This equality realizes the T7 eight-tick octave (period 2^3) and T8 D=3 landmarks inside the forcing chain. It supplies the numerical anchor for downstream synchronization statements such as gap_45 and the lcm condition that produces the 360-degree rotation period. The primary justification remains the Alexander duality argument that nontrivial circle linking occurs only in three dimensions, independent of the cost-algebra or kinship-graph results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.