Blind read-back of Def_ZengPryadko2019.lean

1. BinaryWord

For every type $\iota$, BinaryWord declares the type of all functions $x:\iota\to\mathbb Z/2\mathbb Z$. No finiteness or decidable-equality assumption is part of this abbreviation; if $\iota$ is empty, this function type has exactly one element, the empty (and hence zero) word.

2. homologicalDistance

For arbitrary types $\iota,\kappa,\mu$, assuming only that $\iota$ is finite and has decidable equality, and for $\mathbb Z/2\mathbb Z$-linear maps $d:(\iota\to\mathbb Z/2\mathbb Z)\to(\kappa\to\mathbb Z/2\mathbb Z)$ and $d_{\mathrm{next}}:(\mu\to\mathbb Z/2\mathbb Z)\to(\iota\to\mathbb Z/2\mathbb Z)$, homologicalDistance is the infimum in $\mathbb N\cup\{\top\}$ of the set of values $w$ for which there exists a word $x:\iota\to\mathbb Z/2\mathbb Z$ satisfying $d(x)=0$, $x\notin\operatorname{range}(d_{\mathrm{next}})$, and $w=\operatorname{hammingNorm}(x)$, where the Hamming norm is the number of coordinates at which $x$ is nonzero. Thus it takes the least such Hamming weight when such an $x$ exists and is $\top$ when no such $x$ exists. In particular, $0$ is always in the range of a linear map, so a witnessing $x$ cannot be the zero word; if $\iota$ is empty, the only word is zero, the defining set is empty, and the value is $\top$. There is no hypothesis that $d\circ d_{\mathrm{next}}=0$, and neither $\kappa$ nor $\mu$ is required to be finite.

3. linearMap_apply_eq_sum

For all natural numbers $m,n$, every $\mathbb Z/2\mathbb Z$-linear map $f:(\operatorname{Fin}n\to\mathbb Z/2\mathbb Z)\to(\operatorname{Fin}m\to\mathbb Z/2\mathbb Z)$, every word $x:\operatorname{Fin}n\to\mathbb Z/2\mathbb Z$, and every output coordinate $i\in\operatorname{Fin}m$, the declaration asserts

$$f(x)(i)=\sum_{k\in\operatorname{Fin}n} f(\delta_k)(i)x(k),$$

where $\delta_k$ is the word equal to $1$ at $k$ and $0$ at every other coordinate, and all arithmetic is in $\mathbb Z/2\mathbb Z$. If $n=0$, the sum is empty and equals $0$; if $m=0$, there is no possible binder $i$, so the assertion has no coordinate instance.

4. linearMap_apply_separateDirections

For all natural numbers $m,n,p,q$, all $\mathbb Z/2\mathbb Z$-linear maps $f:(\operatorname{Fin}n\to\mathbb Z/2\mathbb Z)\to(\operatorname{Fin}m\to\mathbb Z/2\mathbb Z)$ and $g:(\operatorname{Fin}q\to\mathbb Z/2\mathbb Z)\to(\operatorname{Fin}p\to\mathbb Z/2\mathbb Z)$, every function $e:\operatorname{Fin}n\to\operatorname{Fin}q\to\mathbb Z/2\mathbb Z$, and coordinates $a\in\operatorname{Fin}m$ and $b\in\operatorname{Fin}p$, the declaration asserts

$$f\bigl(a'\mapsto g(b'\mapsto e(a',b'))(b)\bigr)(a) =g\bigl(b'\mapsto f(a'\mapsto e(a',b'))(a)\bigr)(b).$$

Thus the two linear maps, applied in the two separate coordinate directions and then evaluated at $a,b$, give the same scalar. The quantifiers include $n=0$ and $q=0$, in which case the corresponding input words are empty, and if $m=0$ or $p=0$ there is respectively no possible $a$ or $b$, so the universally quantified assertion is vacuous.

5. linearMap_apply_pointwise_add

