# principia-ym-weak-uv-chain-2026-10-30: `#print axioms` output of the 64 files, checked 2026-10-30 with `lake env lean` (rc=0 for every file, no sorry). All lines are subsets of propext / Classical.choice / Quot.sound; `choice` is `Classical.choice` (printed under `open Classical`).

## ActivityFixedInterval.lean
'ActivityFixedInterval.fixed_interval' depends on axioms: [propext, Classical.choice, Quot.sound]

## AnalyticFloor.lean
'AnalyticFloor.small_field_angle_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'AnalyticFloor.floor_necessary' depends on axioms: [propext, Classical.choice, Quot.sound]
'AnalyticFloor.floor_antitone' depends on axioms: [propext, Classical.choice, Quot.sound]

## BackgroundConstants.lean
'CThetaReadings.hessian_reading_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.hessian_reading_theta_max' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.coefficient_reading_04' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.coefficient_reading_068' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.minimizer_lipschitz' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.K_bg_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.K_bg_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'BackgroundConstants.background_lipschitz' depends on axioms: [propext, Classical.choice, Quot.sound]
'BackgroundConstants.background_lipschitz_numbers' depends on axioms: [propext, Classical.choice, Quot.sound]

## BlockBoundaryCount.lean
'WeightRecursion.weight_step' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.weight_step_plain' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.image_card_boundary' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.image_card_boundary_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.weight_step_sets' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.contraction_of_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.all_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.stationary_schedule' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.stationary_boundary_coeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.stationary_all_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.boundary_coeff_decreases' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.no_schedule_of_delta_ge_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.gap_le_volume_coeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.all_steps_supply' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.stationary_schedule_supply' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.coarse_boundary_le_deg' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.pair_inner' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.pair_volume' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.pair_mix' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.nn_total' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.star_total' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.nn_L2' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.nn_L4' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.star_L2' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.star_L4' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.gamma_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.no_stationary' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.four_cases_pq' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.supply_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.supply_achieved' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.volume_needed' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.per_block_reading_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.supply_nn_L2' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.supply_nn_L4' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.supply_star_L2' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.supply_star_L4' depends on axioms: [propext, Classical.choice, Quot.sound]

## BlockGaussianStep.lean
'BlockGaussianStep.kp_sum_le_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockGaussianStep.completing_square' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockGaussianStep.block_psd_iff_schur' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockGaussianStep.schur_le_restricted' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockGaussianStep.core_posDef' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockGaussianStep.core_quadratic_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockGaussianStep.coupling_step_iff_ratio' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockGaussianStep.ratio_window_iff_quadratic' depends on axioms: [propext, Classical.choice, Quot.sound]

## BoundaryRegulator.lean
'BoundaryRegulator.image_card_boundary' depends on axioms: [propext, Classical.choice, Quot.sound]
'BoundaryRegulator.image_card_boundary_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'BoundaryRegulator.size_condition_boundary' depends on axioms: [propext, Classical.choice, Quot.sound]

## BoxConnectivity.lean
'BoxConnectivity.dist_sum_step' depends on axioms: [propext, Classical.choice, Quot.sound]
'BoxConnectivity.step_inBox' depends on axioms: [propext, Classical.choice, Quot.sound]
'BoxConnectivity.step_edge' depends on axioms: [propext, Classical.choice, Quot.sound]
'BoxConnectivity.exists_boundary_edge' depends on axioms: [propext, Classical.choice, Quot.sound]
'BoxConnectivity.block_is_box' depends on axioms: [propext, Classical.choice, Quot.sound]

## BoxFiberSiteSum.lean
'BoxFiberSiteSum.fiber_swap' depends on axioms: [propext, Classical.choice, Quot.sound]
'BoxFiberSiteSum.box_site_le_fiber' depends on axioms: [propext, Classical.choice, Quot.sound]
'BoxFiberSiteSum.box_site_le_face_weight' depends on axioms: [propext, Classical.choice, Quot.sound]
'BoxFiberSiteSum.box_hsite_of_fiber' depends on axioms: [propext, Classical.choice, Quot.sound]

## BoxFromFace.lean
'BoxFromFace.conn_erase' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.rooted_erase' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.rooted_of_connected' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.Wg_step' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.prod_mono_of_one_le' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.Wg_le' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.point_gf_le_weighted' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.prod_by_color' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.two_color_Wg_le' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.two_color_point_sum' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.two_color_root_set_sum' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.one_add_pow_le_exp' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.fix_of_exp' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.exp_one_le' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.exp_nat_le' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.lattice_fix' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.lattice_face_total' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.lattice_two_color_kp' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.sum_le_of_injOn' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.label_sum_le' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.img_spec' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.img_mem' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.img_adj' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.enc_connected' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.decode' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.enc_eq' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.thin_disjoint' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.card_le_enc' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.weight_le_G' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.encoded_sum_le' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.enc_meets_root' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.two_color_point_gf' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.two_color_root_gf' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.encoded_kp_site' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.intersect_sum_le' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.dobrushin_cond_of_kp' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.encoded_dobrushin' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.key0' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.mem_map_tF' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.mem_map_tL' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.mem_linksOf' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.mem_facesOf' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.mem_facesOf_iff' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.adj_mem_nbFF' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.mem_nbFF' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.adjF_shift' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.fl_mem' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.lf_mem' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.ll_mem' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.blk_add' depends on axioms: [propext, Quot.sound]
'BoxFromFace.sub_blk_mem' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.off_mem' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.card_offFF' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.card_cube81' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.nbFL0_bdd' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.nbLF0_bdd' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.nbLL0_bdd' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.blk_sub_mem_cube' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.card_offc' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.box_hnb' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.box_hdeg' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.bimg_adj' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.bimg_connected' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.box_fix' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.box_kp_site' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.quad_le_pow' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.exp_two_gt' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.box_fails' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.box_holds_761' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.box_hsite' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.box_dobrushin' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.weight_le_Gc' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.encoded_sum_le_c' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.fiber_box_le' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.card_corners' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.card_boxFaces' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.card_boxLinks' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.cell_thin_sub' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.cell_def_sub' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.cell_prod_le' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.box_hz_from_face' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.epsBox_numbers' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.box_hsite_eq_face_sum' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.box_hsite_of_face_sum' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.face_to_box_dobrushin' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.card_nbFF0' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.card_nbFL0' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.card_nbLF0' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.card_nbLL0' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.card_links0' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.lattice_hnb' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.filter_disjSum_left' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.filter_disjSum_right' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.lattice_hdeg' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.lattice_hfour' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.card_boxRoot_links' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.enc_meets_boxRoot' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.box_event_bridge' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.bridge_numbers_gamma' depends on axioms: [propext, choice, Quot.sound]
'BoxFromFace.bridge_numbers_chernoff' depends on axioms: [propext, choice, Quot.sound]

