more work

src/main.typ

@@ -696,13 +696,13 @@ Enunciamo ora un lemma che utilizzeremo più volte in seguito.
     K = D_0 stretch(arrow)^(m_1) dots.c stretch(arrow)^(m_n) D_n = #skein.unit-medium
   $
 
-  con $m_i$ mosse di tipo I, II, III. Ora l'idea modificare questa successione di mosse in modo da ottenere una nuova successione composta solo da mosse II e III che termina con un diagramma composto solo da riccioli.
+  con $m_i$ mosse di tipo I, II, III. Ora l'idea è modificare questa successione di mosse in modo da ottenere una nuova successione composta solo da mosse II e III che termina con un diagramma composto solo da riccioli.
 
   Applichiamo induttivamente le seguenti modifiche ad ogni mossa $m_i$ nella sequenza, tenendo traccia di cosa succede man mano agli incroci:
 
-  - Se abbiamo una mossa di tipo I che rimuove un ricciolo, allora scartiamo la mossa in modo da conservare il ricciolo. In particolare in tutte le mosse successive non utilizzeranno questo incrocio in quanto nella successione originale veniva cancellato quindi questo sarà uno di quei riccioli che rimarrà fino al diagramma finale.
+  - Se abbiamo una mossa di tipo I che rimuove un ricciolo, allora scartiamo la mossa in modo da conservare il ricciolo. In particolare in tutte le mosse successive della sequenza originale non utilizzeranno questo incrocio in quanto questa mossa lo cancellava quindi questo sarà uno di quei riccioli che rimarrà nel nuovo diagramma finale.
 
-  - Se abbiamo una mossa di tipo I che aggiunge un ricciolo, allora possiamo introdurlo sfruttando l'@obs-whitney-trick ovvero il trucco di Whitney. Possiamo creare due riccioli utilizzando solo mosse II e III in modo tale che uno dei due incroci sia quello introdotto dal ricciolo della sequenza originale mentre l'altro sarà in più ma possiamo ignorarlo come nel caso precedente.
+  - Se abbiamo una mossa di tipo I che aggiunge un ricciolo, allora possiamo introdurlo sfruttando l'@obs-whitney-trick ovvero il trucco di Whitney. Possiamo creare due riccioli utilizzando solo mosse II e III in modo tale che uno dei due sia orientato allo stesso modo di quello introdotto dal ricciolo della sequenza originale, l'altro sarà in più ma possiamo ignorarlo come nel caso precedente.
 
     #figure(image("assets/modified-curl-add-before.png", width: 6.5cm))
     #figure(image("assets/modified-curl-add-after.png", width: 13cm))
@@ -1103,7 +1103,13 @@ La dimostrazione procede sempre mostrando l'indipendenza dalla scelta di punto b
 ]
 
 #proof[
-  #todo[work in progress]
+  Per la definizione di nodo banale standard, la prima occorrenza di $i$ è un sopra-incrocio e osserviamo che la parte di diagramma percorsa tra le due occorrenze di $i$ sarà sicuramente sopra il resto del diagramma (la parte dopo la seconda occorrenza di $i$).
+
+  #figure(image("assets/splice-circuits.png", width: 4cm))
+
+  Dunque abbiamo due casi, in una abbiamo due componenti una sopra l'altra, ognuna delle quali sarà ancora in forma discendente in quanto eredita la proprietà che la prima volta che si passa su un incrocio questo è un sopra-incrocio.
+
+  Se assumiamo che il link del caso precedente sia della forma $E_i K = K_1 union K_2$ con $K_1$, $K_2$ i due nodi banali standard allora l'altro caso sarà $e_i K = K_1 hash K_2$. Usiamo ora il @std-unknot-to-curls per cui un nodo banale standard è equivalente a meno di isotopia regolare al diagramma di un nodo formato solo da riccioli. Dunque se $K_1$ e $K_2$ sono equivalenti a diagrammi formati solo da riccioli lo sarà anche $K_1 hash K_2$ sfruttando il fatto che uno dei due diagrammi sovrasta l'altro e possiamo spostarlo utilizzando solo mosse di tipo II o III#margin-note[Prima dire che possiamo ricondurci alla situazione $K_1 union.sq K_2$ e poi incollare].
 ]
 
 #lemma[