# principia-hodge-cm-degenerate の全モジュールの `#print axioms` の出力（モジュールごと）。
# `sorryAx` も `Lean.ofReduceBool` も無い。全行が propext / Classical.choice / Quot.sound の部分集合。
# モジュール 46 本・980 行。

## Principia.CMHodge.CMHodgeClasses  (16 行)
'CMHodge.phi_is_cm_type' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.phi_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.T0_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.T0_hodge' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.two_adm' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.adm_pair_cc_closed' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.T0_not_generated_by_divisors' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.unique_involution' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.Y0_subgroup' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.Y0_cfree' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.T0_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.T0_disjoint' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.stab_trivial' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.cc_add_cc' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.Y0_card_odd' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.Y1_coset' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeCurveClassIntegral  (24 行)
'CMHodge.round_robin_split' depends on axioms: [propext]
'CMHodge.diagonal_pairs_1182' depends on axioms: [propext]
'CMHodge.exact_vs_approx_pair_weight' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.glue_exact_lt_approx' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.glue_exact_ge_deficit' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.CC_in_four_Z' depends on axioms: [propext]
'CMHodge.CC_gcd_eight' depends on axioms: [propext]
'CMHodge.CC_theta_degree' depends on axioms: [propext]
'CMHodge.six_atom_basis_index_not_one' depends on axioms: [propext]
'CMHodge.rounding_margin_safe' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.degree12_after_curve' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.degree12_exact_beats_approx' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.chi_FF_from_pairings' depends on axioms: [propext, Quot.sound]
'CMHodge.chi_FF_closed' depends on axioms: [propext, Quot.sound]
'CMHodge.chi_FF_from_theta_W_squared' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.ext_relation' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.ext1_large' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.index_minus_g_theta' depends on axioms: [propext]
'CMHodge.chi_minus_g_theta' depends on axioms: [propext]
'CMHodge.residual_divisor_pos_def' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.chiN_negative' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.koszul_degenerate_count' depends on axioms: [propext]
'CMHodge.semiregularity_target_dim' depends on axioms: [propext]
'CMHodge.pair_census' depends on axioms: [propext]

