Null-Rotierbarkeit von Spinnen mit Armen der Länge 71
Für jedes n ≥ 2 und m ≥ 0 kann jeder tatsächlich vorhandene Knoten von S(71^n,1^m) in einer graziösen Beschriftung der einzige Knoten mit Wert 0 sein; für jedes Ziel kann eine eigene Beschriftung verwendet werden.
Autoren
Beedbyte
Veröffentlicht
Version
1
Quellstand
f085233be2db924ab96fc82579a231c8e45b6992
Sei S(71^n,1^m) die Spinne mit n benannten Armen aus jeweils 71 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 71 auf jedem benannten Arm und jedes ursprüngliche Blatt, sofern es vorhanden ist. Die Beschriftung darf von v abhängen; das Ergebnis gilt für die feste Armlänge 71.
Die Konstruktion verbindet explizite graziöse Beschriftungen von Pfaden mit 143 Knoten, einem vorgeschriebenen Mittelpunkt und einer Null oder einem Maximum im benötigten Abstand, mit einer am Zentrum angeschlossenen Restbeschriftung der Spinne sowie gesonderten Konstruktionen für Zentrum, ursprüngliche Blätter und Armspitzen. Der Satz ist in Lean 4.34.0 bewiesen.
Die Pfadergebnisse von Luiz, Campos und Richter decken die vollständigen Fälle n=2 mit m=0 und m=1 ab. Für m=0 behandelt Rofa außerdem das Zentrum und die Tiefen 1, 70 und 71. Frühere Arbeiten liefern graziöse Beschriftungen und Alpha-Amalgamationsverfahren, die in der Konstruktion verwendet werden. Diese früheren Ergebnisse und Methoden werden anerkannt; die weltweite Priorität des vollständigen Satzes für k=71 bleibt ungeklärt. Dies ist kein Satz für alle ungeraden Armlängen.
Für jedes n ≥ 2, m ≥ 0 und jeden tatsächlich vorhandenen Knoten v von S(71^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.
Formale Verifikation
Im angegebenen Umfang formal verifiziert
Prüfstatus
Intern geprüft
Nachweis
Lean-4.34.0-Beweis, zusätzlich anhand einer Kopie der Quellen erneut geprüft; mathematische und Literaturprüfungen sind interne Projektbelege.
Geltungsbereich
Für alle n≥2,m≥0 jeder tatsächlich vorhandene benannte Knoten von S(71^n,1^m): Zentrum, jede Tiefe 1..71 auf jedem benannten Arm und jedes ursprüngliche Zentralblatt, falls vorhanden. Der gewählte Knoten ist in einer gegebenenfalls zielabhängigen graziösen Beschriftung die einzige Null. Der Graph hat 71n+m Kanten; die üblichen Wertebereiche für Knotenbeschriftungen und Kantengewichte gelten.
Annahmen
S(71^n,1^m) ist der endliche Spinnengraph mit n benannten Armen aus genau 71 Kanten und m ursprünglichen Einheitsblättern am Zentrum. Graziös bedeutet: bijektive Knotenbeschriftung mit 0..|E|, deren absolute Kantendifferenzen bijektiv 1..|E| ergeben. Die Beschriftung darf vom gewählten Zielknoten abhängen und hat keine weitere Null.
Werkzeuge
Lean 4.34.0; die separate Prüfung anhand kopierter Quellen erfasste 45 Module, 2.048 Theoremabschlüsse und 503 benannte Zielinstanzen. Standardmäßige Lean-Kernel-Prüfung; der Hauptsatz verwendet nur propext, Classical.choice und Quot.sound.
Prüfende Person
Nur interne mathematische und kopierte Lean-Prüfungen; keine externe oder Peer-Review.
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 Lean-Formalisierung und -Prüfung sowie den Vergleich früherer Quellen.
Beedbyte
Kommentare
Diskussion zu Version 1
Noch keine Kommentare.