# Why the sieve produces powers: a complete proof guide

This chapter gives an elementary proof of Moessner's theorem and matches its steps to the actual declarations in [lean/Moessner.lean](https://github.com/archgpt-agent/fengshui-2076/blob/main/lean/Moessner.lean). It proves the result for every natural output index and every positive integer degree. No finite table, numerical pattern, or previously assumed theorem about the sieve is used to close the argument.

The proof has two parts. First, a block recurrence satisfies a local identity that forces the final row to grow by multiplication with the output position. Second, that recurrence is shown to describe the literal deletion-and-prefix-sum algorithm. Both parts are necessary: a recurrence with the right answer would not establish anything about a different algorithm.

## 1. The theorem, with the parameter conventions exposed

Let \(P_{m,q}\) be a zero-indexed stream. Define

\[
P_{0,q}(k)=k+1,
\]

and obtain \(P_{m+1,q}\) by deleting every \((q+2)\)nd entry of \(P_{m,q+1}\), then taking inclusive prefix sums. Consequently, \(P_{m,0}\) applies deletion periods

\[
m+1,m,\ldots,2
\]

to the positive integers, with a prefix sum after each deletion. The theorem is

\[
\boxed{P_{m,0}(k)=(k+1)^{m+1}.}
\]

In the familiar degree notation, put \(d=m+1\). There are \(d-1\) actual passes from the positive integers. At degree one there are none.

| Mathematical role | These notes | Lean | Haskell / JavaScript |
| --- | --- | --- | --- |
| Degree of the final power | \(d\geq1\) | `m + 1` in `moessner m k` | argument of `sieve` / `moessner` |
| Passes from positive integers | \(m=d-1\) | `positiveSieve m 0` | periods `d,d-1,...,2` |
| Zero-based output index | \(k\) | stream argument `k` | list/array index |
| One-based base of the power | \(k+1\) | `(k + 1)` | printed term number |
| A deletion period | \(r\geq2\) | `q + 2` in `deleteEvery q` | `period` / `stride` |
| Retained block width | \(r-1\) | `q + 1` | `stride - 1` |

The extra parameter \(q\) lets the proof discuss intermediate widths instead of proving only the final width-one case. That generality is what makes induction work.

## 2. Start from ones to simplify the invariant

Introduce a second family \(S_{m,q}\). Its starting stream is constant:

\[
S_{0,q}(k)=1.
\]

It has the same recursive deletion-and-summation step as \(P\):

\[
S_{m+1,q}=\operatorname{scan}\big(D_q(S_{m,q+1})\big).
\]

Here `scan` means inclusive prefix sum, and the retained-position map is

\[
(D_qf)(k)
=f\left(\left\lfloor\frac{k}{q+1}\right\rfloor(q+2)
       +(k\bmod(q+1))\right).
\tag{1}
\]

This is `sieve m q` in Lean. The plan is to prove

\[
S_{m,0}(k)=(k+1)^m.
\tag{2}
\]

The apparent extra pass is harmless but must be counted. A deletion from an infinite row of ones still leaves ones. Its inclusive prefix sums are \(1,2,3,\ldots\). Therefore

\[
S_{1,q}(k)=k+1=P_{0,q}(k)
\]

for every \(q\). Applying the same subsequent steps gives

\[
P_{m,q}=S_{m+1,q}.
\tag{3}
\]

For degree four, the positive-integer formulation uses periods 4, 3, 2. The ones formulation uses periods 5, 4, 3, 2; its first pass produces the positive integers. Keeping these two formulations separate prevents the most common off-by-one error.

Lean names for this bridge are `sieve_one` and `positiveSieve_eq_sieve`. We will prove (2) before using (3).

## 3. The block recurrence

For nonnegative integers \(m,q,i,x\), define a number \(R_m^q(i,x)\). It represents a column \(x\) in block \(i\), after \(m\) passes from ones, with retained block width \(q+1\). Define

\[
R_0^q(i,x)=1,
\tag{4}
\]

and

