Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26
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.

The Lehmer code is a bijection Sn→∏i=1n{0,…,i−1}

Statement

For every n∈N, the Lehmer-code map

L:Sn→∏i=1n{0,…,i−1}

is a bijection.

Facts & Assumptions

Given: A natural number n and the Lehmer code map L:Sn→∏i=1n{0,…,i−1}.

[L1]

A function is bijective if it is both injective and surjective (Injection, surjection, bijection).

Proof

technique · constructive
1.1given

For σ∈Sn, the component ℓi(σ) counts entries to the right of position n−i, and there are exactly i−1 such positions, so 0≤ℓi(σ)≤i−1. Thus L(σ) lies in the stated codomain.

1.2construct

Conversely, let (c1,…,cn) lie in the codomain. Begin with the increasing list R=[0,1,…,n−1] of unused values. For i=n,n−1,…,1, put in position n−i the value of R having exactly ci smaller elements in R, and delete that value from R. This choice exists and is unique because R has i elements and 0≤ci<i. Call the resulting permutation σc.

2.1step 1.2algebra

The permutation σc has Lehmer code (c1,…,cn). At the stage for i, all values then left in R will occupy the i−1 positions to the right of position n−i. The chosen value has exactly ci smaller values in R, so exactly ci later entries of σc are smaller than it. This is the defining equality ℓi(σc)=ci.

3.1step 1.2step 2.1L1

The construction is unique. At position 0, all n values are unused and the code coordinate cn requires the entry with exactly cn smaller unused values. After deleting it, coordinate cn−1 uniquely determines the next entry among the remaining values, and so on. Thus any permutation with code c is exactly σc. Step 2.1 gives surjectivity and this uniqueness gives injectivity.

4.1step 3.1L1discharge-construct∎

Therefore L is a bijection. The case n=0 is included: both sides are the singleton empty object.

Depends on

Used by

Dependency tree · two levels

5 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