The Lean proof of 68 proceeds by strong induction on the common rank. If \(X\) and \(Y\) share a gene, that common gene is removed using cancellation and the induction hypothesis is applied to the remainder. If they do not share a gene, the proof splits according to whether some positive sigma level agrees, whether \(X\) contains a positive/negative pair of equal rank, and finally the numerical alternatives corresponding to Djokovic’s inequalities around (15.10).

Write \(\sigma _X(i) = (a_i, b_i)\), \(\sigma _Y(i) = (c_i, d_i)\), and \(r_i = a_i + b_i\), \(s_i = c_i + d_i\) for the level-\(i\) signatures and their rank sums. Since \(X {\lt} Y\) we have \((a_i,b_i) \le (c_i,d_i)\) componentwise and \(r_0 = s_0 = m+2\). Treating both varieties simultaneously: for \(\mathrm{Mix}(\mathrm{Lambda},\mathrm{Pi})\) one has \(a_i = b_i\), \(c_i = d_i\) at odd \(i\) (and integers at even \(i\)); for \(\mathrm{Mix}(\mathrm{Pi},\mathrm{Lambda})\) the roles of even/odd swap. The no-sigma-agreement hypothesis is exactly Djoković’s reduction (16.1),

obtained from the lifting property and the induction hypothesis. Polarized genes carry charge \(g^+,g^-\); nonpolarized genes are written \(g\). A gene of minimal rank in \(X\) is \(g_1\), with \(r(g_1) = m\).

The core dispatches as follows; each branch selects one primitive mutation \(X \to Z\) and closes by propagating a single strict level \(a_m {\lt} c_m\) (or \(b_m {\lt} d_m\)) across a window via the drop inequalities cond_15_6_Mix_Lambda_Pi / cond_15_7_Mix_Lambda_Pi (file MixLambdaPi/Drops.lean) together with the window signature identities sigma_type\(t\)_{eq_before,eq_after,mid} (file MixLambdaPi/SigmaWindow.lean); half-integer increments are handled as in half_le_sigma_diff_at_r.

Preliminary reductions.

• If \(X \supset g^+(m) + g^-(m)\) (equal-rank polarized pair) use \(g^+(m)+g^-(m) \to g(m{-}1)+g(m{+}1)\) (type 7, diagonal). This is already the separately-dispatched disjoint-pair Case 3, so inside Case A we may assume \(X \nsupseteq g^+(m)+g^-(m)\).

• If \(X \supset 2g(m)\) use \(2g(m) \to g^{-\epsilon }(m{-}1)+g^{\epsilon }(m{+}1)\) (type 4, diagonal), \(\epsilon = +\) if \(a_m {\lt} c_m\) and \(\epsilon =-\) otherwise. Afterwards assume \(X \nsupseteq 2g(m)\).

Branch A: \(g_1 = g(m)\) nonpolarized. Let \(g_2\) be a minimal-rank gene of \(X - g_1\), rank \(k {\gt} m\).

• Case 1 (\(g_2 = g(k)\)): from \(a_m {\lt} c_m\) (after a charge switch) and the window chain \(c_i - c_{i+2} \le s_i - s_{i+1} \le s_0 - s_1 \le r_0 - r_1 - 1 = a_i - a_{i+2}\) one gets \(a_j {\lt} c_j\) for \(m \le j \le k\), and \(g(m)+g(k) \to g^-(m{-}1)+g^+(k{+}1)\) (type 4).

• Case 2 (\(g_2 = g^+(k)\)): if \(m \ge 2\), or \(m=1\) with \(b_1 {\lt} d_1\), then \(b_j {\lt} d_j\) for \(m \le j \le k-1\) and \(g(m)+g^+(k) \to g^+(m{-}1)+g(k{+}1)\) (type 5). If \(m=1\) and \(b_1 = d_1\) then \(a_1 {\lt} c_1\), \(X-g_1-g_2\) contains a negative or nonpolarized gene \(g_3\) of minimal rank \(t\), and one uses \(g_2+g_3 \to g(k{-}1)+g(t{+}1)\) (type 7) if \(t\) even (\(g_3 = g^-(t)\)) or \(g_2+g_3 \to g(k{-}1)+g^+(t{+}1)\) (type 6) if \(t\) odd (\(g_3 = g(t)\)).

Branch B: \(g_1 = g^+(m)\) polarized.

