QuandleDB stores and investigates knots using presentations, invariants and semantic indexes. KRL is its resolution language: construct, transform, resolve and retrieve. The implemented Julia parser/evaluator currently covers a retrieval/candidate fragment; the full four-operation design is not yet executable.
-
Skein.jl is an independent Julia library for knot storage, indexing and invariant computation. QuandleDB uses it.
-
KnotTheory.jl is an independent mathematical toolkit for diagrams, braids, invariants and transformations.
-
Tangle is a separate Turing-complete language for knot mathematics. It is not a compilation target for KRL.
-
KRL owns the resolution-language specification; its current implementation lives in
server/krl/here.
Shared knot theory does not imply a shared language architecture or transfer a proof guarantee from one project to another.
KnotTheory.PlanarDiagram → extract_presentation → QuandlePresentation → normalised presentation bytes / hash → finite colouring counts / index candidates
See server/quandle_semantic.jl for the actual functions and
server/test_quandle_axioms.jl for their mathematical regression tests.
The HTTP service integrates these facilities with Skein storage.
A matching fingerprint or selected invariants nominates a candidate. It is not a complete knot-isotopy decision procedure. The normalisation implemented here does not establish a canonical representative for every isotopy class.
The bucket provider returns heuristic candidates. find_equivalent labels them
accordingly and warns that requested invariant lists are not checked by this
provider. Requests for exact, sufficient or necessary assurance fail until the
required evidence checker exists. An absent target is unresolved, not unequal.
A resolution stage preserves the incoming selection, including an empty result.
find_path currently returns structural candidates with a warning; it does not
produce a checked Reidemeister path.
The base-Julia suites run without server package installation:
julia --startup-file=no server/krl/test/lexer_test.jl
julia --startup-file=no server/krl/test/parser_test.jl
julia --startup-file=no server/krl/test/sql_test.jl
julia --startup-file=no server/krl/test/seam_test.jl
julia --startup-file=no server/krl/test/resolution_boundary_test.jlThe KRL Verification workflow runs these before dependency-dependent server tests. The separate KRL repository supplies a cross-repository fragment corpus; see surface contracts.
See the proof narrative for the remaining extraction, normalisation, transformation, colouring-count and ABI obligations. A parser test, a finite mathematical fixture and a general correctness proof establish different things; report each with its actual scope.