Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 18 additions & 4 deletions .github/workflows/krl-verification.yml
Original file line number Diff line number Diff line change
Expand Up @@ -68,9 +68,12 @@ jobs:
julia --color=yes server/krl/test/seam_test.jl

# server/Project.toml [sources] resolves KnotTheory/Skein/AcceleratorGate
# at server/../../../<name>.jl — i.e. two directories above the repo
# checkout ($GITHUB_WORKSPACE/../../<name>.jl). actions/checkout cannot
# write outside the workspace, so check out under deps/ and symlink.
# at server/../../<name>.jl — i.e. one directory above the repo checkout
# ($GITHUB_WORKSPACE/../<name>.jl). actions/checkout cannot write outside
# the workspace, so check out under deps/ and symlink.
# NOTE: keep this in step with server/Project.toml — #83 moved [sources]
# from ../../../ to ../../ without updating the symlink here, which broke
# every instantiate with "expected package KnotTheory to exist at path".
- name: Checkout KnotTheory.jl
uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v4
with:
Expand All @@ -93,8 +96,19 @@ jobs:
run: |
set -euo pipefail
for p in KnotTheory.jl Skein.jl AcceleratorGate.jl; do
ln -sfn "$GITHUB_WORKSPACE/deps/$p" "$GITHUB_WORKSPACE/../../$p"
ln -sfn "$GITHUB_WORKSPACE/deps/$p" "$GITHUB_WORKSPACE/../$p"
done
# Fail loudly here rather than inside Pkg.instantiate, whose error
# ("expected package ... to exist at path") names the path but not
# the cause.
julia --project=server -e '
using TOML
src = TOML.parsefile("server/Project.toml")["sources"]
for (name, spec) in src
path = normpath(joinpath("server", spec["path"]))
isdir(path) || error("[sources] $name -> $(spec["path"]) resolves to $path, which does not exist; the symlink step above is out of step with server/Project.toml")
end
println("PASS: all [sources] paths resolve")'

- name: Instantiate server project
run: julia --color=yes --project=server -e 'using Pkg; Pkg.instantiate()'
Expand Down
26 changes: 15 additions & 11 deletions server/quandle_semantic.jl
Original file line number Diff line number Diff line change
Expand Up @@ -469,15 +469,19 @@ end
const HOMFLY_MAX_CROSSINGS = 15
const HOMFLY_DEFERRED_SENTINEL = "deferred:too_many_crossings"

# KnotTheory's alexander_polynomial computes its polynomial-matrix minor
# determinant by naive cofactor expansion — O(n!) in the minor size, which
# tracks the crossing count. Measured on (2,n)-torus closures (s1^n, the
# worst case: no arc merging): n=12 → 12s, n=13 → 106s, n=16 → 6h+ (this
# hung CI to GitHub's job kill). conway_polynomial CALLS alexander_polynomial
# internally, so it inherits the same bound. jones_polynomial goes through
# the Kauffman bracket instead, which KnotTheory itself hard-limits at 20
# crossings by THROWING — we convert that throw into the same sentinel.
const ALEXANDER_MAX_CROSSINGS = 12
# alexander_polynomial's determinant is now fraction-free Bareiss
# elimination — O(n^3) polynomial operations (KnotTheory.jl#46/#48).
# Re-measured on (2,n)-torus closures (s1^n, the worst case: no arc
# merging): n=40 → 0.07s, n=100 → 0.10s, n=140 → 0.61s. The previous
# bound of 12 was calibrated against the O(n!) cofactor expansion it
# replaced (n=12 → 12s, n=13 → 106s, n=16 → 6h+ and a CI job killed at
# GitHub's 6-hour limit), so it is now an order of magnitude too tight.
# 128 keeps the worst case sub-second while covering every realistic
# diagram. conway_polynomial calls alexander_polynomial, so it shares
# the bound. jones_polynomial instead goes through the Kauffman bracket,
# which is genuinely 2^n and which KnotTheory hard-limits at 20 crossings
# by THROWING — we convert that throw into the same sentinel.
const ALEXANDER_MAX_CROSSINGS = 128
const CONWAY_MAX_CROSSINGS = ALEXANDER_MAX_CROSSINGS
const JONES_MAX_CROSSINGS = 20

