Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)verified 2026-10-22 (gpt-6.1-sol)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Trefoil and figure-eight Jones spans

Example

Assume full AC. The positive trefoil is represented by the closure of the three-crossing two-strand braid σ13; its library Jones polynomial is t+t3−t4, of span 4−1=3, and the corresponding connected reduced alternating diagram has crossing number 3. The figure-eight knot is represented by the closure of the four-crossing three-strand braid whose levels from bottom to top are σ2−1,σ1,σ2−1,σ1; its library Jones polynomial is t−2−t−1+1−t+t2, of span 2−(−2)=4, and the corresponding connected reduced alternating diagram has crossing number 4. The convention is t=A−4.

trefoilTaitgraphb1b2¯gure-eightTaitgraphuvw

These are black Tait graphs; the white graphs are their plane duals. Each graph edge represents one crossing of the corresponding projected diagram.

Facts & Assumptions

Given: Full AC, the two braid closures specified in the example, and the source-chart bracket convention.

[F1]

A positive braid crossing expands as AI+A−1ei and a negative one as A−1I+Aei, where I is through and ei is cup-cap (Bracket smoothings of positive and negative braid crossings).

[F2]

For each state S, the bracket contribution is Aa(S)−b(S)δ∣S∣−1, with δ=−A2−A−2 (Kauffman bracket smoothing and loop value).

[F3]

The positive Artin generator has writhe sign +1, and the negative generator has sign −1 (Oriented crossing signs, diagram writhe, and blackboard framing, The elementary geometric half twist, its support disc, and its opposite).

[F4]

Components of a geometric braid closure correspond to cycles of its endpoint permutation (The closure of a geometric braid).

[F5]

A connected reduced alternating knot diagram with c crossings has Jones span c and realizes crossing number c (Jones span detects crossing number for reduced alternating knots).

[F6]

A diagram is reduced when no region repeats a crossing on its boundary; connected alternating diagrams admit checkerboard colorings and have connected Tait graphs (Reduced alternating link diagram, Checkerboard coloring and Tait graphs, The Tait graphs of a connected projection are connected).

[F7]

Under full AC, VK(t)=fK(t−1/4) with t=A−4 and fD(A)=(−A3)−wr⁡(D)⟨D⟩ (The bracket state sum matches the library Jones specialization).

[A1]

Full AC is the choice-function principle for arbitrary families of nonempty sets (The Axiom of Choice).

Proof

1.1F3F4F6construct

For the closure of σ13, the endpoint permutation is the transposition of the two strands, hence one cycle by [F4]. The three positive crossings form a connected projection. Starting on the left bottom strand, the successive crossing visits are under, over, under; after closure the right bottom strand visits over, under, over. Thus the diagram is alternating. Its black Tait graph has two vertices and three parallel edges, while the white dual graph is a triangle. Both graphs have no loops, so no crossing repeats a region on its boundary; the diagram is reduced by [F6].

1.2F3F4F6construct

For the four-level braid with levels σ2−1,σ1,σ2−1,σ1, the successive endpoint orders are [1,3,2], [3,1,2], [3,2,1], and [2,3,1]. The resulting endpoint permutation is the cycle 1↦3↦2↦1, so the closure is one knot component by [F4]. Traversing it from the first bottom strand gives crossing visits under, over; from the third bottom strand gives under, over, under; and from the second gives over, under, over. The full cyclic sequence alternates. The black Tait graph is the theta graph with two parallel edges between u,v and a two-edge path u−w−v; it has no loops or bridges. Its dual has no loops because the primal has no bridges. Thus both color pairs at every crossing are distinct and the diagram is reduced by [F6].

2.1A1F1F2F3F5F7step 1.1algebra

If exactly k of the three positive crossings use the B-smoothing, the states and circle counts are: k=0: 1 state with 2 circles; k=1: 3 states with 1 circle; k=2: 3 states with 2 circles; k=3: 1 state with 3 circles. Stacking through pairings and cup-cap pairings and closing the two top endpoints to the corresponding bottom endpoints gives these counts. By [F1]–[F2], the grouped contributions are A3δ+3A+3A−1δ+A−3δ2=A−7−A−3−A5. The writhe is 3 by [F3], so [F7] gives V31(t)=(−A3)−3(A−7−A−3−A5)∣t=A−4=t+t3−t4. Its span is 3, and [F5] gives crossing number 3.

3.1A1F1F2F3F5F7step 1.2algebra∎

Encode a state by four bits from bottom to top, with 0 meaning through pairing and 1 meaning cup-cap pairing. Let p be the number of cup-cap choices at positive crossings and q the number at negative crossings; [F1] gives weight exponent 2(q−p). Closing the pairings gives the exhaustive state data statecirclesexponent00003000012−200102200111001002−201013−401101001112−210002210011010103410112211001011012−2111022111110. Thus the five one-circle states contribute 5, the eight two-circle states contribute 4(A2+A−2)δ, and the three three-circle states contribute (1+A4+A−4)δ2. Expanding δ=−A2−A−2 gives ⟨DF⟩=5+4(A2+A−2)δ+(1+A4+A−4)δ2=A8−A4+1−A−4+A−8. There are two positive and two negative crossings, so writhe is 0 by [F3]. By [F7], V41(t)=t−2−t−1+1−t+t2, whose span is 4. Applying [F5] gives crossing number 4.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

41 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources