book18/Series.lean -- axiom report, run by the author on 2026-11-03
command: lake env lean book18/Series.lean   (repository pin: leanprover/lean4:v4.32.0, Mathlib v4.32.0)
result: no errors, no warnings, no sorryAx. The first run had one error in geom_series_converges (simpa did not unfold partialSum); fixed the same day.

'Book18Series.convergesTo_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18Series.geom_partial_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18Series.geom_series_converges' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18Series.bounded_monotone_converges' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18Series.nonneg_series_bounded_converges' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18Series.comparison_test' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18Series.control_constant_unbounded' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book18Series.control_half_geometric' depends on axioms: [propext, Classical.choice, Quot.sound]