## BoxTwoColorKP.lean
'BoxTwoColorKP.conn_erase' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.rooted_erase' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.rooted_of_connected' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.Wg_step' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.prod_mono_of_one_le' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.Wg_le' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.point_gf_le_weighted' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.prod_by_color' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.two_color_Wg_le' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.two_color_point_sum' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.two_color_root_set_sum' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.one_add_pow_le_exp' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.fix_of_exp' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.exp_one_le' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.exp_nat_le' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.lattice_fix' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.lattice_face_total' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.lattice_two_color_kp' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.sum_le_of_injOn' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.label_sum_le' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.img_spec' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.img_mem' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.img_adj' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.enc_connected' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.decode' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.enc_eq' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.thin_disjoint' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.card_le_enc' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.weight_le_G' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.encoded_sum_le' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.enc_meets_root' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.two_color_point_gf' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.two_color_root_gf' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.encoded_kp_site' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.intersect_sum_le' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.dobrushin_cond_of_kp' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.encoded_dobrushin' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.key0' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.mem_map_tF' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.mem_map_tL' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.mem_linksOf' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.mem_facesOf' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.mem_facesOf_iff' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.adj_mem_nbFF' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.mem_nbFF' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.adjF_shift' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.fl_mem' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.lf_mem' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.ll_mem' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.blk_add' depends on axioms: [propext, Quot.sound]
'BoxTwoColorKP.sub_blk_mem' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.off_mem' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.card_offFF' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.card_cube81' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.nbFL0_bdd' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.nbLF0_bdd' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.nbLL0_bdd' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.blk_sub_mem_cube' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.card_offc' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.box_hnb' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.box_hdeg' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.bimg_adj' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.bimg_connected' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.box_fix' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.box_kp_site' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.quad_le_pow' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.exp_two_gt' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.box_fails' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.box_holds_761' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.box_hsite' depends on axioms: [propext, choice, Quot.sound]
'BoxTwoColorKP.box_dobrushin' depends on axioms: [propext, choice, Quot.sound]

## CThetaReadings.lean
'CThetaReadings.hessian_reading_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.hessian_reading_theta_max' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.coefficient_reading_04' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.coefficient_reading_068' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.minimizer_lipschitz' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.K_bg_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.K_bg_value' depends on axioms: [propext, Classical.choice, Quot.sound]

## ChainEndToEnd.lean
'WeakUltravioletExistence.exists_bare_inverse_coupling' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_tendsto_probabilityMeasure' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'WeakUltravioletExistence.exists_common_subseq' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.limit_consistent' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.reflection_positivity_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.approx_invariance_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.closed_mass_lower_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_tendsto_on_countable' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.continuous_extension_of_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_continuous_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.invariance_of_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.quadratic_positivity_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.invariance_extends_by_density' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.tendsto_of_summable_increments' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.subseq_limit_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_block_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_observable_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_observable_full' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.activity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.hbeta_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.small_field_mass_of_rarity' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.small_field_mass_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.expectation_diff_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.split_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.gauge_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.equicontinuous_of_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.vanishing_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.vanishing_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.chain_to_hypotheses' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_kernel_unit' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.projected_remainder_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.coupling_from_unprojected' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.activity_le_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.hbeta_of_steps_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.steps_ker_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.hbeta_agrees' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_field_of_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.chain_to_hypotheses_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.chain_ker_of_chain' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.activity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.hbeta_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.small_field_mass_of_rarity' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'TwoStageSmallField.UltravioletChain.small_field_mass_invariant' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'TwoStageSmallField.UltravioletChain.expectation_diff_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.split_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.gauge_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.equicontinuous_of_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.vanishing_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.vanishing_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.chain_to_hypotheses' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.badSet_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.goodSet_eq_compl' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.block_bad_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.block_bad_le_counts' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.index_bad_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.index_good_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.small_field_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.eta_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.small_field_two_stage_box' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.rarity_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.chain_hypotheses_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.hsf_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'ChainEndToEnd.chain_end_to_end' depends on axioms: [propext, Classical.choice, Quot.sound]
'ChainEndToEnd.chain_ker_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]

## ChainEndToEndFineSupport.lean
'WeakUltravioletExistence.exists_bare_inverse_coupling' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_tendsto_probabilityMeasure' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'WeakUltravioletExistence.exists_common_subseq' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.limit_consistent' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.reflection_positivity_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.approx_invariance_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.closed_mass_lower_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_tendsto_on_countable' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.continuous_extension_of_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_continuous_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.invariance_of_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.quadratic_positivity_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.invariance_extends_by_density' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.tendsto_of_summable_increments' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.subseq_limit_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_block_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_observable_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_observable_full' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.activity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.hbeta_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.small_field_mass_of_rarity' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.small_field_mass_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.expectation_diff_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.split_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.gauge_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.equicontinuous_of_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.vanishing_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.vanishing_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.chain_to_hypotheses' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_kernel_unit' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.projected_remainder_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.coupling_from_unprojected' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.activity_le_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.hbeta_of_steps_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.steps_ker_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.hbeta_agrees' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_field_of_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.chain_to_hypotheses_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.chain_ker_of_chain' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.activity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.hbeta_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.small_field_mass_of_rarity' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'TwoStageSmallField.UltravioletChain.small_field_mass_invariant' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'TwoStageSmallField.UltravioletChain.expectation_diff_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.split_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.gauge_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.equicontinuous_of_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.vanishing_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.vanishing_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.chain_to_hypotheses' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.badSet_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.goodSet_eq_compl' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.block_bad_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.block_bad_le_counts' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.index_bad_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.index_good_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.small_field_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.eta_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.small_field_two_stage_box' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.rarity_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.chain_hypotheses_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.hsf_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'ChainEndToEnd.chain_end_to_end' depends on axioms: [propext, Classical.choice, Quot.sound]
'ChainEndToEnd.chain_ker_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'FineSupportReflection.dependsOn_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'FineSupportReflection.coarse_rp_of_fine_support' depends on axioms: [propext, Classical.choice, Quot.sound]
'FineSupportReflection.integrable_of_bdd' depends on axioms: [propext, Classical.choice, Quot.sound]
'FineSupportReflection.matrix_rp_of_fine_support' depends on axioms: [propext, Classical.choice, Quot.sound]
'FineSupportReflection.reflection_positive_of_fine' depends on axioms: [propext, Classical.choice, Quot.sound]
'FineSupportReflection.positivity_of_fine' depends on axioms: [propext, Classical.choice, Quot.sound]
'FineSupportReflection.chain_end_to_end_fine_support' depends on axioms: [propext, Classical.choice, Quot.sound]

