An einen beliebigen endlichen Graphen H mit konventionell graziöser Beschriftung und gewählter Wurzel mit Label 0 werden zwei benannte Arme mit K=23+24t Kanten angesetzt, wobei t≥1 gilt. Auf jedem neuen Arm kann eine eigene konventionell graziöse Beschriftung die Null in Tiefe 20+22t oder 21+22t platzieren.
Autoren
Beedbyte
Forschungsstand
Abgeschlossen
Veröffentlicht
Version
1
Quellstand
a8125ba821be4b89867d379501a81ebf95445cf2
Sei H ein beliebiger endlicher indizierter Graph mit Q Kanten und einer konventionell graziösen Beschriftung g: Die Knotenlabels sind verschiedene Elemente von 0,…,Q, und die Kantendifferenzen sind genau 1,…,Q. Wähle eine tatsächlich vorhandene Wurzel r mit g(r)=0. Füge an r zwei getrennt benannte Wege mit jeweils K=23+24t Kanten an, identifiziere jeweils ihren Anfangsknoten mit r und erhalte alle Knoten und Kanten von H. Für jeden neuen Arm und jeweils getrennt für die Tiefen d₀=20+22t und d₁=21+22t, gemessen von r, besitzt der angesetzte Graph eine konventionell graziöse Beschriftung, die dem ausgewählten Knoten den Wert 0 zuweist. Dies sind vier getrennte Existenzaussagen; die Beschriftung darf von Arm und Tiefe abhängen. Für H werden weder Baumstruktur, Zusammenhang, Alpha-Beschriftung noch eine vollständige Belegung der Knotenlabels vorausgesetzt. Ist g nicht surjektiv auf 0,…,Q, bleibt die Ausgabe konventionell graziös, muss aber nicht jeden Wert ihres gesamten Knotenlabelbereichs verwenden. Für keinen alten Knoten von H, keine neue Spitze und keine andere Tiefe wird eine Null zugesichert.
Die Konstruktion verwendet einen q24-Alpha-beschrifteten Weg mit 2K Kanten und seinem Mittelpunkt an der Alpha-Grenze. Die ausgewählten Positionen tragen die benötigte Null beziehungsweise das Maximum; Umkehrung des Weges behandelt den gegenüberliegenden Arm. Beim Ansetzen werden die hohen Weglabels um Q verschoben und die Labels von H um K−1. So liegen die Weggewichte in Q+1,…,Q+2K und die Restgewichte in 1,…,Q. Eine Komplementierung der gesamten Beschriftung macht aus dem Maximum am Ziel eine Null und erhält die Kantendifferenzen. Alpha/graziöse Amalgamation und die Verschiebung des oberen Labelbands sind etablierte Verfahren; Barrientos (2022) beschreibt diese Überschneidung auf der Ebene der Operation. Der geprüfte Vergleich klärt nicht, ob frühere Arbeiten genau die vier vorgegebenen Positionen abdecken.
Der Lean-4.34.0-Autorenbeweis, eine getrennte mathematische Prüfung und eine separate Lean-Wiedergabe aus kopierten Quellen wurden als projektinterne Prüfungen erfolgreich abgeschlossen; sie sind keine externe wissenschaftliche Begutachtung. Die weltweite Priorität ist ungeklärt.
Für jedes t≥1 seien K=23+24t, d₀=20+22t und d₁=21+22t. Für jeden endlichen indizierten Graphen H mit Q Kanten und einer konventionell graziösen Beschriftung g:V(H)→{0,…,Q} sowie jeden tatsächlich vorhandenen Knoten r mit g(r)=0 entstehe X durch das Ansetzen zweier getrennt benannter Wege mit jeweils K Kanten an r, wobei H erhalten bleibt. Für jede Seite s∈{links,rechts} und jede Tiefe d∈{d₀,d₁} besitzt X eine konventionell graziöse Beschriftung f mit f(v(s,d))=0. Jede Kombination aus Seite und Tiefe ist eine getrennte Existenzaussage; die vier Beschriftungen dürfen verschieden sein.
Formale Verifikation
Im angegebenen Umfang formal verifiziert
Prüfstatus
Intern geprüft
Nachweis
Lean-Autorenbeweis, getrennte mathematische Prüfung und Lean-Wiedergabe aus kopierten Quellen erfolgreich; dies sind projektinterne Prüfungen.
Geltungsbereich
Für jedes t≥1 seien K=23+24t und d₀=20+22t, d₁=21+22t. Für jeden endlichen indizierten Graphen H mit Q Kanten und einer konventionell graziösen Beschriftung g:V(H)→{0,…,Q} wähle einen tatsächlich vorhandenen Knoten r mit g(r)=0 und füge dort zwei getrennt benannte Wege mit je K Kanten an; H bleibt erhalten. Für jede der beiden Seiten und jede angegebene Tiefe weist eine konventionell graziöse Beschriftung des angesetzten Graphen diesem Knoten die Null zu. Die vier Fälle sind getrennte Existenzaussagen; die Beschriftung darf variieren.
Annahmen
Konventionell graziös bedeutet: eine injektive Knotenbeschriftung mit Werten in 0..|E|, deren Kantendifferenzen genau 1..|E| sind; die Knotenlabels müssen das Intervall nicht vollständig belegen. H ist endlich und indiziert; die gewählte tatsächlich vorhandene Wurzel r trägt Label null. Die beiden neuen Arme sind verschiedene Wege mit jeweils K Kanten; alle alten Knoten und Kanten von H bleiben erhalten.
Werkzeuge
Lean 4.34.0; Autorenbeweis und separate Wiedergabe aus kopierten Quellen erfolgreich.
Prüfende Person
Projektinterne Prüfungen; eine externe Begutachtung oder Peer-Review wird nicht 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 Beweisentwicklung und Lean-/Prüfcode, den gezielten Vergleich früherer Verklebungsliteratur sowie Übersetzungsentwürfe.
Kommentare
Diskussion zu Version 1
Noch keine Kommentare.
Kommentare zu dieser Version bleiben hier erhalten. Zur aktuellen Version kommentieren →