== FaceCorrelationSumRule.lean
'FaceSumRule.row_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSumRule.sum_rule' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSumRule.sum_rule_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSumRule.normalized' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSumRule.proj_fixes' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSumRule.dimension_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSumRule.four_dim' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSumRule.variance_halved' depends on axioms: [propext, Classical.choice, Quot.sound]

== CoarseFaceStiffness.lean
'CoarseStiffness.h_from_angle' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseStiffness.h_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseStiffness.h_le_inv' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseStiffness.decomposition' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseStiffness.gamma_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseStiffness.ratio_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseStiffness.transpose_fix' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseStiffness.free_force_pairing' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseStiffness.free_ratio' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseStiffness.four_dim_ratio' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseStiffness.flux_tree_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseStiffness.flux_link_count' depends on axioms: [propext]
'CoarseStiffness.cs_four' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseStiffness.gamma_lower_direct' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseStiffness.gamma_min_level1_b28' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseStiffness.gamma_min_level2_b28' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseStiffness.gamma_min_level1_b54' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseStiffness.rate_gap' depends on axioms: [propext, Classical.choice, Quot.sound]

== CoarseStiffnessFirstOrder.lean
'CoarseFirstOrder.ratio_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseFirstOrder.gamma_min_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseFirstOrder.first_order' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseFirstOrder.threshold' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseFirstOrder.ledger_c' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseFirstOrder.ledger_threshold' depends on axioms: [propext, Classical.choice, Quot.sound]
'CoarseFirstOrder.ledger_at_28' depends on axioms: [propext, Classical.choice, Quot.sound]

== FaceMomentStiffness.lean
'FaceMoment.gamma_moments' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceMoment.gamma_covariances' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceMoment.forward' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceMoment.inverse' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceMoment.kurtosis' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceMoment.rescaling_keeps_slope' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceMoment.cosine_only' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceMoment.fine_intercept' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceMoment.fine_intercept_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceMoment.coarse_values' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceMoment.threshold' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceMoment.band_lower' depends on axioms: [propext, Classical.choice, Quot.sound]

== StiffnessLevelConstants.lean
'LevelConstants.w2_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevelConstants.w2_value' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevelConstants.w2_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevelConstants.cubic_to_y' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevelConstants.slope_of_kappa' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevelConstants.slope_of_gamma' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevelConstants.equal_paths' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevelConstants.fine_constants' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevelConstants.coarse_constants' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevelConstants.threshold' depends on axioms: [propext, Classical.choice, Quot.sound]
'LevelConstants.thresholds' depends on axioms: [propext, Classical.choice, Quot.sound]

== SpectralFaceMoment.lean
'FaceSpectrum.smul_log_le_log' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSpectrum.neg_log_le_chord' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSpectrum.sum_neg_log_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSpectrum.logMoment_le_per_face' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSpectrum.chord_slope_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSpectrum.single_face_case' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSpectrum.chernoff_glue' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSpectrum.tilt_range' depends on axioms: [propext, Classical.choice, Quot.sound]