`BookProof.ChapterAttentionSink.sum_scoreSoftmax_sink_succ` (beta s0 : ℝ) (s : Fin m → ℝ) (i : Fin m) : ∑ j : Fin m, scoreSoftmax beta (Fin.cons s0 s) j.succ = 1

Initializing...

`BookProof.ChapterAttentionSink.sum_scoreSoftmax_sink_succ` (beta s0 : ℝ) (s : Fin m → ℝ) (i : Fin m) : ∑ j : Fin m, scoreSoftmax beta (Fin.cons s0 s) j.succ = 1 - sinkWeight beta · Prove2Me