### May you live in interesting times

David Snyder, my collaborator on the knots-as-processes work, found a nice counter example to the proof method i used to establish the proof of the main theorem. Perko-pairs are minimal crossing projections with really different wiring diagrams. These pairs are constructed by chains of (mostly) R3 moves. The problem with my proof method was that while the R1 and R2 differences in crossings could be handled with restriction, if you use restriction to handle the R3 moves you essentially end up with completely closed processes after chains of these moves. So, the theorem remains correct, but only because the processes interpreting the knots are completely unobservable -- i.e. have been restricted on all the ports used by all the crossing and wire processes.

i have found a way around the problem. Below i outline the strategy. There are two major components. The first is to recognize that you can label all transitions with crossings or wires. Then you can plug these into R-move-based contexts. Then you build a 1-R move away bisimulation. Then you build R-bisimulation up to R-bisimilarity. Iterating this procedure gets you an equivalence allowing sequences-of-R-move-away bisimulations allowing for nested or overlapping applications of R-moves. The R-move sequences can be used to construct an R-bisimulation up to R-bisimilarity^n and likewise if you are told that two processes in the image of the encoding are R-bisimilar up to R-bisimilarity^ this means, ultimately, that you can demand chains of R-move contexts for every state either process can get into from which you can recover the R-move sequence proof of the ambient isotopy of the knots.

This has implications for the use of spatial logic. The straight up predicates we define can distinguish elements within the same isotopy class -- which for the purposes of ambient isotopy-based searches is too distinguishing. So, one must find a way to coarsen the logic. Intriguingly, the bisimulation construction is cookie cutter in the bisimulation up to techniques. This leads to the most obvious question -- what happens to the HML logics when you pull the bisimulation up to techniqes through the construction of an HML? i believe that no one has considered this question. (i've never seen it in the literature.) So, i believe we can build a knot specific logic by pulling the bisimulation up to construction through the logical construction and exhibit specific examples of queries.

Finally, David has informed me just today that there is a procedure associating to any compact 3-manifold (think some substructure in a cell) a link (more general than a knot but still entirely within our method of encoding). If the procedure is constructive then the end-to-end program to work gives you a storage and retrieval machine for basically all the 3-d structures you might be interested in, and makes quite solid the claim that this is a way to interpret space as behavior.

i have found a way around the problem. Below i outline the strategy. There are two major components. The first is to recognize that you can label all transitions with crossings or wires. Then you can plug these into R-move-based contexts. Then you build a 1-R move away bisimulation. Then you build R-bisimulation up to R-bisimilarity. Iterating this procedure gets you an equivalence allowing sequences-of-R-move-away bisimulations allowing for nested or overlapping applications of R-moves. The R-move sequences can be used to construct an R-bisimulation up to R-bisimilarity^n and likewise if you are told that two processes in the image of the encoding are R-bisimilar up to R-bisimilarity^ this means, ultimately, that you can demand chains of R-move contexts for every state either process can get into from which you can recover the R-move sequence proof of the ambient isotopy of the knots.

This has implications for the use of spatial logic. The straight up predicates we define can distinguish elements within the same isotopy class -- which for the purposes of ambient isotopy-based searches is too distinguishing. So, one must find a way to coarsen the logic. Intriguingly, the bisimulation construction is cookie cutter in the bisimulation up to techniques. This leads to the most obvious question -- what happens to the HML logics when you pull the bisimulation up to techniqes through the construction of an HML? i believe that no one has considered this question. (i've never seen it in the literature.) So, i believe we can build a knot specific logic by pulling the bisimulation up to construction through the logical construction and exhibit specific examples of queries.

Finally, David has informed me just today that there is a procedure associating to any compact 3-manifold (think some substructure in a cell) a link (more general than a knot but still entirely within our method of encoding). If the procedure is constructive then the end-to-end program to work gives you a storage and retrieval machine for basically all the 3-d structures you might be interested in, and makes quite solid the claim that this is a way to interpret space as behavior.