PROOFDAMA · LABORATORIO PUBBLICO

Dai casi finiti a un teorema universale

ProofDama percorre ora due strade verificabili: la scala verso la soluzione 8×8 e la ricerca di un teorema sull’intera famiglia infinita 2n×3×1. Ogni caso deve essere rigenerato, certificato e verificato indipendentemente.

Stato scientifico, senza scorciatoie

La posizione iniziale 8×8 con 12 pezzi per lato non è ancora risolta. Nove benchmark pubblici hanno superato il gate ARM64/x86-64. Nella famiglia a tre righe, anche il caso tenuto fuori 10×3×1 è ora una patta verificata: 46.756.882 posizioni canoniche e 3.787.307.442 valori FID rigiocati su ARM64 e x86-64.

configurazioni storiche nello schema completo

7.245.724.519

stati nel modello storico maggiore

230,1 GB

EGDB W/L/D bloccati per hash

certificati di geometria ridotta

UNIVERSAL THEOREM TRACK · CONGETTURA PREREGISTRATA

Non un’altra scacchiera: una famiglia infinita

I risultati storici suggerivano una stabilizzazione dopo due eccezioni iniziali. Prima del nuovo calcolo abbiamo congelato congettura e falsificatori; 8×3×1 ha poi confermato la previsione senza modificarli. Codex viene usato non solo per risolvere istanze, ma per estrarre l’invariante che potrebbe chiudere una prova induttiva.

Per ogni n ≥ 3: WLD(2n×3×1) = patta

Certificati ARM64/x86-64: 2×3×1 = Bianco, 4×3×1 = Nero, 6×3×1 = patta, 8×3×1 = patta e 10×3×1 = patta. La previsione preregistrata ha superato due larghezze prospettiche.

La dualità dello spazio che si muoveLa rappresentazione vacancy-first è equivalente al motore canonico su 41.701.405 stati e 122.287.690 transizioni. Il primo ciclo CEGAR ha esaminato 164.922.712 cancellazioni e 30.694.340 coppie. Anche la macro-relazione a due semimosse elimina le radici, pur conservando 4.084.852 coppie per il Bianco e 3.795.042 per il Nero, senza contraddizioni W/L/D.

I controesempi respingono relazioni rigide, controller statici e una neutralità troppo forte del dispositivo di bordo; non respingono la congettura delle patte. È invece dimostrata una ricorsione esatta della posizione iniziale T(n) verso T(n−1) più un dispositivo locale. Manca ancora la chiusura del protocollo raggiungibile: nessun teorema universale è dichiarato.

Segui la storia della dimostrazione →Apri la preregistrazione ↗Leggi la dualità dello spazio ↗Apri il rapporto di equivalenza ↗Apri le misure del quoziente ↗Apri il controesempio di chiusura ↗Apri l’audit a lunghezza variabile ↗

INDEPENDENT_REPLAY

Gradino certificato: 2×3×1 = vince il Bianco

Il motore canonico ha rigenerato l’intero grafo raggiungibile senza interrogare il database storico. Il verificatore separato ha ricostruito ogni mossa e respinto quattro mutazioni avversarie.

✓ certificato verificato

nodi certificati

transizioni rigiocate

corruzioni respinte

architetture concordi

Hash identici su M4 arm64 e Hetzner x86-64

SHA-256 artefatto compresso: 088d78d8d62b13be6a50fa917bbfffbe2c9c9b169b3001f03e37c4ed697378ba
SHA-256 JSON canonico: e040b85de655a81391516bb7c639ab29afef4aa6830a1b1cb01825c01f116802
commit generatore: 0d43e1f8241f8c6fd2d383df3dbef460922fabd0

Scarica il certificato ↓Apri il manifest ↗x86-64 replay ↗

Comando di replay

cargo run --release --manifest-path solver_rust/Cargo.toml --bin proof_verify_reduced -- proofs/certificates/proofdama-2x3x1.v1.json.zst --adversarial