For all natural numbers $m,n$, every $\mathbb Z/2\mathbb Z$-linear map $f:(\operatorname{Fin}n\to\mathbb Z/2\mathbb Z)\to(\operatorname{Fin}m\to\mathbb Z/2\mathbb Z)$, words $x,y:\operatorname{Fin}n\to\mathbb Z/2\mathbb Z$, and coordinate $i\in\operatorname{Fin}m$, the declaration asserts $f(k\mapsto x(k)+y(k))(i)=f(x)(i)+f(y)(i)$. If $n=0$, both inputs are the unique empty word; if $m=0$, there is no coordinate $i$ and hence no instance of the assertion.

6. BoundaryTarget

For every dimension function $D:\mathbb N\to\mathbb N$, BoundaryTarget declares a degree-indexed coordinate type with $\operatorname{BoundaryTarget}(D,0)=\varnothing$ and $\operatorname{BoundaryTarget}(D,j+1)=\operatorname{Fin}(D(j))$ for every $j\in\mathbb N$. Consequently, a word on the degree-zero boundary target is the unique function from the empty type to $\mathbb Z/2\mathbb Z$.

7. BasedBinaryChainComplex

BasedBinaryChainComplex declares a structure consisting of: a function $D:\mathbb N\to\mathbb N$; for every $j\in\mathbb N$, a $\mathbb Z/2\mathbb Z$-linear map

$$\partial_j:(\operatorname{Fin}(D(j))\to\mathbb Z/2\mathbb Z) \longrightarrow (\operatorname{BoundaryTarget}(D,j)\to\mathbb Z/2\mathbb Z),$$

whose target is the empty-coordinate word space when $j=0$ and is the word space on $\operatorname{Fin}(D(j-1))$ when $j>0$; a proof that $\partial_j\circ\partial_{j+1}=0$ for every $j\in\mathbb N$; a natural number $L$ called length; and a proof that $D(i)=0$ whenever $L<i$. The declaration imposes no condition that $D(L)$ be nonzero and no minimality condition on $L$. At the lower end, $\partial_0$ has the one-element empty-coordinate codomain and is therefore the zero map. At the upper end, all groups in degrees strictly above $L$ have empty coordinate types, $\partial_{L+1}$ has an empty-coordinate domain and is the zero incoming map to degree $L$, and every still higher boundary also has empty-coordinate domain; when $L=0$, all positive-degree dimensions vanish while $D(0)$ remains unrestricted.

8. chainDistanceAt

For every based binary chain complex $A$ and every $j\in\mathbb N$, chainDistanceAt A j is the infimum in $\mathbb N\cup\{\top\}$ of the Hamming weights of all words $x:\operatorname{Fin}(A.D(j))\to\mathbb Z/2\mathbb Z$ such that $\partial^A_j(x)=0$ and $x\notin\operatorname{range}(\partial^A_{j+1})$; it is $\top$ if there is no such word. At $j=0$, $\partial^A_0$ has empty-coordinate codomain and is zero, so every degree-zero word satisfies the kernel condition, although the non-image condition remains. At $j=A.L$, the incoming map $\partial^A_{A.L+1}$ has empty-coordinate domain and range $\{0\}$, so witnesses are precisely nonzero words in $\ker\partial^A_{A.L}$. For every $j>A.L$, the degree-$j$ coordinate type is empty, its sole word is zero and lies in the range of the next boundary, so the defining set is empty and the distance is $\top$; these statements also cover $A.L=0$.

9. TensorDegreePair

For every $j\in\mathbb N$, TensorDegreePair j is the subtype of pairs $(i,k)\in\operatorname{Fin}(j+1)\times\operatorname{Fin}(j+1)$ whose underlying natural values satisfy $i+k=j$. Thus both entries lie between $0$ and $j$, both endpoint decompositions $(0,j)$ and $(j,0)$ are present, and for $j=0$ the sole element is $(0,0)$.

10. tensorDegreePairFintype

For every $j\in\mathbb N$, tensorDegreePairFintype j noncomputably supplies a finite-type structure on the set of pairs $(i,k)\in\operatorname{Fin}(j+1)^2$ satisfying $i+k=j$, using the injective inclusion of that subtype into the finite product. This declaration adds data enabling finite enumeration; it asserts no ordering or chosen enumeration formula.