## ChainMovingActivity.lean
'WeakUltravioletExistence.exists_bare_inverse_coupling' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_tendsto_probabilityMeasure' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'WeakUltravioletExistence.exists_common_subseq' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.limit_consistent' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.reflection_positivity_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.approx_invariance_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.closed_mass_lower_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_tendsto_on_countable' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.continuous_extension_of_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_continuous_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.invariance_of_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.quadratic_positivity_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.invariance_extends_by_density' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.tendsto_of_summable_increments' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.subseq_limit_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_block_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_observable_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_observable_full' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.activity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.hbeta_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.small_field_mass_of_rarity' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.small_field_mass_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.expectation_diff_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.split_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.gauge_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.equicontinuous_of_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.vanishing_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.vanishing_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.chain_to_hypotheses' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_kernel_unit' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.projected_remainder_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.coupling_from_unprojected' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.activity_le_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.hbeta_of_steps_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.steps_ker_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.hbeta_agrees' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_field_of_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.chain_to_hypotheses_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.chain_ker_of_chain' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.activity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.hbeta_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.small_field_mass_of_rarity' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'TwoStageSmallField.UltravioletChain.small_field_mass_invariant' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'TwoStageSmallField.UltravioletChain.expectation_diff_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.split_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.gauge_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.equicontinuous_of_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.vanishing_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.vanishing_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.chain_to_hypotheses' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.badSet_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.goodSet_eq_compl' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.block_bad_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.block_bad_le_counts' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.index_bad_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.index_good_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.small_field_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.eta_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.small_field_two_stage_box' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.rarity_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.chain_hypotheses_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.hsf_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'ChainEndToEnd.chain_end_to_end' depends on axioms: [propext, Classical.choice, Quot.sound]
'ChainEndToEnd.chain_ker_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'ChainMoving.movingD_of_moving' depends on axioms: [propext, Classical.choice, Quot.sound]
'ChainMoving.step_movingD' depends on axioms: [propext, Classical.choice, Quot.sound]
'ChainMoving.activity_le_movingD' depends on axioms: [propext, Classical.choice, Quot.sound]
'ChainMoving.hbeta_of_steps_movingD' depends on axioms: [propext, Classical.choice, Quot.sound]
'ChainMoving.growing_coefficient_threshold' depends on axioms: [propext, Classical.choice, Quot.sound]
'ChainMoving.step_moving' depends on axioms: [propext, Classical.choice, Quot.sound]
'ChainMoving.activity_le_moving' depends on axioms: [propext, Classical.choice, Quot.sound]
'ChainMoving.hbeta_of_steps_moving' depends on axioms: [propext, Classical.choice, Quot.sound]
'ChainMoving.chain_to_hypotheses_moving' depends on axioms: [propext, Classical.choice, Quot.sound]
'ChainMoving.chain_end_to_end_moving' depends on axioms: [propext, Classical.choice, Quot.sound]
'ChainMoving.fixed_interval' depends on axioms: [propext, Classical.choice, Quot.sound]
'ChainMoving.log_supply' depends on axioms: [propext, Classical.choice, Quot.sound]
'ChainMoving.moving_of_log_threshold' depends on axioms: [propext, Classical.choice, Quot.sound]

## ClassSiteSum.lean
'ClassSiteSum.site_sum_le_class_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassSiteSum.hsite_of_class_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassSiteSum.single_class_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassSiteSum.tail_le_of_ratio' depends on axioms: [propext, Classical.choice, Quot.sound]

## ClassStepRemainder.lean
'ClassStepRemainder.bounded_orbit_small' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.norm_step_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.orbit_in_small_ball' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.coupling_remainder_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.small_rem_form' depends on axioms: [propext, Classical.choice, Quot.sound]

## DifferenceContinuity.lean
'GibbsContinuity.continuous_weighted_integral' depends on axioms: [propext, Classical.choice, Quot.sound]
'GibbsContinuity.partition_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'GibbsContinuity.continuous_gibbs_expectation' depends on axioms: [propext, Classical.choice, Quot.sound]
'GibbsContinuity.continuous_difference_coupling' depends on axioms: [propext, Classical.choice, Quot.sound]

## EvenDifferenceCoupling.lean
'EvenDifferenceCoupling.c_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
'EvenDifferenceCoupling.c_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'EvenDifferenceCoupling.triangle_coefficient_blows_up' depends on axioms: [propext, Classical.choice, Quot.sound]
'EvenDifferenceCoupling.triangle_coefficient_at_tenth' depends on axioms: [propext, Classical.choice, Quot.sound]
'EvenDifferenceCoupling.even_series_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'EvenDifferenceCoupling.coupling_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
'EvenDifferenceCoupling.kernel_constant_scale' depends on axioms: [propext, Classical.choice, Quot.sound]
'EvenDifferenceCoupling.window_scale' depends on axioms: [propext, Classical.choice, Quot.sound]

## GasExpansion.lean
'GasExpansion.expand' depends on axioms: [propext, Classical.choice, Quot.sound]
'GasExpansion.prod_over_components' depends on axioms: [propext, Classical.choice, Quot.sound]
'GasExpansion.polymer_representation' depends on axioms: [propext, Classical.choice, Quot.sound]
'GasExpansion.partition_of_unity' depends on axioms: [propext, Classical.choice, Quot.sound]
'GasExpansion.weight_split' depends on axioms: [propext, Classical.choice, Quot.sound]

## GibbsContinuity.lean
'GibbsContinuity.continuous_weighted_integral' depends on axioms: [propext, Classical.choice, Quot.sound]
'GibbsContinuity.partition_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'GibbsContinuity.continuous_gibbs_expectation' depends on axioms: [propext, Classical.choice, Quot.sound]
'GibbsContinuity.continuousOn_effective_coupling' depends on axioms: [propext, Classical.choice, Quot.sound]
'GibbsContinuity.continuous_expectation_vector' depends on axioms: [propext, Classical.choice, Quot.sound]

## HessianGap.lean
'RegularityStep.abs_prod_sub_prod_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.pointwise_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.expectation_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.equicontinuous_of_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.hessian_reading_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.hessian_reading_theta_max' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.coefficient_reading_04' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.coefficient_reading_068' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.minimizer_lipschitz' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.K_bg_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
'CThetaReadings.K_bg_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.flux_one_plane' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.flux_two_planes' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.flux_three_planes' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.flux_six' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.flux_self_dual' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.flux_nonabelian' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.flux_complex' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.cov_points' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.mix06_points' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.straight_point' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.uniform_in_f1' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.f1_edges' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.gap_at_04' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.K_bg_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.equicontinuous_from_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'HessianGap.K_bg_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]

