QD-2: R3 (Reidemeister-3) invariance — blocked on KnotTheory.jl upstream

[hyperpolymath]

Source: PROOF-NARRATIVE.md §3 QD-2; PROOF-NEEDS.md M2 (existing) extended to QD-2.

Claim

If diagrams D₁ and D₂ differ by a single Reidemeister-3 move, their quandle_descriptor outputs are equal.

Why valuable

PROOF-NEEDS.md M2 covers R1 and R2; R3 is the standing gap. Without R3 we do not have full Reidemeister equivalence — the invariant is incomplete.

Assumptions

• [[A-QD-2.1]] R1+R2+R3 generate isotopy on classical knot diagrams (Reidemeister 1927; standard).
• [[A-QD-2.2]] R3 acts on the fundamental quandle as a permutation of generators (standard quandle-theoretic result).

Blocker

KnotTheory.jl does not currently expose an r3_simplify function. Verified in audit:

$ grep -rn 'r3' /home/hyperpolymath/developer/repos/julia-libraries/KnotTheory.jl/src/

(only r1_simplify and r2_simplify are exposed.)

Acceptance criteria

Two paths to discharge:

Path A — upstream r3_simplify to KnotTheory.jl (preferred long-term)

• Implement r3_simplify(pd::PlanarDiagram) -> PlanarDiagram in KnotTheory.jl.
• Detect R3 trio: three crossings forming a triangle where the over-strand a passes over both b and c.
• Apply the R3 rewrite: swap the over-strand to pass on the other side of the crossing of b and c.
• PR upstream.
• In quandledb, add test_quandle_axioms.jl §10:

  @testset "Reidemeister III: triangle move preserves descriptor" begin
      # Construct a PD with an R3-eligible triangle (small braid-word example)
      pd_before, pd_after = r3_pair_corpus()
      for (before, after) in zip(pd_before, pd_after)
          d_before = quandle_descriptor(before)
          d_after  = quandle_descriptor(r3_simplify(before))
          @test d_before.colouring_count_3 == d_after.colouring_count_3
          @test d_before.colouring_count_5 == d_after.colouring_count_5
          @test d_before.quandle_key == d_after.quandle_key
      end
  end

Path B — hand-construct R3-equivalent PD pairs (interim)

• Hand-construct a small corpus of R3-equivalent PD pairs (trefoil + R3 vs trefoil; figure-eight + R3 vs figure-eight) directly from PD codes.
• Add the @testset above with the explicit corpus.
• File this as the existing test of R3 invariance — clearly noted as "by hand, not r3_simplify-driven."

Path B can land immediately while Path A goes upstream.

Effort

• Path A: ~5d in KnotTheory.jl (R3 detection + rewrite) + ~1d in quandledb (test).
• Path B: ~2d (hand-construction of corpus + test).

Cross-references

• PROOF-NARRATIVE.md §3 QD-2
• PROOF-NEEDS.md M2 (parent obligation)
• ASSUMPTIONS.md A-QD-2.1, A-QD-2.2