11. tensorDegreePairDecidableEq

For every $j\in\mathbb N$, tensorDegreePairDecidableEq j noncomputably supplies a classical decision procedure for equality between two degree pairs $(i,k)$ with $i+k=j$.

12. TensorDegreeIndex

For every pair of based binary chain complexes $A,B$ and every $j\in\mathbb N$, TensorDegreeIndex A B j is the dependent disjoint union

$$\coprod_{\substack{0\le i,k\le j\\i+k=j}} \operatorname{Fin}(A.D(i))\times\operatorname{Fin}(B.D(k)).$$

An element therefore consists of a degree pair $(i,k)$ with $i+k=j$, an $A$-coordinate $a<A.D(i)$, and a $B$-coordinate $b<B.D(k)$. A component is empty if either dimension is zero; at $j=0$ only the component $(0,0)$ occurs. If $A$ and $B$ have recorded lengths $L_A,L_B$, then this entire index type is empty for $j>L_A+L_B$, because every decomposition $i+k=j$ then has $i>L_A$ or $k>L_B$ and hence a zero dimension.

13. tensorDegreeIndexFintype

For every based binary chain complexes $A,B$ and every $j\in\mathbb N$, tensorDegreeIndexFintype A B j noncomputably supplies a finite-type structure on the dependent union of triples $((i,k),a,b)$ with $i+k=j$, $a<A.D(i)$, and $b<B.D(k)$.

14. tensorDegreeIndexDecidableEq

For every based binary chain complexes $A,B$ and every $j\in\mathbb N$, tensorDegreeIndexDecidableEq A B j noncomputably supplies a classical decision procedure for equality between two dependent triples $((i,k),a,b)$ in the degree-$j$ tensor index type.

15. tensorDegreePairLeft

For every implicit $j\in\mathbb N$ and every degree pair $p=(i,k)$ with $i+k=j$, tensorDegreePairLeft p is the degree-$(j+1)$ pair $(i+1,k)$. The finite-index bounds and the equality $(i+1)+k=j+1$ are included as proof data; this is defined also at $j=0$, where it sends $(0,0)$ to $(1,0)$.

16. tensorDegreePairRight

For every implicit $j\in\mathbb N$ and every degree pair $p=(i,k)$ with $i+k=j$, tensorDegreePairRight p is the degree-$(j+1)$ pair $(i,k+1)$. The finite-index bounds and the equality $i+(k+1)=j+1$ are included as proof data; this is defined also at $j=0$, where it sends $(0,0)$ to $(0,1)$.

17. tensorIndexLeft

For every based binary chain complexes $A,B$, implicit $j\in\mathbb N$, degree pair $p=(i,k)$ with $i+k=j$, coordinate $a\in\operatorname{Fin}(A.D(i+1))$, and coordinate $b\in\operatorname{Fin}(B.D(k))$, tensorIndexLeft A B p a b is the degree-$(j+1)$ tensor index $((i+1,k),a,b)$. If either indicated dimension is zero, the corresponding coordinate binder has no inhabitant, so there is no such indexed value.

18. tensorIndexRight

For every based binary chain complexes $A,B$, implicit $j\in\mathbb N$, degree pair $p=(i,k)$ with $i+k=j$, coordinate $a\in\operatorname{Fin}(A.D(i))$, and coordinate $b\in\operatorname{Fin}(B.D(k+1))$, tensorIndexRight A B p a b is the degree-$(j+1)$ tensor index $((i,k+1),a,b)$. If either indicated dimension is zero, the corresponding coordinate binder has no inhabitant, so there is no such indexed value.

19. tensorBoundary

For every based binary chain complexes $A,B$ and every $j\in\mathbb N$, tensorBoundary A B j declares a $\mathbb Z/2\mathbb Z$-linear map from words on the degree-$(j+1)$ tensor index to words on the degree-$j$ tensor index. Explicitly, for an input word $e$ and an output index $z=((i,k),a,b)$ with $i+k=j$, its value is

