'BlockCoercive.coercive' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockCoercive.pair_poincare' depends on axioms: [propext, Classical.choice, Quot.sound]
'CommutingFlips.sum_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'CommutingFlips.one_flip' depends on axioms: [propext, Classical.choice, Quot.sound]
'CommutingFlips.Kprod_odd' depends on axioms: [propext, Classical.choice, Quot.sound]
'CommutingFlips.flip_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
'CommutingFlips.gw_inv' depends on axioms: [propext, Classical.choice, Quot.sound]
'CommutingFlips.weighted_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'CommutingFlips.commuting_flips_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.avg_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.avg_ratio_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.szz_threshold' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.szz_to_wilson_su2' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.be_beats_dobrushin' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.be_with_tail' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.dual_coxeter_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.b0_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'FrameLemma.frame_factor' depends on axioms: [propext, Classical.choice, Quot.sound]
'FrameLemma.frame_factor_Z' depends on axioms: [propext, Classical.choice, Quot.sound]
'FrameLemma.frame_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'FrameLemma.sign_mean_le_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'FrameLemma.ratio_eq_tanh' depends on axioms: [propext, Classical.choice, Quot.sound]
'FrameLemma.jensen_flip' depends on axioms: [propext, Classical.choice, Quot.sound]
'GapFromDecay.log_convex' depends on axioms: [propext, Classical.choice, Quot.sound]
'GapFromDecay.ratio_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
'GapFromDecay.pow_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'GapFromDecay.gap_of_decay' depends on axioms: [propext, Classical.choice, Quot.sound]
'GapFromDecay.gap_of_decay_dense' depends on axioms: [propext, Classical.choice, Quot.sound]
'GapFromDecay.gap_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.ks_strong_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.nogo_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.loop_growth' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.variance_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]
'HolonomyBlind.pow_dom' depends on axioms: [propext, Classical.choice, Quot.sound]
'HolonomyBlind.neumann_dom' depends on axioms: [propext, Classical.choice, Quot.sound]
'HolonomyBlind.weighted_neumann_dom' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.ira_coarse' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.ira_rowsum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.ira_finite_entry' depends on axioms: [propext, Classical.choice, Quot.sound]
'InverseQuad.cs_psd' depends on axioms: [propext, Classical.choice, Quot.sound]
'InverseQuad.inverse_quad_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevyArea.pair_sum_signs' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevyArea.pair_corr_const' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevyArea.quad_reduce' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.flipAt_flipAt' depends on axioms: [propext, Quot.sound]
'Y6.sum_invol' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.moment_offdiag_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.swapAt_swapAt' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.moment_diag_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.cauchy_of_geometric' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.hessian_traceless' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.ope_coeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.leading_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.pair_gram_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.transfer_power_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.transfer_power_attained' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.teleport_flux_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.teleport_denominator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.sum_four_le_sq_sum_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.R4_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.R4_scale' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.gap_decay' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.gap_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.logconvex' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.telescope' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.rate_min' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.su2_twoloop_consistency' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.theta_equiv_refl' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.theta_equiv_symm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.theta_equiv_trans' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.theta_mul_congr' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.theta_const_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.mono_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.mono_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.mono_div' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.log_rpow_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.mono_tendsto_atTop' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.not_bigO_of_rate_gt' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.mono_rate_inj' depends on axioms: [propext, Classical.choice, Quot.sound]
'SchurLogDet.schur_det' depends on axioms: [propext, Classical.choice, Quot.sound]
'SchurLogDet.det_bounds_of_eigen' depends on axioms: [propext, Classical.choice, Quot.sound]
'SchurLogDet.abs_log_det_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.weight_below_rate_vanishes' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.cumulant_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.kappa_free' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.reflect_block' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.nest_block' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.return_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.eps_rare_formula' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.eps_rare_gt_13' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.hodge_sq_two_forms' depends on axioms: [propext]
'Y6.polarizations' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.nielsen_hughes' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.eps_rare_chiral_formula' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.eps_rare_chiral_gt_13' depends on axioms: [propext, Classical.choice, Quot.sound]
'SlabAverage.average_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'SlabConfine.group_average' depends on axioms: [propext, Classical.choice, Quot.sound]
'SlabConfine.factor_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'SlabConfine.tanh_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'SlabConfine.one_sheet' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.tv_le_of_ratio' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.neighbour_count' depends on axioms: [propext]
'Y6.dobrushin_wilson' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.neumann_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.hodge_two_forms_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.two_forms_split' does not depend on any axioms
'Y6.bogomolny' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.instanton_rarity' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.scale_invariant_action_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.jensen_exp' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.twist_free_energy_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.d_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.d_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.two_eq_zero'' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.sub_one_iff' depends on axioms: [propext, Quot.sound]
'TwistLocality.d_move1' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.d_move2' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.coh_refl' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.coh_symm' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.coh_trans' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.coh_step1' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.coh_step2' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.coh_col' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.coh_row' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.coh_origin' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.sheet_connect' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.local_untwist' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.flux_d_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.flux_sheet' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.sheet_not_coboundary' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.flux_gauge_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.pull_central' depends on axioms: [propext]
'TwistLocality.hol_central_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.central_shift_involutive' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwistLocality.twisted_eq_shifted' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.half_interval_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.vortex_weight_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.kappa_le_vortex' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.be_region_small_vortex' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.hess_pointwise_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.kappa_ge_vortex' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.be_entry_from_vortex' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.hankel_psd' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.no_go_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.fractional' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.photon_exp' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.ahs_dirac' does not depend on any axioms
'Y6.sym_matching' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.influence_le_width' depends on axioms: [propext, Classical.choice, Quot.sound]
'Y6.det_accounting' depends on axioms: [propext, Classical.choice, Quot.sound]
