lemma proved decidable or rfl

`neutralityScore_succ`

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

formal statement (Lean)

  37lemma neutralityScore_succ (w : ℕ → ℝ) (t0 : ℕ) :
  38    neutralityScore w (t0 + 1) = (Finset.range 8).sum (fun k => w (t0 + 1 + k)) := by

Decided by rfl or decide.

  39  rfl
  40
  41/-- Simple 8-periodicity predicate (for “8-phase schedules”). -/

Lean names referenced from this declaration's body.

neutralityScore in IndisputableMonolith.Flight.Schedule decl_use
phase in IndisputableMonolith.Foundation.EightTick decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
phase in IndisputableMonolith.NumberTheory.RiemannHypothesis.Wedge decl_use
neutralityScore in IndisputableMonolith.Spiral.SpiralField decl_use