$$\partial^A_{i+1}\bigl(a'\mapsto e((i+1,k),a',b)\bigr)(a) + \partial^B_{k+1}\bigl(b'\mapsto e((i,k+1),a,b')\bigr)(b),$$

with addition in $\mathbb Z/2\mathbb Z$. The first slice ranges over $a'\in\operatorname{Fin}(A.D(i+1))$ and the second over $b'\in\operatorname{Fin}(B.D(k+1))$; the displayed output exists only when $a\in\operatorname{Fin}(A.D(i))$ and $b\in\operatorname{Fin}(B.D(k))$. The definition includes proofs that this coordinate formula preserves addition and scalar multiplication. At $j=0$, the only possible degree pair in the codomain is $(0,0)$. If the codomain index type is empty, the output is the unique empty word; empty source components contribute only empty slices.

20. tensorBoundary_apply

For every based binary chain complexes $A,B$, every $j\in\mathbb N$, every word $e$ on the degree-$(j+1)$ tensor index, and every degree-$j$ tensor index $z=((i,k),a,b)$ with $i+k=j$, the declaration asserts the definitional coordinate equality

$$(\operatorname{tensorBoundary}_{A,B,j}e)(z) = \partial^A_{i+1}\bigl(a'\mapsto e((i+1,k),a',b)\bigr)(a) + \partial^B_{k+1}\bigl(b'\mapsto e((i,k+1),a,b')\bigr)(b).$$

All values and additions are in $\mathbb Z/2\mathbb Z$; if the degree-$j$ tensor index is empty there is no possible $z$, so the universally quantified coordinate statement has no instance.

21. tensorDegreePair_mixed

For every implicit $j\in\mathbb N$ and every degree pair $p=(i,k)$ with $i+k=j$, the declaration asserts equality of the degree-$(j+2)$ dependent pairs obtained by first increasing the left entry and then the right entry or in the opposite order: both are $(i+1,k+1)$. This includes equality of the subtype proof-bearing values, not merely equality of their displayed natural-number coordinates.

22. tensorIndex_mixed

For every based binary chain complexes $A,B$, implicit $j\in\mathbb N$, degree pair $p=(i,k)$ with $i+k=j$, coordinate $a\in\operatorname{Fin}(A.D(i+1))$, and coordinate $b\in\operatorname{Fin}(B.D(k+1))$, the declaration asserts that inserting $((i+1,k),a,b)$ by a right-degree increase equals inserting $((i,k+1),a,b)$ by a left-degree increase; both sides are the same degree-$(j+2)$ tensor index $((i+1,k+1),a,b)$. If either coordinate type is empty, the universal assertion is vacuous because no corresponding $a$ or $b$ exists.

23. tensorBoundary_tensorIndexLeft

For every based binary chain complexes $A,B$, implicit $j\in\mathbb N$, word $e$ on the degree-$(j+2)$ tensor index, pair $p=(i,k)$ with $i+k=j$, coordinate $a\in\operatorname{Fin}(A.D(i+1))$, and coordinate $b\in\operatorname{Fin}(B.D(k))$, the declaration gives the value of the boundary from degree $j+2$ to degree $j+1$ at the left-inserted index $((i+1,k),a,b)$ as

$$\partial^A_{i+2}\bigl(a'\mapsto e((i+2,k),a',b)\bigr)(a) + \partial^B_{k+1}\bigl(b'\mapsto e((i+1,k+1),a,b')\bigr)(b).$$

Here $a'$ ranges over $\operatorname{Fin}(A.D(i+2))$ and $b'$ over $\operatorname{Fin}(B.D(k+1))$, and all arithmetic is in $\mathbb Z/2\mathbb Z$; if the type of $a$ or $b$ is empty, there is no instance of the coordinate assertion.

24. tensorBoundary_tensorIndexRight

