pith. machine review for the scientific record. sign in
theorem proved tactic proof

eight_tick_cancellation

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 219theorem eight_tick_cancellation :
 220    (Finset.range 8).sum (fun k => Complex.exp (2 * Real.pi * Complex.I * k / 8)) = 0 := by

proof body

Tactic-mode proof.

 221  -- Convert from the Foundation's proven theorem
 222  have h := Foundation.EightTick.sum_8_phases_eq_zero
 223  -- The Foundation uses phaseExp k = exp(I * k * π / 4) = exp(2πi * k / 8)
 224  have h_eq : ∀ k : Fin 8, Foundation.EightTick.phaseExp k =
 225      Complex.exp (2 * Real.pi * Complex.I * (k : ℕ) / 8) := by
 226    intro k
 227    unfold Foundation.EightTick.phaseExp Foundation.EightTick.phase
 228    congr 1
 229    push_cast
 230    ring
 231  rw [← Fin.sum_univ_eq_sum_range (fun k => Complex.exp (2 * Real.pi * Complex.I * k / 8))]
 232  have h2 : (∑ k : Fin 8, Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑k / 8)) =
 233            (∑ k : Fin 8, Foundation.EightTick.phaseExp k) := by
 234    congr 1
 235    ext k
 236    rw [h_eq k]
 237  rw [h2, h]
 238
 239/-! ## Summary -/
 240
 241/-- RS derivation of vacuum fluctuations:
 242
 243    1. **τ₀ discreteness**: Time has minimum interval
 244    2. **Uncertainty**: ΔE·Δt ≥ ℏ/2 → ΔE ≥ ℏ/(2τ₀)
 245    3. **Zero-point energy**: Vacuum is not empty
 246    4. **Casimir effect**: Measurable consequence
 247    5. **8-tick interference**: Explains small Λ
 248    6. **Virtual particles**: Transient ledger entries -/

depends on (24)

Lean names referenced from this declaration's body.