English
The index chainTopIdx selects, when independence holds, an index k such that the corresponding root is in the admissible range; otherwise it returns j.
Русский
Индекс chainTopIdx выбирает, если независимость сохраняется, некоторый индекс k такой, что корень удовлетворяет требуемому диапазону; иначе возвращает j.
LaTeX
$$$$ \text{chainTopIdx} \;: \; ι \to ι \quad\text{is defined by }\; \text{if } \text{LinearIndependent}(R, [P.root i, P.root j]) \text{ then } k \text{ with } P.root(j) + k P.root(i) \in \operatorname{range}P.root \text{ else } j.$$$$
Lean4
/-- If `α = P.root i` and `β = P.root j` are linearly independent, this is the index of the root
`β + p • α` where `β - q • α, ..., β - α, β, β + α, ..., β + p • α` is the `α`-chain through `β`.
In the absence of linear independence, it takes a junk value. -/
def chainTopIdx : ι :=
if h : LinearIndependent R ![P.root i, P.root j] then
(P.root_add_nsmul_mem_range_iff_le_chainTopCoeff h).mpr (le_refl <| P.chainTopCoeff i j) |>.choose
else j