\[
R_{m+1}^q(i,x)
=\sum_{a=0}^{x}R_m^{q+1}(i,a)
 +\sum_{j=0}^{i-1}\sum_{a=0}^{q}R_m^{q+1}(j,a).
\tag{5}
\]

An empty sum is zero. Formula (5) adds the retained part of every preceding block and then the current block through column \(x\). The previous row has block width \(q+2\); its final column \(q+1\) is omitted, leaving columns \(0,\ldots,q\).

For an actual stream cell we require \(x<q+1\). The algebraic definition itself is total for every natural \(x\), and the identity below holds on that larger domain. These out-of-block values are useful auxiliary quantities; they are not extra cells in a displayed block.

The first row is especially simple:

\[
R_1^q(i,x)=(x+1)+i(q+1).
\tag{6}
\]

There are \(i(q+1)\) retained ones in preceding blocks and \(x+1\) in the current prefix. This is Lean's `row_one`; (4) and (5) are its definition `row`.

## 4. A weighted-prefix identity

For any sequence \(a_0,a_1,\ldots\) and \(N\geq0\),

\[
\boxed{
\sum_{j=0}^{N-1}\left(j a_j+\sum_{h=0}^{j}a_h\right)
=N\sum_{j=0}^{N-1}a_j.
}
\tag{7}
\]

To prove it, fix an index \(h<N\). In the double sum, \(a_h\) appears in the prefixes ending at \(h,h+1,\ldots,N-1\), for \(N-h\) copies. The separate weighted sum supplies \(h\) further copies. The total is \(N\) copies of every \(a_h\). If \(N=0\), both sides are empty sums and equal zero.

This argument uses only finite distributivity. Lean proves the same identity by induction in `weighted_prefix`. It is the mechanism that turns accumulated corrections into a single multiplier.

## 5. The invariant that compares adjacent widths

For all \(m,q,i,x\geq0\),

\[
\boxed{
R_{m+1}^{q+1}(i,x)
=R_{m+1}^{q}(i,x)+iR_m^{q+1}(i,x).
}
\tag{8}
\]

This is `row_difference`. It compares two computations at the same pass depth but adjacent remaining widths. It does not merely compare successive rows of one numerical table. Widening the block changes both the current prefix and every preceding block; the right-hand correction accounts for both changes.

### Base case

For \(m=0\), use (6):

\[
\begin{aligned}
R_1^{q+1}(i,x)&=(x+1)+i(q+2),\\
R_1^{q}(i,x)+iR_0^{q+1}(i,x)
&=(x+1)+i(q+1)+i.
\end{aligned}
\]

These expressions are equal.

### Inductive step

Assume (8) holds at depth \(m+1\), for every \(q,i,x\). We prove it at depth \(m+2\). Fix \(q,i,x\), and abbreviate

\[
A_j=\sum_{a=0}^{q+1}R_m^{q+2}(j,a),
\qquad
B_j=\sum_{a=0}^{q}R_{m+1}^{q+1}(j,a).
\]

Also write

\[
U=\sum_{a=0}^{x}R_{m+1}^{q+1}(i,a),
\qquad
V=\sum_{a=0}^{x}R_m^{q+2}(i,a).
\]

There are three small calculations.

**The current block prefix.** Apply the induction hypothesis with width parameter \(q+1\), then sum over \(a=0,\ldots,x\):

\[
\sum_{a=0}^{x}R_{m+1}^{q+2}(i,a)=U+iV.
\tag{9}
\]

**The extra boundary column.** Expand (5) at column \(q+1\):

\[
R_{m+1}^{q+1}(j,q+1)
=A_j+\sum_{h=0}^{j-1}A_h
=\sum_{h=0}^{j}A_h.
\tag{10}
\]

**A preceding block.** Apply the induction hypothesis across a full block of the wider computation:

\[
\begin{aligned}
\sum_{a=0}^{q+1}R_{m+1}^{q+2}(j,a)
&=\sum_{a=0}^{q+1}R_{m+1}^{q+1}(j,a)+jA_j\\
&=B_j+\sum_{h=0}^{j}A_h+jA_j.
\end{aligned}
\tag{11}
\]

The second equality separates the boundary column and uses (10).

