From 7468d3047866ced7552fea9fe3df8c52887ed86d Mon Sep 17 00:00:00 2001 From: Carlo Perassi Date: Wed, 23 Sep 2026 16:20:53 +0200 Subject: [PATCH] Update field note 14 for the afternoon's two submissions #285 (Furstenberg separation) and #292 (oriented binary Markov tree) make eight submissions and 61 modules. A draft of this note claimed #285 was the first edge from one contributor's work to another's. Checking every edge showed the opposite: 22 of the 39 internal edges already cross contributors. The note now says that, and points out that the secondary metric dropped in August for want of producers has data after all. Co-Authored-By: Claude Opus 5 --- docs/website/notes/field-note-14.html | 10 ++++++---- docs/website/notes/index.html | 2 +- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/docs/website/notes/field-note-14.html b/docs/website/notes/field-note-14.html index 8f4d8586..e70da412 100644 --- a/docs/website/notes/field-note-14.html +++ b/docs/website/notes/field-note-14.html @@ -3,7 +3,7 @@ - + Field Note 14 — LeanFrontier @@ -24,22 +24,24 @@

23 September 2026 · Field Note 14

The Corpus Starts Eating Its Own Results.

-

Six submissions arrived in a morning. Every one of them is built on something already in the corpus, most of them on results accepted the day before and one on a module accepted three hours earlier, which is the behaviour the whole project exists to test.

+

Eight submissions arrived in a day. Every one is built on something already in the corpus: most on results accepted the day before, one on a module accepted three hours earlier, and one on a module another contributor submitted five weeks ago, which turns out to be the ordinary case rather than a first.

-

Six, each on top of something accepted

+

Eight, each on top of something accepted

Explicit Thue–Morse cube sums. Prouhet's theorem says the two Thue–Morse parity classes of an interval have equal cube sums; Nicomachus evaluates the cube sum of the whole interval. Together they give each half explicitly. The submission shifts the interval by four so that the Prouhet hypothesis for cubes holds automatically and the total divides in two without natural-number division.

Markov tree paths. The corpus already had the Vieta involution and, since yesterday, the ordered descent step. This adds the representation needed to iterate moves: a state of three coordinates, one parameterized move that picks which coordinate is replaced by its Vieta companion, and a walk as a finite list of moves. The single parameterized move is the interesting choice, because three permuted copies of the same theorem is exactly the degenerate family the receiver rejects.

Turán from Caro–Wei. The Caro–Wei bound landed late yesterday evening. By the following morning it had a consumer: the coarser classical bound depending only on vertex and edge counts, derived from it rather than proved again.

Horadam addition formula. Built on the companion-matrix development that landed yesterday morning, using the matrix identity rather than an induction on the recurrence.

The Sylvester reciprocal series. An older accepted result gives the finite telescoping identity for Sylvester's sequence. This one lets the sum run to infinity: the remainder vanishes because the sequence grows without bound, so the reciprocals sum to exactly one. The Egyptian-fraction story that the finite identity had left half-told.

Markov root reachability. The last of the six consumed the third: the path layer that arrived at breakfast, plus yesterday's descent step, give the global statement those two were for. Every positive integer solution of the Markov equation is reachable from (1, 1, 1) by a finite list of coordinate Vieta moves. Three submissions on three consecutive mornings, each one the substrate of the next.

+

Furstenberg separation. The interesting one. It builds on the Furstenberg topology on the integers, which a different contributor submitted on 18 August through a different model family, and proves that the topology separates any two integers by a clopen arithmetic progression and that no singleton is open. Reuse across contributors turns out to be the norm rather than the exception: 22 of the corpus's 39 internal import edges have a source and a target contributed by different people. The pre-registration dropped cross-producer reuse from its secondary metrics in August, on the grounds that a single producer made it undefined. The corpus went and produced the data anyway.

+

An oriented binary Markov tree. The three Vieta moves at a Markov state form an undirected degree-three graph. To compare it with a binary rational tree, one move has to be remembered as the edge back to the parent, leaving two forward choices. This submission records that orientation and claims nothing about the numerical labels, which is where the Markov uniqueness conjecture sits. It is the first entry of the roadmap its own author refreshed hours earlier, and it was written before that refresh had been merged.

What that pattern is worth

-

The corpus is at 59 modules. The pre-registered question behind all of this is whether machine producers accumulate: whether a result, once accepted, gets used, or whether each submission is a fresh start beside the last one. Six consecutive submissions that each import an accepted result are the shape of an answer, though not yet the measurement. What replaces the suspended launcher experiment is a series that measures exactly this, registered before it was computed.

+

The corpus is at 61 modules. The pre-registered question behind all of this is whether machine producers accumulate: whether a result, once accepted, gets used, or whether each submission is a fresh start beside the last one. Eight consecutive submissions that each import an accepted result are the shape of an answer, though not yet the measurement. What replaces the suspended launcher experiment is a series that measures exactly this, registered before it was computed.

They are also the shape the add-only rule now forces. Since yesterday a submission may not edit an existing module; extending one means importing it from a new one. That makes an import edge the only way to build on accepted work, which is convenient for the metric and, for exactly that reason, something the experiment's analysis has to discount rather than celebrate.

diff --git a/docs/website/notes/index.html b/docs/website/notes/index.html index fcd1fde4..1f464396 100644 --- a/docs/website/notes/index.html +++ b/docs/website/notes/index.html @@ -28,7 +28,7 @@

Evidence From the Frontier.

23 September 2026 · Field Note 14

The Corpus Starts Eating Its Own Results.

-

Six submissions in a morning, each built on an accepted result, and one chain of three across three mornings.

+

Eight submissions in a day, each built on an accepted result, and 22 of the corpus's 39 import edges turn out to cross from one contributor to another.

Read the note