## Principia.CMHodge.CMHodgeDegenerate  (14 行)
'CMHodge.no_deg_order_two' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.card_deg_prim' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.deg_prim_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.ann_f6_param' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.param_mem' depends on axioms: [propext, Quot.sound]
'CMHodge.ann_f6_L1' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.cover' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.weight_ge_three' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.weight_three_attained' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.Sset_is_cm_type' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.Texc_card' depends on axioms: [propext, Quot.sound]
'CMHodge.Texc_adm' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.Texc_coset' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.Texc_not_divisorial' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeDegreeTen  (17 行)
'CMHodgeDegreeTen.nonneg_sum_zero_forces' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeDegreeTen.thickening_forces_reduced' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeDegreeTen.deg8_strictly_positive_columns' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeDegreeTen.zeta10_not_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeDegreeTen.zeta10_cubic_coeff_nonzero' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeDegreeTen.full_thickening_length_values' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeDegreeTen.full_thickening_ne_multiplicity' depends on axioms: [propext]
'CMHodgeDegreeTen.triple_intersection_empty' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeDegreeTen.pair_codims' depends on axioms: [propext]
'CMHodgeDegreeTen.shared_sum_eigenvalues' depends on axioms: [propext, Quot.sound]
'CMHodgeDegreeTen.budget_eigen_beats_trace' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeDegreeTen.budget_psd_113' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeDegreeTen.residual_h0_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeDegreeTen.cert_coeffs_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeDegreeTen.cert_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeDegreeTen.deg12_points_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeDegreeTen.window_nonempty' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeDegreeTenBudget  (16 行)
'DegreeTenBudget.koszul_deg2' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeTenBudget.koszul_deg2_fixed_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeTenBudget.three_sq_sub_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeTenBudget.cost_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeTenBudget.cost_ge_balanced' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeTenBudget.budget_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeTenBudget.balanced_cost_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeTenBudget.balanced_minus_budget' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeTenBudget.budget_num' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeTenBudget.balanced_cost_num' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeTenBudget.ell_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeTenBudget.extremal_point' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeTenBudget.cyclic_forces_e3' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeTenBudget.cyclic_e3_neg' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeTenBudget.cyclic_forces_e2' depends on axioms: [propext, Classical.choice, Quot.sound]
'DegreeTenBudget.glued_pair_sum' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeDesignT17over2  (11 行)
'DesignT17Half.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT17Half.q_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT17Half.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT17Half.p0_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT17Half.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT17Half.dq_neg_of_a1_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT17Half.dq_perm12' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT17Half.dq_perm13' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT17Half.dq_swap' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT17Half.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT17Half.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeDesignT35over4  (83 行)
'DesignT35Quarter.charpoly_a' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.charpoly_b' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.charpoly_ab' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.dP1_vals' does not depend on any axioms
'DesignT35Quarter.member0_t35over4_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member0_t35over4_rows' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member1_t35over4_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member1_t35over4_rows' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member2_t35over4_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member2_t35over4_rows' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member3_t35over4_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member3_t35over4_rows' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member4_t35over4_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member4_t35over4_rows' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member5_t35over4_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member5_t35over4_rows' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member0_t17over2_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member0_t17over2_rows' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member1_t17over2_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member1_t17over2_rows' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member2_t17over2_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member2_t17over2_rows' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member3_t17over2_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member3_t17over2_rows' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member4_t17over2_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member4_t17over2_rows' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member5_t17over2_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.member5_t17over2_rows' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.lemmaO_radius_ge_of_P1_t35over4' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.line_point_attains_t35over4' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.lemmaO_radius_ge_of_P1_t17over2' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.line_point_attains_t17over2' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.lemmaO_radius_ge_of_P1_t69over8' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.line_point_attains_t69over8' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.lemmaO_radius_ge_of_P1_span_t35over4' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.lemmaO_radius_ge_of_P1_span_t17over2' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.lemmaO_empty_of_P1_t44over5' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.lemmaO_empty_of_P1_t71over8' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35Quarter.lemmaO_empty_of_P1_t9' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35QuarterCert.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35QuarterCert.q_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35QuarterCert.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35QuarterCert.p0_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35QuarterCert.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35QuarterCert.dq_neg_of_a1_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35QuarterCert.dq_perm12' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35QuarterCert.dq_perm13' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35QuarterCert.dq_swap' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35QuarterCert.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT35QuarterCert.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT703over80Cert.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT703over80Cert.q_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT703over80Cert.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT703over80Cert.p0_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT703over80Cert.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT703over80Cert.dq_neg_of_a1_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT703over80Cert.dq_perm12' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT703over80Cert.dq_perm13' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT703over80Cert.dq_swap' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT703over80Cert.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT703over80Cert.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT879over100Cert.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT879over100Cert.q_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT879over100Cert.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT879over100Cert.p0_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT879over100Cert.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT879over100Cert.dq_neg_of_a1_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT879over100Cert.dq_perm12' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT879over100Cert.dq_perm13' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT879over100Cert.dq_swap' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT879over100Cert.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT879over100Cert.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1759over200Cert.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1759over200Cert.q_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1759over200Cert.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1759over200Cert.p0_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1759over200Cert.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1759over200Cert.dq_neg_of_a1_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1759over200Cert.dq_perm12' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1759over200Cert.dq_perm13' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1759over200Cert.dq_swap' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1759over200Cert.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1759over200Cert.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeDesignT3Point  (18 行)
'DesignT3Point.f_lo_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Point.f_hi_neg' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Point.cubic_enclose' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Point.k_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Point.k_rel' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Point.dqc_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Point.dqc_neg_of_a1_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Point.dqc_perm12' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Point.dqc_perm13' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Point.dqc_swap' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Point.dqs_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Point.qs_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Point.V_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Point.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Point.p0_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Point.qs_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Point.V_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Point.no_design_at_root' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeDesignT71over8  (5 行)
'DesignT71over8Cert.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT71over8Cert.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT71over8Cert.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT71over8Cert.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT71over8Cert.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeDesignT888  (10 行)
'DesignT222over25Cert.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT222over25Cert.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT222over25Cert.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT222over25Cert.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT222over25Cert.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1777over200Cert.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1777over200Cert.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1777over200Cert.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1777over200Cert.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1777over200Cert.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeDesignT8888  (15 行)
'DesignT8887over1000Cert.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT8887over1000Cert.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT8887over1000Cert.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT8887over1000Cert.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT8887over1000Cert.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1111over125Cert.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1111over125Cert.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1111over125Cert.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1111over125Cert.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT1111over125Cert.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT17777over2000Cert.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT17777over2000Cert.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT17777over2000Cert.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT17777over2000Cert.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT17777over2000Cert.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeDesignT88886  (7 行)
'DesignT44443over5000Cert.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT44443over5000Cert.q_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT44443over5000Cert.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT44443over5000Cert.p0_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT44443over5000Cert.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT44443over5000Cert.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT44443over5000Cert.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeDesignT8Impossible  (110 行)
'DesignT8.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT8.q_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT8.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT8.p0_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT8.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT8.dq_neg_of_a1_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT8.dq_perm12' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT8.dq_perm13' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT8.dq_swap' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT8.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT8.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Control.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Control.q_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Control.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Control.p0_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Control.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Control.dq_neg_of_a1_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Control.dq_perm12' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Control.dq_perm13' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Control.dq_swap' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Control.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT3Control.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT4.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT4.q_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT4.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT4.p0_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT4.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT4.dq_neg_of_a1_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT4.dq_perm12' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT4.dq_perm13' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT4.dq_swap' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT4.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT4.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT5.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT5.q_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT5.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT5.p0_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT5.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT5.dq_neg_of_a1_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT5.dq_perm12' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT5.dq_perm13' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT5.dq_swap' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT5.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT5.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT6.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT6.q_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT6.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT6.p0_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT6.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT6.dq_neg_of_a1_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT6.dq_perm12' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT6.dq_perm13' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT6.dq_swap' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT6.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT6.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT13Half.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT13Half.q_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT13Half.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT13Half.p0_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT13Half.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT13Half.dq_neg_of_a1_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT13Half.dq_perm12' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT13Half.dq_perm13' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT13Half.dq_swap' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT13Half.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT13Half.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT7.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT7.q_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT7.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT7.p0_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT7.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT7.dq_neg_of_a1_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT7.dq_perm12' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT7.dq_perm13' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT7.dq_swap' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT7.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT7.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT15Half.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT15Half.q_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT15Half.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT15Half.p0_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT15Half.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT15Half.dq_neg_of_a1_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT15Half.dq_perm12' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT15Half.dq_perm13' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT15Half.dq_swap' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT15Half.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT15Half.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT31Quarter.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT31Quarter.q_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT31Quarter.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT31Quarter.p0_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT31Quarter.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT31Quarter.dq_neg_of_a1_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT31Quarter.dq_perm12' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT31Quarter.dq_perm13' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT31Quarter.dq_swap' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT31Quarter.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT31Quarter.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT33Quarter.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT33Quarter.q_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT33Quarter.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT33Quarter.p0_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT33Quarter.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT33Quarter.dq_neg_of_a1_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT33Quarter.dq_perm12' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT33Quarter.dq_perm13' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT33Quarter.dq_swap' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT33Quarter.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT33Quarter.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeDesignT8p8  (15 行)
'DesignT44over5Cert.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT44over5Cert.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT44over5Cert.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT44over5Cert.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT44over5Cert.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT887over100Cert.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT887over100Cert.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT887over100Cert.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT887over100Cert.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT887over100Cert.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT8871over1000Cert.q_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT8871over1000Cert.p0_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT8871over1000Cert.dq_neg_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT8871over1000Cert.dq_neg_of_some_coord_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignT8871over1000Cert.no_design_of_box_table' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeDesignThreshold  (141 行)
'DesignThreshold.c2_parity_obstruction_of_even_twist' depends on axioms: [propext, Quot.sound]
'DesignThreshold.c2_integral_of_odd_twist' depends on axioms: [propext]
'DesignThreshold.piece_count_le_of_trace_ge_three' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.trace_ge_three_of_norm_ge_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.c2_values' depends on axioms: [propext]
'DesignThreshold.sb1_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.sb2_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.sb3_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.sb4_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.sb5_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.sb6_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.piece1_norms' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.piece2_norms' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.piece3_norms' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.piece4_norms' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.piece5_norms' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.piece6_norms' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d1_1' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d1_2' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d1_3' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d1_4' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d1_5' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d1_6' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d2_1' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d2_2' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d2_3' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d2_4' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d2_5' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d2_6' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d3_1' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d3_2' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d3_3' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d3_4' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d3_5' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d3_6' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d4_1' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d4_2' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d4_3' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d4_4' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d4_5' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d4_6' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d5_1' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d5_2' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d5_3' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d5_4' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d5_5' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d5_6' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d6_1' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d6_2' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d6_3' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d6_4' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d6_5' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.d6_6' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.sb1_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.sb2_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.sb3_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.sb4_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.sb5_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.sb6_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.design_1' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.design_2' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.design_3' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.design_4' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.design_5' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.design_6' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThreshold.no_symmetric_certificate_t7_of_norm_ge_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.P00_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.P01_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.P02_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.P10_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.P11_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.P12_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.P20_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.P21_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.P22_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_000' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_001' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_002' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_010' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_011' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_012' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_020' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_021' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_022' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_100' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_101' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_102' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_110' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_111' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_112' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_120' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_121' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_122' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_200' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_201' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_202' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_210' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_211' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_212' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_220' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_221' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.design_222' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece1_a_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece1_b_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece2_a_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece2_b_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece3_a_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece3_b_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece4_a_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece4_b_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece5_a_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece5_b_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece6_a_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece6_b_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece7_a_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece7_b_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece8_a_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece8_b_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece9_a_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece9_b_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece10_a_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece10_b_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece11_a_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece11_b_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece12_a_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece12_b_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece13_a_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece13_b_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece14_a_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece14_b_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece15_a_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece15_b_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece16_a_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece16_b_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece17_a_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece17_b_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece18_a_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece18_b_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece19_a_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.piece19_b_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdO.weights_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeDesignThresholdT3  (14 行)
'DesignThresholdT3.dual_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdT3.moment_det' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdT3.coef_nonpos_of_quad' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdT3.moment_step' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdT3.dP2_nonneg_of_necessary' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdT3.no_certificate_of_t3_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdT3.dP2V_nonneg_of_necessary' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdT3.f_pos_17777_2000' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdT3.f_pos_88886088' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdT3.f_neg_88886089' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdT3.f_neg_88887' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdT3.f_neg_8889' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdT3.f_neg_14' depends on axioms: [propext, Classical.choice, Quot.sound]
'DesignThresholdT3.no_certificate_at_88887' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeDiscRing  (14 行)
'CMHodgeDiscRing.detA_eq_neg_sq_ring' depends on axioms: [propext, Quot.sound]
'CMHodgeDiscRing.detB_is_norm_ring' depends on axioms: [propext, Quot.sound]
'CMHodgeDiscRing.detB_is_norm_field' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeDiscRing.th_rel' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeDiscRing.detA_eq_neg_sq_adjoin' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeDiscRing.detB_is_norm_adjoin' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeDiscRing.ev_mul' depends on axioms: [propext, Quot.sound]
'CMHodgeDiscRing.mul_assoc'' depends on axioms: [propext, Quot.sound]
'CMHodgeDiscRing.mul_add'' depends on axioms: [propext]
'CMHodgeDiscRing.ev_th_eq_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeDiscRing.ev_th_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeDiscRing.one_mul'' depends on axioms: [propext]
'CMHodgeDiscRing.mul_comm'' depends on axioms: [propext]
'CMHodgeDiscRing.p_eq' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeDiscriminant  (11 行)
'CMHodgeDisc.theta_rel' does not depend on any axioms
'CMHodgeDisc.mul_comm'' depends on axioms: [propext]
'CMHodgeDisc.detA_eq_neg_sq' does not depend on any axioms
'CMHodgeDisc.w_sq_value' does not depend on any axioms
'CMHodgeDisc.detB_is_norm' does not depend on any axioms
'CMHodgeDisc.detB_value' does not depend on any axioms
'CMHodgeDisc.detB_is_norm_Q' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeDisc.nA_values' depends on axioms: [propext]
'CMHodgeDisc.psi_is_odd' depends on axioms: [propext]
'CMHodgeDisc.nB_all_two' depends on axioms: [propext]
'CMHodgeDisc.split_target' depends on axioms: [propext]