• Case 3 (\(m \ge 3\)): one shows \(a_{m+1} {\lt} c_{m+1}\) and \(b_{m-1} {\lt} d_{m-1}\). If \(X \supset 2g_1\) use \(2g^+(m) \to g^+(m{-}2)+g^+(m{+}2)\) (type 8, diagonal); otherwise with \(g_2\) minimal in \(X-g_1\), rank \(k\), take \(g_1+g_2 \to g(m{-}1)+g^+(k{+}1)\) (type 6) if \(g_2 = g(k)\), \(g_1+g_2 \to g(m{-}1)+g(k{+}1)\) (type 7) if \(g_2 = g^-(k)\), and \(g_1+g_2 \to g^+(m{-}2)+g^+(k{+}2)\) (type 8) if \(g_2 = g^+(k)\).

• Case 4 (\(m = 2\)): \(a_3 {\lt} c_3\); if \(b_1 {\lt} d_1\) proceed as in Case 1, else \(a_1 {\lt} c_1\) and with \(g_2\) a negative/nonpolarized gene of minimal rank \(k\) use \(g_1+g_2 \to g(1)+g^+(k{+}1)\) (type 6) if \(g_2 = g(k)\) or \(g_1+g_2 \to g(1)+g(k{+}1)\) (type 7) if \(g_2 = g^-(k)\).

• Case 5 (\(m = 1\)): \(a_1 = b_1 {\lt} c_1 = d_1\), so \(X\) has a negative/nonpolarized gene \(g_2\) of minimal rank \(k\); then \(a_j {\lt} c_j\) for \(1 \le j \le k\) and \(g_1+g_2 \to g^+(k{+}1)\) (type targeting a single gene) if \(g_2 = g(k)\) or \(g_1+g_2 \to g(k{+}1)\) if \(g_2 = g^-(k)\).

The charge-switch “WLOG \(a_m {\lt} c_m\) / \(g_1 = g^+\)” is, in Lean, a local negation argument via MixLambdaPi.Step.of_neg; it is available because the global Case A hypothesis \(a_X(1) {\lt} a_Y(1)\) is invariant under negation at the symmetric odd level \(1\) (for label 1; for label 2 level \(1\) is asymmetric and the global split already fixes the charge).

After removing common genes and applying the lifting reduction, the proof may assume disjoint support and the strict rank-growth condition

where \(\sigma (X^{(i)})=(a_i,b_i)\), \(\sigma (Y^{(i)})=(c_i,d_i)\), \(r_i=a_i+b_i\), and \(s_i=c_i+d_i\). If \(X\) contains a double nonpolarized gene \(2g(m)\), the first §17 branch mutates it as

choosing \(\epsilon \) from the strict component at level \(m\). Thus the remaining core assumes that \(X\) is polarized. In Lean this reduction is the nonpolarized branch preceding the private theorem exists_mutation_le_polarized_remaining.

Let \(m\) be minimal such that \(X\) contains \(g^+(m)+g^-(m)\). Since \(Y^{(m)}\) is nonzero and the relevant parity makes \(r_m,s_m\) even, §17 obtains \(s_m-r_m\ge 2\).

The formal branch splits by multiplicities at this minimal rank.

• If \(X\) contains \(2g^+(m)+2g^-(m)\), use the type-13 style diagonal mutation

  \[ 2g^+(m)+2g^-(m)\longrightarrow 2g(m-1)+2g(m+1). \]

• If \(X\) contains \(2g^\epsilon (m)+g^{-\epsilon }(m)\) but not \(2g^{-\epsilon }(m)\), switch signs if necessary and first handle \(2g^+(m)+g^-(m)\). When \(Y^{(m+1)}\ne 0\), choose the component \(\epsilon _1\) for which

  \[ r^{\epsilon _1}(X^{(m+1)}){\lt}r^{\epsilon _1}(Y^{(m+1)}), \]

  and use

  \[ 2g^+(m)+g^-(m)\longrightarrow 2g(m-1)+g^{\epsilon _1}(m+2). \]

  In Lean this is the type-16 branch. The component choice is matched to the outgoing polarized gene \(g^{\epsilon _1}(m+2)\); the opposite-component alternatives are transferred to type 15 by the drop inequalities.

• If \(Y^{(m+1)}=0\), disjointness and dominance imply \(Y\supset 2g(m+1)\) and hence \(b_{m-1}=1{\lt}d_{m-1}\) in the positive-double normalization. The mutation is

  \[ 2g^+(m)+g^-(m)\longrightarrow g^+(m-2)+2g(m+1), \]

  the type-17 branch. The Lean helpers exists_mutation_le_type17_diagonal_positive and exists_mutation_le_type17_diagonal_negative encode the two sign orientations. The boundary \(m=1\) must be handled separately because the formal source \(g^\epsilon (m-2)\) would have rank zero.

