Lean 4.33.1
Dependencies: Mathlib 4.33.1 (see bundled lake-manifest.json)
File: Richardson.lean
SHA-256: 3e8b3f69da0388a88556a48ff400a5a99fb78f9099e6021bc85b70c5be61c01a
Result: passed

'PaperToLean.Richardson.step_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Richardson.extrapolate_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Richardson.extrapolate_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Richardson.geometric_response' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Richardson.response_vanishes' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Richardson.constant_preserved' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Richardson.finite_spectrum_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Richardson.grid_power' depends on axioms: [propext, Quot.sound]
'PaperToLean.Richardson.polynomial_grid_exact' depends on axioms: [propext, Classical.choice, Quot.sound]