## Principia.CMHodge.CMHodgeDivisor  (32 行)
'CMHodge.resdeg_48677' depends on axioms: [propext]
'CMHodge.resdeg_mem' depends on axioms: [propext]
'CMHodge.norm_of_prime' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.not_norm_of_witness' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.not_norm_two' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.norm_nineteen' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.norm_thirtyseven' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.norm_48677' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.no_ideal_norm_in_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.min_ideal_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.condCount_9_10' does not depend on any axioms
'CMHodge.condCount_9_10_layers' depends on axioms: [propext]
'CMHodge.condCount_9_11' does not depend on any axioms
'CMHodge.system_nonempty' does not depend on any axioms
'CMHodge.system_dim' does not depend on any axioms
'CMHodge.mult_eleven_not_forced' does not depend on any axioms
'CMHodge.exists_eigenspace_with_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.mu38_eigen_section' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.pTorsion_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.mu38_fixed_point_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.neg_fixed_iff_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.twoTorsion_card' depends on axioms: [propext]
'CMHodge.zeta_trivial_on_WF' depends on axioms: [propext]
'CMHodge.zeta_trivial_on_all_cosets' depends on axioms: [propext]
'CMHodge.zeta_nontrivial_on_H1' depends on axioms: [propext]
'CMHodge.wt_eq_cm_type' depends on axioms: [propext]
'CMHodge.wt_sum' depends on axioms: [propext]
'CMHodge.not_gorenstein' depends on axioms: [propext]
'CMHodge.ageNum_ge_58' depends on axioms: [propext]
'CMHodge.ageNum_min' depends on axioms: [propext]
'CMHodge.ageNum_pair' depends on axioms: [propext]
'CMHodge.ageNum_not_integral' depends on axioms: [propext]

