# Mathematics learning collection

This collection develops Moessner's theorem from worked arithmetic to the exact block invariant used in the project's Lean proof, then studies the nine-star projection as a separate mathematical construction.

| Chapter | Main questions | Download |
| --- | --- | --- |
| The sieve, by hand | Why do deletion and addition produce squares, cubes, and fourth powers? How much finite input is enough? | [01-moessner-tutorial.md](01-moessner-tutorial.md) |
| A complete proof | What is the block invariant? Where does exponentiation enter? How do the Lean and Haskell indices correspond? | [02-proof-guide.md](02-proof-guide.md) |
| Practice and connections | What changes if deletion is omitted? How do finite differences and function spaces illuminate the outputs? | [03-exercises-and-solutions.md](03-exercises-and-solutions.md) |
| The ninefold projection | Which stars repeat? Why are there exactly 9, 7, 4, 3, or 2 distinct stars? | [04-ninefold-residue-classification.md](04-ninefold-residue-classification.md) |
| Reproducible examples | Exact rows, deletion masks, powers, residue counts, and charts as decimal strings | [worked-examples.json](worked-examples.json) |
| Independent verification | Regenerate the examples and check the finite sieve, recurrence, and residue formulas with Python integers | [verify_examples.py](verify_examples.py) |

## Suggested learning route

Begin with the square and cube tables in Chapter 1. Read its indexing and finite-prefix sections before trying to implement the algorithm. Chapter 2 gives a complete elementary proof, with each major identity matched to a declaration in `lean/Moessner.lean`. Chapter 3 offers exercises followed by full solutions. Chapter 4 proves the residue classification for every positive integer degree, including degrees beyond the website's current controls.

The operational sieve theorem is classical. The centre-anchored nine-star projection is this project's experimental construction. Its arithmetic properties do not establish a historical practice, a full traditional natal chart, or physical effects. The conventional flight path and the choice of visual orientation supply a coordinate system; they are not premises of the theorem about powers.

## Implementation links

- [Lean arithmetic proof](https://github.com/archgpt-agent/fengshui-2076/blob/main/lean/Moessner.lean)
- [Lean nested-summation correspondence](https://github.com/archgpt-agent/fengshui-2076/blob/main/lean/Summation.lean)
- [Lean bounded-star construction](https://github.com/archgpt-agent/fengshui-2076/blob/main/lean/FengShui.lean)
- [Haskell operational sieve and finite recurrence](https://github.com/archgpt-agent/fengshui-2076/blob/main/haskell/src/Moessner.hs)
- [Haskell finite function spaces](https://github.com/archgpt-agent/fengshui-2076/blob/main/haskell/src/Moessner/Dependent/FunctionSpace.hs)
- [Haskell chart construction](https://github.com/archgpt-agent/fengshui-2076/blob/main/haskell/src/Moessner/FengShui.hs)
- [JavaScript exact-integer engine](https://github.com/archgpt-agent/fengshui-2076/blob/main/website/public/engine.mjs)

The proof guide distinguishes a theorem in the Lean development, an independent pen-and-paper derivation in these notes, and a finite computational check. New results in these notes, including the complete residue classification, are not silently presented as additional Lean theorems.

## Reproduce the numerical examples

From the repository root, run:

```sh
python3 docs/mathematics/verify_examples.py
```

The script uses only the Python standard library. It recomputes the saved JSON and checks 300 sieve and minimal-prefix cases, 500 block-invariant cases, 104 output-power cases, 216 chart cases, and the residue classification through degree 60. These finite checks support implementation review; the proofs in Chapters 2 and 4 establish the corresponding universal statements. To deliberately regenerate the JSON after changing the example specification, add `--write`.

## Source policy

The exposition and derivations are original to these notes. The independent primary reference is [*Formalizing Moessner's Theorem in Nuprl*](https://nuprl-web.cs.cornell.edu/documents/Moessner/) by Mark Bickford, Dexter Kozen, and Alexandra Silva. It provides a separate formalization and background; our proof walkthrough follows the local Lean block recurrence and does not depend on the Nuprl formalization.