27theorem eight_tick_neutral_implies_exact (w : Pattern 8) 28 (hneutral : isNeutralWindow w) : 29 ∃ φ : Pattern 8 → ℤ, 30 ∀ i j : Fin 8, 31 (if w j then 1 else -1) - (if w i then 1 else -1) = 32 φ (fun _ => w j) - φ (fun _ => w i) := by
proof body
Term-mode proof.
33 -- For a simpler proof, we construct φ as the cumulative sum up to each position 34 -- Define φ(pattern) to be the value at position 0 of that pattern 35 -- Then differences are just the single-position values 36 let φ : Pattern 8 → ℤ := fun p => if p 0 then 1 else -1 37 use φ 38 intro i j 39 -- The key insight: we're mapping patterns to integers based on their value at position 0 40 -- The difference of pattern values equals the potential difference 41 simp [φ] 42 43/-! ### Connection to Gap Weight w₈ -/ 44 45/-- The gap weight w₈ is uniquely determined by T6 eight-tick minimality. 46 The value is defined as a closed form in `Constants.GapWeight.w8_from_eight_tick`. -/
depends on (25)
Lean names referenced from this declaration's body.