## Principia.CMHodge.CMHodgeDivisor2  (16 行)
'CMHodge.coeff_zero_of_sum_nonpos' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.defect_core' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.defect_core_general' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.mult_sum_eq' depends on axioms: [propext, Quot.sound]
'CMHodge.three_four_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.sIdx_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.cone_forces_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.cone_forces_equal' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.Stil_eq_image' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.Stil_card' depends on axioms: [propext, Quot.sound]
'CMHodge.Stil_cm' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.weights_eq_Stil' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.Stil_not_coset_union' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.Stil_inter_qr' depends on axioms: [propext, Quot.sound]
'CMHodge.cyclicType_1_1_card' depends on axioms: [propext, Quot.sound]
'CMHodge.Stil_not_cyclic' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeEquivariance  (11 行)
'EquivariantTrace.sum_of_vanishing_offIdentity' depends on axioms: [propext, Classical.choice, Quot.sound]
'EquivariantTrace.card_dvd_of_invariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'EquivariantTrace.trivial_of_exponent_113' depends on axioms: [propext, Classical.choice, Quot.sound]
'EquivariantTrace.window_divisors_M' depends on axioms: [propext, Classical.choice, Quot.sound]
'EquivariantTrace.window_divisors_both' depends on axioms: [propext, Classical.choice, Quot.sound]
'EquivariantTrace.c113_excluded' depends on axioms: [propext]
'EquivariantTrace.ext2_dim4' depends on axioms: [propext, Classical.choice, Quot.sound]
'EquivariantTrace.ext2_dim4_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'EquivariantTrace.ext3_dim6' depends on axioms: [propext, Classical.choice, Quot.sound]
'EquivariantTrace.ext2_zero_consistent_dim6' depends on axioms: [propext, Classical.choice, Quot.sound]
'EquivariantTrace.chi_value' depends on axioms: [propext]

## Principia.CMHodge.CMHodgeExtension  (13 行)
'HodgeExtension.tensor_pair_vanish' depends on axioms: [propext, Classical.choice, Quot.sound]
'HodgeExtension.sol_set_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'HodgeExtension.finrank_block' depends on axioms: [propext, Classical.choice, Quot.sound]
'HodgeExtension.M_symm' depends on axioms: [propext, Classical.choice, Quot.sound]
'HodgeExtension.M_S1_not_comm' depends on axioms: [propext, Classical.choice, Quot.sound]
'HodgeExtension.c1_c2_indep' depends on axioms: [propext, Classical.choice, Quot.sound]
'HodgeExtension.surviving_e1' depends on axioms: [propext, Classical.choice, Quot.sound]
'HodgeExtension.gcdTarget_factor' depends on axioms: [propext]
'HodgeExtension.candidates_filter' depends on axioms: [propext, Classical.choice, Quot.sound]
'HodgeExtension.dvd_of_all_dvd' depends on axioms: [propext, Classical.choice, Quot.sound]
'HodgeExtension.no_upper_bound_from_chi' depends on axioms: [propext]
'HodgeExtension.weak_iff_ext2_eq_54' depends on axioms: [propext, Classical.choice, Quot.sound]
'HodgeExtension.ext2_le_of_injective' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeGlueWindow  (17 行)
'GlueWindow.schur_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
'GlueWindow.schur_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'GlueWindow.schur_eq_flat' depends on axioms: [propext, Classical.choice, Quot.sound]
'GlueWindow.schur_eq_corner' depends on axioms: [propext, Classical.choice, Quot.sound]
'GlueWindow.ell_cyclic_nonpos' depends on axioms: [propext, Classical.choice, Quot.sound]
'GlueWindow.out_const' depends on axioms: [propext]
'GlueWindow.out_dvd_of_collapse' depends on axioms: [propext, Classical.choice, Quot.sound]
'GlueWindow.Qform_span' depends on axioms: [propext, Quot.sound]
'GlueWindow.Qform_dvd_nineteen' depends on axioms: [propext, Quot.sound]
'GlueWindow.typeb_out_dvd' depends on axioms: [propext, Quot.sound]
'GlueWindow.window_cost_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'GlueWindow.window_nonempty' depends on axioms: [propext, Classical.choice, Quot.sound]
'GlueWindow.window_numeric' depends on axioms: [propext, Classical.choice, Quot.sound]
'GlueWindow.outside_total' depends on axioms: [propext, Classical.choice, Quot.sound]
'GlueWindow.outside_total_num' depends on axioms: [propext, Classical.choice, Quot.sound]
'GlueWindow.wedge_dim_le_one' depends on axioms: [propext, Quot.sound]
'GlueWindow.wedge_dim_values' depends on axioms: [propext]

