axioms of the main theorems

Verbatim copy of ~/prove2me_workspace/final/unified/logs/release_axioms.log (file time 2026-10-17 05:51 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]
'SurfaceBlowup.main_dvr_cluster' depends on axioms: [propext, Classical.choice, Quot.sound]
'SurfaceBlowup.cluster_formula_regular' depends on axioms: [propext, Classical.choice, Quot.sound]
'SurfaceBlowup.recip_cluster' depends on axioms: [propext, Classical.choice, Quot.sound]
'SurfaceBlowup.clusterDensity_eq_etale' depends on axioms: [propext, Classical.choice, Quot.sound]
'SurfaceBlowup.binary_nonEtale_null' depends on axioms: [propext, Classical.choice, Quot.sound]
'SurfaceBlowup.monicDensity_eq_etale' depends on axioms: [propext, Classical.choice, Quot.sound]
'SurfaceBlowup.projectiveDensity_eq_etale' depends on axioms: [propext, Classical.choice, Quot.sound]
'SurfaceBlowup.main_dvr_etale' depends on axioms: [propext, Classical.choice, Quot.sound]