DIARIO DI UNA DIMOSTRAZIONE · 2n×3×1
ProofDama non sta semplicemente provando scacchiere sempre più grandi. Sta trasformando risultati finiti in una possibile prova per un’intera famiglia infinita, conservando anche gli esperimenti falliti come controesempi verificabili.
La congettura è confermata da tre casi consecutivi certificati — 6×3×1, 8×3×1 e 10×3×1 sono patte — e possiede ora un lemma ricorsivo esatto. Manca ancora la chiusura induttiva che trasformi questi fatti in un teorema per ogni n ≥ 3.
Congettura preregistrata
Per ogni n ≥ 3: WLD(2n×3×1) = patta
Ogni fase è classificata, non reinterpretata a posteriori.
Il motore canonico include prese obbligatorie e loro priorità, promozione, pezzi catturati che restano temporaneamente bloccanti e il contatore di patta FID. Congettura, casi eccezionali e criteri di falsificazione sono stati fissati prima del test prospettico.
Una previsione modificata dopo il calcolo non è una previsione.
2×3×1 e 4×3×1 sono le eccezioni iniziali. 6×3×1, 8×3×1 e il caso tenuto fuori 10×3×1 risultano patte. Per 10×3 il verificatore ha rigenerato 46.756.882 posizioni canoniche, 144.871.268 archi e 3.787.307.442 valori FID su ARM64 e x86-64.
Molti casi concordi sono evidenza forte, ma non sono ancora una prova universale.
La rappresentazione vacancy-first descrive la partita attraverso le caselle libere, senza perdere colore, tipo dei pezzi, turno, promozione, ostacoli temporanei o stato FID. È stata confrontata esaustivamente con il motore canonico sui casi certificati.
La dualità rende visibile la frontiera che deve restare invariata quando si aggiungono due colonne.
Inserzioni neutre, relazioni a raggio fisso, macro-mosse a due semimosse, controller geometrici statici e diverse proiezioni finite non chiudono la radice. Ogni fallimento conserva il primo controesempio e restringe la classe della relazione successiva.
Un esperimento negativo certificato impedisce di pubblicare una dimostrazione elegante ma falsa.
Dopo la mossa legale di bordo del Bianco, T(n) contiene esattamente una copia di T(n−1) con il Nero al tratto, più il dispositivo locale «pedina nera, pedina bianca, spazio». Il nuovo tentativo di intrusione ha una sola risposta legale: una presa obbligatoria che promuove e termina la sequenza.
La larghezza non deve più essere enumerata: può diventare profondità ricorsiva.
Occorre mostrare che il protocollo ricorsivo raggiungibile dalla radice offre a entrambi i colori una strategia non perdente, per ogni profondità, rispettando priorità delle prese e contatore FID. La neutralità del dispositivo per ogni possibile posizione è falsa; basta e serve la proprietà più stretta lungo l’invariante raggiungibile.
Il teorema nascerà dalla chiusura dell’invariante, non da un altro grande database.
IL PUNTO DI SVOLTA
Prima: risolvere T(n), poi costruire e risolvere T(n+1). Il costo cresce con l’intero grafo.
Ora: verificare una volta tutte le transizioni locali del dispositivo di bordo e dimostrare che la strategia per T(n) viene sollevata a T(n+1).
Codex orchestra il ciclo congettura → generatore → controesempio → raffinamento → verificatore. Non decide che una proposizione è vera: produce codice, test, artefatti e spiegazioni che rendono ogni passaggio controllabile e ripetibile.
PIANO DI CHIUSURA A COSTO CONTROLLATO
Nessun’altra enumerazione larga. Il solo obiettivo è il sollevamento induttivo delle due strategie non perdenti dal caso n al caso n+1.
Lo stato simbolico contiene fase del dispositivo, priorità di cattura, classe FID e una pila di moduli dormienti; non contiene l’intera scacchiera.
Il motore canonico enumera tutte le configurazioni della finestra di frontiera. Ogni transizione deve rientrare nell’invariante, diminuire una misura ben fondata oppure produrre un controesempio.
Il verificatore ricalcola le mosse senza fidarsi degli ID prodotti dal sintetizzatore. Il risultato è un piccolo certificato locale, economico da rigiocare su ARM64 e x86-64.
Caso base certificato T(3). Passo induttivo per entrambi i colori. Lemma di terminazione FID. Solo dopo questi tre elementi la pagina potrà dire “teorema”.
Disciplina proposta: cicli brevi con un’unica ipotesi, test automatico locale e arresto immediato al primo controesempio. I token servono per formulare e revisionare lemmi; il Mac esegue le enumerazioni finite. Niente monitoraggi conversazionali continui e niente nuovi grafi da centinaia di milioni di stati.
Codice, rapporti deterministici e falsificatori sono versionati. Il commit di riferimento preserva anche i tentativi falliti, perché fanno parte della storia scientifica.