INDEPENDENT_REPLAY

Gradino certificato: 4×3×1 = vince il Nero

Il motore canonico ha rigenerato l’intero grafo raggiungibile senza interrogare il database storico. Il verificatore separato ha ricostruito ogni mossa e respinto quattro mutazioni avversarie.

✓ certificato verificato

1581

nodi certificati

2782

transizioni rigiocate

corruzioni respinte

architetture concordi

Hash identici su M4 arm64 e Hetzner x86-64

SHA-256 artefatto compresso: 15b61a4058e45c49bfb3836186e247d28b74578afb986767cb3bce20e2d59321
SHA-256 JSON canonico: 4b10550f9709b4a95f5977323a9e7290e1a314538411ed50cab6763108015f0f
commit generatore: 0d43e1f8241f8c6fd2d383df3dbef460922fabd0

Scarica il certificato ↓Apri il manifest ↗x86-64 replay ↗

Comando di replay

cargo run --release --manifest-path solver_rust/Cargo.toml --bin proof_verify_reduced -- proofs/certificates/proofdama-4x3x1.v1.json.zst --adversarial

INDEPENDENT_REPLAY

Gradino certificato: 6×3×1 = patta

Il motore canonico ha rigenerato l’intero grafo raggiungibile senza interrogare il database storico. Il verificatore separato ha ricostruito ogni mossa e respinto quattro mutazioni avversarie.

✓ certificato verificato

469.144

nodi certificati

1.099.413

transizioni rigiocate

corruzioni respinte

architetture concordi

Hash identici su M4 arm64 e Hetzner x86-64

SHA-256 artefatto compresso: 1f0956c9e2deb7050421bd2df457a89d3821498b67fef7a29bf96f72096d93e1
SHA-256 JSON canonico: 966f3e8e662f103d582449bf7a19964f58f728ee1825d5e2055bcdd3cfea2815
commit generatore: 0d43e1f8241f8c6fd2d383df3dbef460922fabd0

Scarica il certificato ↓Apri il manifest ↗x86-64 replay ↗

Comando di replay

cargo run --release --manifest-path solver_rust/Cargo.toml --bin proof_verify_reduced -- proofs/certificates/proofdama-6x3x1.v1.json.zst --adversarial

INDEPENDENT_REPLAY

Gradino certificato: 8×3×1 = patta

Il motore canonico ha rigenerato l’intero grafo raggiungibile senza interrogare il database storico. Il verificatore separato ha ricostruito ogni mossa e respinto quattro mutazioni avversarie.

✓ certificato verificato

41.230.678

nodi certificati

119.611.015

transizioni rigiocate

corruzioni respinte

architetture concordi

Hash identici su M4 arm64 e Hetzner x86-64

SHA-256 artefatto compresso: e90074bf09542558689626bcb857317a03eb50c698b0def1da25f5f1a61cfd58
SHA-256 JSON canonico: e90074bf09542558689626bcb857317a03eb50c698b0def1da25f5f1a61cfd58
commit generatore: 0d43e1f8241f8c6fd2d383df3dbef460922fabd0

Apri il manifest degli shard ↗Apri il manifest ↗x86-64 replay ↗ARM64 replay ↗

Comando di replay

cargo run --release --manifest-path solver_rust/Cargo.toml --bin proof_verify_reduced -- proofs/certificates/proofdama-8x3x1.v1.sharded-manifest.json --adversarial

INDEPENDENT_REPLAY

Gradino certificato: 4×4×1 = patta

Il motore canonico ha rigenerato l’intero grafo raggiungibile senza interrogare il database storico. Il verificatore separato ha ricostruito ogni mossa e respinto quattro mutazioni avversarie.

✓ certificato verificato

84.670

nodi certificati

172.496

transizioni rigiocate

corruzioni respinte

architetture concordi

