Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08
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.

Meets and joins are not intersection and union of inversion sets: the A2 counterexample

Statement refuted

Statement refuted. For every finite Coxeter system (W,S), every u,v∈W for which u∧v and u∨v exist satisfy

N((u∧v)−1)=N(u−1)∩N(v−1),N((u∨v)−1)=N(u−1)∪N(v−1)

(with N the inversion sets of The geometric inversion set N(w) of an element of a Coxeter group), i.e. meets and joins are computed by intersection and union of inversion sets.

Counterexample (type A2, W=S3). Let S={s,t}, m(s,t)=3, and let αs,αt,αs+αt be the positive roots of A2, so that N(w−1)∈{∅,{αs},{αt},{αs,αs+αt},{αt,αs+αt},Φ+} for w∈W={1,s,t,st,ts,w0} as in All meets and joins of the right weak order of A2 (S3), with the left order and the inversion sets compared. Then:

(i) s∨t=w0 and N(w0−1)=Φ+={αs,αt,αs+αt}, while N(s−1)∪N(t−1)={αs}∪{αt}={αs,αt}⊊Φ+; the union is not even the inversion set of an element of W, and in particular the join is strictly larger than the union.

(ii) st∧ts=1 and N(1)=∅, while N((st)−1)∩N((ts)−1)={αs,αs+αt}∩{αt,αs+αt}={αs+αt}≠∅; the intersection is not the inversion set of an element of W, and in particular the meet is strictly smaller than the intersection.

Correct statement. By Weak order is a partial order with finite graded intervals; covers and the inversion-set criterion (4), w≤Ru,v if and only if N(w−1)⊆N(u−1)∩N(v−1); hence u∧v is the greatest element whose inversion set is contained in the intersection, and dually u∨v is the least element whose inversion set contains the union. Containment, and not equality, is the correct order-theoretic relation.

Facts & Assumptions

Given: The Coxeter matrix of type A2: S={s,t}, m(s,t)=3; the presented group W with length ℓ, the weak orders ≤R,≤L as in The right and left weak orders, intervals, covers, and meets and joins of subsets; the reflection representation ρ on V=RS with simple roots αs=es, αt=et and root system Φ=Φ+⊔Φ−; and w0=sts=tst.

[F1]

The geometric inversion set N(w) of an element of a Coxeter group (1): N(w)={α∈Φ+:ρ(w)α∈Φ−}.

[F2]

All meets and joins of the right weak order of A2 (S3), with the left order and the inversion sets compared: W={1,s,t,st,ts,w0} with ℓ(1)=0, ℓ(s)=ℓ(t)=1, ℓ(st)=ℓ(ts)=2, ℓ(w0)=3; and w0=sts=tst.

[F3]

All meets and joins of the right weak order of A2 (S3), with the left order and the inversion sets compared: the six inversion sets N(w−1) for w=1,s,t,st,ts,w0 are ∅, {αs}, {αt}, {αs,αs+αt}, {αt,αs+αt} and Φ+={αs,αt,αs+αt}.

[F4]

All meets and joins of the right weak order of A2 (S3), with the left order and the inversion sets compared: s∨t=w0 and st∧ts=1, with their universal bound properties recorded there.

[F5]

Weak order is a partial order with finite graded intervals; covers and the inversion-set criterion (4): for all u,v, u≤Rv  ⟺  N(u−1)⊆N(v−1).

[F7]

The right and left weak orders, intervals, covers, and meets and joins of subsets (3): a right meet is a greatest lower bound in ≤R.

[F8]

The right and left weak orders, intervals, covers, and meets and joins of subsets (3): a right join is a least upper bound in ≤R.

Counterexample

1.1F1F2F3givenalgebra

The A2 data: W={1,s,t,st,ts,w0} with the lengths of Fact [F2], and the six inversion sets N(w−1) of Fact [F3]; in particular, no other subset of Φ+ displayed below occurs as an inversion set N(w−1).

2.1F1F4F8step 1.1givenalgebra

Failure of the join equality: s∨t=w0 by [F4] and N(w0−1)=Φ+={αs,αt,αs+αt} by step 1.1, while N(s−1)∪N(t−1)={αs}∪{αt}={αs,αt}. The union {αs,αt} is not among the six sets of step 1.1, so it is not the inversion set N(w−1) of any element w∈W; in particular N((s∨t)−1)=Φ+≠{αs,αt}=N(s−1)∪N(t−1), refuting the join half of the displayed statement.

2.2F1F4F7step 1.1givenalgebra

Failure of the meet equality: st∧ts=1 by [F4] and N(1)=∅ by step 1.1, while N((st)−1)∩N((ts)−1)={αs,αs+αt}∩{αt,αs+αt}={αs+αt} is nonempty; this intersection is not among the six sets of step 1.1 either, so it is not the inversion set N(w−1) of any element, and N((st∧ts)−1)=∅≠{αs+αt}=N((st)−1)∩N((ts)−1), refuting the meet half of the displayed statement.

3.1F5F6F7F8step 2.1step 2.2givenalgebra∎

The corrected containment statement: by the criterion [F5], for every w∈W, w≤Ru and w≤Rv if and only if N(w−1)⊆N(u−1) and N(w−1)⊆N(v−1), equivalently N(w−1)⊆N(u−1)∩N(v−1). Since W is finite, [F6] guarantees that u∧v and u∨v exist; by [F7], the meet is the greatest such lower bound. Dually, [F5] gives w≥Ru,v if and only if N(w−1)⊇N(u−1)∪N(v−1), and [F8] makes the join the least such upper bound. Thus the meet inversion set is the greatest inversion set contained in the intersection, and the join inversion set is the least inversion set containing the union; steps 2.1 and 2.2 show both containments can be strict. No Choice is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

30 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