IRF logo

Das UND-Gatter gattert nicht: Eine Korrektheitslücke in der Gewinnbedingungs-Konstruktion

IRF Technical Note Nr. 15 — ein Erratum zu Abschnitt 6 von Raumschach und Berechnungskomplexität

International Raumschach Federation  ·  IRF Technical Notes, Nr. 15  ·  2026

Abschnitt 6 des konsolidierten Papiers (Raumschach und Berechnungskomplexität) beschreibt einen UND-Gatter-/Gewinnbedingungs-Mechanismus, bei dem ein Turm V, der auf der Linie einer schachbietenden Figur sitzt, sich genau dann zurückzieht, wenn jeder von mehreren Booleschen Eingabe-Token entlang seiner Reihenlinie abgezweigt ist. Fortgesetzte Arbeit auf dem Weg zur vollständigen Zusammenstellung einer nichttrivialen Formel prüfte diesen Mechanismus erstmals gegen einen tatsächlichen Generator für legale Züge mit mehr als einem Eingabe-Token in echter Sequenz — eine Konfiguration, die kein früherer Test, einschließlich der eigenen Verifikation aus Abschnitt 6, geprüft zu haben scheint. Das Ergebnis ist eine echte Korrektheitslücke: Der Mechanismus liefert Schachmatt, sobald der einzelne, V am nächsten liegende Token abzweigt, unabhängig vom Zustand jedes weiter entfernten Tokens — das logische Gegenteil des behaupteten UND. Diese Notiz dokumentiert den Befund, führt seine Ursache auf eine Annahme über den Strahl der schachbietenden Figur zurück, die bei teilweisem Rückzug nicht zutrifft, benennt, welche anderen Konstruktionen dieses Projekts betroffen sind und welche nicht, und stellt eine verifizierte Lösung vor: Vs eigenes Gatter ist für genau einen benachbarten Token korrekt, und beliebige Boolesche Formeln lassen sich korrekt zusammensetzen, indem die gesamte Logik der Teilformeln abseits von Vs Feld berechnet und das Ergebnis in die Anwesenheit oder Abwesenheit dieses einen Tokens eingespeist wird — auf Kosten der Einzeltoken-„Dreifachfunktion“-Zusammensetzung, die dieses Projekt verfolgt hatte.

I. Zusammenfassung

Das konsolidierte Papier (Raumschach und Berechnungskomplexität, Abschnitt 6) beschreibt den UND-Gatter-/Gewinnbedingungs-Mechanismus wie folgt: Ein Turm V sitzt an dem Punkt, an dem seine eigene Reihenlinie eine zum König verlaufende Triagonallinie schneidet, mit Booleschen Eingabe-Token weiter entlang derselben Reihenlinie, von denen jeder Vs Rückzug blockiert, wenn er Falsch ist, und von der Linie abzweigt, wenn er Wahr ist; Vs Rückzug ist „genau dann legal, wenn jeder Token abgezweigt ist.“ Sobald legal, so das Papier, öffnet Vs Rückzug die Triagonallinie für ein schachbietendes Einhorn, das gleichzeitig Schach bietet und das letzte Fluchtfeld des Königs schließt.

Fortgesetzte rechnerische Arbeit auf dem Weg zur vollständigen Zusammenstellung einer nichttrivialen Formel prüfte diesen Mechanismus erstmals gegen einen tatsächlichen Generator für legale Züge mit mehr als einem Eingabe-Token in echter Sequenz — ein Fall, den die ursprüngliche Verifikation (Note Nr. 9 sowie die eigenen Tests aus Abschnitt 6 des konsolidierten Papiers) offenbar nicht geprüft hat, da alle früheren Tests nur prüften, ob V ein bestimmtes, vollständig zurückgezogenes Fluchtfeld unter einer einzigen vorab gewählten Zuweisung erreichen konnte. Diese Prüfung fand eine echte Korrektheitslücke: Der Mechanismus implementiert, wie spezifiziert, kein UND für mehr als einen Eingabe-Token. Er liefert Schachmatt, sobald irgendein einzelner Token, der V am nächsten liegt, abgezweigt ist, unabhängig vom Zustand jedes weiter entfernten Tokens. Dies ist das Gegenteil des behaupteten Verhaltens und näher an ODER als an UND.

II. Die zugrundeliegende Ursache

Die Korrektheit des Gatters hängt von einer Annahme ab, die sich als nicht zutreffend erweist: dass V sich vollständig bis zu seinem designierten Fluchtfeld zurückziehen müsse, bevor der Strahl des schachbietenden Einhorns aufgedeckt wird. Tatsächlich verläuft der Strahl des schachbietenden Einhorns speziell durch Vs Heimatfeld — den einen Punkt, an dem Vs Reihenlinie die Triagonallinie des Königs schneidet —, nicht durch das Fluchtfeld. In dem Moment, in dem V dieses eine Heimatfeld verlässt, aus jedem Grund und zu jedem Zielfeld, ist der Strahl des Einhorns frei und Abzugsschach wird geliefert. Dies wurde direkt bestätigt: Bewegt man V nur ein einziges Feld von seiner Heimatposition weg, mit einem schachbietenden Einhorn, das irgendwo weiter außen auf derselben Triagonallinie mit freier Bahn platziert ist, entsteht sofortiges Schachmatt — bevor das Einhorn selbst überhaupt einen Zug gemacht hat, und unabhängig davon, wie weit V tatsächlich gekommen ist.

