正确性证明
本章在边权互异的前提下，严格证明第\ref{sec:base-tree}节与第\ref{sec:types}节所述算法在
$\deg_T(1)=k$ 的可行域内输出“最大边优先”的词典序最小生成树，且最优解唯一。
词典序与基本交换性质
\newcommand{\maxlex}{\text{maxlex}}
📝定义 1.7.1 最大边优先的词典序
对生成树 $T$，记其边权从小到大排序为
$\mathbf{w}(T)=(w_{[1]}(T)\le\cdots\le w_{[n-1]}(T))$。
给定两棵树 $T,T'$，定义
$ \mathbf{w}(T)\prec_{\maxlex}\mathbf{w}(T') $
当且仅当存在最小的 $t\in\{1,\dots,n-1\}$ 使得
$w_{[n-t]}(T)\neq w_{[n-t]}(T')$ 且
$w_{[n-t]}(T)<w_{[n-t]}(T')$。
💡引理 1.7.2 环性质：最小版
设 $T$ 为生成树，$e\notin T$。将 $e$ 加入 $T$ 形成唯一环 $\mathcal{C}$。
若存在 $f\in\mathcal{C}$ 使 $w(e)<w(f)$，则令 $T':=T-f+e$，有
$\mathbf{w}(T')\prec_{\maxlex}\mathbf{w}(T)$。
📝证明
$T$ 与 $T'$ 的边权多重集仅在 $\{f\}$ 被 $\{e\}$ 替换处不同。
因权互异，排序后两向量自大到小比较时，最早出现差异的坐标由 $w(f)$ 变为更小的 $w(e)$，
故得结论。
💡引理 1.7.3 割性质：最小版
设 $(S,\bar S)$ 为任意割，其最小跨割边为 $e^\star$。
若某可行树 $T$ 在该割上使用了边 $e\neq e^\star$（必有 $w(e)>w(e^\star)$），
则存在 $T'$ 在度约束不变的前提下满足
$\mathbf{w}(T')\prec_{\maxlex}\mathbf{w}(T)$。
📝证明
将 $e^\star$ 加入 $T$ 得环 $\mathcal{C}$，且 $\mathcal{C}$ 含 $e$。
由引理~\ref{lem:cycle} 用 $e^\star$ 替换 $e$ 得严格改进；若 $e$ 与 1 不相邻，
则度数不变；若 $e$ 与 1 相邻，则 $e^\star$ 亦跨同一割且与 1 相邻（否则不连通），
因此 $\deg(1)$ 亦不变。
基树阶段的必要性与最优性
回顾第\ref{sec:base-tree}节：在 $V\setminus\{1\}$ 上仅用 $E_0$ 升序 Kruskal
得到最小生成森林 $F_0^{\min}$，连通块为 $C_1,\dots,C_r$；
对每个块取与 1 相连的最小边
$b_{\min}(C_i)=\arg\min\{w(1,v)\mid v\in C_i\}$，并令
$T_r^{\min}=F_0^{\min}\cup\{b_{\min}(C_i):i=1,\dots,r\}$。
💡引理 1.7.4 可行性必要条件
若存在可行树 $T$ 满足 $\deg_T(1)=k$，则：
(i) 对任意 $i$，块 $C_i$ 与 1 至少有一条边相连；
(ii) $r\le k\le \deg_G(1)$。
📝证明
若某 $C_i$ 无与 1 相连之边，则任何生成树都无法连接 1 与该块，矛盾。
因为每个 $C_i$ 至少需一条 $1$-边与整体相连，故 $k\ge r$；
同时 $k$ 不得超过顶点 1 的度上界 $\deg_G(1)$。
💡命题 1.7.5 块内最小 $1$-边的必选性
设 $T$ 为任一可行树且 $\deg_T(1)\ge r$。
对任意 $i$，若 $T$ 在割 $(C_i,\bar C_i)$ 上使用的与 1 相连的边不是
$b_{\min}(C_i)$，则存在可行树 $\tilde T$ 满足
$\mathbf{w}(\tilde T)\prec_{\maxlex}\mathbf{w}(T)$。
📝证明
割 $(C_i,\bar C_i)$ 的最小跨割边为 $b_{\min}(C_i)$。
若 $T$ 用了其他较大的跨割边 $e$，由引理~\ref{lem:cut} 将其替换为
$b_{\min}(C_i)$ 得严格改进；替换前后均为 $1$-边，$\deg(1)$ 不变。
💡推论 1.7.6 基树的词典序最优性（在 $\deg\ge r$ 的可行域内）
在所有满足 $\deg(1)\ge r$ 的可行树中，$T_r^{\min}$ 在
$\prec_{\maxlex}$ 下最优，且在互异权下唯一。
📝证明
若某可行树在某块上未使用 $b_{\min}(C_i)$，按命题~\ref{prop:block-min} 可严格改进。
当所有块均使用 $b_{\min}(C_i)$ 时，非 $1$-边部分因 $F_0^{\min}$ 的最优性而最小；
唯一性由互异权给出。
一类/二类 $1$-边与单步最优选择
设当前树为 $T$（初始取 $T_r^{\min}$）。对任一未选 $1$-边 $e=(1,x)$，记
$$
M_T(1,x):=\max{\,w(f)\mid f\in P_T(1,x)\,},
$$
其中 $P_T(1,x)$ 为 $T$ 中从 1 到 $x$ 的唯一路径。
加入 $e$ 后按环性质删除路径最大边（记为 $\mathrm{argmax}_T(1,x)$）。
📝定义 1.7.7 一类/二类 $1$-边
若 $w(e) < M_T(1,x)$，称 $e$ 为一类边（改进步）；
若 $w(e) > M_T(1,x)$，称 $e$ 为二类边（劣化步）。
💡引理 1.7.8 一类边产生严格改进
若 $e$ 为一类边，则令 $T':=T-\mathrm{argmax}_T(1,x)+e$，有
$\mathbf{w}(T')\prec_{\maxlex}\mathbf{w}(T)$。
📝证明
环 $\mathcal{C}=P_T(1,x)\cup\{e\}$ 上最大边权为 $M_T(1,x)$；
由 $w(e)<M_T(1,x)$ 与引理~\ref{lem:cycle} 立即得到。
💡引理 1.7.9 无一类边时只能劣化
若对所有未选 $1$-边 $e$ 均有 $w(e)\ge M_T(1,x)$，
则任意加入一条 $1$-边并删除环上最大边后的树 $T'$ 都满足
$\mathbf{w}(T)\preceq_{\maxlex}\mathbf{w}(T')$，
且当存在严格不等式时为劣化。
📝证明
由定义所有候选都为二类边或 $w(e)=M_T$ 的平权边；
替换将某处较小的值提升为 $w(e)\ge M_T$，因此不可能改进。
💡引理 1.7.10 单步贪心的必要性
设当前存在至少一条一类边。令
$$
e^\star \in \arg\max_{e=(1,x)\ \text{一类}} M_T(1,x).
$$
则在所有“加入一条 $1$-边并删除环上最大边”的可行单步中，
选择 $e^\star$ 得到的树 $T^\star$ 在 $\prec_{\maxlex}$ 意义下最优。
📝证明
任取另一一类边 $e$ 得到 $T_e$。
两种结果均以将某一条路径最大边 $M_T(1,\cdot)$ 替换为更小的 $w(e)$ 的方式改进。
比较两者的最靠后的不同坐标，必对应于较大的那条
$M_T(1,\cdot)$。选择 $M_T$ 最大的 $e^\star$ 使该坐标降幅最大，
从而在词典序上不劣且严格更优（互异权）。
💡引理 1.7.11 二类边的序内最优
若已不存在一类边且必须继续增加 $\deg(1)$ 才能达到 $k$，
则在所有单步中，选择 $w(e)$ 最小的二类边得到的树在
$\prec_{\maxlex}$ 上最优（损失最小）。
📝证明
由引理~\ref{lem:no-type1}，任何选择都会在某一坐标造成非负向的变化；
为了使首个差异坐标的增幅尽可能小，应取 $w(e)$ 最小的二类边。
全局最优性：归纳与交换论证
记算法从 $T_0:=T_r^{\min}$ 出发，
按“先一类后二类；一类内按 $M_T(1,x)$ 降序，二类内按 $w(e)$ 升序”的规则，
依次得到 $T_1,T_2,\dots$，直至 $\deg_{T_s}(1)=k$。
记输出为 $T_{\mathrm{alg}}:=T_s$。
💡定理 1.7.12 前缀最优性
对任意 $t\in\{0,1,\dots,s\}$，在所有满足 $\deg(1)=r+t$ 的可行生成树中，
$T_t$ 在 $\prec_{\maxlex}$ 下最优。
📝证明
对
$t$ 作归纳。
$t=0$ 由推论~\ref{cor:base-opt} 成立。
设结论对
$t-1$ 成立。考虑任意可行树
$S$ 满足
$\deg_S(1)=r+t$。
从
$S$ 中删去一条与 1 相连的边，得到某
$S'$ 使
$\deg_{S'}(1)=r+t-1$。
由归纳假设，
$\mathbf{w}(T_{t-1})\preceq_{\maxlex}\mathbf{w}(S')$。
从 $\deg=r+t-1$ 提升到 $r+t$ 的单步中，算法按引理~\ref{lem:greedy-step} 或
\ref{lem:type2-order} 取到该步的词典序最优选择，
因此
$\mathbf{w}(T_t)\preceq_{\maxlex}\mathbf{w}(S)$。
（形式化地，可将 $S$ 的该一步改写为从 $S'$ 的某一单步；
若 $S'$ 不等于 $T_{t-1}$，用交换论证在不劣化的情况下把
$S'$ 的选择调整为 $T_{t-1}$ 的选择，再应用单步最优性。）
💡定理 1.7.13 全局正确性与唯一性
若可行性成立，则算法输出 $T_{\mathrm{alg}}$ 在所有满足 $\deg(1)=k$ 的生成树中
$\prec_{\maxlex}$ 最优；且在互异权下唯一。
📝证明
取 $t=s=k-r$，由定理~\ref{thm:prefix} 直接得最优性；
唯一性由互异权与每一步的严格改进/最小损失给出。
度约束与连通性的保持
💡引理 1.7.14 连通性与度数保持
在增添阶段的每一步，加入一条 $1$-边并删除环上最大边，所得始终为生成树；
且若删除的不是 $1$-边，则 $\deg(1)$ 增 1；若删除的是已加入的 $1$-边则不发生（算法不作此删除）。
📝证明
加入一边成环，删去环上一边仍为生成树是图论基本事实。
算法实现上每步都删除路径最大边，而路径最大边必为非 $1$-边（见第~\ref{sec:offline-key} 节的指派或在线求解的路径最大性——若为 $1$-边则与一类/二类的定义矛盾），故度数按预期单调增加直至 $k$。
实现细节的正确性（指派与排序键）
本节说明第~\ref{sec:offline-key} 的“指派”仅用于实现效率，与正确性一致。
💡命题 1.7.15 指派的正确性
在 Kruskal（升序）构造 $F_0^{\min}$ 的并查集中，合并两个块 $A,B$ 的
$E_0$-边 $e_0$ 被指派给
$\max\{m(A),m(B)\}$ 所对应的那条最小 $1$-边；
该 $1$-边一旦被选入树，其所替换（删除）的正是 $e_0$ 或权值不小于 $w(e_0)$ 的路径最大边。
📝证明 思路
在合并前，$A,B$ 各自的“最小 $1$-边”分别为 $m(A),m(B)$。
两块并成后，先选入较小者不会使当前块内部出现比 $e_0$ 更大的非 $1$-边成为路径最大值；
当随后选入较大的那条最小 $1$-边时，跨越的路径上最重的非 $1$-边即为 $e_0$（或其不小者），因此与在线定义 $M_T(1,x)$ 一致。形式化证明可用对 Kruskal 合并序列的归纳与“最小生成森林的瓶颈唯一性”完成。
💡推论 1.7.16 离线排序键与在线 $M_T$ 的一致
用 $w(\mathrm{kill}(e))$ 作为一类边的排序键，等价于在线以
$M_T(1,x)$ 的降序排序；因此不影响第~\ref{lem:greedy-step} 的最优性结论。
小结
综上：可行时，基树阶段（命题\ref{prop:block-min}、推论\ref{cor:base-opt}）给出在
$\deg\ge r$ 的词典序最优前缀；增添阶段每一步的选择分别由
引理\ref{lem:greedy-step} 与引理\ref{lem:type2-order} 保证单步最优，
并由定理\ref{thm:prefix} 的归纳交换论证提升为全局最优；度与连通性由
引理\ref{lem:maintain} 保证；实现上的“指派”与排序键（命题\ref{prop:assign}）与在线瓶颈一致（推论\ref{cor:offline-online}）。
最终结论见定理~\ref{thm:global}：算法确为“最大边优先”的词典序最小、且 $\deg(1)=k$ 的唯一最优解。