## Principia.CMHodge.CMHodgeIdealInDivisor  (18 行)
'CMHodgeIdealInDivisor.cube_alt_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealInDivisor.koszul_condition_count' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealInDivisor.koszul_condition_count_g8' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealInDivisor.h0_gTheta' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealInDivisor.index_negative' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealInDivisor.lambda64_fails' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealInDivisor.thin_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealInDivisor.sigma_gap_two' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealInDivisor.sigma_gap_g8' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealInDivisor.deg8_from_deg6' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealInDivisor.sigma_eq_g_of_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealInDivisor.conditions_exceed_sections' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealInDivisor.conditions_ratio' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealInDivisor.ratio_g8' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealInDivisor.R10_coeffs' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealInDivisor.R10_degree' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealInDivisor.pi_alg_ne_pi_geo' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealInDivisor.pi_pairing_mismatch' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeIdealSecant  (11 行)
'CMHodgeIdealSecant.sym3_mixed' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealSecant.cubic_moment_form' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealSecant.e2_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealSecant.e3_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealSecant.frame_exhaust' depends on axioms: [propext]
'CMHodgeIdealSecant.ten_pairs' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealSecant.four_transversals' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealSecant.key_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealSecant.moment_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealSecant.psd_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIdealSecant.isotropic_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeIntegralModel  (25 行)
'CMHodgeIntegralModel.norms_dvd_7560' does not depend on any axioms
'CMHodgeIntegralModel.sden_dvd_7560' does not depend on any axioms
'CMHodgeIntegralModel.not_dvd_4032' depends on axioms: [propext]
'CMHodgeIntegralModel.g_factorisation' depends on axioms: [propext]
'CMHodgeIntegralModel.lcm_2520_1080' does not depend on any axioms
'CMHodgeIntegralModel.convex_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIntegralModel.t_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIntegralModel.t_is_square' depends on axioms: [propext]
'CMHodgeIntegralModel.zeta8_closed' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIntegralModel.zeta10_closed' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIntegralModel.zeta12_closed' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIntegralModel.deg8_from_deg6' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIntegralModel.R10_coeff_theta5' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIntegralModel.R10_coeff_theta3W' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIntegralModel.R10_coeff_thetaW2' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIntegralModel.R10_degree_7560' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIntegralModel.deg12_required' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIntegralModel.deg12_required_closed' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIntegralModel.not_in_cone_of_functional' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIntegralModel.not_effective_of_neg_degree' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIntegralModel.pairs_lower_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIntegralModel.sigma2_le_third' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIntegralModel.row_sum_zero_quadratic' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeIntegralModel.degree_sum_7560' depends on axioms: [propext]
'CMHodgeIntegralModel.gcd_dvd_degree' depends on axioms: [propext]

## Principia.CMHodge.CMHodgeIntersection  (11 行)
'CMHodge.squeeze_three' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.squeeze_three_defect_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.squeeze_two' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.squeeze_two_both' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.weights_not_deficient' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.allowed_top_pos' depends on axioms: [propext, Quot.sound]
'CMHodge.allowed_not_extreme' depends on axioms: [propext, Quot.sound]
'CMHodge.koszul_degree' depends on axioms: [propext, Quot.sound]
'CMHodge.places_nonneg_of_mult' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.defect_incompatible_with_mult' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.inter_seven_attained' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeLevelOne  (26 行)
'CMHodge.cmTypes_all_cm' depends on axioms: [propext]
'CMHodge.deg_prim_card' depends on axioms: [propext]
'CMHodge.SM_deg_prim' depends on axioms: [propext]
'CMHodge.level1_card' depends on axioms: [propext]
'CMHodge.level1_split' depends on axioms: [propext]
'CMHodge.cosets_level1' depends on axioms: [propext]
'CMHodge.reps_in_rest' depends on axioms: [propext]
'CMHodge.rest_cover' depends on axioms: [propext]
'CMHodge.reps_distinct_orbits' depends on axioms: [propext]
'CMHodge.pat_values' depends on axioms: [propext]
'CMHodge.pat_deg_prim' depends on axioms: [propext]
'CMHodge.pat_not_S' depends on axioms: [propext]
'CMHodge.pat_two_of_three' depends on axioms: [propext]
'CMHodge.cls_reps' depends on axioms: [propext]
'CMHodge.deg_prim_cover' depends on axioms: [propext]
'CMHodge.reciprocity_S' depends on axioms: [propext]
'CMHodge.reciprocity_P1' depends on axioms: [propext]
'CMHodge.reciprocity_P2' depends on axioms: [propext]
'CMHodge.level1_uniform' depends on axioms: [propext]
'CMHodge.card_lists' depends on axioms: [propext]
'CMHodge.codim1_A1' depends on axioms: [propext]
'CMHodge.codim2_A1' depends on axioms: [propext]
'CMHodge.codim2_A2' depends on axioms: [propext]
'CMHodge.admD_unique' depends on axioms: [propext]
'CMHodge.no_complementary_pairing_V' depends on axioms: [propext]
'CMHodge.split_weil_condition_V' depends on axioms: [propext]

