def definition def or abbrev

`neutralityScore`

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

formal statement (Lean)

  51def neutralityScore (w : ℕ → ℝ) (t0 : ℕ) : ℝ :=

proof body

Definition body.

  52  (Finset.range 8).sum (fun k => w (t0 + k))
  53
  54/- Pitch slope proxy: multiplicative growth per full turn (Δθ = 2π).
  55   For r(θ)=r0·φ^{κ θ/(2π)}, the per-turn ratio equals φ^{κ}. -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

eightGateNeutral_shift_invariance in IndisputableMonolith.Flight.Schedule decl_use
neutralityScore in IndisputableMonolith.Flight.Schedule decl_use
neutralityScore_shift1_of_periodic8 in IndisputableMonolith.Flight.Schedule decl_use
neutralityScore_succ in IndisputableMonolith.Flight.Schedule decl_use

depends on (3)

Lean names referenced from this declaration's body.

multiplicative in IndisputableMonolith.Algebra.CostAlgebra decl_use
neutralityScore in IndisputableMonolith.Flight.Schedule decl_use
r0 in IndisputableMonolith.Masses.Anchor decl_use