Dies bringt das beabsichtigte Mehrtoken-UND zum Einsturz. Betrachten wir zwei Eingabe-Token, T1 am nächsten zu V und T2 als nächstes, beide unmittelbar benachbart ohne Lücke dazwischen (die stärkstmögliche Platzierung, direkt getestet statt angenommen). Ist x1 Wahr, zweigt T1 ab und räumt das an V angrenzende Feld. V hat nun einen legalen Zug — ein Feld, auf T1s alte Position —, unabhängig davon, ob x2 Wahr oder Falsch ist, denn ob ein Turm überhaupt irgendeinen Zug in eine Richtung machen darf, hängt nur davon ab, ob das nächstgelegene Hindernis vorhanden ist, nicht von irgendeinem weiter entfernten Hindernis auf der Linie. Dieser eine Feldzug genügt: Er räumt Vs Heimatfeld, und Schachmatt folgt unmittelbar, ganz gleich, ob T2 (das x2 darstellt) überhaupt abgezweigt ist.

Dies wurde direkt und präzise verifiziert: Mit x1 = Wahr und x2 = Falsch hat V genau einen legalen Zug (auf das von T1 geräumte Feld); die Ausführung dieses Zuges erzeugt eine Stellung, in der der König im Schach steht mit null legalen Erwiderungen — Schachmatt —, obwohl die Konjunktion x1 ∧ x2 Falsch ist. Ein Kontrollfall (x1 = Falsch, x2 = Wahr) bestätigt, dass der nächstgelegene Token allein genügt, um V vollständig zu blockieren, unabhängig von weiter entfernten Token: V hat null legale Züge. Zwischen den beiden Fällen ist das Muster eindeutig: Das Ergebnis folgt ausschließlich dem Zustand des V nächstgelegenen Tokens. Jeder andere Token in der Kette ist logisch wirkungslos.

III. Warum frühere Verifikation dies nicht erfasste

Jeder Test seit der eigenen Verifikation aus Abschnitt 6 — einschließlich der nachfolgenden Zusammensetzungs-, Taktabgleichs- und Spielbaumarbeit dieses Projekts — prüfte Vs Legalität, indem gefragt wurde, ob V ein bestimmtes, vollständig zurückgezogenes Zielfeld erreichen könne, wobei Eingabe-Token direkt gemäß einer vorab gewählten Booleschen Zuweisung platziert (oder weggelassen) wurden. Diese Prüfung liefert zufällig genau dann die richtig aussehende Antwort, wenn die Geometrie V niemals einen partiellen, nicht-terminalen legalen Zug zur Alternative gibt — was auf jede getestete Konfiguration zutraf, im Allgemeinen weil Token mit Lücken angeordnet waren, oder weil nur ein einzelner Token im Spiel war, oder weil Zusammensetzungstests Wahrheitswerte direkt verdrahteten, statt eine echte Mehrtoken-Kette mit benachbarter Platzierung aufzubauen. Die Lücke tritt nur zutage, wenn (a) mehr als ein Token in echter Sequenz auf Vs Linie sitzt, (b) der nächstgelegene unabhängig von den anderen abzweigen kann, und (c) die Gewinnbedingungsprüfung genau die Frage stellt, die der Mechanismus tatsächlich beantwortet — „hat V überhaupt irgendeinen legalen Zug“ —, statt der Ersatzfrage — „kann V dieses eine bestimmte Feld erreichen.“ Kein Test vor diesem stellte (c) bei gleichzeitigem Vorliegen von (a) und (b).

IV. Was betroffen ist und was nicht

Nicht betroffen: die Konstruktionen für Korridor, Ebenenübergang und ODER-Gatter (Abschnitte 5 und 7), die nicht auf Vs Heimatfeld-/Triagonallinien-Trick angewiesen sind. Der allgemeine Befund, dass Raumschachs dritte Dimension das Leitungskreuzungshindernis des klassischen Schachs beseitigt (Abschnitt 3), ist ein strukturelles, brettgeometrisches Argument, unabhängig von diesem Gadget, und ebenfalls nicht betroffen.

Betroffen: die UND-Gatter-/Gewinnbedingungs-Konstruktion aus Abschnitt 6, insbesondere ihre Behauptung, eine beliebige Anzahl Boolescher Eingaben korrekt zu gattern. Die Konstruktion ist für genau einen Eingabe-Token korrekt (es gibt nichts, wozu ein zweiter Token wirkungslos wäre). Sie ist, wie spezifiziert, für zwei oder mehr nicht korrekt.

