bibkey: gupta2025biorderability
authors: Vaishnavi Gupta; Hitesh Raundal
year: 2025
title: Biorderability of knot quandles of knots up to eight crossings
doi: 10.48550/arXiv.2505.19573
url: https://arxiv.org/abs/2505.19573v1
claim: "The generator order D2 for Q(8_20) could be extendable to a biorder."
strata_touched:
  - D5/S0/Certificates/Quandles/PresentedQuandle
  - D5/S0/Certificates/Quandles/SixRelationObstruction
  - D5/S0/Certificates/Quandles/EightTwentyNonBiorderable
license: citation-only
triage: anchor

The full presented quandle of the oriented 8_20 diagram

Gupta and Raundal, arXiv:2505.19573v1, section “Eight Crossing Knots”, subsection “Knot 8_20”, Figure fig8_20, equations 8_20_1 through 8_20_8, and Table tbl8_20, row D2. The original source says:

The quandle Q(8_20) is generated by labelings of arcs of the diagram, and the relations are given by

In the source’s right-quandle operation the eight equations are b*e=a, c*g=b, d*g=e, g*e=h, f*d=g, d*a=c, a*c=h, f*c=e. The paragraph immediately following the figure supplies the coloring (a,b,c,d,e,f,g,h)=(7,6,5,0,2,8,1,3) in Core(Z/9Z). After Table tbl8_20 the authors state:

Linear order on the generating set of Q(8_20) as in D2 in Table tbl8_20 could be extendable to a biorder on Q(8_20).

This is an author-stated possibility, not a numbered conjecture. The implemented claim is the necessary existence assertion: one LinearOrder on the entire quandle for which both translations are strictly increasing. Its negation rules out every generator order and hence D2; the proof does not assume the table is exhaustive. It does not address the paper’s separate figure-eight possibility.

Verified locator

DOI: 10.48550/arXiv.2505.19573. URL: https://arxiv.org/abs/2505.19573v1. Scope: Eight Crossing Knots / Knot8_20, Figure fig8_20, equations 8_20_1–8_20_8, Table tbl8_20 row D2 and the following possibility paragraph. D2 is an unnumbered author possibility.

Formal source map and conventions

PresentedQuandle is the quotient of unrestricted finite expressions in eight generators, action and inverse action by exactly equivalence, congruence, the quandle axioms and all eight equations. Its Quandle instance and universal evaluation/uniqueness proofs implement an algebraic presentation. The quotient includes inverse-action terms; no positive-word shelf, finite quotient or full conjugation group replaces the carrier. No separation or coloring map is an assumption of the closed claim or result.

Mathlib’s Shelf.act y x means the paper’s x*y. Its dihedral instance directly has Shelf.act v u=2*v-u. Mathlib’s group conjugation instance has the opposite conjugation convention, Shelf.act y x=y*x*y^(-1), so using that instance directly would not represent the paper’s group example y^(-1)*x*y. This implementation uses no group-conjugation model.

The identification of this oriented diagram presentation with the fundamental knot quandle Q(8_20) is the explicit external mathematical input from the primary source. There is no kernel theorem of ambient isotopy, diagram classification or topological knot recognition. Source fidelity and its applicability to the actual author possibility require independent review.

Mathematical mechanism and limits

In an arbitrary linearly ordered idempotent magma strictly increasing in each variable, relations 3–8 force d=g. For d<g, monotonicity and its reflection give d<e<g, c<d, a<d, a<c, h<c, and e<h, a strict cycle. The opposite branch follows in the dual order. The exact finite coloring satisfies ALL eight relations and extends to the whole carrier by the presentation universal property. It separates d (color 0) and g (color 1). It is used only for separation, with no injectivity or order on the target assumed. The closed contradiction concerns all elements of the presented quandle, without a finiteness assumption.

The coloring and presentation are already in the primary paper; neither is new. The general term-algebra construction is standard universal algebra, newly implemented here only because no supplier was found in the searched pinned library. The order argument is an attributed implementation of the predecessor ordinary proof, not an independent rediscovery.

Bounded source inquiry (2026-11-02) found only v1 under the exact arXiv id and four arXiv records under a quandle/biorderability query: 2505.19573v1, 2307.08605v1, 2106.00290v4 and 2010.07159v3. The earlier between-input inequalities of 2010.07159v3 Proposition 3.9, right-orderability results and criteria for ordered Alexander quandles are prior work, not results claimed here. These searches do not establish global current openness, publication absence, priority or novelty. An independent source/literature review is pending and was not read by the implementation agent. Implementation is repo-prior-exposed. No original-resolution, unique, official-acceptance or KPI credit follows from compiling this candidate.

The supplied primary text has SHA256 169ddc39dceb0b64eb7e68ef5c054ba7b82adcc03d1f09c4d83c63974b562328. Its relevant locators are equations at supplied-text lines 1409–1416, the separator paragraph at 1426 and the possibility statement at 1446.

A bounded third-party supplier check found thea-vik/power-quandle-lean at commit 452437602c4be2e6c5ad5f5224b068baabfdf9e1. Its leanpkg.toml pins Lean 3.23.0 and Mathlib 834d491dd7c0aa0ed423bf1253d6d56182f6aa6e; src/free_pq.lean constructs free power quandles, with a unit and integer powers governed by extra axioms in src/power_quandle.lean. It is not a Lean 4.35 Mathlib Quandle supplier and replacing the present algebraic theory by that stronger theory would change the presentation. Its existence is prior formal work on related term quotients, not an absence or novelty claim. The public repository search returned one Lean/quandle repository; the attempted Reservoir API search endpoint returned HTTP 404, so that endpoint supplied no search evidence. No third-party source was imported or copied.