Dependencies

For each of the five varieties, \(X\) mutates to \(Y\) if and only if there is a nonempty finite chain of primitive steps

Thus the one-step descent theorem yields exactly Djoković’s “enough mutations” statement, not merely its local reduction lemma.

For \(k \in \mathbb {N}\), \(X_{\le k}\) (below) filters genes with rank \(\le k\), and \(X_{{\gt} k}\) (above) filters genes with rank \({\gt} k\). We have \(X = X_{\le k} + X_{{\gt} k}\).

A chromosome is a finitely supported function \(X \colon \mathtt{Gene} \to \mathbb {N}\), i.e. a formal sum of genes with non-negative integer multiplicities. We write \(\mathtt{Chromosome} = \mathtt{Gene} \to _0 \mathbb {N}\).

For chromosomes \(X\) and \(Y\), we say \(X\) dominates \(Y\) (written \(Y \le X\)) if \(\mathrm{sig}(Y^{(k)}) \le \mathrm{sig}(X^{(k)})\) componentwise for all \(k \ge 0\), where \(X^{(k)}\) denotes the \(k\)-th derivative.

The lift operation is an additive homomorphism mapping a gene \((n,\varepsilon )\) to \((n+1,\varepsilon )\).

The prime (derivative) operation \(X \mapsto X'\) is the additive homomorphism that maps a gene \((n, \varepsilon )\) to the gene \((n-1,\varepsilon )\) when \(n{\gt}1\), and sends rank-one genes to \(0\).

The rank of a chromosome \(X\) is \(\mathrm{rank}(X) = \sum _g X(g) \cdot \mathrm{rank}(g)\).

The signature of a chromosome \(X\) is the additive extension: \(\mathrm{sig}(X) = \sum _{g} X(g) \cdot \mathrm{sig}(g) \in \mathbb {Q} \times \mathbb {Q}\).

A gene \(g = (n, \varepsilon )\) consists of a rank \(n \in \mathbb {N}\) and a type \(\varepsilon \in \mathtt{GeneType}\).

For \(n \ge 1\) and a type \(\varepsilon \), \(\mathtt{Gene.ofRank}\, n\, \varepsilon \) is the one-gene chromosome consisting of the gene \((n,\varepsilon )\) with multiplicity one; for \(n=0\) it is the zero chromosome. The variant \(\mathtt{Gene.ofRankAlt}\) uses the alternating type \((-1)^{n-1}\varepsilon \).

The signature of a gene \(g = (n, \varepsilon )\) is a pair \((a, b) \in \mathbb {Q} \times \mathbb {Q}\) defined by:

• If \(\varepsilon = \mathtt{NonPolarized}\): \((a,b) = (n/2,\, n/2)\).

• If \(\varepsilon = \mathtt{Positive}\): \((a,b) = (\lceil n/2 \rceil ,\, \lfloor n/2 \rfloor )\).

• If \(\varepsilon = \mathtt{Negative}\): \((a,b) = (\lfloor n/2 \rfloor ,\, \lceil n/2 \rceil )\).

A gene type is one of three polarization types: \(\mathtt{NonPolarized}\), \(\mathtt{Positive}\), or \(\mathtt{Negative}\). There is a natural involution \(\varepsilon \mapsto -\varepsilon \) that swaps \(\mathtt{Positive}\) and \(\mathtt{Negative}\) and fixes \(\mathtt{NonPolarized}\).

A pair \((X, Y)\) of chromosomes forms a mutation if:

1. \(X \ne Y\),

2. \(\mathrm{sig}(X) = \mathrm{sig}(Y)\),

3. \(X \le Y\) (the target dominates the source).

A chromosome is non-polarized if every gene in its support has type \(\mathtt{NonPolarized}\).

A chromosome \(X\) is polarized if every gene in its support has type \(\ne \mathtt{NonPolarized}\).

The prime operation on varieties induces a permutation of the five labels: \(V_i' = V_{\pi (i)}\).

The two primitive relations have exactly the nine constructors above; their step relations add an arbitrary common remainder.

For \(1{\lt}m\le n\),

For \(1{\lt}m\le n\),

For \(m\le n\),

For \(m\le n\),

For \(m\le n\),

For \(1{\lt}m\le n\),

For \(m\le n\),

For \(1{\lt}m\le n\),

A primitive mutation on \(\mathrm{Mix}(\mathrm{Lambda},\mathrm{Pi})\) is one of the five types above; a step is a primitive mutation plus an arbitrary common summand. The variety \(\mathrm{Mix}(\mathrm{Pi},\mathrm{Lambda})\) (label \(2\)) carries the mirror-image relations (MixPiLambda.Primitive, MixPiLambda.Step).

For \(m\le n\),

For \(m{\lt}n\),

For \(m{\lt}n\),

For \(m\le n\),

For \(1{\lt}m\le n\),

The global mutation step relation is indexed by the five labels. Its five cases are the concrete relations Pi.Step, MixLambdaPi.Step, MixPiLambda.Step, Mix2LambdaPi.Step, and MixPi2Lambda.Step.

Every chromosome decomposes as \(X = X_{\mathrm{odd}} + X_{\mathrm{even}}\) where \(X_{\mathrm{odd}}\) (resp. \(X_{\mathrm{even}}\)) collects genes of odd (resp. even) rank.

A primitive mutation on \(\mathrm{Pi}\) is exactly one of the three types above. Adding a common chromosome belongs to the separate step relation below.

A step on \(\mathrm{Pi}\) is a primitive mutation plus an arbitrary summand: \(\mathrm{Step}(X+Z, Y+Z)\) whenever \(\mathrm{Primitive}(X, Y)\).

For \(1\le m\le n\),

This is equation (8.1).

For \(1{\lt}m\le n\),

This is equation (8.2).

Put \(g_\varepsilon (r)=g^{(-1)^{r-1}\varepsilon }(r)\). For \(1\le m\le n\),

Lean’s Gene.ofRankAlt implements the alternating subscript. This is equation (8.3).

For a chromosome \(X\), the sigma sequence is the function \(\sigma _X(k) = \mathrm{sig}(X^{(k)}) \in \mathbb {Q} \times \mathbb {Q}\). We write \(a_X(k) = \sigma _X(k).1\) and \(b_X(k) = \sigma _X(k).2\).

A variety is an additive submonoid of \(\mathtt{Chromosome}\).

The five labeled varieties \(V_0, \ldots , V_4\) indexed by \(\mathrm{Fin}\, 5\) are:

• \(V_0 = \mathrm{Pi}\)

• \(V_1 = \mathrm{Mix}(\mathrm{Lambda}, \mathrm{Pi})\)

• \(V_2 = \mathrm{Mix}(\mathrm{Pi}, \mathrm{Lambda})\)

• \(V_3 = \mathrm{Mix}(2\mathrm{Lambda}, \mathrm{Pi})\)

• \(V_4 = \mathrm{Mix}(\mathrm{Pi}, 2\mathrm{Lambda})\)

The variety \(\mathrm{Lambda}\) is the filtered variety of all non-polarized chromosomes.

Given a pair of varieties \((V_1, V_2)\), the mixed variety \(\mathrm{Mix}(V_1, V_2)\) consists of all chromosomes whose even part lies in \(V_1\) and odd part lies in \(V_2\).

The variety \(\mathrm{Pi}\) is the filtered variety of all polarized chromosomes.

Given a predicate \(p\) on genes, the filtered variety \(V_p\) consists of all chromosomes whose support satisfies \(p\).

The dominance preorder is an ordered cancel additive monoid structure on chromosomes. In particular, subtracting the same present gene from two strictly ordered chromosomes preserves strict order.

Prime lowers the rank of an \(\mathtt{ofRank}\) generator by one, iterated prime lowers it by the number of iterations, and the coefficient of a gene \(g\) in \(X'\) is the coefficient of the rank-shifted gene \((g.rank+1,g.type)\) in \(X\).

The below/above filters decompose a chromosome. The below part of rank at most \(k\) is killed by \(k\) primes, so \(X\) can be reconstructed from \(X^{(k)}\) by lifting, together with its below-\(k\) part.

If \(\mathrm{sig}(X)=0\), then \(X=0\).

The signature of \(\mathtt{Gene.ofRank}\, n\, \varepsilon \) is the signature of the corresponding gene when \(n\ne 0\), and zero when \(n=0\). For polarized types the file also records the one-step recurrence obtained by lowering the rank and changing, or preserving, the sign according to the parity.

For any chromosome \(X\), the sum of the two signature components equals the rank: \(\mathrm{sig}(X).1 + \mathrm{sig}(X).2 = \mathrm{rank}(X)\).

If \(X, Y \in \mathrm{Pi}\) satisfy \(\mathrm{sig}(X^{(k)}) = \mathrm{sig}(Y^{(k)})\) for all \(k \ge 0\), then \(X = Y\).

For any gene \(g\), we have \(a(g) + b(g) = \mathrm{rank}(g)\).

If \(X \ne 0\), then \(\mathrm{maxRank}(X') {\lt} \mathrm{maxRank}(X)\).

Each of type 4–8 satisfies \(X \ne Y\), preserves total signature, and satisfies \(X\le Y\) in the dominance order, in both parity orientations.

Without the Case A inequality, the full §15.10 sub-case follows from 78: if \(a_X(1) {\lt} a_Y(1)\) apply Case A directly; otherwise \(a_X(1) = a_Y(1)\) and one applies Case A to the negated pair \((-X, -Y)\) (which stays in the same variety, swaps the sigma components, and turns the equality into the strict Case A inequality), then transports the resulting step back through \(\mathrm{Step}\) under negation (MixLambdaPi.Step.of_neg). Both mixed varieties are handled this way, closing Case 4 in the joint induction.

If an iterated prime \(X^{(k)}\) admits a step to \(U\) in the corresponding prime-shifted label, then that step lifts to a step \(X\to Z\) in the original label, with \(Z^{(k)}=U\). Moreover the signatures of \(X^{(i)}\) and \(Z^{(i)}\) agree for every \(i\le k\).

Type 1 mutations satisfy \(X_1 \le Y_1\).

Type 1 mutations preserve the signature at all levels: \(\mathrm{sig}(X_1^{(k)}) = \mathrm{sig}(Y_1^{(k)})\) for all \(k\).

Type 2 mutations satisfy \(X_2 \le Y_2\).

Type 2 mutations preserve the signature at all levels.

Type 3 mutations satisfy \(X_3 \le Y_3\).

Type 3 mutations preserve the signature at all levels.

\((X')_{\mathrm{even}} = (X_{\mathrm{odd}})'\) and \((X')_{\mathrm{odd}} = (X_{\mathrm{even}})'\).

Every primitive mutation satisfies the mutation conditions.

A step remains a mutation after adding the same polarized summand to both sides.

For \(X, Y \in \mathrm{Pi}\), if \(X \le Y\) and \(Y \le X\), then \(X = Y\). Hence \(\mathrm{Pi}\) carries a partial order.

\(\mathrm{Lambda}' = \mathrm{Lambda}\).

The prime operation is a left inverse to lift: \((\mathrm{lift}\, X)' = X\) for all \(X\).

\(\mathrm{Pi}' = \mathrm{Pi}\).

If \(p\) is lift-stable (i.e. \(p(g)\) iff \(p(\mathrm{lift}(g))\)), then the prime of a filtered variety is itself: \(V_p' = V_p\).

The sigma sequence is antitone (componentwise decreasing).

The inequalities between \(b_0\) and \(a_1\) detect the sign of a rank-one polarized gene. Summing this test over a chromosome produces a negative gene whenever \(b_0{\gt}a_1\).

The alternating inequalities imply useful global comparisons: later drops are bounded by the initial drop, and telescoping gives \(a_1-a_i \le b_0-b_{i-1}\) for \(i\ge 1\).

The first and second components separately form decreasing sequences and both are eventually zero. These are the formal versions of conditions (15.2) and (15.3).

If \(X \in \mathrm{Pi}\), the successive drops \(a_X(k)-a_X(k+1)\) and \(b_X(k)-b_X(k+1)\) satisfy the alternating inequalities (15.6) and (15.7).

If \(X {\lt} Y\) in \(\mathrm{Pi}\), then \(\sigma _X(k) \le \sigma _Y(k)\) componentwise for all \(k\) with strict inequality for some \(k\).

There exists \(K\) such that \(\sigma _X(k) = 0\) for all \(k \ge K\).

The components of the sigma sequence satisfy interlacing inequalities. If \(k\) is even, then \(b_X(k+1) \le a_X(k)\) and \(a_X(k+1) \le b_X(k)\). If \(k\) is odd, the inequalities are reversed.

For a type-3 primitive mutation, the sigma sequence of the target is obtained from the source by adding an explicit interval-supported increment.

For a polarized chromosome, the drop in the first sigma component from \(k\) to \(k+1\) counts genes in \(X^{(k)}\) that are positive in the alternating basis; the drop in the second component counts the corresponding negative genes.

If \(X \in \mathrm{Pi}\), the signature components of \(X\) are natural numbers.

In the disjoint-support case, if \(X\) contains a positive and a negative gene of equal rank, the proof extracts the corresponding type-1 primitive source and shows that the resulting mutation remains below \(Y\). The Lean proof packages the rank-absence and summand-extraction facts used for this step as internal auxiliaries of this lemma.

For every label \(i\), the variety prime of \(V_i\) is exactly \(V_{\pi (i)}\). Iterating this equality tracks membership after iterated prime operations.

If the two component varieties are closed under taking odd and even parts, then prime swaps the two entries of a mixed variety: \(\mathrm{Mix}(V_1,V_2)'=\mathrm{Mix}(V_2',V_1')\).

YoungDiagram/Theorem6/MixCase4.lean Let \(X, Y \in \mathrm{Mix}(\mathrm{Lambda},\mathrm{Pi})\) have equal rank \(m+2\) with \(X {\lt} Y\) in the dominance order (\(Y\) dominates \(X\)), and suppose

1. (disjoint supports) no gene is positive in both \(X\) and \(Y\);

2. (no sigma agreement) there is no \(k \ge 1\) with \(X^{(k)\prime } \ne 0\) and \(\sigma _X(k) = \sigma _Y(k)\);

3. (no polarized pair) \(X\) contains no positive/negative gene pair of equal rank;

4. (Case A inequality) \(a_X(1) {\lt} a_Y(1)\).

Then there is a step from \(X\) to some \(Z \le Y\) in \(\mathrm{Mix}(\mathrm{Lambda},\mathrm{Pi})\). The mirror declaration exists_mutation_le_fifteen_ten_PL_caseA closes the label-\(2\) orientation.

For any \(X,Y\in \mathrm{Pi}\) of rank \(n\) with \(X{\lt}Y\), there exists \(Z\in \mathrm{Pi}\) such that \(\mathrm{Step}(X,Z)\) and \(Z\le Y\). Iterating this one-step result gives the mutation chain in Theorem 6.

Let \(V\) be any of the five varieties in (6.2), and let \(X,Y\in V\) have equal rank. If \(X{\lt}Y\), then there exists \(Z\in V\) such that

Label \(0\) is proved by strong induction inside \(\Pi \). Labels \(1\) and \(2\) are proved together because prime exchanges their varieties; labels \(3\) and \(4\) are proved by the analogous joint induction. In each proof, common genes are cancelled, equality at a positive sigma level is reduced by the lifting theorem, and the remaining strict case is discharged by the primitive classification of §15, §16, or §17. The joint Lean entry points are MixVarietyJoint.exists_mutation_le_joint and Mix2LambdaJoint.exists_mutation_le_joint.

Every constructor of (8.1)–(8.17) has distinct source and target, preserves total signature, and satisfies source \(\le \) target. Hence adding a common remainder also produces a mutation.