## KPToDobrushin.lean
'KPToDobrushin.intersect_sum_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'KPToDobrushin.dobrushin_cond_of_kp' depends on axioms: [propext, Classical.choice, Quot.sound]

## KernelMarginNumbers.lean
'SmallRemKernel.UltravioletChain.activity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.hbeta_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.small_field_mass_of_rarity' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.small_field_mass_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.expectation_diff_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.split_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.gauge_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.equicontinuous_of_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.vanishing_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.vanishing_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.chain_to_hypotheses' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_kernel_unit' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.projected_remainder_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.coupling_from_unprojected' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.activity_le_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.hbeta_of_steps_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.steps_ker_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.hbeta_agrees' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_field_of_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.chain_to_hypotheses_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.chain_ker_of_chain' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.half_b2_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.half_b2_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_bound_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c04_fails_beta28' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c04' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_beta28_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_c04_fform_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta28_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta54_c04' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta40_c04_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginNumbers.bRatioTwo_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginNumbers.C2_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginNumbers.margin_beta28' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginNumbers.margin_beta54' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginNumbers.steps_beta28' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginNumbers.hbeta_beta28' depends on axioms: [propext, Classical.choice, Quot.sound]

## KernelMarginStages.lean
'MarginRatioTwo.half_b2_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.half_b2_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_bound_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c04_fails_beta28' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c04' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_beta28_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_c04_fform_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta28_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta54_c04' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta40_c04_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_necessary' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_sufficient' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_beta28_fails_tau1' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_beta28_fails_tau3' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_33_tau1_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_33_tau3_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_33_tau3_l16_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_36_tau1_l16_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_36_tau3_l16' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_38_tau1_l16' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_38_tau3_l36_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.one_sub_lambda' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_of' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_33_tau1_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_33_tau3_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_36_tau1_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_36_tau3_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_36_tau3_l16' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_38_tau1_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_38_tau1_l16' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_38_tau3_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_38_tau3_l16' depends on axioms: [propext, Classical.choice, Quot.sound]

## KernelMarginWindow.lean
'SmallRemKernel.UltravioletChain.activity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.hbeta_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.small_field_mass_of_rarity' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.small_field_mass_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.expectation_diff_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.split_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.gauge_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.equicontinuous_of_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.vanishing_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.vanishing_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.chain_to_hypotheses' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_kernel_unit' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.projected_remainder_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.coupling_from_unprojected' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.activity_le_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.hbeta_of_steps_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.steps_ker_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.hbeta_agrees' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_field_of_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.chain_to_hypotheses_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.chain_ker_of_chain' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.half_b2_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.half_b2_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_bound_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c04_fails_beta28' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c04' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_beta28_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_c04_fform_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta28_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta54_c04' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta40_c04_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginNumbers.bRatioTwo_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginNumbers.C2_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginNumbers.margin_beta28' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginNumbers.margin_beta54' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginNumbers.steps_beta28' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginNumbers.hbeta_beta28' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginWindow.margin_beta33' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginWindow.margin_beta36' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginWindow.margin_beta38' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginWindow.c04_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginWindow.c04_ball_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginWindow.c022_ball' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginWindow.steps_window' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginWindow.hbeta_beta33' depends on axioms: [propext, Classical.choice, Quot.sound]

## KernelWindowTable.lean
'MarginRatioTwo.half_b2_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.half_b2_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_bound_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c04_fails_beta28' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c04' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_beta28_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_c04_fform_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta28_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta54_c04' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta40_c04_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_necessary' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_sufficient' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_beta28_fails_tau1' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_beta28_fails_tau3' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_33_tau1_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_33_tau3_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_33_tau3_l16_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_36_tau1_l16_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_36_tau3_l16' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_38_tau1_l16' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.window_38_tau3_l36_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.one_sub_lambda' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_of' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_33_tau1_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_33_tau3_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_36_tau1_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_36_tau3_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_36_tau3_l16' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_38_tau1_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_38_tau1_l16' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_38_tau3_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelMarginStages.margin_38_tau3_l16' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelWindowTable.window_30_tau1_l0_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelWindowTable.window_30_tau3_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelWindowTable.window_43_tau1_l36' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelWindowTable.window_54_tau1_l36' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelWindowTable.window_38_tau1_l36_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelWindowTable.window_36_tau1_l16_fails'' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelWindowTable.margin_30_tau3_l0' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelWindowTable.margin_43_tau1_l36' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelWindowTable.margin_54_tau1_l36' depends on axioms: [propext, Classical.choice, Quot.sound]
'KernelWindowTable.measured_inside' depends on axioms: [propext, Classical.choice, Quot.sound]

## LargeFieldCoupling.lean
'PolymerGasDobrushin.Z_empty' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.sum_powerset_ite_forall' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.compat_insert' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.Z_insert' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.remove_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.dobrushin' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.Z_ge_exp' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.log_Z_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'KPToDobrushin.intersect_sum_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'KPToDobrushin.dobrushin_cond_of_kp' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasKP.kp_gas_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasFreeEnergy.Z_le_prod' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasFreeEnergy.abs_log_Z_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasFreeEnergy.sum_mu_le_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldCoupling.sum_mu_le_card_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldCoupling.difference_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldCoupling.large_rem_from_gas' depends on axioms: [propext, Classical.choice, Quot.sound]

## LargeFieldStep.lean
'LargeFieldStep.rarity_chernoff' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldStep.rarity_ennreal' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldStep.healing_deterministic' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldStep.healing_markov' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldStep.kp_threshold' depends on axioms: [propext, Classical.choice, Quot.sound]

## LargeFieldSupply.lean
'LargeFieldSupply.supply_union' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldSupply.phi_antitone' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldSupply.fixed_angle_monotone' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldSupply.supply_anti_form' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldSupply.block_mgf_indep' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldSupply.block_mgf_holder' depends on axioms: [propext, Classical.choice, Quot.sound]

## LargeSetRegulator.lean
'LargeSetRegulator.full_blocks_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeSetRegulator.image_card_regulated' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeSetRegulator.image_card_fraction' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeSetRegulator.size_condition_regulated' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeSetRegulator.weight_preserving_contraction' depends on axioms: [propext, Classical.choice, Quot.sound]

