Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-10
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.

Boone positive history reconstruction

Statement

Assume AC. If Σ=X#qjY is special and LΣR=q in G2 for auxiliary words L,R on x,ri, then Σ=XqjY=q in the positive semigroup Γ.

Facts & Assumptions

Given: The auxiliary equation in the embedded group G2. All equalities of spelled tape words below are explicitly distinguished from group equalities.

[F1]

Freely reduced auxiliary comparisons have a common rule-letter length; at positive length their identity spelling has a central rule pinch. (Boone reduced auxiliary words have no rule pinches)

[F2]

The associated subgroups have free bases ai=Fi#qa(i)Gi,sx and bi=Hi#qb(i)Ki,sx1. The tape retraction, infinite order of x, involution θ fixing tape letters and inverting x, and finite multiple-letter Britton hold. (Boone base groups and associated free bases)

[F3]

In the embedded rule group G2, the exact HNN convention is ri1ari=ϕi(a) for aAi. Together with [F2], conjugation by ri1 carries the displayed basis of Ai to that of Bi, and conjugation by ri carries Bi back to Ai. (Boone hnn tower and auxiliary subgroups)

[F4]

A free product has unique reduced syllable expressions. (Normal form theorem for free products)

[F5]

A reduced HNN word with stable letters cannot represent identity. (Britton's lemma)

[F6]

The indexed semigroup rules are Fiqa(i)Gi=Hiqb(i)Ki, with Fi,Gi,Hi,KiSˉ positive and possibly empty. Equality in Γ is generated by finite symmetric contextual replacements, so either orientation of each rule is permitted in positive contexts. (Boone machine semigroup and augmented configurations)

[F7]

Sharp changes each tape-letter sign without reversing order, preserves concatenation and free reduction, and is involutive. For a special spelling Σ=X#qjY, the associated positive word is Σ=XqjY. (Boone group presentation and special word)

[A1]

Assume AC, used for the HNN normal forms. (The Axiom of Choice)

Proof

1.1

We prove a stronger assertion: for freely reduced, possibly signed tape words X,Y, the equation LX#qjYR=q forces X,Y to be positive and XqjY=q in Γ. Freely reduce L,R, which does not change their elements. By [F1] their rule-letter counts have a common value p. We use strong induction on p, under the AC normal-form assumptions.

F1A1givenF7
1.2

If p=0, the equation is xmX#qjYxn=q in G0=HF(Qˉ), since the base embeds. Unique reduced syllables give qj=q, xmX#=1 and Yxn=1. Applying ρ shows the freely reduced tape words X#,Y are empty. Infinite order of x then gives m=n=0. Thus X,Y are empty positive words and XqjY=q literally, proving the initial case.

F1F2F4
1.3

We first establish the tape sign test used at a pinch. Suppose Z is a freely reduced signed tape word and ZxaT1=sx. Choose its reduced basis spelling u in sx. Then xau1Z=1 in H. Expand u1 in tape stable letters and x. This expansion has no tape pinch: opposite successive tape signs of the same label would come from consecutive inverse basis letters, forbidden by basis reduction; opposite signs of different labels are not a pinch. Any cancellations of neighboring x,x1 do not change this observation. The same is true of Z, since it is freely reduced. If Z began with s1, the only possible first pinch in xau1Z would be across that seam. The last basis letter of u1 would have to be sx, giving exactly sxs1. For the tape relation s1xs=x2, such a pinch requires xx2, impossible because x has infinite order and 1 is not an even integer. If u is empty there is no seam pinch at all. Multiple-letter Britton therefore rules out a negative first letter of Z. Thus Z is empty or begins positively.

F2F5
1.4

Suppose p>0 and assume the stronger assertion for all smaller counts. By [F1], write L=L3riϵxm,R=xnriϵL4, where xmX#qjYxn lies in Ai if ϵ=1, or in Bi if ϵ=1. Each of L3,L4 has p1 rule letters. To treat both orientations uniformly, put (P,qc,Q,P,qd,Q,η)={(Fi,qa(i),Gi,Hi,qb(i),Ki,1),ϵ=1,(Hi,qb(i),Ki,Fi,qa(i),Gi,1),ϵ=1. Then the edge subgroup is E=P#qcQ,Tη and conjugation by riϵ carries P#qcQ to (P)#qdQ and sends sxη to sxη.

F1F2F3givenF6
2.1

If instead ZxaT1, apply θ. It fixes every signed tape word and sends Zxa to ZxaT1, so the same sign test holds. A mirrored test also holds: if xaZTη, invert to obtain Z1xaTη. The first-letter test for Z1 says that Z is empty or ends negatively. These conclusions cover both η=1,1 and a=0 without exception.

F2step 1.3
2.2

Membership of xmX#qjYxn in E gives a word in Tη and a=P#qcQ. Choose one with the fewest occurrences of a±1 and reduce every intervening Tη basis word. There cannot be zero occurrences, since a tape element has no state syllable. In the product of this expression with the inverse of xmX#qjYxn, free-product reduction must cancel state letters. A state cancellation entirely among two consecutive a occurrences with opposite signs has intervening coefficient either Qu(Q)1 or (P#)1uP#, where uTη. Its being identity forces u=1, so the two inverse occurrences could be removed, contradicting minimality. Therefore the single state letter of the coefficient must cancel with one of these occurrences, and after that no further state occurrences can remain: any further reduction would again remove an inverse pair already excluded by minimality. Exactly one positive a occurs, qj=qc, and comparison of its left and right coefficients yields xmX#=uP#,Yxn=Qv(u,vTη). The state sign is positive because the original coefficient contains qj, not qj1, in the free state factor.

F2F4step 1.4
3.1

Reduce (Q)1Y freely to Z. From step 2.2, Zxn=vTη. If any letter of (Q)1 survived the seam cancellation, Z would start negatively, since Q is positive. This contradicts steps 1.3 and 2.1. Thus Y=QY1 as an exact spelling, and Y1 is empty or starts positively. Likewise reduce X#(P#)1 to Z. Then xmZ=uTη. If any letter from (P#)1 survived, Z would end positively; the mirrored test in step 2.1 excludes this. Hence X=X1P as a spelling, and X1# is empty or ends negatively. Both X1,Y1 are subwords of the original reduced words and so are reduced. These conclusions include completely empty remainders and empty P,Q.

step 1.3step 2.1step 2.2F6F7
4.1

Substituting the spellings from step 3.1 into the coefficient equations and cancelling the terminal/initial tape factors gives u=xmX1#,v=Y1xn. By [F2]–[F3], the applicable edge isomorphism restricts to θ on Tη, because it sends each of its basis elements sxη to sxη. Thus its values on these particular elements are θ(u)=xmX1# and θ(v)=Y1xn. Replacing the central pinch in the original equation gives (L3xm)X1#(P)#qdQY1(xnL4)=q. This computation is valid for both signs of ϵ; for ϵ=1 it uses the inverse edge map, which still restricts to the same involution θ.

F2F3step 1.4step 2.2step 3.1algebraF7
5.1

The word X1#(P)# is freely reduced: each factor is reduced, the second is negative, and a nonempty first factor ends negatively by step 3.1. No opposite pair can occur at the seam. Similarly QY1 is reduced, since Q is positive and a nonempty Y1 starts positively. Empty factors introduce no seam. Sharp preserves free reduction, so X1P is also freely reduced. Freely reduce the two auxiliary factors in step 4.1; their rule counts can only decrease and are at most p1. By [F1] their new counts agree. The induction hypothesis therefore applies and makes X1P and QY1 positive, with X1PqdQY1=qin Γ. Because the two concatenations were freely reduced spellings, their subwords X1,Y1 are themselves positive. Consequently X=X1P and Y=QY1 are positive.

F1step 3.1step 4.1step 1.1F6F7
6.1

If ϵ=1, the original positive word is X1Fiqa(i)GiY1, which rewrites by rule i to X1Hiqb(i)KiY1=q. If ϵ=1, it is X1Hiqb(i)KiY1, which rewrites by the reverse of the same semigroup equation to X1Fiqa(i)GiY1=q. Both uses have positive contexts by step 5.1. This completes the induction for signed words. For the special words of the statement, positivity was already given, so the resulting equality is exactly Σ=q.

step 1.4step 5.1step 1.1F6F7

Source locator

Rotman, Chapter 12, printed pp.443–447, Lemma 12.15. The tape sign tests, both rule orientations, and empty remainders are proved explicitly above; the source leaves the reverse orientation to the reader.

Depends on

Used by

Dependency tree · two levels

23 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