English
The function simplicialEvalσ measures a cumulative evaluation by decrementing when encountering smaller indices, mirroring a right-to-left sweep.
Русский
Функция simplicialEvalσ измеряет накопленную оценку, уменьшая значение при встрече меньших индексов.
LaTeX
$$$\\\\text{simplicialEvalσ}:\\\\mathbb{N}^* \\\\to \\\\mathbb{N},\\quad (a :: L) \\\\mapsto \\\\text{if } a < \text{simplicialEvalσ}(L) j \\\\text{then } \\\\text{simplicialEvalσ}(L) j - 1 \\\\text{else } \\\\text{simplicialEvalσ}(L) j.$$$
Lean4
/-- `simplicialEvalσ` is a lift to ℕ of `(toSimplexCategory.map (standardσ m L _ _)).toOrderHom`.
Rather than defining it as such, we define it inductively for less painful inductive reasoning,
(see `simplicialEvalσ_of_isAdmissible`).
It is expected to produce the correct result only if `L` is admissible, and values for
non-admissible lists should be considered junk values. Similarly, values for out-of-bonds inputs
are junk values. -/
def simplicialEvalσ (L : List ℕ) : ℕ → ℕ := fun j ↦
match L with
| [] => j
| a :: L => if a < simplicialEvalσ L j then simplicialEvalσ L j - 1 else simplicialEvalσ L j