## Lattice24KP.lean
'Lattice24KP.conn_erase' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.rooted_erase' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.rooted_of_connected' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.Wg_step' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.prod_mono_of_one_le' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.Wg_le' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.point_gf_le_weighted' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.prod_by_color' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.two_color_Wg_le' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.two_color_point_sum' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.two_color_root_set_sum' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.one_add_pow_le_exp' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.fix_of_exp' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.exp_one_le' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.exp_nat_le' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lattice_fix' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lattice_face_total' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lattice_two_color_kp' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.sum_le_of_injOn' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.label_sum_le' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.img_spec' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.img_mem' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.img_adj' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.enc_connected' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.decode' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.enc_eq' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.thin_disjoint' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.card_le_enc' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.weight_le_G' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.encoded_sum_le' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.enc_meets_root' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.two_color_point_gf' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.two_color_root_gf' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.encoded_kp_site' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.intersect_sum_le' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.dobrushin_cond_of_kp' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.encoded_dobrushin' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.key0' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.mem_map_tF' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.mem_map_tL' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.mem_linksOf' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.mem_facesOf' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.mem_facesOf_iff' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.adj_mem_nbFF' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.mem_nbFF' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.adjF_shift' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.fl_mem' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lf_mem' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.ll_mem' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.card_links0' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.adj24_mem' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.adj24_shift' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.mem_nbFF24' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.fl24_mem' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lf24_mem' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.ll24_mem' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.card_nbFF24_0' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.card_nbFL24_0' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.card_nbLF24_0' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.card_nbLL24_0' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lattice24_hnb' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.filter_disjSum_left' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.filter_disjSum_right' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lattice24_hdeg' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lattice_hfour' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lattice24_fix' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lattice24_face_total' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.encoded_kp_site24' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.lattice_kp_site24' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.quad_le_pow' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.exp_two_gt' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.face24_fails' depends on axioms: [propext, choice, Quot.sound]
'Lattice24KP.face24_holds_685' depends on axioms: [propext, choice, Quot.sound]

## LatticeBlockReflection.lean
'LatticeBlockReflection.continuous_retract' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.norm_retract_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.retract_of_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.retract_mul_unit' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.covariant_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.mul_star_of_star_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.covariant_path' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.covariant_average' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.covariant_retract' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.blockmap_equivariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.equivariant_comp' does not depend on any axioms
'LatticeBlockReflection.invariant_pullback' does not depend on any axioms
'LatticeBlockReflection.continuous_path_prod' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.continuous_link' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.continuous_blockmap' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.measurable_refl' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.site_reflection_positive' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.site_reflection_positive_measure' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.pushforward_reflection_positive' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.pullback_mem_positive' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.pushforward_consistent' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.pushforward_reflection_positive_prob' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeBlockReflection.pushforward_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]

## LatticeTwoColorKP.lean
'LatticeTwoColorKP.conn_erase' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.rooted_erase' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.rooted_of_connected' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.Wg_step' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.prod_mono_of_one_le' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.Wg_le' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.point_gf_le_weighted' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.prod_by_color' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.two_color_Wg_le' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.two_color_point_sum' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.two_color_root_set_sum' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.one_add_pow_le_exp' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.fix_of_exp' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.exp_one_le' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.exp_nat_le' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.lattice_fix' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.lattice_face_total' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.lattice_two_color_kp' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.sum_le_of_injOn' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.label_sum_le' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.img_spec' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.img_mem' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.img_adj' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.enc_connected' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.decode' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.enc_eq' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.thin_disjoint' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.card_le_enc' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.weight_le_G' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.encoded_sum_le' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.enc_meets_root' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.two_color_point_gf' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.two_color_root_gf' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.encoded_kp_site' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.intersect_sum_le' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.dobrushin_cond_of_kp' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.encoded_dobrushin' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.key0' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.mem_map_tF' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.mem_map_tL' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.mem_linksOf' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.mem_facesOf' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.mem_facesOf_iff' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.adj_mem_nbFF' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.mem_nbFF' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.adjF_shift' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.fl_mem' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.lf_mem' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.ll_mem' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.card_nbFF0' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.card_nbFL0' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.card_nbLF0' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.card_nbLL0' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.card_links0' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.lattice_hnb' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.filter_disjSum_left' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.filter_disjSum_right' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.lattice_hdeg' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.lattice_hfour' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.lattice_kp_site' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.lattice_dobrushin' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.blk_add' depends on axioms: [propext, Quot.sound]
'LatticeTwoColorKP.sub_blk_mem' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.box_offset' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.card_boxOff' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.box_degree' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.box_image_connected' depends on axioms: [propext, choice, Quot.sound]
'LatticeTwoColorKP.box_diag' depends on axioms: [propext, choice, Quot.sound]

## MarginNumbers.lean
'MarginNumbers.half_b_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginNumbers.margin_beta28' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginNumbers.margin_beta54' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginNumbers.lambda_window' depends on axioms: [propext, Classical.choice, Quot.sound]

## MarginRatioTwo.lean
'MarginRatioTwo.half_b2_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.half_b2_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_bound_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c04_fails_beta28' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.ball_c04' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_beta28_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_c04_fform_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta28_c022' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta54_c04' depends on axioms: [propext, Classical.choice, Quot.sound]
'MarginRatioTwo.margin2_ker_beta40_c04_fails' depends on axioms: [propext, Classical.choice, Quot.sound]

## MovingActivity.lean
'MovingActivity.activity_le_moving' depends on axioms: [propext, Classical.choice, Quot.sound]
'MovingActivity.large_rem_moving' depends on axioms: [propext, Classical.choice, Quot.sound]
'MovingActivity.log_threshold' depends on axioms: [propext, Classical.choice, Quot.sound]
'MovingActivity.constant_D_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'MovingActivity.chain_moving' depends on axioms: [propext, Classical.choice, Quot.sound]

## NontreeBackground.lean
'ClassStepRemainder.bounded_orbit_small' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.norm_step_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.orbit_in_small_ball' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.coupling_remainder_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.small_rem_form' depends on axioms: [propext, Classical.choice, Quot.sound]
'TreeGaugeLocality.treeGauge_step' depends on axioms: [propext, Quot.sound]
'TreeGaugeLocality.gfix_tree_edge' depends on axioms: [propext, Quot.sound]
'TreeGaugeLocality.invariant_depends_on_nontree' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.abs_prod_sub_prod_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.pointwise_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.expectation_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.equicontinuous_of_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.nontree_small_ball' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.quadratic_fields' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.shift_difference' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.shift_stays' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.invariant_factors' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.pointwise_from_nontree' depends on axioms: [propext, Classical.choice, Quot.sound]