Expand All @@ -498,7 +502,7 @@ end
_safe_alexander_serialised(pd::KnotTheory.PlanarDiagram) -> String

Alexander polynomial, guarded by `ALEXANDER_MAX_CROSSINGS` (the upstream
determinant is O(n!) cofactor expansion). Returns the deferred sentinel
determinant is O(n^3) Bareiss elimination). Returns the deferred sentinel
above the bound.
"""
function _safe_alexander_serialised(pd::KnotTheory.PlanarDiagram)::String
Expand All @@ -510,7 +514,7 @@ end
_safe_conway_serialised(pd::KnotTheory.PlanarDiagram) -> String

Conway polynomial, guarded by `CONWAY_MAX_CROSSINGS` (upstream it is
computed FROM the Alexander polynomial, so it shares the O(n!) cost).
computed FROM the Alexander polynomial, so it shares that cost).
Returns the deferred sentinel above the bound.
"""
function _safe_conway_serialised(pd::KnotTheory.PlanarDiagram)::String
Expand Down
24 changes: 17 additions & 7 deletions server/test_br5_fuzz.jl
Original file line number Diff line number Diff line change
Expand Up @@ -120,13 +120,23 @@ end

@testset "BR-5: crossing-order invariance on random braid words" begin
rng = MersenneTwister(BR5_SEED + 1)
# KNOWN-BROKEN (upstream): the polynomial segments of quandle_key
# (alexander/conway/homfly from KnotTheory.jl) are crossing-order
# sensitive on some diagrams — the polynomials are not normalised to a
# canonical unit (±t^k), so 25/200 seeded trials disagree. The layers
# this repo owns (presentation_hash, colouring counts) are asserted
# hard below; the key mismatch count is tracked and marked broken so
# the marker must be removed once KnotTheory.jl normalises.
# KNOWN-BROKEN (upstream KnotTheory.jl#51): the polynomial segments of
# quandle_key are crossing-order sensitive on multi-component LINKS.
# Measured over this 200-trial corpus, splitting by Delta(1):
# links (Delta(1)=0): 11 mismatch, 87 agree
# knots (Delta(1)=±1): 0 mismatch, 102 agree
# Knots became fully order-invariant when KnotTheory#48 landed the
# Delta(1)=+1 normalisation; that fix cannot apply to links, where
# Delta(1)=0 and the code falls back to an order-sensitive rule. Worse,
# conway_polynomial reconstructs from an assumed symmetry about
# exponent 0, which no link satisfies (even span ⟹ half-integer
# centre), so it returns genuinely DIFFERENT polynomials for the same
# link (e.g. 1 + z² vs 1) — not merely a different unit.
# NOTE: this count did NOT move when #48 merged. The earlier
# attribution of these mismatches to the alexander/conway sign
# convention was wrong; the sign fix was real but orthogonal.
# The layers this repo owns (presentation_hash, colouring counts) are
# asserted hard below and hold on every trial.
quandle_key_mismatches = 0
for trial in 1:BR5_TRIALS
nstrands = rand(rng, 3:4)
Expand Down
59 changes: 33 additions & 26 deletions server/test_quandle_axioms.jl
Original file line number Diff line number Diff line change
Expand Up @@ -512,22 +512,32 @@ end
end

