Veröffentlichungen / rule-30-checkerboard-completion

Rule 30: andere Startzeilen, dieselbe Entwicklung auf der linken Seite

Du liest eine feste Version. Zur aktuellen Version

Eine einzelne Eins bei 0 und ein nach rechts unendliches 1010…-Muster ab 0 liefern dieselbe Mittelfolge; alle übrigen Zellen sind anfangs 0. Auch die Entwicklung links von der Mitte stimmt überein.

Ich vergleiche zwei Startzeilen: eine mit einer einzigen Eins bei 0 und eine mit Einsen bei 0, 2, 4, 6, … . Alle anderen Zellen sind 0.

Die Zeilen unterscheiden sich an unendlich vielen Stellen. Trotzdem stimmen ihre Werte in der Mitte zu jeder Zeit überein. Dasselbe gilt an jeder Position links von der Mitte.

                    Mitte
Einzelzelle:    …000 | 1 | 000000…
Rechter Strahl: …000 | 1 | 010101…

Die Regel lautet neu = links XOR (mitte OR rechts). Mit F^t(u)(n) bezeichne ich den Wert an Position n nach t Schritten aus der Startzeile u. Die Zeilen sind über alle ganzzahligen Positionen definiert; die Positionen steigen nach rechts an.

Für die beiden Zeilen gilt:

F^t(Einzelzelle)(n) = F^t(rechter Strahl)(n)
für alle t ≥ 0 und alle n ≤ 0.

Die allgemeine Aussage

Sei u eine beliebige binäre Zeile. Ihre rechteste belegte Zelle liegt bei R≥1: u(R)=1, und für alle n>R gilt u(n)=0. Links davon ist die Zeile beliebig.

Dann gibt es eine Zeile v, die ab einer positiven Position nach rechts räumlich abwechselnd 1, 0, 1, 0, … enthält und für die gilt:

F^t(v)(n) = F^t(u)(n)
für alle t ≥ 0 und alle n ≤ 0.

Das abwechselnde Muster betrifft die Startzeile im Raum. Es sagt nicht, dass eine feste Zelle zeitlich abwechselnd 0 und 1 annimmt.

Das Einzelzellbeispiel hat R=0 und fällt deshalb nicht direkt unter die allgemeine Aussage. Es folgt aus der ersten Konstruktion unten: Bei R−1=-1 steht eine 0, und diese Konstruktion lässt die gesamte Entwicklung an allen Positionen n≤R unverändert.

So entsteht die neue Zeile

Es gibt zwei Fälle.

Die Zelle bei R−1 ist 0. Die Zeile bleibt bis Position R unverändert. Rechts ergänzen wir belegte Zellen bei R+2, R+4, R+6, …. Die Entwicklung an jeder Position n≤R bleibt gleich.

Die Zelle bei R−1 ist 1. Wir verschieben die rechteste belegte Zelle von R nach R+1 und lassen den Rest unverändert. An jeder Position n≤R−1 stimmen die Werte für alle t≥0 überein. Am neuen rechten Rand stehen bei R und R+1 die Werte 01. Dort können wir die erste Konstruktion anwenden.

Wegen R≥1 bleibt in beiden Fällen die Entwicklung an allen Positionen n≤0 gleich.

Warum die Änderungen rechts bleiben

Der Beweis nutzt zwei lokale Identitäten. Wir setzen E=R+t; das ist der nach rechts wandernde Rand der ursprünglichen Zeile.

Wenn u(R−1)=0 gilt, ergänzen wir zunächst nur eine Zelle bei R+2. Die beiden Entwicklungen unterscheiden sich dann genau an diesen Stellen:

t gerade:   {E+2}
t ungerade: {E, E+1, E+2}

Alle angegebenen Positionen liegen rechts von R, denn der ungerade Fall tritt erstmals bei t=1 auf. Die Identität folgt durch Induktion mit einer Prüfung der lokalen Regel am wandernden Rand. An der entscheidenden Stelle ist der mittlere Eingang der lokalen Dreiernachbarschaft in beiden Entwicklungen 1. Deshalb hängt mitte OR rechts dort nicht vom rechten Eingang ab.

Die neue äußerste Zelle hat wieder eine 0 direkt links neben sich. Wir können also zwei Positionen weiter rechts die nächste Zelle ergänzen und fortfahren. Jede endliche Ergänzung erhält denselben linken Bereich.

Der Übergang zum unendlichen Strahl nutzt die endliche Abhängigkeit der Regel. Für ein festes t und eine feste Position n wird der Wert nur von den Anfangszellen in [n−t,n+t] bestimmt. Eine hinreichend lange endliche Ergänzung stimmt dort mit der unendlichen überein. Damit gilt die Gleichheit an diesem Punkt für beliebige t und n≤R.

Beim Verschieben der äußersten Zelle im zweiten Fall lauten die Unterschiede:

t gerade:   {E, E+1}
t ungerade: {E+1}

