Getrennte Nullplatzierungen in jeder inneren Tiefe zweier 119-Kanten-Arme
An eine gewählte Wurzel eines endlichen Graphen mit vorgegebener graziöser Beschriftung und Wurzelwert null werden zwei neue Arme mit je 119 Kanten angefügt. Jede innere Tiefe 1–118 eines Arms kann in einer eigenen Beschriftung den Wert null erhalten. Die Quellen beweisen außerdem acht angegebene Tiefen nahe den Spitzen für K=30·4^r−1, r≥1.
Autoren
Beedbyte
Veröffentlicht
Version
1
Quellstand
2861f5ff90990462308728d0958dab2ee1e8b103
Sei H ein beliebiger endlicher Graph mit Q Kanten, einer angegebenen Wurzel o und einer vorgegebenen konventionellen graziösen Beschriftung g. Die Knotenlabels sind verschiedene Werte aus 0,…,Q, die absoluten Kantendifferenzen sind genau 1,…,Q, und g(o)=0. Alle Knoten und Kanten von H bleiben erhalten. An o werden zwei getrennt benannte Arme mit je 119 Kanten angefügt; o wird mit Index 119 eines Pfades mit 238 Kanten identifiziert. Für jede Tiefe d=1,…,118 auf jedem der neuen Arme besitzt der gesamte Verbund eine konventionelle graziöse Beschriftung, die dem ausgewählten Knoten den Wert null zuweist. Jedes Ziel erhält eine eigene Beschriftung; die Knotenlabels liegen in 0,…,Q+238 und die Kantendifferenzen sind genau 1,…,Q+238.
Die vorgegebene Wurzelbeschriftung mit Wert null ist eine Voraussetzung. H muss weder zusammenhängend, azyklisch, ein Baum, alpha-beschriftet noch onto-beschriftet sein; Q=0 ist zulässig. Der Satz schreibt weder für die gemeinsame Wurzel noch für eine neue Spitze in Tiefe 119 oder alte Knoten von H den Wert null vor und liefert keine einzelne Beschriftung mit mehreren Nullzielen.
Die Quellen beweisen außerdem eine getrennte Familie nahe den Spitzen. Für jede ganze Zahl r≥1 sei K=30·4^r−1. Unter derselben Voraussetzung eines vorgegebenen graziösen H mit Wurzelwert null besitzt jede Tiefe K−8,…,K−1 auf jedem neu angefügten K-Kanten-Arm eine eigene konventionelle graziöse Beschriftung des gesamten Verbunds mit Kantenbereich 2K+Q. Diese acht Tiefen stammen aus vier Paaren von Quellsätzen. Damit werden weder alle inneren Tiefen für r>1 noch sämtliche ungeraden Armlängen bewiesen.
Der feste K119-Beweis verbindet den beibehaltenen Satz für 1–114 mit terminalen Seed-Beweisen für 115–116 und 117–118. Zertifizierte Alpha-Pfade werden durch etablierte Alpha/graziöse Knoten-Amalgamation angefügt; trägt der gewählte Pfadknoten das Maximum, wird die gesamte Beschriftung komplementiert. Ältere Quellen dieser Verklebung sind Huang–Kotzig–Rosa, wiedergegeben bei Panpa, Imnang und Wasuanankul (2025, Satz 2.5) und Shan–Zhong (2026, Lemma 1). Auch die an Endpunkten angepasste Pfadverkettung ist eine ältere Operation; sie erscheint bei Adamaszek (Lemma 1) und im Beweis von Hicks–Ollis–Schmitt (Lemma 4.5).
Zweimalige Anwendung von Shan–Zhong (Satz 2) liefert bereits die Fälle in Tiefe 1 und 2 für beliebiges H auf jedem der beiden Arme; Luiz–Campos–Richter (2017, Satz 14) behandelt einen Pfad mit einem zentralen Blatt. Diese Operationen und Spezialfälle werden als frühere Arbeit anerkannt. Ob ältere Ergebnisse den gesamten K119-Bereich 1–118 implizieren, bleibt ungeklärt; dazu gehört die vollständige Alpha/Pfad-Konstruktion von Cattell (2007). Ob die vollständige Aussage für die Tiefen 1–118 bereits bekannt war, ist ungeklärt.
Für jeden endlichen Graphen H mit Q Kanten, angegebener Wurzel o und vorgegebener konventioneller graziöser Beschriftung g mit g(o)=0 werden an o zwei benannte Arme mit je 119 Kanten angefügt. Für jede Tiefe d=1,…,118 auf jedem neuen Arm besitzt der gesamte Verbund eine eigene konventionelle graziöse Beschriftung mit Kantenbereich Q+238, die dem gewählten Knoten den Wert null zuweist. Die Beschriftung darf von Arm und Tiefe abhängen.
Formale Verifikation
Im angegebenen Umfang formal verifiziert
Prüfstatus
Intern geprüft
Nachweis
K119Through118.expanded beweist die exakte Graphaussage. Ein getrennter projektinterner Lean-4.34.0-Replay aus kopierten Quellen baute alle 68 Quellmodule neu auf und prüfte den Satz sowie seine angegebenen Grenzen. Dies ist eine projektinterne Prüfung, keine externe Begutachtung.
Geltungsbereich
Alle alten Knoten und Kanten von H bleiben erhalten. Null wird getrennt für jede innere Tiefe 1..118 eines neuen Arms vorgegeben. Weder die Spitzen bei Tiefe 119 noch die gemeinsame Wurzel, alte Zielknoten von H oder gleichzeitige Nullwerte sind umfasst. Die Knotenlabels sind injektiv in 0..Q+238; Surjektivität der Ausgabe wird nicht behauptet.
Annahmen
H ist endlich; g ist vorgegeben und injektiv in 0..Q, mit absoluten Kantendifferenzen genau 1..Q und g(o)=0. Q=0 ist zulässig. H muss weder zusammenhängend, azyklisch, ein Baum, alpha-beschriftet noch onto-beschriftet sein.
Werkzeuge
Lean 4.34.0; frische Quellkompilierung mit Warnungen als Fehler. Kernel, Compiler, Standardbibliothek und kodierte Graphdefinitionen bleiben die formale Vertrauensgrenze.
Prüfende Person
Getrennte projektinterne Prüfungen; keine externe Begutachtung behauptet.
Für jede ganze Zahl r≥1 sei K=30·4^r−1. An die Wurzel eines beliebigen endlichen Graphen H mit Q Kanten und vorgegebener konventioneller graziöser Nullbeschriftung an der Wurzel werden zwei benannte K-Kanten-Arme angefügt. Jede Tiefe K−8,…,K−1 auf jedem Arm besitzt eine eigene konventionelle graziöse Beschriftung des gesamten Verbunds, die dem Ziel den Wert null zuweist und den Kantenbereich 2K+Q hat.
Formale Verifikation
Im angegebenen Umfang formal verifiziert
Prüfstatus
Intern geprüft
Nachweis
Der Quellabschluss enthält die rooted_both-Satzpaare aus TerminalNormalized, TerminalSeed56, TerminalSeed34 und TerminalSeed12. Ihre kompilierten Satzaussagen liefern die acht Tiefen; der getrennte projektinterne Replay aus kopierten Quellen prüft den beibehaltenen Abschluss und die neuen All-r-Hauptsätze.
Geltungsbereich
Für diese Familie werden nur die acht Tiefen K−8..K−1 behauptet. Damit sind weder alle inneren Tiefen für r>1 noch sämtliche ungeraden K bewiesen. Der alte Graph H bleibt erhalten; Wurzel, Spitzen, alte H-Zielknoten und gleichzeitige Nullwerte sind nicht umfasst.
Annahmen
r≥1 und K=30·4^r−1; H ist endlich und besitzt eine vorgegebene konventionelle graziöse Beschriftung g, injektiv in 0..Q, mit Kantendifferenzen 1..Q und g(o)=0. H muss weder zusammenhängend, ein Baum, alpha-beschriftet noch onto-beschriftet sein.
Werkzeuge
Lean 4.34.0; Quellabschluss und exakte Satzköpfe bleiben im versionierten Paket erhalten.
Prüfende Person
Getrennte projektinterne Prüfungen; keine externe Begutachtung behauptet.
Dateien & Reproduktion
Keine Dateien angehängt.
Beiträge & KI-Unterstützung
Beiträge
Jordi Gartner veröffentlicht diese Arbeit über Beedbyte.
KI-Unterstützung
KI-Werkzeuge unterstützten die dokumentierte Lean-Implementierung, Reproduktions- und Prüfscripts sowie die Entwürfe der deutschen und vereinfachten chinesischen Übersetzungen.
Kommentare
Diskussion zu Version 1
Noch keine Kommentare.