# padic-regulator-valuation (2026-10-09): `#print axioms` output, by module (31 modules, 360 lines). # Each module checked alone with `lake env lean`, Lean 4 v4.33.1, Mathlib 0df444a3. # Every line is a subset of [propext, Classical.choice, Quot.sound]; sorryAx 0. ## PadicRegulatorValuation.PadicHeightValuation (5) 'PadicHeight.dvd_pow_sub_one' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.fermatQuot_additive' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.norm_det_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.norm_det_div_sq_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.norm_height_div_sq_le' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation2 (6) 'PadicHeight.exists_fermatQuot' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.not_dvd_two' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.fermatQuot_sub_iff_of_sq_eq_cube' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.eval_sub_eval_dvd_sq' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.dvd_sq_pow_totient' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.fermatQuot_mul_pow_sq' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation3 (6) 'PadicHeight.exists_fermatQuot'' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.sq_dvd_one_add_pow_sub' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.sq_dvd_pow_sub_one_of_isPow' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.sq_dvd_pow_sub_one_iff_isPow' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.sq_dvd_pow_sub_one_of_sq_eq_cube' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.sq_dvd_alpha_sub_beta_of_isPow' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation4 (7) 'PadicHeight.sq_dvd_one_add_pow_sub' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.sq_dvd_one_add_mul_pow_sub_one' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.sq_dvd_one_add_sq_mul_pow_sub_one' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.fermatQuot_scale' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.fermatQuot_scale_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.dvd_det_of_col_dvd' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.pow_succ_dvd_det_of_col' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation5 (12) 'PadicHeight.pow_dvd_det_of_forall_dvd' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.pow_sub_two_dvd_det_of_offdiag' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.regulator_valuation_of_split_anomalous' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.regulator_valuation_of_split_anomalous_offdiag' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.sq_dvd_one_add_pow_sub' depends on axioms: [propext, Quot.sound] 'PadicHeight.fermatQuot_deform' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.affine_zero_unique' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.lambda_eq_zero_iff_split' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.lambda_dichotomy' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.exists_unique_lambda_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.slope_of_rho' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.regulator_valuation_of_split_anomalous_iff_split' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation6 (11) 'PadicHeight.weight_split' depends on axioms: [propext, Quot.sound] 'PadicHeight.twelve_dvd_weight' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.three_mul_sum_mul_succ' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.two_mul_sum_succ' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.sum_pole_orders' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.cusp_sum_eq_m' depends on axioms: [propext, Quot.sound] 'PadicHeight.twelve_m_eq' depends on axioms: [propext, Quot.sound] 'PadicHeight.mul_compl_le_half_mul_half' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.not_dvd_half_mul_half' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.eq_C_mul_of_dvd_of_natDegree_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.m_values' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation7 (13) 'PadicHeight.inv_one_sub_add_inv_one_sub_inv' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.nodal_root_ne_one' depends on axioms: [propext, Quot.sound] 'PadicHeight.twelve_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.first_term_residue' depends on axioms: [propext, Quot.sound] 'PadicHeight.cast_ne_zero_of_le' depends on axioms: [propext, Quot.sound] 'PadicHeight.second_term_leading_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.residues_do_not_cancel' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.two_mul_sum_Icc_id' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.six_mul_sum_Icc_sq' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.sum_cusp_split' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.twelve_mul_sum_cusp_orders' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.eq_of_le_of_sum_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.card_Icc_cusp' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation8 (11) 'PadicHeight.sq_sub_cube_dvd_of_dvd_a1' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.sq_sub_cube_dvd_of_sq_dvd_psi' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.exists_fermatQuot' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.dvd_three_mul_sub_two_mul' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.two_mul_sub_eq_neg' depends on axioms: [propext, Quot.sound] 'PadicHeight.sub_ne_zero_of_two_mul_eq_three_mul' depends on axioms: [propext, Quot.sound] 'PadicHeight.sub_eq_neg_half' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.exists_shift_dvd_a1' depends on axioms: [propext, Quot.sound] 'PadicHeight.add_val_exactly_one' depends on axioms: [propext, Quot.sound] 'PadicHeight.not_dvd_of_val_one' depends on axioms: [propext] 'PadicHeight.quadratic_value_mem_of_entries_mem' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation9 (5) 'PadicHeight.bilin_rank_one_of_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.not_dvd_of_congr_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.det_conj_diagonal' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.det_conj_diagonal_one_p' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.reg_eq_of_det_eq' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation10 (8) 'PadicHeight.bilin_eq_of_vanishing_on_hyperplane' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.bilin_zero_of_mem_radical' depends on axioms: [propext, Quot.sound] 'PadicHeight.gram_det_three_eq_zero' depends on axioms: [propext, Quot.sound] 'PadicHeight.det_two_dvd_iff' depends on axioms: [propext, Quot.sound] 'PadicHeight.pow_dvd_det_of_offdiag_block' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.fermatQuot2_add' depends on axioms: [propext] 'PadicHeight.dvd_three_mul_sub_two_mul_two' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.split_const_eq' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation11 (10) 'PadicHeight.X_pow_three_dvd_sub_trunc' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.eval_cube_dvd' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.eval_shift_of_deriv_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.sq_dvd_pow_add_sub' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.fermatQuot2_move' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.lambda2_affine' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.lambda2_const_of_slope_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.lambda2_lift_bijective' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.lambda2_unique_zero_lift' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.b_eq_slope_mul_kappa' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation12 (16) 'PadicHeight.eval_shift_first_digit' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.first_digit_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.eval_shift_depth_two' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.first_digit_ne_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.master_symm' depends on axioms: [propext, Quot.sound] 'PadicHeight.master_add_left' depends on axioms: [propext, Quot.sound] 'PadicHeight.master_smul_left' depends on axioms: [propext, Quot.sound] 'PadicHeight.master_vanish_on_ker_chi' depends on axioms: [propext, Quot.sound] 'PadicHeight.master_mem_radical' depends on axioms: [propext, Quot.sound] 'PadicHeight.master_eq_of_gam_eq_smul' depends on axioms: [propext, Quot.sound] 'PadicHeight.master_offdiag_ne_iff' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.master_diag_eq_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.master_bad_class_unique' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.det_three_layer' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.det_eq_zero_of_rank_one_block' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.det_sq_dvd_iff' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation13 (10) 'PadicHeight.eval_quartic_dvd' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.eval_shift_second_digit' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.fermatQuot_second_move' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.root_factor' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.dvd_iff_dvd_sub_root' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.unique_bad_class' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.exists_bad_class' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.second_digit_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.second_digit_criterion' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.a1_correction_cancels' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation14 (11) 'PadicHeight.dvd_iff_dvd_first' depends on axioms: [propext, Quot.sound] 'PadicHeight.sq_dvd_sub_crit' depends on axioms: [propext] 'PadicHeight.val_one_of_crit_ne' depends on axioms: [propext, Quot.sound] 'PadicHeight.sq_dvd_of_crit' depends on axioms: [propext] 'PadicHeight.trichotomy' depends on axioms: [propext, Quot.sound] 'PadicHeight.min_two_ne_of_ne_of_min_le_one' depends on axioms: [propext, Quot.sound] 'PadicHeight.min_two_eq_of_two_le' depends on axioms: [propext, Quot.sound] 'PadicHeight.min_two_ne_iff' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.exists_same_data_diff_val' depends on axioms: [propext] 'PadicHeight.scaling_shift_square' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.q2_additive' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation15 (14) 'PadicHeight.inv_pred_cube' depends on axioms: [propext, Quot.sound] 'PadicHeight.neg_inv_pred_cube' depends on axioms: [propext, Quot.sound] 'PadicHeight.q2_quotient' depends on axioms: [propext, Quot.sound] 'PadicHeight.q2_quotient_dvd' depends on axioms: [propext, Quot.sound] 'PadicHeight.sq_cube_step' depends on axioms: [propext, Quot.sound] 'PadicHeight.denominator_third_digit' depends on axioms: [propext, Quot.sound] 'PadicHeight.cube_dvd_sub_crit' depends on axioms: [propext, Quot.sound] 'PadicHeight.cube_dvd_of_crit' depends on axioms: [propext, Quot.sound] 'PadicHeight.not_cube_dvd_of_crit_ne' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.cube_dvd_iff_crit' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.quadrichotomy' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.exists_same_second_diff_third' depends on axioms: [propext] 'PadicHeight.min_three_ne_iff' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.min_three_eq_of_three_le' depends on axioms: [propext, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation16 (16) 'PadicHeight.low_terms_vanish' depends on axioms: [propext, Quot.sound] 'PadicHeight.p_mult_second_digit' depends on axioms: [propext] 'PadicHeight.w_local' depends on axioms: [propext] 'PadicHeight.inv_x_correction' depends on axioms: [propext] 'PadicHeight.w_ne_zero_iff' depends on axioms: [propext] 'PadicHeight.inv_pred_quartic' depends on axioms: [propext, Quot.sound] 'PadicHeight.neg_inv_pred_quartic' depends on axioms: [propext, Quot.sound] 'PadicHeight.denominator_fourth_digit' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.theta_eta_cancels' depends on axioms: [propext, Quot.sound] 'PadicHeight.cubic_term_vanishes' depends on axioms: [propext] 'PadicHeight.fourth_digit_reduction' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.quartic_dvd_iff_crit' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.exists_same_third_diff_fourth' depends on axioms: [propext] 'PadicHeight.min_four_ne_iff' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.min_four_eq_of_four_le' depends on axioms: [propext, Quot.sound] 'PadicHeight.quintichotomy' depends on axioms: [propext, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation17 (13) 'PadicHeight.pow_sub_pow_expand' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.exists_exact_part' depends on axioms: [propext] 'PadicHeight.unit_pow_diff_exact' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.shift_depth_exact' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.shift_depth_dvd' depends on axioms: [propext, Quot.sound] 'PadicHeight.quotient_by_p_sq' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.theta_sensitivity_exact' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.theta_digit_determined' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.three_layers_determine' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.layer_three_moves_digit_two' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.nondegeneracy_needed' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.nondegenerate_gives_exact' depends on axioms: [propext, Quot.sound] 'PadicHeight.layer_digit_correspondence' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation18 (17) 'PadicHeight.sq_valuation_one' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.psi_deriv_valuation_one' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.bracket_divisible' depends on axioms: [propext] 'PadicHeight.nd_iff_bracket' depends on axioms: [propext] 'PadicHeight.nd_of_bracket_exact' depends on axioms: [propext] 'PadicHeight.m_p_integral' depends on axioms: [propext, Quot.sound] 'PadicHeight.m_g_integral' depends on axioms: [propext, Quot.sound] 'PadicHeight.resultant_weight' depends on axioms: [propext, Quot.sound] 'PadicHeight.resultant_weight_split' depends on axioms: [propext, Quot.sound] 'PadicHeight.ne_zero_of_const_mul_pow' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.eval_ne_zero_of_isCoprime' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.nondegeneracy_summary' depends on axioms: [propext] 'PadicHeight.twentyfour_dvd_sq_sub_one' depends on axioms: [propext, Quot.sound] 'PadicHeight.resultant_weight_K' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.resultant_weight_S' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.m_K_add_m_S' depends on axioms: [propext, Quot.sound] 'PadicHeight.nd_iff_S_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation19 (14) 'PadicHeight.serre_deriv_disc_zero' depends on axioms: [propext, Quot.sound] 'PadicHeight.gauss_sum_closed' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.min_sum_closed' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.cusp_ord_total' depends on axioms: [propext, Quot.sound] 'PadicHeight.resultant_weight_dPsi' depends on axioms: [propext] 'PadicHeight.m_S_eq' depends on axioms: [propext] 'PadicHeight.weight_two_p_vanishes' depends on axioms: [propext, Quot.sound] 'PadicHeight.pow_card_self' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.cS_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.deriv_zero' does not depend on any axioms 'PadicHeight.deriv_one' does not depend on any axioms 'PadicHeight.deriv_sum' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.deriv_pow_succ' depends on axioms: [propext] 'PadicHeight.deriv_eval_chain' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation20 (12) 'PadicHeight.isogeny_A1' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.isogeny_A1_domain' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.isogeny_A2_core' depends on axioms: [propext, Quot.sound] 'PadicHeight.isogeny_A2' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.deriv_eval_of_factor' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.residue_iff' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.const_mod_p_deriv' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.lead_cancel' depends on axioms: [propext, Quot.sound] 'PadicHeight.lc_difference' depends on axioms: [propext] 'PadicHeight.deg_K_eq' depends on axioms: [propext, Quot.sound] 'PadicHeight.weight_L' depends on axioms: [propext, Quot.sound] 'PadicHeight.two_n_add_one_eq_zero' depends on axioms: [propext, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation21 (17) 'PadicHeight.D_eval_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.D2_eval_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.log_deriv_ratio' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.telescope_term' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.telescope_sum' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.residue_value' depends on axioms: [propext, Quot.sound] 'PadicHeight.residue_value_zmod' depends on axioms: [propext, Quot.sound] 'PadicHeight.sign_flip_invariance' depends on axioms: [propext, Quot.sound] 'PadicHeight.balanced_repr' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.ordq_total' depends on axioms: [propext, Quot.sound] 'PadicHeight.weight_ResK' depends on axioms: [propext] 'PadicHeight.mK_even' depends on axioms: [propext, Quot.sound] 'PadicHeight.exponent_two_nsq' depends on axioms: [propext] 'PadicHeight.exponent_case_3mod4' depends on axioms: [propext] 'PadicHeight.exponent_case_1mod4' depends on axioms: [propext, Quot.sound] 'PadicHeight.sign_exponent' depends on axioms: [propext] 'PadicHeight.eps_cases' depends on axioms: [propext, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation22 (14) 'PadicHeight.card_cases' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.two_p_forces_five' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.sq_not_dvd' depends on axioms: [propext, Quot.sound] 'PadicHeight.dvd_of_unit_mul' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.dvd_of_unit_sq_mul' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.sigma_third_coeff' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.sigma_fourth_coeff' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.padicVal_eq_zero_of_lt' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.log_term_depth_small' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.log_term_depth_five' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.log_term_depth_ne_five' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.log_term_factor' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.five_fifth_term' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeight.cp_one_line' depends on axioms: [propext, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation23 (18) 'PadicHeightStar.mu2_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightStar.mu4_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightStar.mu6_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightStar.mu6_no_b2_cube' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightStar.lambda3_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightStar.lambda_depth_mono' depends on axioms: [propext, Quot.sound] 'PadicHeightStar.lambda_depth_m2_e2' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightStar.x_form_suffices' depends on axioms: [propext, Quot.sound] 'PadicHeightStar.val_thirty' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightStar.val_three_sixty' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightStar.val_thirty_seven' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightStar.mu6_visible_at_ten' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightStar.theta_depth_j5_p5' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightStar.theta_depth_j5_p7' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightStar.log_term_j10_five' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightStar.log_term_j10_seven' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightStar.layer_depth' depends on axioms: [propext, Quot.sound] 'PadicHeightStar.data_count_linear' depends on axioms: [propext, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation24 (19) 'PadicHeightLayer.theta_rate_digit' depends on axioms: [propext, Quot.sound] 'PadicHeightLayer.ledger_rate_digit' depends on axioms: [propext, Quot.sound] 'PadicHeightLayer.gap_is_e' depends on axioms: [propext, Quot.sound] 'PadicHeightLayer.ledger_lags' depends on axioms: [propext, Quot.sound] 'PadicHeightLayer.ledger_lags_general' depends on axioms: [propext, Quot.sound] 'PadicHeightLayer.uniform_in_k' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightLayer.exact_pred_not_at' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightLayer.no_cancel' depends on axioms: [propext, Quot.sound] 'PadicHeightLayer.at_most_one_vanishes' depends on axioms: [propext, Quot.sound] 'PadicHeightLayer.layer_is_needed' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightLayer.fermat_digit' depends on axioms: [propext, Quot.sound] 'PadicHeightLayer.fermat_digits_needed' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightLayer.data_count' depends on axioms: [propext, Quot.sound] 'PadicHeightLayer.data_count_step' depends on axioms: [propext, Quot.sound] 'PadicHeightLayer.four_theta' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightLayer.four_ledger_e2' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightLayer.fifth_layer_hidden_at_four' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightLayer.fourth_digit_of_F' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightLayer.four_data_count' depends on axioms: [propext] ## PadicRegulatorValuation.PadicHeightValuation25 (18) 'PadicHeightCM.ledger_lags_any_m' depends on axioms: [propext, Quot.sound] 'PadicHeightCM.cm_lags_ten' depends on axioms: [propext, Quot.sound] 'PadicHeightCM.m1_leads_iff' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightCM.m1_leads_of_unit_c' depends on axioms: [propext, Quot.sound] 'PadicHeightCM.boundary_cancel_m1' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightCM.boundary_cancel_pow' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightCM.boundary_cancel_of_card' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightCM.boundary_p7_m3' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightCM.boundary_p7_exception' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightCM.boundary_m1_vs_m3_p7' depends on axioms: [propext, Quot.sound] 'PadicHeightCM.cm_prime_mod_three' depends on axioms: [propext, Quot.sound] 'PadicHeightCM.cm_no_anomalous_of_mod_two' depends on axioms: [propext, Quot.sound] 'PadicHeightCM.cm_seven_nineteen' depends on axioms: [propext] 'PadicHeightCM.cm_not_thirteen' depends on axioms: [propext, Quot.sound] 'PadicHeightCM.cm_ledger_invisible_before_eleventh' depends on axioms: [propext] 'PadicHeightCM.cm_no_local_invariant_before_eleventh' depends on axioms: [propext, Quot.sound] 'PadicHeightCM.layer_is_needed_cm' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightCM.cm_gap_at_k' depends on axioms: [propext, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation26 (12) 'PadicHeightLeading.leading_val_ge_rank' depends on axioms: [propext, Quot.sound] 'PadicHeightLeading.rank_le_leading_val' depends on axioms: [propext, Quot.sound] 'PadicHeightLeading.leading_val_eq_rank_of_nonsplit_rank_one' depends on axioms: [propext, Quot.sound] 'PadicHeightLeading.leading_val_gt_rank_of_split_le_one' depends on axioms: [propext, Quot.sound] 'PadicHeightLeading.leading_val_eq_rank_iff_of_normal' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightLeading.exists_two_ranks_same_leading_val' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightLeading.admissible_leading_two_of_rank_le_two' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightLeading.prime_dvd_det_two_iff' depends on axioms: [propext, Quot.sound] 'PadicHeightLeading.det_two_split_ne_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightLeading.exists_pair_eq_one' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightLeading.onto_iff_det_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicHeightLeading.onto_iff_reduced_det_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation27 (12) 'PadicDepthHeight.log_denom_ge' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicDepthHeight.height_ge_of_depth' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicDepthHeight.depth_lt_of_height_lt' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicSurjectivity.surjective_pair_iff' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicSurjectivity.surjective_of_shallow_kernel_element' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicClosureIndex.index_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicClosureIndex.index_ge_two_iff' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicClosureIndex.index_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicNullModel.det_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicNullModel.card_det_zero_of_ne' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicNullModel.card_det_zero_of_fst_eq_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicNullModel.density_det_zero' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation28 (10) 'PadicCofactor.cofactor_log_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicCofactor.cofactor_eq_one_of_slack_lt' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicCofactor.max_eq_iff' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicClosureCollapse.factor_through_chi' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicClosureCollapse.two_ne_zero_of_ne_two' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicClosureCollapse.diag_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicPairLaw.exact_of_deeper' depends on axioms: [propext, Quot.sound] 'PadicPairLaw.pair_law_j3' depends on axioms: [propext, Quot.sound] 'PadicPairLaw.pair_law_F_leads' depends on axioms: [propext, Quot.sound] 'PadicTwoRoutes.card_two_routes' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.PadicHeightValuation29 (10) 'PadicTranslateLinear.ratio_of_ker_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicTranslateLinear.vanish_of_chi_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicTranslateDigit.shift_quadratic' depends on axioms: [propext, Quot.sound] 'PadicTranslateDigit.ledger_digit' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicTranslateDigit.kappa_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicTranslateDigit.separates' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicInverseLedger.inverse_n3' depends on axioms: [propext, Quot.sound] 'PadicInverseLedger.translate_quadratic' depends on axioms: [propext] 'PadicInverseLedger.second_difference' depends on axioms: [propext, Quot.sound] 'PadicInverseLedger.counterexample_digits' depends on axioms: [propext] ## PadicRegulatorValuation.PadicHeightValuationCanonical (9) 'PadicCanonicalHeight.beta_le_remainder_of_local_bounds' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicCanonicalHeight.remainder_sub_slack' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicCanonicalHeight.canonical_ge_of_depth' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicCanonicalHeight.depth_lt_of_canonical_lt' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicCanonicalHeight.four_mul_comp_le_sq' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicCanonicalHeight.comp_le_half' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicCanonicalHeight.surjective_pair_iff'' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicCanonicalHeight.surjective_of_canonical_lt_four_log_add_beta' depends on axioms: [propext, Classical.choice, Quot.sound] 'PadicCanonicalHeight.surjective_of_naive_or_canonical' depends on axioms: [propext, Classical.choice, Quot.sound] ## PadicRegulatorValuation.AnomalousEulerFactor (4) 'AnomalousEuler.ap_of_anomalous' depends on axioms: [propext, Classical.choice, Quot.sound] 'AnomalousEuler.unit_root_identity' depends on axioms: [propext, Quot.sound] 'AnomalousEuler.sub_one_associated_p' depends on axioms: [propext, Quot.sound] 'AnomalousEuler.sub_one_associated_p_of_pred' depends on axioms: [propext, Quot.sound]