Formalization / certificates
axioms of the main theorems
Verbatim copy of ~/prove2me_workspace/final/unified/logs/release_axioms.log (file time 2026-10-16 12:32 UTC). raw.
'SurfaceBlowup.main_dvr' depends on axioms: [propext, Classical.choice, Quot.sound] 'SurfaceBlowup.main_field_form' depends on axioms: [propext, Classical.choice, Quot.sound] 'SurfaceBlowup.main_field_form_ramified' depends on axioms: [propext, Classical.choice, Quot.sound] 'SurfaceBlowup.recip_main' depends on axioms: [propext, Classical.choice, Quot.sound]