Ebenfalls betroffen, zur erneuten Prüfung ausstehend: die in Abschnitt 6 behauptete Skalierung auf drei Eingaben („ohne Änderung auf drei Eingaben skaliert verifiziert“) sowie die eigene Korrektheit des ODER-Gatters unter Zusammensetzung, da der Fluchtmechanismus des ODER-Gatters in der späteren Zusammensetzungsarbeit dieses Projekts direkt in dieselbe Reihenlinie wie eine UND-Gatter-Eingabe verdrahtet wurde, unter Verwendung derselben Feld-Räumungs-Logik, die nun als für sequenzielles Mehrtoken-Gattern unkorrekt erwiesen ist. Jede zusammengesetzte Struktur, die auf den Dateien test_assembly_composite.py, test_double_composite.py oder test_single_token_composition.py dieses Projekts aufbaut, erbt aus demselben Grund diese Lücke: Jede verdrahtete einen berechneten Booleschen Wert in die Anwesenheit oder Abwesenheit eines einzelnen Ersatz-Tokens auf Vs Linie — genau der Einzeltoken-Fall, den diese Notiz als korrekt zeigt —, aber keine testete zwei oder mehr unabhängig bewegliche Token auf derselben Linie in echter Sequenz, wo die Lücke tatsächlich liegt.

V. Lösung: Eine korrekte Konstruktion, mit echten Kosten

Aktualisierung, nach weiterer Arbeit hinzugefügt: Eine korrekte Lösung existiert, wenn auch begrenzter als die ursprüngliche Behauptung. Keine der beiden oben genannten Richtungen (kaskadierte paarweise Gatter, Entkopplung des schachbietenden Strahls von Vs entferntem Feld) war nötig; die Reparatur ist einfacher und kostet Umfang. Sie wurde direkt gegen den Generator bestätigt:

Die Kosten: Dies ist eine echte Reparatur der Korrektheit, nicht des ursprünglichen Anspruchs. Es ist nicht mehr zutreffend, dass eine einzelne physische Figur zugleich doppelte oder dreifache Funktion erfüllen kann — als eigener beweglicher Token einer Teilformel, als Reihenlinien-Blocker und als Figur auf dem schachbietenden Strahl, alles gleichzeitig —, wie Abschnitt 6 und die eigenen Dateien test_single_token_composition.py und test_double_composite.py dieses Projekts annahmen. Zusammensetzung erfordert nun einen expliziten, gesonderten Verdrahtungsschritt zwischen einer verifizierten Teilformel und dem einen Token, der tatsächlich für das Matt zählt. Ob ein Entwurf existiert, der Einzeltoken-Zusammensetzung ohne Verdrahtung wiederherstellt, ohne den ursprünglichen Fehler dieser Notiz erneut einzuführen, bleibt offen; nicht mehr offen ist, ob irgendeine korrekte Konstruktion für beliebige Formeln dieser Art existiert — sie existiert, und wurde geprüft.

VI. Schluss

Der UND-Gatter-/Gewinnbedingungs-Mechanismus aus Abschnitt 6 des konsolidierten Papiers gattert, wie ursprünglich spezifiziert, kein Boolesches Eingabe-Paar mit mehr als einer Eingabe korrekt: Matt wird geliefert, sobald der V nächstgelegene Token abzweigt, unabhängig von jedem anderen Token in der Kette, was näher an ODER als am behaupteten UND liegt. Dies wurde direkt gegen den Generator für legale Züge mit unmittelbar an V angrenzend platzierten Token verifiziert — die stärkste verfügbare Anordnung —, wodurch Platzierung als Ursache ausgeschlossen wird. Die Lücke war in keinem Test vor diesem sichtbar, weil jeder frühere Test, einschließlich der eigenen Zusammensetzungs- und Spielbaumarbeit dieses Projekts, eine Ersatzbedingung prüfte (kann V ein bestimmtes Feld erreichen), die nur im Einzeleingabe-Fall mit der tatsächlichen Gewinnbedingung (hat V überhaupt irgendeinen legalen Zug) zusammenfällt. Eine korrekte Reparatur wurde gefunden und für beliebige, aus ODER und UND aufgebaute Formeln verifiziert: Vs eigenes Gatter auf genau einen benachbarten Token beschränken und die gesamte Logik der Teilformeln vollständig abseits von Vs Feld berechnen, das Ergebnis einspeisend. Dies stellt die Korrektheit wieder her, auf Kosten der Einzeltoken-Dreifachfunktions-Zusammensetzung, die dieses Projekt verfolgt hatte; ob diese stärkere Eigenschaft wiederhergestellt werden kann, sofern überhaupt möglich, bleibt offen.

Literaturverzeichnis