@testset "KT-2 ext: polynomial guards return sentinels above their bounds" begin
# Build a synthetic 16-crossing PD by braid word s1^16 — a genuine
# (2,16)-torus-link diagram (post KnotTheory#43; before that fix the
# broken braid closure made this degenerate and cheap, which is how the
# missing guards went unnoticed). 16 crossings exceeds
# HOMFLY_MAX_CROSSINGS (15) and ALEXANDER/CONWAY_MAX_CROSSINGS (12,
# the O(n!) upstream determinant: 12 → 12s, 13 → 106s, 16 → 6h+ and a
# CI job killed at GitHub's 6-hour limit), but not JONES_MAX_CROSSINGS
# (20, Kauffman bracket: 2.8s measured at 16).
pd_large = from_braid_word(join(["s1" for _ in 1:16], ".")).pd
d_large = quandle_descriptor(pd_large)
@test d_large.homfly_polynomial == HOMFLY_DEFERRED_SENTINEL
@test d_large.alexander_polynomial == HOMFLY_DEFERRED_SENTINEL
@test d_large.conway_polynomial == HOMFLY_DEFERRED_SENTINEL
# Jones stays real at 16 crossings — a sentinel here would mean the
# bound was tightened without re-measuring.
@test d_large.jones_polynomial != HOMFLY_DEFERRED_SENTINEL
# Each polynomial has its OWN bound, set by its own measured cost model,
# so one diagram cannot exercise them all. Both cases below are genuine
# (2,n)-torus-link diagrams (post KnotTheory#43 — before that fix the
# broken braid closure made them degenerate and cheap, which is how the
# missing guards went unnoticed until CI hung for 6 hours).

# 16 crossings: above HOMFLY's 15 (skein recursion is exponential), but
# below Jones' 20 (Kauffman bracket, 2.8s measured here) and far below
# alexander/conway's 128 (Bareiss, O(n^3)).
pd16 = from_braid_word(join(["s1" for _ in 1:16], ".")).pd
d16 = quandle_descriptor(pd16)
@test d16.homfly_polynomial == HOMFLY_DEFERRED_SENTINEL
@test d16.jones_polynomial != HOMFLY_DEFERRED_SENTINEL
@test d16.alexander_polynomial != HOMFLY_DEFERRED_SENTINEL
@test d16.conway_polynomial != HOMFLY_DEFERRED_SENTINEL

# 130 crossings: above every bound — all four defer. This also pins the
# alexander/conway bound itself: if someone raises it without raising
# this fixture, the test fails rather than silently going quiet.
pd_over = from_braid_word(join(["s1" for _ in 1:130], ".")).pd
@test length(pd_over.crossings) > ALEXANDER_MAX_CROSSINGS
d_over = quandle_descriptor(pd_over)
@test d_over.alexander_polynomial == HOMFLY_DEFERRED_SENTINEL
@test d_over.conway_polynomial == HOMFLY_DEFERRED_SENTINEL
@test d_over.jones_polynomial == HOMFLY_DEFERRED_SENTINEL
@test d_over.homfly_polynomial == HOMFLY_DEFERRED_SENTINEL
end

@testset "KT-2 ext: Jones polynomial distinguishes the test knots" begin
Expand Down Expand Up @@ -675,17 +685,14 @@ end
t = quandle_descriptor(trefoil().pd)
@test t.conway_polynomial == "0:1,2:1"

# Figure-eight ∇(z) = 1 - z² → "0:1,2:-1"
# KNOWN-BROKEN (upstream KnotTheory.jl#42): the computed value is
# "0:-1,2:1" = -(1 - z²). Conway is canonically normalised (∇(unknot)=1,
# so there is NO legitimate unit ambiguity) — the sign flip comes from
# the Alexander determinant's row/sign convention on mixed-sign
# diagrams, the same missing unit normalisation tracked in #42. The
# trefoil and cinquefoil (all-positive crossings) are unaffected.
# First caught here: this fixture suite (issue #32) merged behind the
# 6-hour CI hang and had never actually executed before.
# Figure-eight ∇(z) = 1 - z² → "0:1,2:-1". This was @test_broken: the
# computed value was -(1 - z²) because alexander normalised its unit by
# "leading coefficient positive", the wrong canonical choice on
# mixed-sign knots. Fixed upstream (KnotTheory.jl#48) by normalising to
# Δ(1) = +1, the Conway normalisation — the marker then reported
# "unexpected pass", which is exactly the signal it existed to produce.
f = quandle_descriptor(figure_eight().pd)
@test_broken f.conway_polynomial == "0:1,2:-1"
@test f.conway_polynomial == "0:1,2:-1"

# Cinquefoil ∇(z) = 1 + 3z² + z⁴ → "0:1,2:3,4:1"
c = quandle_descriptor(cinquefoil().pd)
Expand Down
Loading