abbrev 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)

  34abbrev neutralityScore := SpiralField.neutralityScore

Definition body.

  35
  36/-- Shift lemma for the neutrality score: shifting the start index shifts the sampled window. -/

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

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

Lean names referenced from this declaration's body.

score in IndisputableMonolith.Ethics.CostModel decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
score in IndisputableMonolith.Measurement decl_use
neutralityScore in IndisputableMonolith.Spiral.SpiralField decl_use