## Principia.CMHodge.CMHodgeNonnegLift  (10 行)
'CMHodgeNonnegLift.nonneg_lift' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeNonnegLift.nonneg_lift_explicit' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeNonnegLift.two_dvd_pairCoeff' does not depend on any axioms
'CMHodgeNonnegLift.pairCoeff_diag' depends on axioms: [propext]
'CMHodgeNonnegLift.four_dvd_pairCoeff_diag' depends on axioms: [propext]
'CMHodgeNonnegLift.pairCoeff_example' depends on axioms: [propext]
'CMHodgeNonnegLift.distinct_pair_breaks_mod_four' depends on axioms: [propext]
'CMHodgeNonnegLift.pairCoeff_generates_two' depends on axioms: [propext]
'CMHodgeNonnegLift.target_two_not_four' depends on axioms: [propext, Quot.sound]
'CMHodgeNonnegLift.four_versus_two' depends on axioms: [propext, Quot.sound]

## Principia.CMHodge.CMHodgeNormal  (19 行)
'CMHodge.nef_pos_of_prod_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.nef_pos_of_int_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.box_forces_norm_gt' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.no_box_of_norm_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.binom_sum_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.pinch_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.perm_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.perm_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodge.Sl_cm' does not depend on any axioms
'CMHodge.Sl'_cm' does not depend on any axioms
'CMHodge.wt_values' does not depend on any axioms
'CMHodge.wt_level_one' does not depend on any axioms
'CMHodge.wt_conj' does not depend on any axioms
'CMHodge.PhiW_eq' does not depend on any axioms
'CMHodge.PhiW_length' does not depend on any axioms
'CMHodge.PhiW_shift_closed' depends on axioms: [propext, Quot.sound]
'CMHodge.control_level_one'' does not depend on any axioms
'CMHodge.control_not_induced' depends on axioms: [propext, Quot.sound]
'CMHodge.hom_mu19_to_pm_trivial' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeOddMonomialWall  (12 行)
'CMHodgeOddMonomialWall.four_dvd_x3y_coeff' depends on axioms: [propext]
'CMHodgeOddMonomialWall.twelve_dvd_xyz2_coeff' depends on axioms: [propext]
'CMHodgeOddMonomialWall.four_dvd_sum_x3y' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeOddMonomialWall.two_mul_ne_neg_three' depends on axioms: [propext, Quot.sound]
'CMHodgeOddMonomialWall.two_mul_ne_neg_one' depends on axioms: [propext, Quot.sound]
'CMHodgeOddMonomialWall.symmetric_wall_four' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeOddMonomialWall.symmetric_wall_twelve' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeOddMonomialWall.odd_monomial_wall' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeOddMonomialWall.mixed_atom_breaks_mod_four' depends on axioms: [propext, Quot.sound]
'CMHodgeOddMonomialWall.six_dvd_cross' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeOddMonomialWall.twentyfour_dvd_diff' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeOddMonomialWall.twelve_dvd_g_of_rows' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeOrderTriples  (9 行)
'OrderTriples.Q_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'OrderTriples.Q_le_cost' depends on axioms: [propext, Classical.choice, Quot.sound]
'OrderTriples.mixed_eq' depends on axioms: [propext]
'OrderTriples.ell_eq' depends on axioms: [propext]
'OrderTriples.anti_sq_eq_disc' depends on axioms: [propext, Quot.sound]
'OrderTriples.e3_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'OrderTriples.weight_le_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'OrderTriples.weight_eq_zero_scaled' depends on axioms: [propext, Classical.choice, Quot.sound]
'OrderTriples.mixed_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeProductCurve  (16 行)
'CMHodge.SM_is_cm_type' depends on axioms: [propext]
'CMHodge.SM_card' depends on axioms: [propext]
'CMHodge.SM_stab_trivial' depends on axioms: [propext, Quot.sound]
'CMHodge.SM_ne_quadratic' depends on axioms: [propext, Quot.sound]
'CMHodge.adm20_iff' depends on axioms: [propext]
'CMHodge.adm11_none' depends on axioms: [propext]
'CMHodge.adm40_iff' depends on axioms: [propext]
'CMHodge.adm22_iff' depends on axioms: [propext]
'CMHodge.adm31_iff' depends on axioms: [propext]
'CMHodge.coset_not_divisorial' does not depend on any axioms
'CMHodge.count31_eq' depends on axioms: [propext]
'CMHodge.count22_eq' depends on axioms: [propext]
'CMHodge.count40_eq' depends on axioms: [propext]
'CMHodge.level1_breakdown' depends on axioms: [propext]
'CMHodge.split_weil_condition' depends on axioms: [propext]
'CMHodge.no_complementary_pairing' depends on axioms: [propext]