## PolymerBlocking.lean
'PolymerBlocking.recount_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerBlocking.blocking_kp' depends on axioms: [propext, Classical.choice, Quot.sound]

## PolymerComponents.lean
'PolymerComponents.conn_symm' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.conn_trans' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.conn_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.mem_component' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.self_mem_component' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.component_subset' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.component_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.mem_components' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.components_disjoint' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.components_union' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.components_nonempty' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.conn_within_component' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.components_connected' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.components_nonadjacent' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.component_of_piece' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.expand' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.prod_over_components' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.polymer_representation' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.weight_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.components_satisfy_gas' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.polymer_representation_components' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.weight_split_components' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.gas_term_structure' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerComponents.component_counted' depends on axioms: [propext, Classical.choice, Quot.sound]

## PolymerGasDobrushin.lean
'PolymerGasDobrushin.Z_empty' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.sum_powerset_ite_forall' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.compat_insert' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.Z_insert' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.remove_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.dobrushin' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.Z_ge_exp' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.log_Z_ge' depends on axioms: [propext, Classical.choice, Quot.sound]

## PolymerGasFreeEnergy.lean
'PolymerGasDobrushin.Z_empty' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.sum_powerset_ite_forall' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.compat_insert' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.Z_insert' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.remove_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.dobrushin' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.Z_ge_exp' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.log_Z_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'KPToDobrushin.intersect_sum_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'KPToDobrushin.dobrushin_cond_of_kp' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasKP.kp_gas_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasFreeEnergy.Z_le_prod' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasFreeEnergy.abs_log_Z_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasFreeEnergy.sum_mu_le_card' depends on axioms: [propext, Classical.choice, Quot.sound]

## PolymerGasKP.lean
'PolymerGasDobrushin.Z_empty' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.sum_powerset_ite_forall' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.compat_insert' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.Z_insert' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.remove_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.dobrushin' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.Z_ge_exp' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasDobrushin.log_Z_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'KPToDobrushin.intersect_sum_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'KPToDobrushin.dobrushin_cond_of_kp' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGasKP.kp_gas_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]

## PolymerGeometry.lean
'PolymerGeometry.union_activity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGeometry.image_cover' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGeometry.image_size_condition' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGeometry.block_fiber_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerGeometry.contraction_iff' depends on axioms: [propext, Classical.choice, Quot.sound]

## PolymerMerge.lean
'PolymerMerge.intersect_sum_le'' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerMerge.one_side_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'PolymerMerge.merge_pairs_le' depends on axioms: [propext, Classical.choice, Quot.sound]

## PullbackOrbitLimit.lean
'PullbackOrbit.orbit_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound]
'PullbackOrbit.orbit_rate' depends on axioms: [propext, Classical.choice, Quot.sound]
'PullbackOrbit.limit_independent' depends on axioms: [propext, Classical.choice, Quot.sound]
'PullbackOrbit.pushforward_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound]
'PullbackOrbit.compact_unique_cluster' depends on axioms: [propext, Classical.choice, Quot.sound]

## ReflectionSupportScale.lean
'ReflectionSupportScale.DependsOn.mono' does not depend on any axioms
'ReflectionSupportScale.dependsOn_comp' depends on axioms: [propext, Quot.sound]
'ReflectionSupportScale.dependsOn_positive_of_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'ReflectionSupportScale.dependsOn_reach_comp' depends on axioms: [propext, Classical.choice, Quot.sound]
'ReflectionSupportScale.exists_factor_of_dependsOn' depends on axioms: [propext, Classical.choice, Quot.sound]
'ReflectionSupportScale.reach_sum_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'ReflectionSupportScale.reach_le_half_of_m0' depends on axioms: [propext, Classical.choice, Quot.sound]
'ReflectionSupportScale.reach_total_le_half' depends on axioms: [propext, Classical.choice, Quot.sound]
'ReflectionSupportScale.m0_examples' depends on axioms: [propext, Classical.choice, Quot.sound]
'ReflectionSupportScale.m0_zero_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'ReflectionSupportScale.coarse_rp_of_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'ReflectionSupportScale.coarse_rp_of_fine_support' depends on axioms: [propext, Classical.choice, Quot.sound]
'ReflectionSupportScale.rp_down' depends on axioms: [propext, Classical.choice, Quot.sound]
'ReflectionSupportScale.weak_uv_block_skeleton_cofinal' depends on axioms: [propext, Classical.choice, Quot.sound]
'ReflectionSupportScale.even_cofinal' depends on axioms: [propext, Quot.sound]
'ReflectionSupportScale.cofinal_of_all' depends on axioms: [propext, Classical.choice, Quot.sound]

## RegularityConstant.lean
'ClassStepRemainder.bounded_orbit_small' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.norm_step_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.orbit_in_small_ball' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.coupling_remainder_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.small_rem_form' depends on axioms: [propext, Classical.choice, Quot.sound]
'TreeGaugeLocality.treeGauge_step' depends on axioms: [propext, Quot.sound]
'TreeGaugeLocality.gfix_tree_edge' depends on axioms: [propext, Quot.sound]
'TreeGaugeLocality.invariant_depends_on_nontree' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.abs_prod_sub_prod_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.pointwise_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.expectation_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.equicontinuous_of_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.nontree_small_ball' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.quadratic_fields' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.shift_difference' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.shift_stays' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.invariant_factors' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.pointwise_from_nontree' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityConstant.lipschitz_on_ball' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityConstant.Keta_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityConstant.Keta_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityConstant.expectation_from_nontree' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityConstant.expectation_Keta' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityConstant.equicontinuous_from_Keta' depends on axioms: [propext, Classical.choice, Quot.sound]