For every based binary chain complexes $A,B$, implicit $j\in\mathbb N$, word $e$ on the degree-$(j+2)$ tensor index, pair $p=(i,k)$ with $i+k=j$, coordinate $a\in\operatorname{Fin}(A.D(i))$, and coordinate $b\in\operatorname{Fin}(B.D(k+1))$, the declaration gives the value of the boundary from degree $j+2$ to degree $j+1$ at the right-inserted index $((i,k+1),a,b)$ as

$$\partial^A_{i+1}\bigl(a'\mapsto e((i+1,k+1),a',b)\bigr)(a) + \partial^B_{k+2}\bigl(b'\mapsto e((i,k+2),a,b')\bigr)(b).$$

Here $a'$ ranges over $\operatorname{Fin}(A.D(i+1))$ and $b'$ over $\operatorname{Fin}(B.D(k+2))$, and all arithmetic is in $\mathbb Z/2\mathbb Z$; if the type of $a$ or $b$ is empty, there is no instance of the coordinate assertion.

25. tensorBoundary_boundary

For every based binary chain complexes $A,B$ and every $j\in\mathbb N$, the declaration asserts that the composite of the tensor boundary from degree $j+2$ to degree $j+1$ with the tensor boundary from degree $j+1$ to degree $j$ is the zero $\mathbb Z/2\mathbb Z$-linear map:

$$\operatorname{tensorBoundary}_{A,B,j}\circ \operatorname{tensorBoundary}_{A,B,j+1}=0.$$

Equivalently, every degree-$(j+2)$ word is sent to the zero word on every degree-$j$ tensor coordinate. The quantifier includes $j=0$; if a relevant source or target tensor index type is empty, the corresponding equality reduces to equality of maps involving a one-element empty-coordinate word space.

26. TensorBoundaryTarget

For every based binary chain complexes $A,B$, TensorBoundaryTarget A B declares a degree-indexed coordinate type with value $\varnothing$ at degree $0$ and value $\operatorname{TensorDegreeIndex}(A,B,j)$ at degree $j+1$, namely the dependent union of triples $((i,k),a,b)$ with $i+k=j$, $a<A.D(i)$, and $b<B.D(k)$. Thus a word on the degree-zero target is the unique empty word, while the target in positive degree $j+1$ is exactly the tensor coordinate type one degree lower.

27. tensorBoundaryAt

For every based binary chain complexes $A,B$, tensorBoundaryAt A B declares for each $j\in\mathbb N$ a $\mathbb Z/2\mathbb Z$-linear map from words on the degree-$j$ tensor index to words on TensorBoundaryTarget A B j: at $j=0$ it is the zero map from the degree-zero tensor word space to the empty-coordinate word space, and at $j+1$ it is tensorBoundary A B j, whose value at $((i,k),a,b)$ with $i+k=j$ is $\partial^A_{i+1}(a'\mapsto e((i+1,k),a',b))(a)+\partial^B_{k+1}(b'\mapsto e((i,k+1),a,b'))(b)$. If the recorded lengths are $L_A,L_B$, the degree-$j$ source index is empty for $j>L_A+L_B$; in particular, the boundary in degree $L_A+L_B+1$ has empty domain and is the zero incoming map to the highest possibly nonempty degree, and all higher-degree domains are also empty. The lower endpoint is separately fixed by the $j=0$ zero-map clause, including when $L_A=L_B=0$.

28. tensorBoundaryAt_boundaryAt

For every based binary chain complexes $A,B$ and every $j\in\mathbb N$, the declaration asserts

$$\operatorname{tensorBoundaryAt}_{A,B,j} \circ \operatorname{tensorBoundaryAt}_{A,B,j+1}=0.$$

Thus every degree-$(j+1)$ tensor word is sent to zero after the two consecutive paper-indexed boundary maps. At $j=0$, the outer boundary is the explicitly defined zero map to the empty-coordinate word space; for $j>0$ the equality is the corresponding consecutive tensorBoundary equality. The assertion also includes degrees above the sum of the recorded lengths, where the source word spaces are empty-coordinate one-element spaces.

29. tensorProductDistanceAt