Auch das folgt durch lokale Induktion. Die Unterschiede bleiben strikt rechts von R−1. Zusammen mit der anschließenden Ergänzung ergibt sich die allgemeine Aussage.

Was offen bleibt

Die ergänzte Startzeile enthält rechts unendlich viele Einsen. Die Konstruktion liefert daher weder eine endliche Startzeile für eine beliebig vorgegebene Mittelfolge noch eine Aussage über die spätere Periodizität der Mittelspalte beim Einzelzellstart.

Verwandte Arbeiten behandeln die Rekonstruktion in seitlicher Richtung, Diagonalstrukturen und Einschränkungen von Zeitspuren, darunter Wolframs Rekonstruktionsnotiz, Rowlands Arbeit über lokale Strukturen und Kopras Ergebnisse zu Zeitspuren. Ob diese genaue Konstruktion schon früher beschrieben wurde, habe ich nicht geklärt.

Quellen und Prüfungen

Diese Notiz verwendet den Quellenstand 85d7d83c06f692f3fa7d19af42b6c988e0f58ca0. Die allgemeine Aussage für R≥1 heißt Rule30.full_checkerboard_completion_exists in Phase20ExplicitCompletion.lean. Für das Einzelzellbeispiel mit R=0 gibt es eigene formale Beweise in Phase17InfiniteFiber.lean: Rule30.infiniteEvenRow_same_left_trace und Rule30.infiniteEvenRow_same_center.

Für diese Notiz wurden alle zehn dafür geprüften Lean-Module mit Lean 4.34.0 in einem frischen Verzeichnis neu gebaut. Der Lauf war erfolgreich. Ein KI-Agent hat außerdem das Randargument rekonstruiert und eine separate, zeitlich begrenzte Simulation ausgeführt. Die Simulation prüft endliche Fälle; die Aussage für alle Zeiten beruht auf dem Beweis und seiner Lean-Verifikation.

Aussagen & Nachweise

R30-CHECKERBOARD-COMPLETION Beweis vorgelegt

Für jede binäre Zeile u mit ihrer rechtesten belegten Zelle bei R≥1 gibt es eine Zeile v mit einem nach rechts schließlich alternierenden 1,0,1,0,…-Muster, sodass F^t(v)(n)=F^t(u)(n) für alle t≥0 und n≤0 gilt; der linke Halbstrahl von u ist beliebig.

Formale Verifikation
Im angegebenen Umfang formal verifiziert
Prüfstatus
Intern geprüft
Nachweis
Frozen source 85d7d83c06f692f3fa7d19af42b6c988e0f58ca0: proofs/phase20_explicit_checkerboard_completion.md and formal/Phase20ExplicitCompletion.lean, exact theorem Rule30.full_checkerboard_completion_exists. Internal review/math-audit.md, 2026-10-08: PASS for the stated theorem after fresh proof reconstruction and Lean rebuild. Phase20ExplicitCompletion.lean SHA-256 afaba14b19f00aa57747bf9d8c42ea03e2b7bb2ec6acf423eebf0b893a8fadaf. The supplied later data commit 7cd3e0cdebf3802942d1579a96387ef1ece92374 was context only and was not needed for this proof.
Geltungsbereich
Full binary initial rows on the integer line. For every rightmost one R≥1, there is an S≥1 and a row v with v(n)=1 iff n-S is even for n≥S, preserving every t≥0 and every n≤0. No restriction on the left tail. The R=0 lone seed is checked separately; no assertion for all rows with R=0.
Annahmen
Synchronous Rule 30 on the infinite integer line: next = left XOR (center OR right). u(R)=1, u(n)=0 for n>R, and R≥1. No left-support or initial-center-bit assumption.
Werkzeuge
Lean 4.34.0, x86_64-w64-windows-gnu, commit 293d5d0c0c3f3dded4688b3ccd6a33939ac5102b. Fresh rebuild of the ten frozen modules passed on 2026-10-08. Lean executable SHA-256 a8040e2cab341c12116ab591fed9f761816f5f6b08554f6cc1680e86dfbba0a2. Named theorem axioms: propext, Classical.choice, Quot.sound.
Prüfende Person
One independent runtime AI subagent, 2026-10-08; reconstructed argument, matched exact Lean hypotheses, rebuilt frozen dependency closure and ran a separately written bounded replay. Internal AI review only; no human, external or peer review is asserted.

R30-SINGLE-SEED-CHECKERBOARD Beweis vorgelegt

Die nur bei 0 belegte Zeile und die genau bei 0,2,4,… belegte Zeile entwickeln sich unter Rule 30 für alle t≥0 und n≤0 gleich und haben damit dieselbe Mittelfolge.

