Null-Rotierbarkeit von Spinnen mit Armen der Länge 23
Für jedes n ≥ 2 und m ≥ 0 kann jeder tatsächlich vorhandene Knoten von S(23^n,1^m) in einer graziösen Beschriftung den Wert 0 erhalten; für jeden ausgewählten Knoten wird eine eigene Beschriftung verwendet.
Autoren
Beedbyte
Veröffentlicht
Version
1
Quellstand
b7546e3aac1a25e6a62c1a9eeb8794049ad093ed
Dieses Ergebnis beweist die Null-Rotierbarkeit von S(23^n,1^m) für jedes n ≥ 2 und m ≥ 0. Das Zentrum, jeder Knoten in den Tiefen 1 bis 23 auf jedem der n benannten Arme und jedes ursprüngliche Zentrumsblatt bei m > 0 können jeweils in einer graziösen Beschriftung den Wert 0 erhalten. Die Beschriftung darf vom ausgewählten Knoten abhängen; für m = 0 gibt es keine Zentrumsblätter.
Null-Rotierbarkeit fragt, ob eine graziöse Beschriftung den Wert 0 an einem beliebig gewählten Knoten platzieren kann und dabei die geforderten verschiedenen Knotenbeschriftungen und Kantendifferenzen erhält. Die Konstruktion kombiniert explizite Alpha-Pfad-Zertifikate mit einer festgelegten Mittelpunktbeschriftung mit der klassischen Alpha-Amalgamation und einer Konstruktion für den ungeraden Rest. Damit werden jeder Armname, jede Tiefe, das Zentrum und jedes tatsächlich vorhandene Blatt erfasst.
Frühere Arbeiten decken die vollständigen Pfadfälle n = 2, m = 0 und n = 2, m = 1 ab: Der erste ist das Pfadergebnis von Rosa, wie es Luiz, Campos und Richter wiedergeben; ihr Satz 14 behandelt den Pfad mit einem Zentrumsblatt. Die klassische Alpha-Amalgamation liefert ein hier verwendetes Konstruktionswerkzeug. Diese Ergebnisse bilden einschlägige frühere Fälle und Bausteine für den angegebenen Satz.
Für jede ganze Zahl n ≥ 2, jede ganze Zahl m ≥ 0 und jeden tatsächlich vorhandenen Knoten v von S(23^n,1^m) gibt es eine graziöse Beschriftung f dieses Graphen mit f(v)=0. Die Beschriftung darf von v abhängen.
Formale Verifikation
Im angegebenen Umfang formal verifiziert
Prüfstatus
Intern geprüft
Nachweis
Das root-geprüfte öffentliche feste k23-Quellpaket bei Commit b7546e3aac1a25e6a62c1a9eeb8794049ad093ed enthält den Satz GracefulBoundary.K23Full.all_vertices in source/K23Full.lean; die README des Pakets dokumentiert den Lean-4.34.0-Build und das Replay des kopierten Quelltexts.
Geltungsbereich
Für jedes n ≥ 2 und m ≥ 0 jeden tatsächlich vorhandenen benannten Knoten der endlichen Spinne S(23^n,1^m): ihr Zentrum, jeden der 23 Tiefenknoten auf jedem Arm (Fin n) und jedes ihrer m ursprünglichen Zentrumsblätter, falls vorhanden. Für jeden ausgewählten Knoten v gibt es eine möglicherweise andere graziöse Beschriftung f mit f(v)=0. Der Graph hat 23n+m Kanten; die Knoten werden mit 0..23n+m und die Kantengewichte mit 1..23n+m beschriftet.
Annahmen
S(23^n,1^m) ist die endliche Spinne mit n Armen aus jeweils genau 23 Kanten und m ursprünglichen Einheitsblättern am Zentrum. Eine graziöse Beschriftung bildet die Knoten bijektiv auf 0 bis |E| ab und erzeugt durch absolute Differenzen der Endpunktwerte eine Bijektion der Kanten auf 1 bis |E|. Jeder ausgewählte Knoten wird separat behandelt.
Werkzeuge
Lean 4.34.0; alle 27 eingefrorenen Paketmodule in Reihenfolge frisch mit -DwarningAsError=true kompiliert; Satz GracefulBoundary.K23Full.all_vertices; beim Replay des kopierten Quelltexts wurden 27 Module frisch kompiliert und 1.649 paketeigene Theoremabschlüsse ausschließlich gegen die Standardaxiome von Lean geprüft. Formale projektinterne Prüfungen.
Prüfende Person
Nur projektinterne Prüfungen; es ist keine externe Begutachtung oder Peer-Review dokumentiert.
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 Konstruktion und Beweisentwicklung, die Programmierung, die Prüfung konkreter Beschriftungszertifikate und die Prüfung der zitierten Quellen.
Beweist die Null-Rotierbarkeit jedes tatsächlich vorhandenen Knotens von S(23^n,1^m) für n ≥ 2 und m ≥ 0, mit einer eigenen graziösen Beschriftung für jeden ausgewählten Knoten.
Diese Version zitieren
Beedbyte. Null-Rotierbarkeit von Spinnen mit Armen der Länge 23. Beedbyte, v1, 2026-10-10.
Beedbyte
Kommentare
Diskussion zu Version 1
Noch keine Kommentare.