For every based binary chain complexes $A,B$ and every $j\in\mathbb N$, tensorProductDistanceAt A B j is the infimum in $\mathbb N\cup\{\top\}$ of the Hamming weights of words $x$ on the degree-$j$ tensor index such that $\operatorname{tensorBoundaryAt}_{A,B,j}(x)=0$ and $x$ is not in the range of $\operatorname{tensorBoundaryAt}_{A,B,j+1}$; it is $\top$ when there is no such word. At $j=0$, the first boundary is explicitly zero, so every degree-zero word satisfies the kernel condition. If the recorded lengths are $L_A,L_B$, then at $j=L_A+L_B$ the next-degree tensor index is empty and the incoming boundary has range $\{0\}$, so witnesses are precisely the nonzero words in the kernel at that degree; for every $j>L_A+L_B$, the degree-$j$ tensor index itself is empty, its only word is zero and lies in the incoming range, and the distance is $\top$. These endpoint statements still apply when one or both lengths are zero.

30. componentDistanceMinimum

For every based binary chain complexes $A,B$ and every $j\in\mathbb N$, componentDistanceMinimum A B j is the infimum in $\mathbb N\cup\{\top\}$ of the nonempty finite set

$$\left\{ \operatorname{chainDistanceAt}(A,i)\, \operatorname{chainDistanceAt}(B,j-i) \;\middle|\; i\in\operatorname{Fin}(j+1) \right\},$$

where each factor itself is the infimum of the Hamming weights of degree-appropriate kernel words outside the next-boundary image, or $\top$ when no such word exists, and multiplication is multiplication in $\mathbb N\cup\{\top\}$. Because $i<j+1$, one always has $i\le j$, so the natural-number subtraction $j-i$ does not truncate below zero. Both endpoint choices are included: $i=0$ contributes $d_0(A)d_j(B)$ and $i=j$ contributes $d_j(A)d_0(B)$. When $j=0$, there is exactly one choice, $i=0$, so the value is exactly $d_0(A)d_0(B)$; for $j>0$, the infimum is the minimum of the $j+1$ displayed values, allowing repeated values and values equal to $\top$.

31. oneComplex

For all natural numbers $r,c$ and every $\mathbb Z/2\mathbb Z$-linear map $P:(\operatorname{Fin}c\to\mathbb Z/2\mathbb Z)\to(\operatorname{Fin}r\to\mathbb Z/2\mathbb Z)$, oneComplex P declares a based binary chain complex with dimensions $D(0)=r$, $D(1)=c$, and $D(i)=0$ for every $i\ge2$; boundaries $\partial_0=0$ into the empty-coordinate word space, $\partial_1=P$, and $\partial_i=0$ for every $i\ge2$; and recorded length $1$. It supplies proofs that every consecutive composite is zero and that $D(i)=0$ whenever $1<i$. Thus the lower boundary is zero and the incoming boundary $\partial_2$ at the upper end has empty-coordinate domain and is zero. The construction includes $r=0$ and $c=0$: if either is zero its corresponding degree has only the empty word, and the recorded length remains $1$ even if the degree-one dimension, or both displayed dimensions, is zero.

32. chainDistanceBefore

For every based binary chain complex $A$, chainDistanceBefore A declares a function $\mathbb N\to\mathbb N\cup\{\top\}$ with value $\top$ at input $0$ and, at input $j+1$, value equal to the infimum of the Hamming weights of all words $x:\operatorname{Fin}(A.D(j))\to\mathbb Z/2\mathbb Z$ satisfying $\partial^A_j(x)=0$ and $x\notin\operatorname{range}(\partial^A_{j+1})$, again with value $\top$ if no such word exists. Thus input $1$ returns the degree-zero distance, while input $0$ is fixed to $\top$ without testing any boundary or word. If $A$ has recorded length $L$, input $L+1$ returns the possibly finite distance in the highest possibly nonempty degree $L$, whereas every input $k>L+1$ returns $\top$ because degree $k-1$ has zero dimension and its sole zero word lies in the next-boundary range; when $L=0$, input $1$ is the degree-zero distance and every input above $1$ is $\top$.