audit-session032-axioms.txt
19 declarations audited · 3 standard axioms only · updated 08-24-2026
Raw #print axioms transcript
'NguyenRH1.gapCircle_threshold' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.not_isNontrivialZero_on_gapCircle' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesTerm_norm_eq_div' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sum_zeroMult_le_of_im_band' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.nine_le_log_of_16002_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.series_tail_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesFun_norm_le_split' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.half_le_log_two' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Nat.log_floor_two_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.log_three_le_two_log' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.two_pow_log_floor_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.dyadic_family_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.shell_low' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.shell_inlo' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.shell_inhi' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.shell_up' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.norm_circle_sub_abs_im_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.shell_crit' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesFun_norm_le_gapCircle' depends on axioms: [propext, Classical.choice, Quot.sound]