pith. machine review for the scientific record. sign in
def definition def or abbrev high

implications

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 178def implications : List String := [

proof body

Definition body.

 179  "i² = -1 from 4 ticks = π rotation",
 180  "Waves from continuous phase accumulation",
 181  "Unitarity from phase conservation",
 182  "Fermion sign from 2π rotation = 8 ticks = 1"
 183]
 184
 185/-! ## The 8th Roots of Unity -/
 186
 187/-- The 8th roots of unity ζ_k = e^{2πik/8} for k = 0,...,7.
 188
 189    These are exactly the 8-tick phases!
 190    They form a group under multiplication (cyclic group Z₈). -/

depends on (14)

Lean names referenced from this declaration's body.