## Principia.CMHodge.CMHodgePureSquareWall  (8 行)
'CMHodgePureSquareWall.expand_third' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgePureSquareWall.trilinear_reduction' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgePureSquareWall.rank_one_atom' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgePureSquareWall.diagonal_atom' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgePureSquareWall.two_mul_sum_ne_fifteen' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgePureSquareWall.no_all_even_multiplicities' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgePureSquareWall.pure_square_wall' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgePureSquareWall.half_not_integral' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeRestrictionRank  (14 行)
'RestrictionRank.ker_le_ker_comp' depends on axioms: [propext, Quot.sound]
'RestrictionRank.ker_le_inf' depends on axioms: [propext, Classical.choice, Quot.sound]
'RestrictionRank.rank_ge_of_ker_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'RestrictionRank.rank_ge_57' depends on axioms: [propext, Classical.choice, Quot.sound]
'RestrictionRank.ker_ne_of_dim' depends on axioms: [propext, Classical.choice, Quot.sound]
'RestrictionRank.ht2_count' depends on axioms: [propext, Classical.choice, Quot.sound]
'RestrictionRank.chosen_traces' depends on axioms: [propext, Quot.sound]
'RestrictionRank.pair_s1' depends on axioms: [propext, Classical.choice, Quot.sound]
'RestrictionRank.pair_h2' depends on axioms: [propext]
'RestrictionRank.pair_old' depends on axioms: [propext]
'RestrictionRank.budget_eq' depends on axioms: [propext]
'RestrictionRank.window_s1' depends on axioms: [propext, Classical.choice, Quot.sound]
'RestrictionRank.window_h2' depends on axioms: [propext, Classical.choice, Quot.sound]
'RestrictionRank.window_old' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeRoundingBudget  (10 行)
'CMHodgeRoundingBudget.rounding_solves' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeRoundingBudget.rounding_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeRoundingBudget.rounding_nonneg_solution' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeRoundingBudget.margin_beats_error' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeRoundingBudget.margin_le_budget_div' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeRoundingBudget.budget_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeRoundingBudget.cauchy_schwarz_three' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeRoundingBudget.rankone_quad_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeRoundingBudget.budget_psd_of_trace_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeRoundingBudget.trace_within_budget' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeScalarWall  (12 行)
'CMHodgeScalarWall.phi_I' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeScalarWall.phi_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeScalarWall.psi_atom_is_square' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeScalarWall.psi_component_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeScalarWall.psi_theta_cubed' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeScalarWall.phi_P_values' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeScalarWall.phi_R_values' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeScalarWall.psi_thetaW' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeScalarWall.psi_thetaW_neg' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeScalarWall.psi_G6' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeScalarWall.scalar_shared_wall' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeScalarWall.not_in_cone_of_functional' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeSecant  (22 行)
'CMHodgeSecant.det4_eq_pf_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecant.detH_d4_is_square' depends on axioms: [propext, Quot.sound]
'CMHodgeSecant.detH_d2_class' depends on axioms: [propext, Quot.sound]
'CMHodgeSecant.split_target4' depends on axioms: [propext]
'CMHodgeSecant.split_target2' depends on axioms: [propext]
'CMHodgeSecant.num_types' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecant.bb_dims' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecant.bb1_formula' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecant.bb_total' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecant.pi_not_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecant.ker_pi_dim' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecant.eqpairs_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecant.diag2_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecant.a_ker_dim' does not depend on any axioms
'CMHodgeSecant.no_pair_meets_all' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecant.ht2_dim6' does not depend on any axioms
'CMHodgeSecant.ht2_dim3' does not depend on any axioms
'CMHodgeSecant.ker_alpha_total' does not depend on any axioms
'CMHodgeSecant.period_dim' depends on axioms: [propext]
'CMHodgeSecant.period_dim_M2' depends on axioms: [propext]
'CMHodgeSecant.no_selfdual_realisation' depends on axioms: [propext, Quot.sound]
'CMHodgeSecant.d_value' does not depend on any axioms

## Principia.CMHodge.CMHodgeSecantGrading  (17 行)
'CMHodgeSecantGrading.grade_cards' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecantGrading.pat_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecantGrading.kb1_exactly_one_term' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecantGrading.kb1_total_pairs' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecantGrading.bb1_split' depends on axioms: [propext]
'CMHodgeSecantGrading.expv_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecantGrading.deg_cards' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecantGrading.odd_even_cards' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecantGrading.c0_from_a' depends on axioms: [propext, Quot.sound]
'CMHodgeSecantGrading.a_to_c' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecantGrading.beta1_vanishes_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecantGrading.top_pairing' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecantGrading.pairing_with_alpha0' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecantGrading.two_place_coincidence' depends on axioms: [propext, Quot.sound]
'CMHodgeSecantGrading.three_place_no_coincidence' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSecantGrading.ht2_split' depends on axioms: [propext]
'CMHodgeSecantGrading.ht2_values' depends on axioms: [propext]

## Principia.CMHodge.CMHodgeSecantGraph  (18 行)
'SecantGraph.isolated_points' depends on axioms: [propext, Quot.sound]
'SecantGraph.unnormalised_points' depends on axioms: [propext, Quot.sound]
'SecantGraph.twist_three' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecantGraph.points_needed' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecantGraph.one_class' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecantGraph.second_difference_weight' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecantGraph.slot_on_exponential' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecantGraph.degree_eight_piece' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecantGraph.degree_eight_sign_small' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecantGraph.degree_eight_sign_large' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecantGraph.c2_design_nine' depends on axioms: [propext, Quot.sound]
'SecantGraph.c2_twist_nine' depends on axioms: [propext]
'SecantGraph.design_nine_counts' depends on axioms: [propext]
'SecantGraph.factor_through_zero' depends on axioms: [propext, Quot.sound]
'SecantGraph.still_empty' depends on axioms: [propext, Quot.sound]
'SecantGraph.nonample_control' does not depend on any axioms
'SecantGraph.ht2_dim' does not depend on any axioms
'SecantGraph.kernel_split' does not depend on any axioms

