English
For a state u in XgcdType, define the vector vp as the product of the 2×2 matrix with the 2-vector, after augmenting entries by 1: w, x, y, z, a, b are filled from u, with a = ap + 1, b = bp + 1, w = wp + 1, z = zp + 1. Then vp is the pair (sp, tp) such that the product corresponds to the vector v = (sp + 1, tp + 1).
Русский
Для состояния u в XgcdType определить вектор vp как произведение матрицы на вектор после дополнения на 1: элементы w, x, y, z и возмещения a = ap + 1, b = bp + 1, а также w = wp + 1, z = zp + 1 задаются компонентами u. Тогда vp = (sp, tp) задаёт вектор v = (sp + 1, tp + 1).
LaTeX
$$$vp(u) = \\bigl( u.wp + u.x + u.ap + u.wp \\cdot u.ap + u.x \\cdot u.bp,\; u.y + u.zp + u.bp + u.y \\cdot u.ap + u.zp \\cdot u.bp \\bigr).$$$
Lean4
/-- The map `v` gives the product of the matrix
[[w, x], [y, z]] = [[wp + 1, x], [y, zp + 1]]
and the vector [a, b] = [ap + 1, bp + 1]. The map
`vp` gives [sp, tp] such that v = [sp + 1, tp + 1].
-/
def vp : ℕ × ℕ :=
⟨u.wp + u.x + u.ap + u.wp * u.ap + u.x * u.bp, u.y + u.zp + u.bp + u.y * u.ap + u.zp * u.bp⟩
