|
| 1 | +<!-- |
| 2 | +SPDX-License-Identifier: CC-BY-SA-4.0 |
| 3 | +SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 4 | +--> |
| 5 | + |
| 6 | +[](https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/frayed-knot-toolkit) |
| 7 | +[](https://github.com/hyperpolymath/palimpsest-license) <embed |
| 8 | +src="https://api.thegreenwebfoundation.org/greencheckimage/github.com" |
| 9 | +data-link="https://www.thegreenwebfoundation.org/green-web-check/?url=github.com" /> |
| 10 | + |
| 11 | +This directory contains the formalization of **Frayed Knot** theory |
| 12 | +using the dependently typed programming language and proof assistant |
| 13 | +**Agda**. It provides foundational definitions, topological states, and |
| 14 | +structural facts regarding knot crossings, resolutions, and strand |
| 15 | +choreographies. |
| 16 | + |
| 17 | +This project provides a comprehensive toolkit for formalizing Frayed |
| 18 | +Knot Theory. |
| 19 | + |
| 20 | +<div id="toc"> |
| 21 | + |
| 22 | +</div> |
| 23 | + |
| 24 | +# Overview |
| 25 | + |
| 26 | +The project explores the mathematics and topology of "frayed" knots. It |
| 27 | +models knots mathematically by defining strands, orientations, crossing |
| 28 | +signs (Positive, Negative), and resolutions (A-Smooth, B-Smooth). The |
| 29 | +toolkit is designed to formally verify and prove structural properties |
| 30 | +about knot crossings and the choreographic interactions of their |
| 31 | +strands. |
| 32 | + |
| 33 | +# Project Structure |
| 34 | + |
| 35 | +The project primarily consists of Agda (`.agda`) files that construct |
| 36 | +the formal proofs and definitions, alongside an empty Julia (`.jl`) file |
| 37 | +intended for future numerical or programmatic implementation. |
| 38 | + |
| 39 | +## Core Modules |
| 40 | + |
| 41 | +- `FrayedKnot.agda` Defines the basic topological objects including: |
| 42 | + |
| 43 | + - `Resolution` (`A-Smooth`, `B-Smooth`) |
| 44 | + |
| 45 | + - `CrossingSign` (`Positive`, `Negative`) |
| 46 | + |
| 47 | + - `BranchKind` (`Split`, `Preserve`) |
| 48 | + |
| 49 | + - `TopologicalState` (Tracking component counts and resolution |
| 50 | + history) |
| 51 | + |
| 52 | + - Logic for resolving crossings and fraying nodes, including |
| 53 | + structural lemmas and successor-state proofs. |
| 54 | + |
| 55 | +<!-- --> |
| 56 | + |
| 57 | +- `ChoreographicFrayedKnot.agda` Focuses on the choreographic aspects of |
| 58 | + strands. It defines `Strand` types, `Orientation` (`Over`, `Under`), |
| 59 | + `Distinct` proofs for strands, and projects knot paths, capturing |
| 60 | + navigation over and under crossings. |
| 61 | + |
| 62 | +<!-- --> |
| 63 | + |
| 64 | +- `FrayedKnotDiagram.agda` & `FrayedKnotLabeled.agda` (Core internal |
| 65 | + modules) Define the structures for constructing diagrams from |
| 66 | + crossings and applying labels to track crossing signs and topological |
| 67 | + states across a full diagram. |
| 68 | + |
| 69 | +<!-- --> |
| 70 | + |
| 71 | +- `FrayedKnotExamples.agda` Contains practical examples and theorems. |
| 72 | + For instance, it provides diagrams (`allPositive₂`, `mixed₂`), |
| 73 | + constructs explicit toy signatures/profiles, and formally proves |
| 74 | + distinction theorems (e.g., `profiles-differ`) which show that |
| 75 | + different crossing configurations yield mathematically distinct |
| 76 | + profiles. |
| 77 | + |
| 78 | +<!-- --> |
| 79 | + |
| 80 | +- `FrayedKnotUniformity.agda` Explores uniformity properties and lemmas |
| 81 | + across the knot formalization. |
| 82 | + |
| 83 | +<!-- --> |
| 84 | + |
| 85 | +- `frayed_knot.jl` A placeholder Julia script indicating planned support |
| 86 | + for numerical analysis, simulation, or algorithm execution related to |
| 87 | + frayed knots. |
| 88 | + |
| 89 | +# Getting Started |
| 90 | + |
| 91 | +To verify the proofs in this project, you need to have **Agda** |
| 92 | +installed along with the **Agda Standard Library**. |
| 93 | + |
| 94 | +1. **Install Agda:** Follow the instructions on the [Agda |
| 95 | + Wiki](https://wiki.portal.chalmers.se/agda/pmwiki.php) or your |
| 96 | + package manager. |
| 97 | + |
| 98 | +2. **Type-check the project:** You can load the root files in your |
| 99 | + editor (e.g., using Emacs with `agda-mode`) to verify all proofs, or |
| 100 | + run: `` `bash `` `agda` `FrayedKnotExamples.agda`\` |
| 101 | + |
| 102 | +# Theory and Architecture |
| 103 | + |
| 104 | +The theoretical foundation builds on basic knot theory concepts (like |
| 105 | +the Kauffman bracket’s A/B smoothings) and extends them to "frayed" |
| 106 | +interpretations. It tracks how local resolutions affect the global |
| 107 | +topological state (e.g., the number of components) and uses dependent |
| 108 | +types to statically guarantee structural facts—such as the binary nature |
| 109 | +of fraying and the impossibility of profile equalities between distinct |
| 110 | +knot configurations. |
| 111 | + |
| 112 | +# Status |
| 113 | + |
| 114 | +The Agda formalization is currently in active development with several |
| 115 | +foundational lemmas and main distinction theorems already proven. The |
| 116 | +Julia script represents planned numerical support, reflecting the |
| 117 | +hyperpolymath architectural preference for cross-language workflows (in |
| 118 | +this case, Agda for proofs and Julia for high-performance scientific |
| 119 | +computing). |
0 commit comments