OreAlgebraLean verification blueprint
1
Kauers–Schneider verification
▼
1
Section 2: classical Stirling identity
2
Section 3, Id. 1: \(q\)-Stirling of the second kind
3
Section 3, Id. 2: \(q\)-Stirling of the first kind (corrected)
4
Section 3, Id. 3: printed statement (classical \(S_1\)), proved; plus corrected generic-\(q\) analogs
5
Section 3, Id. 4: fully deformed variant (Carlitz-weighted resolution)
6
Section 3, companion report: the signed array form
7
Section 3, Item 5: \(q\)-Worpitzky identity
Dependency graph
1 Kauers–Schneider verification
1
Section 2: classical Stirling identity
2
Section 3, Id. 1: \(q\)-Stirling of the second kind
3
Section 3, Id. 2: \(q\)-Stirling of the first kind (corrected)
4
Section 3, Id. 3: printed statement (classical \(S_1\)), proved; plus corrected generic-\(q\) analogs
5
Section 3, Id. 4: fully deformed variant (Carlitz-weighted resolution)
6
Section 3, companion report: the signed array form
7
Section 3, Item 5: \(q\)-Worpitzky identity