Now expand \(R_{m+2}^{q+1}(i,x)\) using (5), substitute (9) and (11), and apply (7) with \(N=i\):

\[
\begin{aligned}
R_{m+2}^{q+1}(i,x)
&=U+iV+\sum_{j=0}^{i-1}
   \left(B_j+jA_j+\sum_{h=0}^{j}A_h\right)\\
&=U+\sum_{j=0}^{i-1}B_j
  +i\left(V+\sum_{j=0}^{i-1}A_j\right)\\
&=R_{m+2}^{q}(i,x)+iR_{m+1}^{q+1}(i,x).
\end{aligned}
\]

The last line is exactly (5), once for each parenthesized part. This completes the induction and proves (8) on its full stated domain.

The local subproof names in Lean are `own`, `boundary`, and `previous`. They correspond to (9), (10), and (11), respectively. The proof uses addition rather than subtraction, so it does not depend on a hidden assumption that natural-number differences stay nonnegative.

## 6. The width-one output must be a power

Define

\[
O_m(i)=R_m^0(i,0).
\tag{12}
\]

Each block now has one retained column. Formula (5) becomes

\[
O_{m+1}(i)=\sum_{j=0}^{i}R_m^1(j,0).
\tag{13}
\]

This is `output_succ`. We will prove

\[
O_{m+1}(i)=(i+1)O_m(i).
\tag{14}
\]

For \(m=0\), (4) and (6) give \(O_0(i)=1\) and \(O_1(i)=i+1\), establishing (14).

For all remaining cases, fix \(m\geq0\) and put \(a_j=R_m^1(j,0)\). The adjacent-width invariant (8), with \(q=0\), gives

\[
R_{m+1}^1(j,0)
=O_{m+1}(j)+ja_j
=\sum_{h=0}^{j}a_h+ja_j,
\]

where the second equality uses (13). Summing over \(j=0,\ldots,i\), then applying (7) with \(N=i+1\), yields

\[
\begin{aligned}
O_{m+2}(i)
&=\sum_{j=0}^{i}R_{m+1}^1(j,0)\\
&=(i+1)\sum_{j=0}^{i}a_j\\
&=(i+1)O_{m+1}(i).
\end{aligned}
\]

Together with the base case, this proves (14). Starting from \(O_0(i)=1\), ordinary induction now gives

\[
\boxed{O_m(i)=(i+1)^m.}
\tag{15}
\]

This is the point at which exponentiation enters the proof: it is characterized by the recurrence \(a^0=1\), \(a^{m+1}=a\,a^m\). The earlier sieve recurrence never assumed that characterization for its output. The matching Lean theorems are `output_succ_mul` and `output_eq_power`.

## 7. Why these arrays really are the operational sieve

We must connect the arithmetic arrays to actual deletion. The bridge is

\[
\boxed{
S_{m,q}\big(i(q+1)+x\big)=R_m^q(i,x)
\quad\text{when }0\leq x<q+1.
}
\tag{16}
\]

We prove (16) by induction on \(m\), generalizing all other indices.

At \(m=0\), both sides are one. For the step, consider a retained index \(j(q+1)+a\), with \(0\leq a<q+1\). Division and remainder give

\[
\left\lfloor\frac{j(q+1)+a}{q+1}\right\rfloor=j,
\qquad
(j(q+1)+a)\bmod(q+1)=a.
\]

By (1), deletion maps this index to source position \(j(q+2)+a\). The induction hypothesis for the previous stream \(S_{m,q+1}\) is applicable because \(a<q+2\). Its value is \(R_m^{q+1}(j,a)\).

The inclusive prefix ending at \(i(q+1)+x\) consists of all columns \(0,\ldots,q\) in blocks \(0,\ldots,i-1\), then columns \(0,\ldots,x\) in block \(i\). Splitting that finite sum and substituting the previous values gives exactly (5). This proves (16).

The finite-sum splitting is `sum_blocks_prefix`, and the source-position calculation is `deleteEvery_block`. The bridge itself is `sieve_eq_row`. Setting \(q=0\) and \(x=0\) in (16), and then applying (15), gives

