Null-Rotierbarkeit von Spinnen mit Armen der Länge 47
Für jedes n ≥ 2 und m ≥ 0 kann jeder tatsächlich vorhandene Knoten von S(47^n,1^m) der einzige Knoten mit Wert 0 in einer graziösen Beschriftung sein; für jedes Ziel kann eine eigene Beschriftung verwendet werden.
Autoren
Beedbyte
Veröffentlicht
Version
1
Quellstand
28e8174b8b1ab5a82261c4160f3674b9120f7484
Sei S(47^n,1^m) die Spinne mit n benannten Armen aus jeweils 47 Kanten und m ursprünglichen Einheitsblättern am Zentrum. Für jedes n ≥ 2, m ≥ 0 und jeden tatsächlich vorhandenen Knoten v gibt es eine graziöse Beschriftung f mit f(v)=0 und f(w)=0 genau dann, wenn w=v. Dies umfasst das Zentrum, jede Tiefe von 1 bis 47 auf jedem benannten Arm und jedes vorhandene ursprüngliche Blatt. Die Beschriftung darf von v abhängen. Das Ergebnis gilt für die feste Armlänge 47; es ist kein Satz für alle ungeraden Armlängen.
Der Beweis verbindet graziöse Beschriftungen von Pfaden mit 95 Knoten, einem vorgeschriebenen Mittelpunkt und einer Null oder einem Maximum in festgelegtem Abstand, die klassische Alpha-Amalgamation, wie sie Shan und Zhong darstellen, mit einer Restbeschriftung der Spinne sowie gesonderte Konstruktionen für Zentrum, ursprüngliche Blätter und Armspitzen. Eine Lean-4.34.0-Formalisierung und ein separates Lean-Replay des kopierten Quelltexts prüfen den Satz; dies sind projektinterne Prüfungen.
Frühere Arbeiten decken den vollständigen Pfadfall S(47^2,1^0)=P95 und den Fall mit einem Zentrumsblatt S(47^2,1^1) einschließlich aller Knoten ab. Bahls, Lake und Wertheim geben graziöse Beschriftungen für Spinnen mit gleich langen Armen ohne Zentrumsblätter an und verwenden bei einer ungeraden Armzahl eine Beschriftung mit einer Null im Zentrum. Diese Ergebnisse sind relevante Überschneidungen, formulieren für sich genommen aber nicht den vollständigen Satz für alle n,m und alle Knoten. Die historische Priorität bleibt ungeklärt.
Für jedes n ≥ 2, m ≥ 0 und jeden tatsächlich vorhandenen Knoten v von S(47^n,1^m) gibt es eine graziöse Beschriftung f mit f(v)=0 und für jeden Knoten w gilt: f(w)=0 genau dann, wenn w=v.
For all n≥2,m≥0, every actual named vertex of S(47^n,1^m), including center, every depth 1..47 on each named arm and all original center leaves when present; the selected vertex is the unique zero in a possibly target-specific graceful labeling. The graph has 47n+m edges and the standard graceful label and weight ranges.
Annahmen
S(47^n,1^m) is the finite spider with n named arms of exactly 47 edges and m original unit leaves attached to the center. Graceful means a bijection of vertices to 0..|E| whose absolute edge differences biject to 1..|E|. The labeling can depend on the selected target vertex and has no other zero.
Werkzeuge
Lean 4.34.0; 42 modules freshly compiled with -DwarningAsError=true in author freeze and separate copied-source replay; principal theorem GracefulBoundary.K47Full.all_vertices_unique_zero; internal mathematical composition check. Standard Lean kernel verification.
Prüfende Person
Internal mathematical composition audit and separate copied-source Lean replay only; no external or peer review is claimed.
Dateien & Reproduktion
Keine Dateien angehängt.
Beiträge & KI-Unterstützung
Beiträge
Jordi Gartner veröffentlicht diese Arbeit über Beedbyte.
KI-Unterstützung
Methoden: KI-Werkzeuge unterstützten die Entwicklung der Konstruktion, die Formalisierung und Prüfung des Beweises sowie den Vergleich früherer Quellen; die Lean-4.34.0-Formalisierung verifiziert den angegebenen Satz.
Beedbyte
Kommentare
Diskussion zu Version 1
Noch keine Kommentare.