Is this a Weyr matrix?

Question

There's a type of n×n matrix W called the basic Weyr canonical form. Such a matrix is described by its blocks and has the following properties, using the following reference diagram:

• the main diagonal blocks W_ii are n_i×n_i matrices of the form λI_ni where I_ni is the n_i×n_i identity matrix.
• n₁ ≥ n₂ ≥ ... ≥ n_r
• the first superdiagonal blocks W_k-1,k for k ∈ 2..r are n_k-1×n_k matrices that are full column rank in row-reduced echelon form, or more simply put, I_nk sitting on top of n_k-1 - n_k rows of zeros.
• all other blocks are 0 matrices.

For example:

• The main diagonal blocks (yellow) are such that the n_i are 4, 2, 2, and 1.
• The first superdiagonal blocks are in green.
• The grey zone consists of all the other blocks, which are all 0.

For this challenge we will assume λ=1.

Input

A square matrix with 0s and 1s in any convenient format.

Output

Output one of two distinct values for whether the input matrix is Weyr or not Weyr.

Rules

This is code-golf. Fewest bytes in each language wins. Standard rules/loopholes apply.

Test cases

Presented as arrays of rows.

Weyr:

[[1]] 
[[1,1],[0,1]] 
[[1,0,1,0,0],[0,1,0,1,0],[0,0,1,0,1],[0,0,0,1,0],[0,0,0,0,1]]
[[1,0,0,1,0,0,0,0,0],[0,1,0,0,1,0,0,0,0],[0,0,1,0,0,1,0,0,0],[0,0,0,1,0,0,1,0,0],[0,0,0,0,1,0,0,1,0],[0,0,0,0,0,1,0,0,1],[0,0,0,0,0,0,1,0,0],[0,0,0,0,0,0,0,1,0],[0,0,0,0,0,0,0,0,1]]
[[1,0,0,0,1,0,0,0,0],[0,1,0,0,0,1,0,0,0],[0,0,1,0,0,0,0,0,0],[0,0,0,1,0,0,0,0,0],[0,0,0,0,1,0,1,0,0],[0,0,0,0,0,1,0,1,0],[0,0,0,0,0,0,1,0,1],[0,0,0,0,0,0,0,1,0],[0,0,0,0,0,0,0,0,1]]

Non-Weyr:

[[0]]
[[1,0],[1,1]]
[[1,0,0,1,0,0],[0,1,0,0,0,0],[0,0,1,0,0,1],[0,0,0,1,0,0],[0,0,0,0,1,0],[0,0,0,0,0,1]]
[[1,0,1,0,0],[0,1,0,0,0],[0,0,1,0,0],[0,0,0,1,0],[0,0,0,0,1]]
[[1,0,0,1,0,0,0,0,0],[0,1,0,0,1,0,0,0,0],[0,0,1,0,0,1,0,0,0],[0,0,0,1,0,0,0,0,0],[0,0,0,0,1,0,1,0,0],[0,0,0,0,0,1,0,1,0],[0,0,0,0,0,0,1,0,1],[0,0,0,0,0,0,0,1,0],[0,0,0,0,0,0,0,0,1]]

Answer 1

K (ngn/k), 91 88 84 80 81 bytes

{x~e|(-n)#'(0*x),'(!n)=\:,/(-1_b)+1_0{x#!y}':|-n-':|b:|\@[-1++/|\|+x|e:=n:#x;]\0}

Try it online!

Answer 2

Python 2, 270 bytes

lambda m,w=0:{w}&{0,len(m)}and I(m)or any(I([l[:i]for l in m[:i]])*I([l[i:j+i]for l in m[:j]])*(sum(sum(m[:i]+[l[:i]for l in m],[]))==2*i+j)and f([l[i:]for l in m[i:]],j)for i in range(w,len(m))for j in range(1,i+1))
I=lambda m:all(sum(l)==l[i]>0for i,l in enumerate(m))

Try it online!

Explanation:

Recursively checks blocks for identity and their superdiagonal blocks.

I checks if a matrix is an identity matrix

I=lambda m:all(sum(l)==l[i]>0for i,l in enumerate(m))

For each block of the input matrix, the function checks that it is an identity, and that there is another identity matrix block, to it's right. The next iteration then looks at a block of that size.

{w}&{0,len(m)}and I(m)                # if the while matrix is an identity matrix,
                                      # return true (but only the first time or last block)
or
any(
 I([l[:i]for l in m[:i]])                         # the current block is identity
 *I([l[i:j+i]for l in m[:j]])                     # and, the smaller block to the right is identity
 *(sum(sum(m[:i]+[l[:i]for l in m],[]))==2*i+j)   # and everything below and to the right (not the
                                                  # smaller block), are 0
 and f([l[i:]for l in m[i:]],j)                   # and the remaining matrix is alse Weyr(recursively)
 for i in range(w,len(m))             # for each block size i
 for j in range(1,i+1)                # for each smaller right block of size j
)