\[
S_{m,0}(k)=O_m(k)=(k+1)^m,
\]

which is `sieve_eq_power`. Finally, use (3):

\[
P_{m,0}(k)=S_{m+1,0}(k)=(k+1)^{m+1}.
\]

This is Lean's theorem `moessner`, and it completes the proof of the positive-integer algorithm.

## 8. A map of the formal proof

The file defines its own finite sum, `sum n f`, meaning \(f(0)+\cdots+f(n-1)\). Thus `sum (x + 1)` is an inclusive sum through \(x\); `sum i` stops before \(i\). It imports `Std`, with no external mathematical library required for this development.

| Declaration | Mathematical job |
| --- | --- |
| `sum_congr`, `sum_add`, `sum_mul`, `sum_const` | Basic finite-sum algebra |
| `weighted_prefix` | Identity (7), used to combine width corrections |
| `row`, `row_one` | Recurrence (5), and its first row |
| `row_difference` | Adjacent-width invariant (8) |
| `output`, `output_succ` | Width-one output and equation (13) |
| `output_succ_mul`, `output_eq_power` | Multiplication recurrence and powers |
| `deleteEvery`, `step`, `sieve` | Literal ones-stream algorithm |
| `deleteEvery_block`, `sum_blocks_prefix` | Source indexing and finite prefix partition |
| `sieve_eq_row`, `sieve_eq_power` | Operational bridge and ones theorem |
| `positiveSieve_eq_sieve`, `moessner` | Positive-integer formulation |
| `g_eq_row` | Correspondence with the alternative triangle coordinates |

For the positive-integer algorithm, the theorem covers every natural output index and every positive degree. Degree zero is included only in the auxiliary formulation starting from ones. The website's controls of degree 1 through 9 are a presentation and resource choice. A proof assistant's guarantee is about the stated Lean definitions. It does not automatically prove that a separate Haskell compiler, JavaScript engine, or rendered animation implements those definitions correctly.

To check the Lean development in an environment with its pinned toolchain installed:

```bash
cd lean
lake build
```

To inspect the logical dependencies of a theorem in a Lean file importing `Moessner`, use, for example:

```lean
#print axioms Moessner.moessner
#print axioms Moessner.sieve_eq_power
```

These commands audit dependencies; reading a theorem's source is distinct from running the checker. No new Lean proof was added by these explanatory notes.

## 9. Matching the Haskell recurrence and stream implementation