• If only \(g^+(m)+g^-(m)\) is present, with neither double multiplicity, §17 first uses a strict gap at level \(m-1\). If the same component is strict at level \(m+1\), use

  \[ g^+(m)+g^-(m)\longrightarrow g^+(m-2)+g^-(m+2) \]

  or its sign-swapped counterpart. If the forward component is equal, the drop inequalities transfer strictness to the other component. If both components at \(m+1\) are equal, then \(Y^{(m+1)}=0\), so \(Y\supset 2g(m+1)\); choose a maximal-rank remaining gene \(g^\epsilon (k)\) in \(X-g^+(m)-g^-(m)\) and use

  \[ g^\epsilon (k)+g^+(m)+g^-(m) \longrightarrow g^\epsilon (k-2)+2g(m+1). \]

  The smallest-rank cases are treated separately: rank \(1\) at label \(3\) uses the paper’s minimal-rank remainder argument, while rank \(2\) at label \(4\) uses the even-rank boundary argument. Above the boundary the same Type 11 window profile applies after the parity normalization.

Once all equal-rank pairs have been eliminated, let \(m\) be the minimum rank of a gene in \(X\) and, after sign switch, assume \(X\supset g^+(m)\) and \(X\not\supset g^-(m)\). The paper then splits into four cases.

• \(m\ge 3\). Drop inequalities give \(a_{m+1}{\lt}c_{m+1}\) and \(b_{m-1}{\lt}d_{m-1}\). If \(X\supset 2g^+(m)\), use \(2g^+(m)\to g^+(m-2)+g^+(m+2)\). Otherwise take the minimum-rank gene \(g^\epsilon (k)\) in \(X-g^+(m)\) and use \(g^+(m)+g^\epsilon (k)\to g^+(m-2)+g^\epsilon (k+2)\), with the inequalities propagated along the window from \(m\) to \(k\).

• \(m=2\). First obtain \(a_3{\lt}c_3\). If \(b_1{\lt}d_1\), reduce to the preceding pattern. If \(b_1=d_1\), then \(a_1{\lt}c_1\) and a minimal negative gene \(g^-(k)\) with \(k\ge 4\) exists. If \(a_{k+1}{\lt}c_{k+1}\) use \(g^+(2)+g^-(k)\to g^+(k+2)\); otherwise the inequalities force \(X\supset 2g^-(k)\) and one uses \(g^+(2)+2g^-(k)\to 2g(k+1)\).

• \(m=1\) and \(X\supset 2g^+(1)\). Minimality gives a negative gene \(g^-(k)\), \(k\ge 3\). If \(a_{k+1}{\lt}c_{k+1}\) use \(2g^+(1)+g^-(k)\to g^+(k+2)\); otherwise force \(X\supset 2g^-(k)\) and use \(2g^+(1)+2g^-(k)\to 2g(k+1)\).

• \(m=1\) and \(X\not\supset 2g^+(1)\). The gap \(s_1-r_1\ge 2\) implies that \(X\) has at least three genes. Write \(X=g^+(1)+g^\epsilon (k)+g^{\epsilon _1}(t)+X_1\) with \(3\le k\le t\) and no gene of \(X_1\) below \(t\). Mutate

  \[ g^\epsilon (k)+g^{\epsilon _1}(t) \longrightarrow g^\epsilon (k-2)+g^{\epsilon _1}(t+2), \]

  closing by the strict gaps at \(k-1\) and the propagated window inequalities; the subcase \(k=t\) uses the same-sign rank difference comparison at levels \(k-1\) and \(k+1\).

The Lean statements quantify over every \(n\) and take \(X,Y\in V(n)=\{ T\in V:\operatorname {rank}(T)=n\} \). This is equivalent to the paper’s whole-variety formulation, which assumes \(X\le Y\) and \(\operatorname {sig}(X)=\operatorname {sig}(Y)\). Indeed, equality of signatures implies equality of ranks, while under \(X\le Y\), equality of ranks forces equality of the two signature components at level zero.

The strong induction therefore requires equal rank only for each pair to which its hypothesis is applied. Removing a common gene lowers both ranks by the same amount. In the sigma-agreement branch, \(\sigma _X(k)=\sigma _Y(k)\) implies that \(X^{(k)}\) and \(Y^{(k)}\) have equal rank; their common new rank is strictly smaller than the original one. Odd \(k\) may exchange labels \(3\) and \(4\), but it does not disturb this rank equality.