## RegularityRadius.lean
'TwoStageSmallField.UltravioletChain.activity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.hbeta_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.small_field_mass_of_rarity' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'TwoStageSmallField.UltravioletChain.small_field_mass_invariant' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'TwoStageSmallField.UltravioletChain.expectation_diff_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.split_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.gauge_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.equicontinuous_of_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.vanishing_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.vanishing_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.chain_to_hypotheses' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.badSet_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.goodSet_eq_compl' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.block_bad_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.block_bad_le_counts' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.index_bad_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.index_good_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.small_field_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.eta_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.small_field_two_stage_box' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.rarity_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.chain_hypotheses_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.hsf_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.bounded_orbit_small' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.norm_step_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.orbit_in_small_ball' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.coupling_remainder_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.small_rem_form' depends on axioms: [propext, Classical.choice, Quot.sound]
'TreeGaugeLocality.treeGauge_step' depends on axioms: [propext, Quot.sound]
'TreeGaugeLocality.gfix_tree_edge' depends on axioms: [propext, Quot.sound]
'TreeGaugeLocality.invariant_depends_on_nontree' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.abs_prod_sub_prod_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.pointwise_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.expectation_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.equicontinuous_of_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.nontree_small_ball' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.quadratic_fields' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.shift_difference' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.shift_stays' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.invariant_factors' depends on axioms: [propext, Classical.choice, Quot.sound]
'NontreeBackground.pointwise_from_nontree' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityConstant.lipschitz_on_ball' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityConstant.Keta_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityConstant.Keta_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityConstant.expectation_from_nontree' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityConstant.expectation_Keta' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityConstant.equicontinuous_from_Keta' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityRadius.compl_real_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityRadius.two_stage_compl_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityRadius.amp_lt_one_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityRadius.amp_lt_one_numbers' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityRadius.window_radius_inside' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityRadius.Keta_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityRadius.expectation_eta' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityRadius.equicontinuous_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]

## RegularityStep.lean
'RegularityStep.abs_prod_sub_prod_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.pointwise_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.expectation_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'RegularityStep.equicontinuous_of_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]

## SharpWindow.lean
'SharpWindow.sharp_necessary' depends on axioms: [propext, Classical.choice, Quot.sound]
'SharpWindow.sharp_sufficient' depends on axioms: [propext, Classical.choice, Quot.sound]
'SharpWindow.lipschitz_form_implies_sharp' depends on axioms: [propext, Classical.choice, Quot.sound]
'SharpWindow.maps_ball_sharp' depends on axioms: [propext, Classical.choice, Quot.sound]
'SharpWindow.lipschitz_step' depends on axioms: [propext, Classical.choice, Quot.sound]
'SharpWindow.sharp_beta28_tau1' depends on axioms: [propext, Classical.choice, Quot.sound]
'SharpWindow.margin_beta28_sharp' depends on axioms: [propext, Classical.choice, Quot.sound]
'SharpWindow.sharp_beta20_tau3' depends on axioms: [propext, Classical.choice, Quot.sound]
'SharpWindow.sharp_beta16_tau1_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'SharpWindow.sharp_entire_orbit' depends on axioms: [propext, Classical.choice, Quot.sound]

## SizeSplitKP.lean
'SizeSplitKP.sum_split_by_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'SizeSplitKP.fat_sum_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'SizeSplitKP.geometric_tail_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'SizeSplitKP.size_split_site_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'SizeSplitKP.fat_condition_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'SizeSplitKP.allowed_eps_scale' depends on axioms: [propext, Classical.choice, Quot.sound]

## SmallRemKernel.lean
'SmallRemKernel.UltravioletChain.activity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.hbeta_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.small_field_mass_of_rarity' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.small_field_mass_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.expectation_diff_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.split_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.gauge_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.equicontinuous_of_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.vanishing_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.vanishing_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.UltravioletChain.chain_to_hypotheses' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_kernel_unit' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.projected_remainder_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.coupling_from_unprojected' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.activity_le_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.hbeta_of_steps_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.steps_ker_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.hbeta_agrees' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.small_rem_field_of_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.chain_to_hypotheses_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'SmallRemKernel.chain_ker_of_chain' depends on axioms: [propext, Classical.choice, Quot.sound]

## SupplyLedger.lean
'WeightRecursion.weight_step' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.weight_step_plain' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.image_card_boundary' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.image_card_boundary_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.weight_step_sets' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.contraction_of_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.all_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.stationary_schedule' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.stationary_boundary_coeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.stationary_all_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.boundary_coeff_decreases' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.no_schedule_of_delta_ge_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.gap_le_volume_coeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.all_steps_supply' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.stationary_schedule_supply' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.coarse_boundary_le_deg' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.pair_inner' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.pair_volume' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.pair_mix' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.nn_total' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.star_total' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.nn_L2' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.nn_L4' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.star_L2' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.star_L4' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.gamma_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.no_stationary' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.four_cases_pq' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.supply_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.supply_achieved' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.volume_needed' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.per_block_reading_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.supply_nn_L2' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.supply_nn_L4' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.supply_star_L2' depends on axioms: [propext, Classical.choice, Quot.sound]
'BlockBoundaryCount.supply_star_L4' depends on axioms: [propext, Classical.choice, Quot.sound]
'SupplyLedger.log_four_lt' depends on axioms: [propext, Classical.choice, Quot.sound]
'SupplyLedger.supply_L4_numbers' depends on axioms: [propext, Classical.choice, Quot.sound]
'SupplyLedger.supply_L4_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'SupplyLedger.regenerated_step' depends on axioms: [propext, Classical.choice, Quot.sound]
'SupplyLedger.exp_twelve_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'SupplyLedger.regenerated_contraction_L2' depends on axioms: [propext, Classical.choice, Quot.sound]
'SupplyLedger.regenerated_contraction_L4' depends on axioms: [propext, Classical.choice, Quot.sound]
'SupplyLedger.regenerated_all_steps' depends on axioms: [propext, Classical.choice, Quot.sound]

## TreeGauge.lean
'TreeGauge.treeGauge_root' depends on axioms: [propext, Quot.sound]
'TreeGauge.treeGauge_step' depends on axioms: [propext, Quot.sound]
'TreeGauge.treeGauge_trivializes' depends on axioms: [propext, Quot.sound]
'TreeGauge.exists_tree_gauge' depends on axioms: [propext, Quot.sound]
'TreeGauge.tree_gauge_unique' depends on axioms: [propext]

## TreeGaugeLocality.lean
'TreeGaugeLocality.treeGauge_step' depends on axioms: [propext, Quot.sound]
'TreeGaugeLocality.gfix_tree_edge' depends on axioms: [propext, Quot.sound]
'TreeGaugeLocality.invariant_depends_on_nontree' depends on axioms: [propext, Classical.choice, Quot.sound]

## TwoColorEncoding.lean
'TwoColorEncoding.conn_erase' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.rooted_erase' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.rooted_of_connected' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.Wg_step' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.prod_mono_of_one_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.Wg_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.point_gf_le_weighted' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.prod_by_color' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.two_color_Wg_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.two_color_point_sum' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.two_color_root_set_sum' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.one_add_pow_le_exp' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.fix_of_exp' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.exp_one_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.exp_nat_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.lattice_fix' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.lattice_face_total' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.lattice_two_color_kp' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.sum_le_of_injOn' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.label_sum_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.img_spec' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.img_mem' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.img_adj' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.enc_connected' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.decode' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.enc_eq' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.thin_disjoint' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.card_le_enc' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.weight_le_G' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.encoded_sum_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.enc_meets_root' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.two_color_point_gf' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.two_color_root_gf' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.encoded_kp_site' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.intersect_sum_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.dobrushin_cond_of_kp' depends on axioms: [propext, choice, Quot.sound]
'TwoColorEncoding.encoded_dobrushin' depends on axioms: [propext, choice, Quot.sound]