Hash identici su M4 arm64 e Hetzner x86-64

SHA-256 artefatto compresso: 5997acfd0baacb1ad76b7a4b26e69f4676603580363c8d0b0908704216a5b4ae
SHA-256 JSON canonico: a755765ec87be91f0326ae9bf3a810ab4d8702b897540accae056159c79ee449
commit generatore: dd3e3d8abee3eb5b8f363b08dc1d8881c4aef143

Scarica il certificato ↓Apri il manifest ↗

Comando di replay

cargo run --release --manifest-path solver_rust/Cargo.toml --bin proof_verify_reduced -- proofs/certificates/proofdama-4x4x1.v1.json.zst --adversarial

INDEPENDENT_REPLAY

Gradino certificato: 4×6×1 = vince il Nero

Il motore canonico ha rigenerato l’intero grafo raggiungibile senza interrogare il database storico. Il verificatore separato ha ricostruito ogni mossa e respinto quattro mutazioni avversarie.

✓ certificato verificato

1.054.289

nodi certificati

2.787.382

transizioni rigiocate

corruzioni respinte

architetture concordi

Hash identici su M4 arm64 e Hetzner x86-64

SHA-256 artefatto compresso: e6302960b8b7942e38a40346a6daac52dfd757d8ba928cab6587b0dcb0c53e44
SHA-256 JSON canonico: b822b5024f85581d9c93dda222d1ed5606db97ffb53c038158178ce4d40614a5
commit generatore: b6ba3363c88d3aaf70deb0060b037945bbdf49f7

Scarica il certificato ↓Apri il manifest ↗

Comando di replay

cargo run --release --manifest-path solver_rust/Cargo.toml --bin proof_verify_reduced -- proofs/certificates/proofdama-4x6x1.v1.json.zst --adversarial

INDEPENDENT_REPLAY

Gradino certificato: 6×4×1 = patta

Il motore canonico ha rigenerato l’intero grafo raggiungibile senza interrogare il database storico. Il verificatore separato ha ricostruito ogni mossa e respinto quattro mutazioni avversarie.

✓ certificato verificato

27.598.544

nodi certificati

77.183.716

transizioni rigiocate

corruzioni respinte

architetture concordi

Hash identici su M4 arm64 e Hetzner x86-64

SHA-256 artefatto compresso: b4493562df224346cfd4564d6a8c605879a3c006cc5e6c84c80c13d64337c758
SHA-256 JSON canonico: b4493562df224346cfd4564d6a8c605879a3c006cc5e6c84c80c13d64337c758
commit generatore: 2c619fef3c540351d018f98122f9bef6b565a405

Apri il manifest degli shard ↗Apri il manifest ↗x86-64 replay ↗

Comando di replay

cargo run --release --manifest-path solver_rust/Cargo.toml --bin proof_verify_reduced -- proofs/certificates/proofdama-6x4x1.v1.sharded-manifest.json --adversarial

INDEPENDENT_REPLAY

Gradino certificato: 4×8×1 = patta

Il motore canonico ha rigenerato l’intero grafo raggiungibile senza interrogare il database storico. Il verificatore separato ha ricostruito ogni mossa e respinto quattro mutazioni avversarie.

✓ certificato verificato

4.617.877

nodi certificati

14.125.387

transizioni rigiocate

corruzioni respinte

architetture concordi

Hash identici su M4 arm64 e Hetzner x86-64

SHA-256 artefatto compresso: 14acbaa88de3a6f52729adaca1b3110c33057a62485b1b628e224faeecea0503
SHA-256 JSON canonico: 0d61ad29ab5ca9c4f07017a55588f9381894cba0ba9d09c1ae537966d65e2739
commit generatore: fc7fa02a86e3dc3d06c6267801c1cd17fd04cf58

Scarica il certificato ↓Apri il manifest ↗

Comando di replay

