Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27
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.

Generalised associativity: in a monoid the product of a finite list does not depend on the bracketing, and in a commutative monoid it does not depend on the order of the factors either

Statement

Let (M,⋅,e) be a monoid and let g:N→M, with finite products ∏i<ngi as in The product g0g1⋯gn−1 of a finite list in a monoid, by recursion, with the empty product (n=0) equal to the identity.

  1. Splitting law. For all m,n∈N,

    ∏i<m+ngi  =  (∏i<mgi)⋅(∏j<ngm+j).

  2. Regrouping law (bracketing does not matter). Let s:N→N satisfy s0=0 and sj≤sσ(j) for every j, and for each j let cj be the unique natural number with sj+cj=sσ(j). Put Bj:=∏l<cjgsj+l, the product of the j-th block of consecutive factors. Then for every r∈N,

    ∏j<rBj  =  ∏i<srgi.

    In words: cut the list g0,…,gsr−1 into consecutive blocks in any way whatever, multiply out each block, and multiply the results in order; the answer is the product of the whole list.

  3. Commutative case (order does not matter). Suppose in addition that M is commutative. Let n∈N and let π∈Sym⁡(n) be a permutation of the von Neumann natural n={0,…,n−1} (The symmetric group Sym⁡(X): the bijections of a set X under composition). Let h:N→M be any family with hi=gπ(i) for every i<n. Then

    ∏i<nhi  =  ∏i<ngi.

Facts & Assumptions

Given: A monoid (M,⋅,e), a family g:N→M, and the products of The product g0g1⋯gn−1 of a finite list in a monoid, by recursion, with the empty product (n=0) equal to the identity, which satisfy ∏i<0ui=e and ∏i<σ(n)ui=(∏i<nui)⋅un for every family u:N→M, and whose value ∏i<nui depends only on u0,…,un−1.

[L2]

The monoid laws: ⋅ is associative and e is a two-sided identity (Semigroup and monoid).

[L3]

Addition on N: m+0=m and m+σ(n)=σ(m+n), so in particular m+1=σ(m) (Addition of natural numbers); addition is commutative and associative (Addition is commutative, Addition is associative) and cancellative (Addition is cancellative).

[L4]

Order on N: m≤n means m+k=n for some k∈N, and m<n means m≤n with m≠n (Order on the natural numbers); m≤n  ⟺  m+k≤n+k and m<n  ⟺  m+k<n+k (Order is compatible with addition); exactly one of m<n, m=n, n<m holds (Trichotomy of the order on N); m<n  ⟺  σ(m)≤n (Discreteness: σ(n) is the immediate successor); and every n≠0 is a successor (Every nonzero natural number is a successor).

[L5]

On N the order is membership: m<n  ⟺  m∈n, so n={ m:m<n }; and m<σ(n)  ⟺  m≤n; and n∉n (On N the order is membership: m<n  ⟺  m∈n, The natural numbers N (von Neumann)).

[L6]

A permutation of n is a bijection n→n; bijections are injective and surjective, and composites of injections are injective (The symmetric group Sym⁡(X): the bijections of a set X under composition, Injection, surjection, bijection).

Proof

technique · induction
1.1

Splitting law, base n=0: the left side is ∏i<m+0gi=∏i<mgi, and the right side is (∏i<mgi)⋅∏j<0gm+j=(∏i<mgi)⋅e=∏i<mgi; so the two agree, for every m.

basegivenL2L3
1.2

Splitting law, inductive hypothesis: fix n and assume ∏i<m+ngi=(∏i<mgi)⋅(∏j<ngm+j) for every m and every family g.

ih
1.3

Write uj:=gm+j, a family N→M, so that ∏j<ngm+j=∏j<nuj and un=gm+n.

given
1.4

In claim 2 the natural cj exists because sj≤sσ(j), and it is unique by cancellation, so Bj is well defined for every j and B:N→M is a family.

givenL3L4
1.5

Regrouping law, base r=0: the left side is ∏j<0Bj=e and the right side is ∏i<s0gi=∏i<0gi=e.

basegiven
1.6

Regrouping law, inductive hypothesis: assume ∏j<rBj=∏i<srgi for this r.

ih
1.7

Commutative case, base n=0: both products are empty, hence both equal e.

basegiven
1.8

Commutative case, inductive hypothesis: fix n and assume that for every family g, every π∈Sym⁡(n) and every family h with hi=gπ(i) for i<n, one has ∏i<nhi=∏i<ngi.

ih
1.9

Successor step, the data. Let π∈Sym⁡(σ(n)) and let h satisfy hi=gπ(i) for every i<σ(n). Put k:=π−1(n), so k<σ(n), that is k≤n, and let r be the natural with k+r=n; then k+σ(r)=σ(k+r)=σ(n).

givenL3L4L5L6choose
1.10

The skip map. Define δ:N→N by δ(i)=i when i<k and δ(i)=σ(i) when k≤i; the two clauses are exhaustive and mutually exclusive by trichotomy, so δ is a function. It is injective: two arguments below k with equal images are equal; two arguments at least k have equal images only if their successors agree, hence only if they agree; and if i<k≤j then δ(i)=i<k≤j<σ(j)=δ(j).

