含久期项的ODE系统通解归纳证明的标准形式化梳理求助

我现在遇到一个关于含久期项的微分方程组通解的归纳证明形式化问题——这个方程组因为特征值重复，用若尔当标准形求解。

我能看懂证明的推导过程，但它明明是归纳法的思路，我却没法把它整理成标准的“数学归纳法”结构：也就是先证基例$P(1)$成立，再假设$P(n)$成立进而推出$P(n+1)$成立，或者从$P(n-1)$推$P(n)$的形式。

我附上了证明的截图（避免转述出错，也省得重新打字），还修正了一处下标小错误，高亮了我想融入归纳结构的关键信息。目前我有两个初步思路，但都不确定对不对，想请大家帮忙看看：

• 思路1：
  把$k-j$作为第$n$个归纳项，这样第$n-1$个情况就对应$k-j-1 = k-(j+1)$。
  这样就能对应证明里“假设$j+1$时成立”的表述。
  基例$P(1)$我猜是$j=0$的情况，也就是证明里写的$w'_k = λw_k \implies w_k = c_ke^{λt}$，不过这里有点矛盾，因为证明里$j \in [1,(k-1)]$，这只是我初步的想法。

• 思路2：
  把$k$作为归纳的$n$，采用强归纳法：假设对于所有$j \in [1,(k-1)]$，命题$P(k-1)$都成立，进而推出$P(k)$成立。
  基例$P(1)$就是$w'_1 = λw_1 \implies w_1 = c_1e^{λt}$，不过证明里没写这一步。

备注：内容来源于stack exchange，提问作者CormJack