cargo run --release --manifest-path solver_rust/Cargo.toml --bin proof_verify_reduced -- proofs/certificates/proofdama-4x8x1.v1.json.zst --adversarial

INDEPENDENT_REPLAY

Gradino certificato: 4×6×2 = vince il Nero

Il motore canonico ha rigenerato l’intero grafo raggiungibile senza interrogare il database storico. Il verificatore separato ha ricostruito ogni mossa e respinto quattro mutazioni avversarie.

✓ certificato verificato

191.244.930

nodi certificati

519.719.086

transizioni rigiocate

corruzioni respinte

architetture concordi

Hash identici su M4 arm64 e Hetzner x86-64

SHA-256 artefatto compresso: 6ec1c63a4af5cae15980589fc40bf45e7a5924be0dcda4020cf40324d2163258
SHA-256 JSON canonico: 6ec1c63a4af5cae15980589fc40bf45e7a5924be0dcda4020cf40324d2163258
commit generatore: a6b058440fb44f665c6572e56da7946da6d92cd3

Apri il manifest degli shard ↗Apri il manifest ↗x86-64 replay ↗

Comando di replay

cargo run --release --manifest-path solver_rust/Cargo.toml --bin proof_verify_reduced -- proofs/certificates/proofdama-4x6x2.v1.sharded-manifest.json --adversarial

I benchmark-ancora selezionati

Apri lo schema storico completo →

Scacchiera	Pezzi/lato	Risultato	Stati modello / prova	Evidenza
2x3x1	1	vince il Bianco	2 modello storico 2 ProofDama FID	certificato verificato
4x3x1	2	vince il Nero	123 modello storico 1581 ProofDama FID	certificato verificato
6x3x1	3	patta	11.576 modello storico 469.144 ProofDama FID	certificato verificato
8x3x1	4	patta	816.565 modello storico 41.230.678 ProofDama FID	certificato verificato
4x4x1	2	patta	2836 modello storico 84.670 ProofDama FID	certificato verificato
4x6x1	2	vince il Nero	26.404 modello storico 1.054.289 ProofDama FID	certificato verificato
6x4x1	3	patta	616.526 modello storico 27.598.544 ProofDama FID	certificato verificato
4x8x1	2	patta	101.023 modello storico 4.617.877 ProofDama FID	certificato verificato
6x6x1	3	patta	15.418.942 modello storico	retrogrado storico
4x6x2	4	vince il Nero	4.167.753 modello storico 191.244.930 ProofDama FID	certificato verificato
8x5x1	4	patta	1.131.369.960 modello storico	retrogrado storico
8x6x1	4	patta	7.245.724.519 modello storico	retrogrado storico
6x9x1	3	patta	263.390.069 modello storico	retrogrado storico
8x8x3	12	sconosciuto	— modello storico	obiettivo

Dalla misura al teorema

1 · Regole canoniche

Un solo motore FID per mosse, prese, promozioni e stato di patta.

2 · Enumerazione

Retrogrado per basi finali e df-pn graph-aware per le obbligazioni del medio gioco.

3 · Certificato

Il worker produce un artefatto versionato, con dipendenze e hash dei dati.

4 · Verifica indipendente

Un verificatore separato rigioca ogni obbligazione e rifiuta prove incomplete.

Perché due conteggi possono differire?

Le vecchie pagine di gioco riportavano talvolta i record della base usata dal player, mentre lo schema storico riportava gli stati del modello retrogrado dichiarato. Il catalogo ora conserva entrambi i campi e non li presenta più come la stessa misura.

Prossimo traguardo verificabile

Sul percorso universale non verranno costruiti altri enormi grafi per larghezze crescenti. Il prossimo gate è un controllore ricorsivo limitato all’invariante raggiungibile dalla radice, verificato localmente contro prese obbligatorie e FID. Dovrà sollevare entrambe le strategie non perdenti da T(n) a T(n+1), oppure produrre un controesempio preciso.