How addition becomes a power.

A small rule with a surprising destination

Begin with the positive integers. Delete certain positions. Add the surviving entries from left to right. Repeat with a smaller deletion interval. The resulting row is a familiar power sequence, even though the procedure itself never raises a number to a power.

This is the power form of Moessner’s theorem. The classical mathematical construction is our starting point. The subsequent projection into Flying Star labels is an original experiment in this project, with a different purpose and a separate set of claims.

1. Choose a degree d and an output count N. Begin with the finite row 1, 2, …, Nd.
2. For each stride q = d, d − 1, …, 2: number the current row from one, remove positions divisible by q, and replace the survivors with their inclusive running totals.
3. Keep the final row. It contains N entries: 1^d, 2^d, …, N^d. Degree one requires no deletion or summation pass.

The workbench above constructs six final terms. Select a running total to inspect its contributing survivors. In the written examples below, four final terms keep every row short enough to read.

Squares: one pass, odd increments

For degree two, start with eight integers to obtain four outputs. Removing positions 2, 4, 6, and 8 leaves the odd numbers. Their running totals are the squares.

The difference identity explains this case directly: the next odd increment grows the previous square into the next square. The finite prefix matters. To obtain N squares, begin with 2N entries; this provides exactly N survivors rather than an incomplete last pass.

Cubes: let one row prepare the next

For degree three, the deletion strides are 3, then 2. Begin with twelve entries. The first pass removes positions 3, 6, 9, and 12, then accumulates the remaining eight entries. The second pass acts on that new row.

That new row begins 1, 3, 7, 12, 19, 27, 37, 48. Its even positions contain 3, 12, 27, and 48. These are the entries removed in the second pass. In particular, 3 and 27 are removed even though neither value is even.

For example, 19 = 3³ − 2³ and 37 = 4³ − 3³. The final prefix sum telescopes to n³. A proof for every degree must explain how the earlier passes produce the required increments, not just recognize the final four answers.

Fourth powers: the same rule, one layer deeper

For degree four, begin with sixteen entries and use strides 4, 3, and 2. Every pass removes four entries. The row lengths descend through 16, 12, 8, and 4, while the values grow.

After the first sum, remove positions 3, 6, 9, and 12 of the twelve-entry row. Their values are 6, 24, 54, and 96. After the next sum, the final survivors are 1, 15, 65, 175.

These examples make the mechanism inspectable. They also suggest the right general question: what invariant describes an intermediate row before the final powers appear? That is where the proof begins.

From convincing rows to a proof

A collection of correct examples provides useful checks. The general theorem needs a statement covering every permitted degree and position. The project’s proof and construction notes separate that theorem from implementation tests.

1. Specify the operators. Define deletion using one-based position in the current row, and define inclusive prefix summation. This fixes the off-by-one choices before any proof or program is assessed.
2. Describe intermediate values. Use a recurrence or nested-sum invariant that survives each deletion-and-summation pass. Establish the base case and the step that moves between layers. A final-row difference identity alone does not establish this invariant.
3. Connect the construction to powers. Derive M_d(n) = n^d from the operational definition for arbitrary positive d and n. Cornell’s independent formal account ↗ supplies another route through the classical theorem.
4. Justify the finite prefix. Before stride q there are Nq entries; deletion removes N, leaving N(q − 1). Every output prefix depends only on earlier entries. Starting with Nd therefore supplies exactly N final terms.
5. Prove the projection separately. Show that the modular result lies in 1…9, the centre stays fixed, and degree one agrees with the sequential reference.

The included Lean development formalizes arithmetic and finite constructions. Browser and Haskell tests check their implementations against independently computed powers, including large exact integers. The project does not claim a machine-checked refinement from those implementations into Lean. Each form of evidence has a visible boundary.

One power, two constructive viewpoints

The retained typed construction gives powers a second interpretation. A total function from a d-element set to an n-element set is determined by d output choices, each with n possibilities. There are n^d such functions.

In this viewpoint, a function is an explicit output table. Extending the input domain by one element chooses a new output and a smaller table, yielding the recurrence n^d+1 = n × n^d. The empty input domain contributes one empty table.

This connects the new study to the project’s original computational construction: exact summations, finite choices, indexed types, and structural evidence. The sieve generates integers; a finite-function enumeration explains the power as a cardinality; the nine-palace rule then reduces that integer. These are related operations, not interchangeable definitions of a traditional chart.

A vector with a stated length does not, by itself, establish that an enumeration has every function exactly once. Completeness and uniqueness need their own argument. Likewise, dependent choices whose later possibilities vary with earlier choices produce nested sums; they need not yield powers. The technical guides make these distinctions explicit.

From an exact integer to a star label

Keep the full sieve output before taking a remainder. The fixed palace path is Centre → NW → W → NE → S → N → SW → E → SE. At zero-based path position k, choose centre c ∈ {1,…,9} and arithmetic direction ε ∈ {+1,−1}, then assign:

At k = 0, M_d(1) − 1 = 0, so the centre remains c. At degree one, the offset is k, which recovers the sequential base flight. Rotating the display between south-up and north-up changes no palace identity or arithmetic.

For degree two, centre 9, and forward direction, the Northwest palace has k = 1. Its exact value is M₂(2) = 4, its offset is 3, and its displayed star is 1 + mod(8 + 3, 9) = 3. The observatory exposes this calculation for every palace, alongside the unreduced integer and the baseline.

The reference is one sequential base-chart layer. Facing direction, building period, mountain stars, water stars, and school-specific rules would require a broader traditional model. A mathematically correct reduction does not establish physical effects on a place or its inhabitants.

Why a higher degree can contain fewer stars

Higher degree means a different arithmetic rule. It does not imply a larger statistical variance, a more balanced chart, or a stronger influence. Modulo nine, much of the growing integer is intentionally forgotten.

For every d ≥ 2, the terms at n = 3, 6, and 9 are divisible by nine. They therefore share a residue and a projected star. No higher-degree pattern in this family can be a permutation of all nine stars. Changing the centre translates residue labels; reversing direction negates them. Both operations preserve which entries collide.

The six residues coprime to nine form a cyclic multiplicative group of order six. For d ≥ 2, taking d-th powers gives 6 / gcd(d, 6) distinct unit residues, plus the common zero residue. Thus the number of distinct stars is 1 + 6 / gcd(d, 6). For example, degree five has seven distinct stars; degree six has two.

The projected sequences repeat with period six in the degree once d ≥ 2. The exact integer sequences continue to change. This contrast is useful to study: one can inspect residue collisions, compare prefix growth, or propose a different modulus while retaining the full calculation. A different modulus would also leave the nine-star labeling convention and would need its own interpretation.

Take the construction to your desk

The downloadable notes develop the sieve, the retained typed construction, proof scope, and possible mathematical extensions. They are plain-text Markdown files, suitable for reading, annotation, and version comparison.

Reproduce the arithmetic with the exact worked rows (JSON) and the example checker (Python).

Return to the Flying Star Observatory to vary centre, degree, and direction, inspect all stages, and export an exact audit as JSON. Its SVG export records a particular visual arrangement. Use the source notes to keep the classical theorem and this project’s experimental application distinct.