[Moessner.hs](https://github.com/archgpt-agent/fengshui-2076/blob/main/haskell/src/Moessner.hs) evaluates `sieve d` by positional deletion and inclusive prefix sums over arbitrary-precision `Integer`. It starts from `[1..]` and applies periods `[d,d-1..2]`. Therefore its intended correspondence is

\[
\texttt{sieve d !! k}=P_{d-1,0}(k),
\]

for \(d\geq1\) and \(k\geq0\), after unwrapping the successful result. The theorem establishes the right-hand stream's value. Tests and code review establish agreement between implementations; the repository does not contain a proof of Haskell language semantics transporting the Lean theorem to compiled machine code.

The Haskell table model uses an additional fixed parameter \(n\geq0\), levels \(\ell\), block indices \(i\), and columns \(x\). Write its entry as \(G_\ell(i,x;n)\). Its initial level is

\[
G_0(i,x;n)=i(n+2)+x+1.
\]

For \(1\leq\ell\leq n+1\), the implementation uses the local recurrences

\[
\begin{aligned}
G_\ell(0,0;n)&=G_{\ell-1}(0,0;n),\\
G_\ell(i,0;n)&=G_{\ell-1}(i,0;n)
               +G_\ell(i-1,n-\ell+1;n) &&(i>0),\\
G_\ell(i,x;n)&=G_\ell(i,x-1;n)+G_{\ell-1}(i,x;n) &&(x>0).
\end{aligned}
\]

Unroll the final recurrence across a row, then the boundary recurrence across preceding blocks. This gives

\[
G_\ell(i,x;n)
=\sum_{a=0}^{x}G_{\ell-1}(i,a;n)
 +\sum_{j=0}^{i-1}\sum_{a=0}^{n-\ell+1}G_{\ell-1}(j,a;n).
\]

It is the same prefix recurrence with a different choice of coordinates:

\[
\boxed{G_\ell(i,x;n)=R_{\ell+1}^{\,n+1-\ell}(i,x),
\qquad 0\leq\ell\leq n+1.}
\]

Lean's `g_eq_row` proves this correspondence for its `g` definition. At the final level \(\ell=n+1\), the remaining width is one, so

\[
G_{n+1}(i,0;n)=(i+1)^{n+2}.
\]

For degree \(d\geq2\), use \(n=d-2\). The local table constructor allocates the boundary columns needed by the recurrence and rejects invalid indices. It is important that the previous-block endpoint is \(n-\ell+1\): changing it by one changes the retained block width and hence the theorem.

The Haskell module also exposes `paperM`, which evaluates an accumulated-triangle expression, while Lean's `M` is defined operationally. Their identical names or expected numerical values should not be mistaken for a direct foreign-language proof. The declaration `M_eq_g` connects Lean's `M` to its own final triangle cell; the Haskell verification suite supplies finite checks for its independently evaluated formulas.

## 10. Nested sums and function-space counting

The source-index formula (1) can also be written

\[
\left\lfloor\frac{k}{q+1}\right\rfloor(q+2)
 +(k\bmod(q+1))
=k+\left\lfloor\frac{k}{q+1}\right\rfloor.
\]

Consequently, opening the recursive stream computation yields the nested-sum recurrence

\[
V_0(x,j)=1,
\qquad
V_{p+1}(x,j)=\sum_{i=0}^{x}
V_p\left(i+\left\lfloor\frac{i}{j}\right\rfloor,j+1\right),
\qquad j\geq1.
\]

[Summation.lean](https://github.com/archgpt-agent/fengshui-2076/blob/main/lean/Summation.lean) proves `visit_eq_sieve`, hence

\[
V_p(x,1)=(x+1)^p.
\]

A different calculation chooses one of \(x+1\) possibilities independently at each of \(p\) positions. Its count satisfies

\[
C_0(x)=1,
\qquad C_{p+1}(x)=(x+1)C_p(x),
\]

so it also equals \((x+1)^p\). This is the cardinality of total functions from a \(p\)-element domain to an \((x+1)\)-element codomain.

The Lean theorem `nestedMoessner_eq_constantNested` equates these counts. It does not select a particular bijection between dependent-bound paths and ordinary function tables. [FunctionSpace.hs](https://github.com/archgpt-agent/fengshui-2076/blob/main/haskell/src/Moessner/Dependent/FunctionSpace.hs) separately enumerates canonical output tables with type `Vec (Pow a b) (FiniteFunction b a)`. Its interpretation concerns total finite values and extensional functions, excluding nontermination and distinctions between different programs computing the same function.

These connections explain why powers are natural mathematical objects to compare with the sieve. They do not replace the operational bridge proved in Section 7.

## 11. Scope of the chart theorems

[FengShui.lean](https://github.com/archgpt-agent/fengshui-2076/blob/main/lean/FengShui.lean) defines a chart as a function from nine palaces to `Fin 9`. Display labels add one to the stored residue. It proves that the centre is preserved, degree one recovers sequential flight, and every displayed star is between 1 and 9. Its `anchoredOffset_eq_power` uses `sieve_eq_power` to identify the exact offset with \((i+1)^d-1\).

The complete modulo-nine classification in [Chapter 4](04-ninefold-residue-classification.md) is an additional mathematical proof in prose. The current Lean file contains concrete collision examples, but it does not yet formalize that entire classification. No arithmetic theorem establishes traditional interpretations or empirical efficacy.

## Independent primary reference

Mark Bickford, Dexter Kozen, and Alexandra Silva, [*Formalizing Moessner's Theorem in Nuprl*](https://nuprl-web.cs.cornell.edu/documents/Moessner/), 2012. This is an independent formalization using a different development. It provides background and a useful comparison of proof design. The proof above is derived from the local block recurrence and uses only the elementary identities it states and proves.