L4L5construct
2.1

Splitting law, successor step: m+σ(n)=σ(m+n), so ∏i<m+σ(n)gi=∏i<σ(m+n)gi=(∏i<m+ngi)⋅gm+n; applying the hypothesis and then associativity, this equals ((∏i<mgi)⋅∏j<nuj)⋅un=(∏i<mgi)⋅((∏j<nuj)⋅un)=(∏i<mgi)⋅∏j<σ(n)uj, which is the claim at σ(n).

step 1.2step 1.3givenL2L3
2.2

δ maps n into σ(n)∖{k}, and onto it. If i<k then δ(i)=i≠k and i<k≤n<σ(n). If k≤i<n then δ(i)=σ(i) with k≤i<σ(i), so δ(i)≠k, and i<n gives σ(i)<σ(n) by compatibility of the order with adding 1. Conversely let y<σ(n) with y≠k. If y<k then y<k≤n, so y<n and y=δ(y). If k<y then y≠0, so y=σ(x) for some x; from k<σ(x) we get k≤x, and from σ(x)<σ(n) we get x<n, so y=σ(x)=δ(x) with x<n.

step 1.9step 1.10L4L5
3.1

By induction the splitting law holds for all m,n∈N; this is claim 1.

step 1.1step 2.1L1
3.2

The reduced permutation. Set π′:=π∘δ restricted to n. By step 2.2 it maps n into π[σ(n)∖{k}], and since π is a bijection of σ(n) with π(k)=n, that image set is σ(n)∖{n}=n; the same step gives surjectivity onto it, and π′ is injective as a composite of injections. So π′∈Sym⁡(n).

step 1.9step 2.2L5L6
4.1

Regrouping law, successor step: ∏j<σ(r)Bj=(∏j<rBj)⋅Br=(∏i<srgi)⋅∏l<crgsr+l by the hypothesis, and the splitting law with m=sr and n=cr turns the right-hand side into ∏i<sr+crgi=∏i<sσ(r)gi. By induction claim 2 holds for every r.

step 3.1step 1.4step 1.5step 1.6givenL1
4.2

Splitting the permuted product. By step 1.9 and the splitting law, ∏i<σ(n)hi=∏i<k+σ(r)hi=(∏i<khi)⋅(∏j<σ(r)hk+j); and since σ(r)=1+r, a second application of the splitting law to the family j↦hk+j gives ∏j<σ(r)hk+j=(∏j<1hk+j)⋅(∏l<rhk+1+l)=hk⋅∏l<rhk+σ(l).

step 3.1step 1.9givenL3
4.3

Recognising the shorter permuted product. Let wi:=hδ(i). For i<k one has wi=hi, and for l<r one has wk+l=hσ(k+l)=hk+σ(l); so the splitting law at m=k, n=r gives ∏i<nwi=(∏i<khi)⋅∏l<rhk+σ(l). Moreover wi=hδ(i)=gπ(δ(i))=gπ′(i) for every i<n, by step 2.2 and step 3.2.

step 3.1step 1.9step 1.10step 2.2step 3.2L3
5.1

Moving the removed factor to the end. hk=gπ(k)=gn, and M is commutative, so (∏i<khi)⋅(hk⋅∏l<rhk+σ(l))=((∏i<khi)⋅∏l<rhk+σ(l))⋅gn, using commutativity to exchange hk with the block to its right and associativity to regroup.

step 1.9step 4.2givenL2
6.1

Applying the hypothesis. The family w satisfies wi=gπ′(i) for i<n with π′∈Sym⁡(n), so the inductive hypothesis gives ∏i<nwi=∏i<ngi; combining with steps 4.2, 5.1 and 4.3, ∏i<σ(n)hi=(∏i<ngi)⋅gn=∏i<σ(n)gi, which is the claim at σ(n).

step 1.8step 3.2step 4.2step 5.1step 4.3given
7.1

By induction claim 3 holds for every n; with claims 1 and 2 already established, the theorem is proved.

step 3.1step 4.1step 1.7step 6.1L1discharge-induction∎

Remarks

  • What "does not depend on the bracketing" means here, exactly. The library introduces no formal syntax of bracketed expressions, so the claim is made in the equivalent working form of claim 2: any way of cutting the list into consecutive blocks, multiplying each block out, and multiplying the block values in order returns the same element. Every bracketing of g0g1⋯gn−1 is obtained by iterating that cut, so claim 2 is what is used whenever one drops brackets in a long product.

  • The order of the factors is a separate question from the bracketing. Claim 2 holds in any monoid and never moves a factor past another; claim 3 does move factors, and is false without commutativity. In Sym⁡({1,2,3}) the two transpositions (1 2) and (2 3) already give τρ≠ρτ (Sym⁡(X) is a group under composition, and it is non-abelian whenever X has at least three distinct elements).

  • The empty product carries the induction. Both inductions start at n=0 with the value e; N contains 0, so this is a real base case and not a degenerate convention.

Depends on

Used by

Dependency tree · two levels

34 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