Equation 1729

In this chapter we study magmas that satisfy equation 1729,

\[ x = (y \diamond y) \diamond ((y \diamond x) \diamond y).\qquad\text{(1)} \]

for all \(x,y\). Using the squaring operator \(Sy := y \diamond y\) and the left and right multiplication operators \(L_y x := y \diamond x\) and \(R_y x = x \diamond y\), this law can be written as

\[ L_{Sy} R_y L_{y} x = x. \]

This implies that \(L_y\) is injective and \(L_{Sy}\) is surjective, hence \(L_{Sy}\) is invertible. If \(y\) is a square (i.e., \(y \in SM\)), then \(L_y\) and \(L_{Sy}\) are both invertible, hence now \(R_y\) is also invertible, with inverse \(R_y^{-1} = L_y L_{Sy}\). We rewrite this as

\[ L_y = R_y^{-1} L_{Sy}^{-1}\qquad\text{(2)} \]

for all \(y \in SM\).

To build a magma satisfying 1729 but not 817, it thus suffices to produce

  • a 1729 magma \(SM\);
  • a set \(N\) of “non-squares”;
  • a squaring map \(S': N \to SM\);
  • bijections \(L'_a, R'_a: N \to N\) for all \(a \in SM\) satisfying the axioms (i)-(iv); and
  • an operation \(\diamond': N \times N \to SM \uplus N\) satisfying the axioms (v)-(vii).

The magma \(SM\) is defined as follows:

DefinitionDefinition of \(SM\)#

Take \(SM\) to be a countably infinite abelian group of exponent \(4\), generated by generators \(E_n\) for \(n \in \mathbb{N}\) subject to the relations \(4E_n=0\).

Lean

Formalized as Eq1729.SM.

Sources
LeanEq1729.SM
Used by 2
Used byPartial solution · Definition of \(R'_a\)

LemmaBasic properties of \(SM\)#

\(SM\) is a 1729 magma, the squaring operation \(S: SM \to SM\) is just the doubling map \(Sa = 2a\), and the double squaring map \(S^2: SM \to SM\) is constant: \(S^2 a = 0\) for all \(a \in SM\).

Proof

Routine verification.

Lean

Formalized as Eq1729.SM_square_eq_double, Eq1729.SM_square_square_eq_zero, Eq1729.SM_satisfies_1729.

Sources
LeanEq1729.SM_square_eq_double · Eq1729.SM_square_square_eq_zero · Eq1729.SM_satisfies_1729

We now define \(N\), as well as some Cayley graph structures on it.

DefinitionDefinition of \(N\)#

Take \(N\) to be the free non-abelian group with a generator \(e_a\) for each \(a \in SM\), thus \(N\) is the set of reduced words using the alphabet \(e_a\), \(e_a^{-1}\). Two elements \(x,y \in SM\) are said to be adjacent if \(x = e_a y\) or \(y = e_a x\) for some \(a \in SM\); this defines a left Cayley graph on \(N\). We make a partial ordering \(\leq\) on \(N\) by declaring \(y \leq x\) if \(y\) is a right subword of \(x\) (or equivalently, \(y\) is on the unique simple path from \(1\) to \(x\)). For instance, if \(a,b,c \in SM\) are distinct, then

\[ 1 \leq e_c \leq e_b^{-1} e_c \leq e_a e_b^{-1} e_c. \]

If \(x \in N\) is not the identity, we define the parent of \(x\) to be the unique element \(y \in N\) adjacent to \(x\) whose reduced word is shorter. For instance, the parent of \(e_a e_b^{-1} e_c\) is \(e_b^{-1} e_c\).

Lean

Formalized as Eq1729.N, Eq1729.N_order, Eq1729.parent.

Sources
LeanEq1729.N · Eq1729.N_order · Eq1729.parent
Used by 3
Used byBasic properties of \(N\) · Partial solution · Definition of \(R'_a\)

LemmaBasic properties of \(N\)#

\(N\) is countable, and \(\leq\) is a partial ordering.

Proof

Routine verification.

Lean

Formalized as Eq1729.N_countable, Eq1729.N_order.

Sources
LeanEq1729.N_countable · Eq1729.N_order
Uses 1
Statement usesDefinition of \(N\)

We will define the right multiplication operators \(R'_a: N \to N\) using the group action:

DefinitionDefinition of \(R'_a\)#

We set

\[ R'_a x := e_a x\qquad\text{(3)} \]

for all \(a \in SM\) and \(x \in N\).

Lean

Formalized as Eq1729.R'.

Sources
LeanEq1729.R'
Uses 2 · Used by 1
Statement usesDefinition of \(SM\) · Definition of \(N\)
Used byBasic properties of \(R'_a\)

LemmaBasic properties of \(R'_a\)#

The operators \(R'_a\) are bijective and satisfy axiom (ii).

Proof

Routine verification.

Lean

Formalized as Eq1729.R'_axiom_iia, Eq1729.R'_axiom_iib.

Sources
LeanEq1729.R'_axiom_iia · Eq1729.R'_axiom_iib
Uses 1
Statement usesDefinition of \(R'_a\)

We defer construction of the squaring map \(S': N \to SM\) for now, but turn to left-multiplication. From two applications of (2) and the exponent 4 hypothesis we have

\[ L'_a = (R'_a)^{-1} (L'_{2a})^{-1} = (R'_a)^{-1} L'_0 R'_{2a}. \]

Thus, once \(L'_0\) is specified, we can define \(L'_a\) for all other \(a \in SM\) by the rule

\[ L'_a := (R'_a)^{-1} L'_0 R'_{2a}.\qquad\text{(4)} \]

Furthermore, from the \(a=0\) case of (2) we must also have the axiom

  • (i') \((L'_0)^2 = (R'_0)^{-1}\).

Conversely, we have

LemmaUsing \(L'_0\) to construct \(L'_a\)#

Suppose we have a bijection \(L'_0: N \to N\) that satisfies axiom (i'), and then define \(L'_a\) for all \(a \in SM\) by the formula (4). Then this recovers \(L'_0\) when \(a=0\) (to formalize this it may be convenient to give \(L'_0\) and \(L'_a\) distinct names), and the \(L'_a\) are all bijections and satisfy axiom (i). Furthermore, we have

\[ (L'_a)^{-1} := (R'_{2a})^{-1} L'_0 R'_0 R'_{a}\qquad\text{(5)} \]

for all \(a \in SM\).

Proof

Routine verification.

Lean

Formalized as Eq1729.L'.

Sources
LeanEq1729.L' · Eq1729.L'_0_eq_L₀'

We now write the other remaining axioms in terms of \(L'_0\) rather than \(L'_a\) using (4), (5), (3), and the magma law on \(SM\):

  • (iii') If \(R'_a x = y\) for some \(a \in SM\) and some \(x,y \in N\), then \((R'_{S'y})^{-1} L'_0 R'_{2S'y} (R'_{a - S'x})^{-1} L'_0 R'_{2(a - S'x)} y = x\).
  • (iv') For all \(x \in N\), we have \((R'_{S'x})^{-1} L'_0 R'_{2S'x} (R'_{S'x})^{-1} L'_0 R'_{2S'x} x = x\).
  • (v) For all \(x \in N\), we have \(x \diamond' x = S'x\).
  • (vi') For all \(y \in N\) and \(a \in SM\), we have \(e_a y \diamond' y = a - S'y\).
  • (vii') For all \(x,y \in N\) with \(x \diamond' y\) not already covered by rules (v) or (v'), we have \(x \diamond' y = z\) for some \(z \in N\). Furthermore, \(z \diamond' x = (R'_{2S'x})^{-1} L'_0 e_0 e_{S'x} y\).

Our task is now to find a function \(S': N \to SM\), a bijection \(L'_0: N \to N\), and an operation \(\diamond': N \times N \to M\) satisfying axioms (i'), (iii'), (iv'), (v), (vi'), (vii').

We will again use a greedy construction for this, but with some modifications. Firstly, the axiom (i'), together with (3) means that we cannot restrict \(L'_0\) to be partially defined on just finitely many values: any relation of the form

\[ L'_0 x = y \]

for some \(x,y \in N\) would automatically imply that

\[ L'_0 (R'_0)^n x = (R'_0)^n y\qquad\text{(6)} \]

and also

\[ L'_0 (R'_0)^n y = (R'_0)^{n-1} x\qquad\text{(7)} \]

for all \(n \in \mathbb{Z}\). Thus, \(L'_0\) becomes defined on two right cosets \(\langle e_0 \rangle x\), \(\langle e_0 \rangle y\) of \(N\), where \(\langle e_0 \rangle := \{ e_0^n: n \in \mathbb{Z}\}\) is an infinite cyclic subgroup of \(N\). In general, we will require that \(L'_0\) is defined on a finite union of cosets of \(\langle e_0\rangle\).

In a somewhat similar vein, axiom (vii'), if iterated naively, would mean that a given entry \(x \diamond' y = z\) of the multiplication table could potentially generate an infinite sequence of further entries, which unfortunately do not have as regular a pattern as the iterations (6), (7) of axiom (i'). So we will need to truncate this iteration by creating an addition category of “pending” identities \(I[x,y,z]\) of the form “\(z \diamond' x = (R'_{2S'x})^{-1} L'_0 R'_0 e_{S'x} y\)” for some \(x,y,z \in N\), which will be temporarily undefined because \(S'x\) is undefined. More precisely,

DefinitionPartial solution#

A partial solution \((L'_0, \diamond', S', {\mathcal I})\) is a collection of the following data:

  • A partially defined function \(L'_0: N \to N\), defined on a finite union of right cosets of \(\langle e_0\rangle\);
  • A partially defined operation \(\diamond': N \times N \to M\), defined on a finite set;
  • A partially defined function \(S': N \to SM\), defined on a finite set; and
  • A finite collection \({\mathcal I}\) of “pending identities” \(I[x,y,z]\), which one can think of either as ordered triples of elements \(x,y,z \in N\), or as formal strings of the form “\(z \diamond' x = (R'_{2S'x})^{-1} L'_0 R'_0 R'_{S'x} y\)” for some \(x,y,z \in N\).

Furthermore, the following axioms are satisfied:

  • (i”) \(L'_0 x\) is defined and equal to \(y\), then we have the identities (6), (7) for all \(n\in \mathbb{Z}\).
  • (S) If \(S'x\) is defined for some \(x \in N\), then \(S'y\) is defined for all \(y \leq x\).
  • (iii”) If \(R'_a x = y\) for some \(a \in SM\) and some \(x,y \in N\), and \(S'x, S'y\) are defined, then \((R'_{S'y})^{-1} L'_0 R'_{2S'y} (R'_{a-S'x})^{-1} L'_0 R'_{2(a-S'x)} y\) is defined and equal to \(x\).
  • (iv”) If \(x \in N\) is such that \(S'x\) is defined, then \((R'_{S'x})^{-1} L'_0 R'_{2S'x} (R'_{S'x})^{-1} L'_0 R'_{2S'x} x\) is defined and equal to \(x\).
  • (v”) If \(x \in N\) and \(x \diamond' x\) is defined, then \(S'x\) is defined and equal to \(x \diamond' x\).
  • (vi”) For all \(y \in N\) and \(a \in SM\), if \(R'_a y \diamond' y\) is defined, then \(a - S'y\) is defined and equal to \(R'_a y \diamond' y\).
  • (vii”) For all \(x,y \in N\) and \(x\) is not equal to \(y\) or \(R'_a y\) for any \(a \in SM\), and \(x \diamond' y\) is defined, then it is equal to some \(z \in N\). Furthermore, either \(I[x,y,z]\) is a pending identity, or else \(z \diamond' x\) and \((R'_{2S'x})^{-1} L'_0 R'_0 R'_{S'x} y\) are defined and equal to each other.
  • (P) If \(I[x,y,z]\) is a pending identity, then \(x,y,z \in N\), and \(Sx\) and \(z \diamond' x\) are undefined. Furthermore, \(z\) is not equal to \(x\) or \(R'_a x\) for any \(a \in SM\), and \(y\) is not of the form \((R'_0)^n x\) or \((R'_0)^n y_0\) for any \(n\), where \(y_0\) is the parent of \(x\).
  • (P') If \(I[x,y,z]\) and \(I[x,y',z]\) are pending identities, then \(y=y'\).
  • (P”) If \(I[x,y,z]\) is a pending identity, then \(x \diamond' y = z\).
  • (L) If \(y\) is the parent of \(x\) with \(x = R'_a y\), and \((R'_{a-S'y})^{-1} L'_0 R'_{2(a-S'y)} x\) is defined, then it is not equal to \(x\).

We say that one partial solution \((\tilde L'_0, \tilde \diamond', \tilde S', \tilde {\mathcal I})\) extends another if \((L'_0, \diamond', S', {\mathcal I})\) if \(\tilde L'\) is an extension of \(L'_0\), \(\tilde \diamond'\) is an extension of \(\diamond'\), and \(\tilde S'\) is an extension of \(S'\). (No constraint is imposed on the final components \(\tilde {\mathcal I}, {\mathcal I}\).) This is a preordering.

Lean

Formalized as Eq1729.PartialSolution.

Sources
LeanEq1729.PartialSolution
Uses 2 · Used by 2
Statement usesDefinition of \(SM\) · Definition of \(N\)
Used byChain of partial solutions · Existence of partial solution

LemmaExistence of partial solution#

There exists a partial solution.

Proof

Set \(L'_0, \diamond', S'\) to be empty functions, and have the set of pending identities to also be empty. The verification of the required axioms is then routine.

Lean

Formalized as Eq1729.TrivialPartialSolution.

Sources
LeanEq1729.TrivialPartialSolution
Uses 1 · Used by 1
Statement usesPartial solution
Used by1729 does not imply 817

LemmaChain of partial solutions#

Suppose that one has a sequence \((L'_{0,n}, \diamond'_{n}, S'_{n}, {\mathcal I}_n)\) of partial solutions, each one an extension of the previous, such that for any \(x, y \in N\), \(L'_{0,n} x\), \(x \diamond'_{n} y\), and \(S'_n x\) are defined for some \(n\). Then there exists a 1729 magma that does not satisfy 817.

Proof

Take the direct limit of the chain to obtain total functions \(L'_0, \diamond', S'\). The axioms (i'), (iii'), (iv”), (v”), (vi”), (vii”) of the partial solutions then easily imply that the direct limit satisfies the axioms (i'), (iii'), (iv'), (v), (vi'), (vii') (one also uses axiom (P) to note that all pending identities disappear in the direct limit). The claim now follows from Reduction to new axioms.

Lean

Formalized as Eq1729.use_chain.

Sources
LeanEq1729.use_chain
Uses 1 · Used by 1
Statement usesPartial solution
Used by1729 does not imply 817

Now we seek to enlarge a partial solution. We first make an easy observation:

PropositionEnlarging \(L'_0\)#

Suppose one has a partial solution in which \(L'_0 x\) is undefined for some \(x \in N\). Then one can extend the partial solution so that \(L'_0 x\) is now defined.

Proof

By axiom (i”), \(L'_0 (R'_0)^n x\) is undefined for every integer \(n\). Let \(d = E_m\) be a generator of \(SM\) that does not appear as a component of any index of any of the generators \(e_a\) appearing anywhere in the partial solution; such a \(d\) exists due to the finiteness hypotheses. We set \(L'_0 x := e_d\), and then extend by (6), (7), thus

\[ L'_0 (R'_0)^n x := (R'_0)^n e_d \]

and

\[ L'_0 (R'_0)^n e_d := (R'_0)^{n-1} x. \]

Because of the new nature of \(d\), no collisions in the partial function \(L_0\) are created by this operation. It is then easy to check that axiom (i”) is preserved by this operation, whereas none of the other axioms (S), (iii”), (iv”), (v”), (vi”), (vii”), (P), (P'), (P”) are affected by this extension. With some effort, axiom (L) can also be verified.

Lean

Formalized as Eq1729.enlarge_L₀'.

Sources
LeanEq1729.enlarge_L₀'
Used by 2
Used by1729 does not imply 817 · Enlarging \(L'_0\) many times

As a corollary, we have

PropositionEnlarging \(L'_0\) many times#

Suppose one has a partial solution. Let \(A\) be a finite subset of \(N\). Then one can extend the partial solution so that \(L'_0 x\) is now defined for all \(x \in A\).

Proof

Iterate Proposition Enlarging \(L'_0\) in the obvious fashion.

Lean

Formalized as Eq1729.enlarge_L₀'_multiple.

Sources
LeanEq1729.enlarge_L₀'_multiple
Uses 1 · Used by 1
Proof usesEnlarging \(L'_0\)
Used byEnlarging \(S'\) with induction hypothesis

Next, we provide a tool for enlarging the domain of definition of \(S'\). The main step is the following inductive one with extra axioms.

PropositionEnlarging \(S'\) with induction hypothesis and axioms#

Suppose one has a partial solution in which \(S'x\) is undefined for some \(x \in N\), but \(S'y\) is defined for all \(y < x\). (This hypothesis is vacuous for \(x=1\).) Let \(y_0\) be the parent of \(x\) (if \(x \neq 1\)), and assume the following additional axioms:

  • (A) If \(R'_a x = y_0\) for some \(a \in SM\), then \(L'_0 R'_{S' y_0} x\) is defined.
  • (B) If \(x = R'_a y_0\) for some \(a \in SM\), then \(L'_0 R'_{2(a-S'y_0)} x\) is defined.
  • (C) If \(I[x,y,z]\) for some \(y,z \in N\), and \(S'z\) is defined, then \(L'_0 R'_0 R'_{S'z} x\) is defined.

Then one can extend the partial solution so that \(S'x\) is now defined.

Proof

Let \(d_0, d_1 \in SM\) be generators \(E_{n_0}\) of \(SM\) that do not appear in the index \(a\) of any \(e_a\) that currently appears in the partial solution (of which there are only finitely many). We also set some further distinct generators \(d'_{y,z} \in SM\) for \(y,z \in SM\) that are distinct from each other and all previous generators (this is possible as we have infinitely many generators). We set \(S'x, x \diamond' x := d_0\); this preserves axiom (S) and (v”). We set

\[ L'_0 R'_{2d_0} x := e_{d_1} \]
\[ L'_0 R'_{2d_0} (R'_{d_0})^{-1} e_{d_1} := R'_{d_0} x \]

and then extend these choices using (6), (7) to recover axiom (i'), thus for instance

\[ L'_0 (R'_0)^n R'_{2d_0} x := (R'_0)^n e_{d_1} \]

and

\[ L'_0 (R'_0)^n e_{d_1} := (R'_0)^{n-1} R'_{2d_0} x \]

for all \(n \in \mathbb{Z}\).

To retain axiom (iii”), we perform the following actions:

  • If \(y_0\) is undefined, do nothing.
  • If \(R'_a x = y_0\) for some \(a \in SM\) (so that \(L'_0 R'_{S'y_0} x\) is defined, by hypothesis (A)), set \(L'_0 R'_{2(a-d_0)} y_0 := R'_{a-d_0} (R'_{2S'y_0})^{-1} R'_0 L'_0 R'_{S'y_0} x\). Then extend using (6), (7).
  • If \(x = R'_a y_0\) for some \(a \in SM\) (so that \(L'_0 R'_{2(a-Sy_0)} x\) is already defined, by hypothesis (B)), set \(L'_0 R'_{2d_0} (R'_{a-S'y_0})^{-1} L'_0 R'_{2(a-Sy_0)} x :=R'_{d_0} y_0\), and extend using (6), (7).

To retain axiom (P), we perform the following actions for each pending identity of the form \(I[x,y,z]\) for some \(y,z\), executed in some arbitrary order.

  • Remove this identity \(I[x,y,z]\) from the list of pending identities.
  • Set \(L'_0 R'_0 R'_{d_0} y := e_{d'_{y,z}}\), and \(x' \diamond y' := z'\), where \((x',y',z') := (z, x, (R'_{2d_0})^{-1} e_{d'_{y,z}})\). Extend all the new definitions of \(L'_0\) using (6), (7).
  • If \(S'x'\) is undefined, add \(I[x',y',z']\) as a pending identity.
  • If instead \(S'x'\) is defined (which makes \(L'_0 R'_0 R'_{S'x'} y'\) defined, by axiom (C)), set \(x'' \diamond y'' = z''\), where \((x'',y'',z'') := (z', x', (R'_{2S'x'})^{-1} L'_0 R'_0 R'_{S'x'} y')\). Then add \(I[x'',y'',z'']\) as a pending identity.

One can check that these definitions do not cause any collisions in the partial function \(L'_0\), and that axioms (i'), (iii'), (iv”), (v”), (vii”), (P), (P'), (P”) are preserved; the remaining axiom (vi”) is unaffected by this extension. Axiom (L) can also be shown to be preserved after a tedious calculation.

Lean

Formalized as Eq1729.enlarge_S'_induction_with_axioms.

Sources
LeanEq1729.enlarge_S'_induction_with_axioms
Used by 1
Used byEnlarging \(S'\) with induction hypothesis

PropositionEnlarging \(S'\) with induction hypothesis#

Suppose one has a partial solution in which \(S'x\) is undefined for some \(x \in N\), but \(S'y\) is defined for all \(y < x\). (This hypothesis is vacuous for \(x=1\).) Then one can extend the partial solution so that \(S'x\) is now defined.

Proof

Let \(y_0\) be the parent of \(x\), that is to say the unique neighbor of \(x\) in the path to \(1\) (this is only defined for \(x \neq 1\)), then by axiom (i”) \(y_0\) is the unique neighbor for which \(S'y_0\) is defined, and we either have \(x = R'_a y_0\) or \(R'_a x = y_0\) for some unique \(a \in SM\).

By using Enlarging \(L'_0\) many times, we may impose axioms (A), (B), (C) without loss of generality, as this only imposes a finite set of conditions. The claim now follows from Enlarging \(S'\) with induction hypothesis and axioms.

Lean

Formalized as Eq1729.enlarge_S'_induction.

Sources
LeanEq1729.enlarge_S'_induction
Uses 2 · Used by 1
Proof usesEnlarging \(L'_0\) many times · Enlarging \(S'\) with induction hypothesis and axioms
Used byEnlarging \(S'\)

As a corollary, we have

PropositionEnlarging \(S'\)#

Suppose one has a partial solution in which \(S'x\) is undefined for some \(x \in N\). Then one can extend the partial solution so that \(S'x\) is now defined.

Proof

Obtained by induction from Proposition Enlarging \(S'\) with induction hypothesis, using the fact that there are no infinite descending chains in \(N\).

Lean

Formalized as Eq1729.enlarge_S'.

Sources
LeanEq1729.enlarge_S'
Uses 1 · Used by 2
Proof usesEnlarging \(S'\) with induction hypothesis
Used by1729 does not imply 817 · Enlarging \(\diamond\)

Finally, we give a tool for enlarging \(\diamond\):

PropositionEnlarging \(\diamond\)#

Suppose one has a partial solution in which \(x \diamond' y\) is undefined for some \(x,y \in N\). Then one can extend the partial solution so that \(x \diamond' y\) is now defined.

Proof

By applying Enlarging \(S'\) as needed, we may assume without loss of generality that \(S'x\) and \(S'y\) are already defined (among other things, this removes the possibility that \(x \diamond' y\) is part of a pending identity). If this makes \(x \diamond' y\) defined, then we are done, so we may assume that this is not the case.

Similarly, by using Enlarging \(L'_0\), we may assume without loss of generality that \(L'_0 R'_0 R'_{S'x} y\) is defined.

We now divide into cases:

Case 1: \(x=y\). In this case we set \(x \diamond' y := S'x\). It is clear that this preserves axiom (v”), and no other axiom is impacted.

Case 2: If \(x = R'_a y\) for some \(a \in SM\), then we set \(x \diamond' y := a - S'y\). This preserves axiom (vi”), and no other axiom is impacted.

Case 3: If \(x\) is not equal to \(y\) or \(R'_a y\) for any \(a \in SM\). Let \(d_0 \in SM\) be a generator that does not appear as a component of any index of any of the generators \(e_a\) appearing anywhere in the partial solution. We set \(x \diamond' y := z\) with \(z := e^2_{d_0}\).

This temporarily disrupts axiom (vii”). To recover it, we perform the following actions.

  • Set \(x' \diamond' y' = z'\), where \((x',y',z') := (z, x, (R'_{2S'x})^{-1} L_0 R'_0 R'_{Sx} y)\).
  • Add \(I[x',y',z']\) as a pending identity.

One can check that these definitions do not cause any collisions in the partial function \(L'_0\), and that axioms (i'), (vii'), (P), (P') are preserved; the remaining axioms (S), (iii”), (iv”), (v”), (vi”) are unaffected by this extension.

Lean

Formalized as Eq1729.enlarge_op.

Sources
LeanEq1729.enlarge_op
Uses 1 · Used by 1
Proof usesEnlarging \(S'\)
Used by1729 does not imply 817

Theorem1729 does not imply 817#

There exists a magma that satisfies equation 1729 but not equation 817.

Proof

Starting from Existence of partial solution and applying Enlarging \(L'_0\), Enlarging \(S'\), Enlarging \(\diamond\) alternatingly, one can find a chain of partial solution that are total in the limit. The claim now follows from Chain of partial solutions.

Lean

Formalized as Eq1729.not_817.

Sources
LeanEq1729.not_817
Uses 5
Proof usesExistence of partial solution · Enlarging \(L'_0\) · Enlarging \(S'\) · Enlarging \(\diamond\) · Chain of partial solutions

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.