## Principia.CMHodge.CMHodgeSecondDifference  (16 行)
'SecondDifference.delta_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecondDifference.cross_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecondDifference.nonpos_slot' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecondDifference.delta_lower_simple' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecondDifference.slot_min' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecondDifference.delta_lower_sharp' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecondDifference.delta_sharp_equality' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecondDifference.ratio_form' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecondDifference.region_positive' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecondDifference.boundary_t3' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecondDifference.K_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecondDifference.one_variable_positive' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecondDifference.equal_pieces' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecondDifference.equal_pieces_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecondDifference.equal_pieces_neg' depends on axioms: [propext, Classical.choice, Quot.sound]
'SecondDifference.no_full_separation' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeSheafSecant  (14 行)
'CMHodgeSheafSecant.mth_symm' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSheafSecant.mth_charpoly' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSheafSecant.mth_trace' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSheafSecant.mth_det' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSheafSecant.tg_det' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSheafSecant.ug_det' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSheafSecant.gram_unimodular' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSheafSecant.newton_e3' depends on axioms: [propext]
'CMHodgeSheafSecant.pi_from_theta_W' depends on axioms: [propext]
'CMHodgeSheafSecant.W_trace_dual' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSheafSecant.only_deg_222' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSheafSecant.multinomial_222' depends on axioms: [propext]
'CMHodgeSheafSecant.moment_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeSheafSecant.split_sheaf_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeSupportSplit  (17 行)
'SupportSplit.eq_zero_of_comp_eq_zero' depends on axioms: [propext, Quot.sound]
'SupportSplit.eq_bot_of_le_ker' depends on axioms: [propext, Quot.sound]
'SupportSplit.iSup_eq_bot_of_killed' depends on axioms: [propext, Classical.choice, Quot.sound]
'SupportSplit.restriction_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'SupportSplit.survives' depends on axioms: [propext, Classical.choice, Quot.sound]
'SupportSplit.eq_zero_of_disjoint' depends on axioms: [propext, Classical.choice, Quot.sound]
'SupportSplit.no_gluing' depends on axioms: [propext, Classical.choice, Quot.sound]
'SupportSplit.chosen_traces' depends on axioms: [propext, Quot.sound]
'SupportSplit.components_count' depends on axioms: [propext]
'SupportSplit.pieces_count' depends on axioms: [propext]
'SupportSplit.class_sum' depends on axioms: [propext, Quot.sound]
'SupportSplit.shared_pairs' does not depend on any axioms
'SupportSplit.free_components' depends on axioms: [propext]
'SupportSplit.rank_count' does not depend on any axioms
'SupportSplit.lefschetz_double' does not depend on any axioms
'SupportSplit.chi_double_theta' depends on axioms: [propext]
'SupportSplit.chi_triple_theta' depends on axioms: [propext]

## Principia.CMHodge.CMHodgeToddSecant  (14 行)
'CMHodgeToddSecant.sinh_deg3_coeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeToddSecant.G6_pairing' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeToddSecant.isotropic_J6' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeToddSecant.isotropic_J8' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeToddSecant.isotropic_todd_ratio' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeToddSecant.isotropic_J4' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeToddSecant.isotropic_J8_neg' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeToddSecant.adjunction_deg4' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeToddSecant.adjunction_deg3' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeToddSecant.fl_rank2' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeToddSecant.kt_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeToddSecant.todd_region_nonempty' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeToddSecant.witness_satisfies_kt' depends on axioms: [propext, Classical.choice, Quot.sound]
'CMHodgeToddSecant.witness_breaks_416_hypothesis' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeTraceThreeCertificate  (21 行)
'TraceThreeCertificate.amgm_nat' depends on axioms: [propext, Classical.choice, Quot.sound]
'TraceThreeCertificate.p_mem' depends on axioms: [propext, Classical.choice, Quot.sound]
'TraceThreeCertificate.p_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'TraceThreeCertificate.col1' depends on axioms: [propext, Classical.choice, Quot.sound]
'TraceThreeCertificate.col2' depends on axioms: [propext, Classical.choice, Quot.sound]
'TraceThreeCertificate.col3' depends on axioms: [propext, Classical.choice, Quot.sound]
'TraceThreeCertificate.col4' depends on axioms: [propext, Classical.choice, Quot.sound]
'TraceThreeCertificate.col5' depends on axioms: [propext, Classical.choice, Quot.sound]
'TraceThreeCertificate.col6' depends on axioms: [propext, Classical.choice, Quot.sound]
'TraceThreeCertificate.col7' depends on axioms: [propext, Classical.choice, Quot.sound]
'TraceThreeCertificate.col8' depends on axioms: [propext, Classical.choice, Quot.sound]
'TraceThreeCertificate.col9' depends on axioms: [propext, Classical.choice, Quot.sound]
'TraceThreeCertificate.col10' depends on axioms: [propext, Classical.choice, Quot.sound]
'TraceThreeCertificate.col11' depends on axioms: [propext, Classical.choice, Quot.sound]
'TraceThreeCertificate.col12' depends on axioms: [propext, Classical.choice, Quot.sound]
'TraceThreeCertificate.col13' depends on axioms: [propext, Classical.choice, Quot.sound]
'TraceThreeCertificate.col14' depends on axioms: [propext, Classical.choice, Quot.sound]
'TraceThreeCertificate.delta_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TraceThreeCertificate.T_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'TraceThreeCertificate.delta_neg' depends on axioms: [propext, Classical.choice, Quot.sound]
'TraceThreeCertificate.no_design' depends on axioms: [propext, Classical.choice, Quot.sound]

## Principia.CMHodge.CMHodgeWeilType  (10 行)
'CMHodge.nA_values' depends on axioms: [propext]
'CMHodge.weil_type_unique' depends on axioms: [propext]
'CMHodge.nB_sum_four' depends on axioms: [propext]
'CMHodge.psi_shift_closed' depends on axioms: [propext]
'CMHodge.count31F_eq' depends on axioms: [propext]
'CMHodge.adm31F_iff' depends on axioms: [propext]
'CMHodge.weil_monomials_adm' depends on axioms: [propext]
'CMHodge.conj_weil_monomials_not_adm' depends on axioms: [propext]
'CMHodge.weil_monomials_not_adm_21' depends on axioms: [propext]
'CMHodge.min_dim_twelve' depends on axioms: [propext, Quot.sound]