Formale Verifikation
Im angegebenen Umfang formal verifiziert
Prüfstatus
Intern geprüft
Nachweis
Frozen source 85d7d83c06f692f3fa7d19af42b6c988e0f58ca0: formal/Phase17InfiniteFiber.lean, Rule30.infiniteEvenRow_same_left_trace and Rule30.infiniteEvenRow_same_center. File SHA-256 b85bedaa8878aa67f10b5270f4d575c76eff6d60a4b0f7ff9bd6cb9c9104264c. Internal review/math-audit.md checks this R=0 case separately and includes its module in the fresh build. The independent bounded replay also checked this pair through t=128 on n=-128,...,0; that finite replay is supplementary, not the all-time proof.
Geltungsbereich
The two specified full binary rows, including all negative positions initially zero; every nonnegative time and all integer positions n≤0. This is a direct zero-penultimate completion at R=0, not an extension of the general R≥1 theorem to all R=0 rows.
Annahmen
Synchronous Rule 30 on the infinite integer line. u(n)=1 iff n=0; v(n)=1 iff n is a nonnegative even integer. In particular u(-1)=0.
Werkzeuge
Lean 4.34.0, x86_64-w64-windows-gnu, commit 293d5d0c0c3f3dded4688b3ccd6a33939ac5102b. Fresh rebuild of the ten frozen modules passed on 2026-10-08. Lean executable SHA-256 a8040e2cab341c12116ab591fed9f761816f5f6b08554f6cc1680e86dfbba0a2. Named theorem axioms: propext, Classical.choice, Quot.sound.
Prüfende Person
One independent runtime AI subagent, 2026-10-08; reconstructed argument, matched exact Lean hypotheses, rebuilt frozen dependency closure and ran a separately written bounded replay. Internal AI review only; no human, external or peer review is asserted.

R30-PRIZE-STILL-OPEN Ungeklärt

Diese Konstruktion entscheidet die schließliche Nichtperiodizität der Mittelspalte des Einzelzellstarts nicht und schließt kein vorgeschlagenes Periodenwort aus.

Formale Verifikation
Keine formale Verifikation
Prüfstatus
Intern geprüft
Nachweis
Scope of proofs/phase20_explicit_checkerboard_completion.md at frozen source 85d7d83c06f692f3fa7d19af42b6c988e0f58ca0 and internal review/math-audit.md, 2026-10-08. Equality of two initial-row traces does not decide whether the shared center trace is eventually periodic.
Geltungsbereich
The separate Rule 30 single-seed center-column prize problem.
Prüfende Person
Internal AI mathematical and editorial scope checks; no claimed resolution of the open problem.

Dateien & Reproduktion

Prüfsummen kennzeichnen die genauen Dateien. Code wird als Download bereitgestellt und von dieser Website nicht ausgeführt.

Beiträge & KI-Unterstützung

KI-Unterstützung

KI half bei Beweis, Code, Quellensuche und Übersetzungen. Der genaue Lean-Build und eine gesonderte Rekonstruktion des Randarguments stehen oben.

Quellen

  1. Stephen Wolfram — A New Kind of Science, Rule 30 reconstruction note (p. 1087)
  2. Eric Rowland — Local Nested Structure in Rule 30
  3. Johan Kopra — Rapid left expansivity (2023), Corollary 3.7 and Problem 3.10
  4. David L. Condrey — Finite Configurations Cannot Generate a Constant Trace in Rule 30 (2026)

Versionsgeschichte

VersionVeröffentlichtÄnderungshinweis
v4Publikationsangaben aktualisiert.
v3Deutsche und chinesische Übersetzungen der vorhandenen Metadaten zu Nachweisen, Geltungsbereich, Annahmen, Werkzeugen und Prüfenden ergänzt. Aussagen, Beweise, Status und englischer Quelltext bleiben unverändert; der Prüfstatus wurde nicht angehoben.
v2Status der Veröffentlichung präzisiert und englische, deutsche und chinesische Texte überarbeitet; der Status der drei Behauptungen, der Beweis und die Belege bleiben unverändert.
v1Forschungsnotiz veröffentlicht; die Priorität ist weiterhin ungeklärt.
Archivierter Wortlaut

Redaktioneller Entwurf nach drei internen KI-Textprüfungen. Der genaue allgemeine Satz für R>=1 und das separate Einzelstartzellen-Beispiel für R=0 wurden in einer unabhängigen internen KI-Mathematikprüfung mit einem erneuten Build von zehn Modulen in Lean 4.34.0 geprüft. Die Priorität in der Fachliteratur ist ungeklärt; der Entwurf wurde nicht veröffentlicht.

Diese Version zitieren

Jordi Gartner. Rule 30: andere Startzeilen, dieselbe Entwicklung auf der linken Seite. Beedbyte, v2, 2026-10-08.

https://beedbyte.tech/de/publications/rule-30-checkerboard-completion/v/2

SHA-256 — Version9d8e02cbdc49042b613f3be62824863c56dfc2d92b04492262991848e562766b

Kommentare

Diskussion zu Version 2

Noch keine Kommentare.

Kommentare zu dieser Version bleiben hier erhalten. Zur aktuellen Version kommentieren →