implications
plain-language theorem explainer
The definition supplies a four-item list that records how the 8-tick phase rotation accounts for the appearance of the imaginary unit, oscillatory waves, unitary evolution, and the fermion sign change. A physicist examining the origin of complex numbers inside quantum mechanics would reference the list when tracing i back to discrete phase steps. The entry is assembled by direct enumeration of the four consequences already obtained from the phase map kπ/4.
Claim. The list records: $i^2 = -1$ follows from a 4-tick rotation equaling a half-turn, waves arise from continuous accumulation of phase, unitarity is preserved by phase conservation, and fermions change sign under a $2π$ rotation that equals eight ticks.
background
Module MATH-001 sets the local goal of recovering $i^2 = -1$ from the Recognition Science 8-tick structure. The upstream EightTick.phase definition supplies the phases $kπ/4$ for $k = 0,…,7$, which are exactly the 8th roots of unity. Constants.tick fixes the fundamental time quantum $τ_0 = 1$, so that four ticks correspond to a $π$ rotation and eight ticks to a full $2π$ turn. The module documentation states that rotation by two ticks multiplies by $i$ while rotation by four ticks multiplies by $-1$.
proof idea
The declaration is a direct definition that builds the List String by writing the four explanatory sentences. No lemmas are applied; the body simply enumerates the consequences already derived from the phase map and the tick unit.
why it matters
The entry condenses the main physical payoffs of the 8-tick octave (T7 in the forcing chain) for complex analysis and quantum mechanics. It sits inside the MATH-001 development whose target is to show that the imaginary unit is the generator of those discrete rotations. The list therefore bridges the algebraic structure of the phase group to the appearance of $i$ in the Schrödinger equation and in Euler’s formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.