## TwoColorPolymerSum.lean
'TwoColorPolymerSum.conn_erase' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.rooted_erase' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.rooted_of_connected' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.Wg_step' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.prod_mono_of_one_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.Wg_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.point_gf_le_weighted' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.prod_by_color' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.two_color_Wg_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.two_color_point_sum' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.two_color_root_set_sum' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.one_add_pow_le_exp' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.fix_of_exp' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.exp_one_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.exp_nat_le' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.lattice_fix' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.lattice_face_total' depends on axioms: [propext, choice, Quot.sound]
'TwoColorPolymerSum.lattice_two_color_kp' depends on axioms: [propext, choice, Quot.sound]

## TwoStageSmallField.lean
'TwoStageSmallField.UltravioletChain.activity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.hbeta_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.small_field_mass_of_rarity' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'TwoStageSmallField.UltravioletChain.small_field_mass_invariant' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'TwoStageSmallField.UltravioletChain.expectation_diff_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.split_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.gauge_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.equicontinuous_of_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.vanishing_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.vanishing_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.UltravioletChain.chain_to_hypotheses' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.badSet_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.goodSet_eq_compl' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.block_bad_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.block_bad_le_counts' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.index_bad_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.index_good_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.small_field_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.eta_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.small_field_two_stage_box' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.rarity_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.chain_hypotheses_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]
'TwoStageSmallField.hsf_two_stage' depends on axioms: [propext, Classical.choice, Quot.sound]

## UltravioletAssembly.lean
'LatticeGauge.LocProjection.euler_of_homogeneous' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.marginal_of_fixed' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.schur_homogeneous' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.proj_idem' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.proj_decomp' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.loc_comm' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.comm_sub_proj' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.iterate_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.iterate_contract_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.iterate_contract_remainder' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.marginal_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.other_direction_drifts' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.other_direction_not_fixed' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.restrictKer_opNorm_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.exists_unique_fixed_ker' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.kkt_gauge_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.kkt_scale' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.kkt_homogeneous' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.pull_succ'' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.pull_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.dist_pull_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.pull_orbit' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.exists_unique_entire_orbit' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.ball_step_from_loc_A' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.window_from_loc_A' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.window_radius' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.window_numbers' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.pull_mem_sets' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.dist_pull_le_sets' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.exists_unique_entire_orbit_sets' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.isClosed_stageSet' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.window_from_loc_A_stages' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.LocProjection.stage_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.bounded_orbit_small' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.norm_step_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.orbit_in_small_ball' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.coupling_remainder_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.small_rem_form' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldStep.rarity_chernoff' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldStep.rarity_ennreal' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldStep.healing_deterministic' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldStep.healing_markov' depends on axioms: [propext, Classical.choice, Quot.sound]
'LargeFieldStep.kp_threshold' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.activity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.hbeta_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.small_field_mass_of_rarity' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.small_field_mass_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.expectation_diff_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.split_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.gauge_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.equicontinuous_of_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.vanishing_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.vanishing_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.chain_to_hypotheses' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletAssembly.window_orbit_small' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletAssembly.small_rem_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletAssembly.rarity_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletAssembly.coupling_steps_of_parts' depends on axioms: [propext, Classical.choice, Quot.sound]

## UltravioletChain.lean
'UltravioletChain.activity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.hbeta_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.small_field_mass_of_rarity' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.small_field_mass_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.expectation_diff_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.split_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.gauge_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.equicontinuous_of_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.vanishing_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.vanishing_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.chain_to_hypotheses' depends on axioms: [propext, Classical.choice, Quot.sound]

## UltravioletGlue.lean
'WeakUltravioletExistence.exists_bare_inverse_coupling' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_tendsto_probabilityMeasure' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'WeakUltravioletExistence.exists_common_subseq' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.limit_consistent' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.reflection_positivity_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.approx_invariance_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.closed_mass_lower_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_tendsto_on_countable' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.continuous_extension_of_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_continuous_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.invariance_of_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.quadratic_positivity_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.invariance_extends_by_density' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.tendsto_of_summable_increments' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.subseq_limit_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_block_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_observable_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_observable_full' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.activity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.hbeta_of_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.small_field_mass_of_rarity' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.small_field_mass_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.expectation_diff_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.split_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.gauge_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.equicontinuous_of_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.vanishing_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.vanishing_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletChain.chain_to_hypotheses' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletGlue.glue_bare_coupling' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletGlue.glue_observable' depends on axioms: [propext, Classical.choice, Quot.sound]
'UltravioletGlue.glue_small_field' depends on axioms: [propext, Classical.choice, Quot.sound]

## VertexClassWindow.lean
'LatticeGauge.VertexClassWindow.pullback_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.VertexClassWindow.pullback_vertex_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.VertexClassWindow.two_component_step' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.VertexClassWindow.weight_choice' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.VertexClassWindow.tau_v_number' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.VertexClassWindow.tau_v_number_tau3' depends on axioms: [propext, Classical.choice, Quot.sound]

## WeakUltravioletExistence.lean
'WeakUltravioletExistence.exists_bare_inverse_coupling' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_tendsto_probabilityMeasure' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'WeakUltravioletExistence.exists_common_subseq' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.limit_consistent' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.reflection_positivity_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.approx_invariance_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.closed_mass_lower_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_tendsto_on_countable' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.continuous_extension_of_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.exists_subseq_continuous_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.invariance_of_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.quadratic_positivity_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.invariance_extends_by_density' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.tendsto_of_summable_increments' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.subseq_limit_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_block_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_observable_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_observable_full' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeakUltravioletExistence.weak_uv_skeleton' depends on axioms: [propext, Classical.choice, Quot.sound]

## WeightRecursion.lean
'WeightRecursion.weight_step' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.weight_step_plain' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.image_card_boundary' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.image_card_boundary_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.weight_step_sets' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.contraction_of_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.all_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.stationary_schedule' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.stationary_boundary_coeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.stationary_all_steps' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.boundary_coeff_decreases' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.no_schedule_of_delta_ge_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.gap_le_volume_coeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.all_steps_supply' depends on axioms: [propext, Classical.choice, Quot.sound]
'WeightRecursion.stationary_schedule_supply' depends on axioms: [propext, Classical.choice, Quot.sound]