'Komorebi.PaperIV.cyclicProjector' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.coeff_cyclicProjector' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclicProjector_eq_zero_of_residue_ne' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclicProjector_eq_of_mod_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclicProjector_idempotent' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclicProjector_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.sum_cyclicProjector' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclicProjector_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclicProjector_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclicProjector_product_packet' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclicProjector_product_other' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclic_product_law' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finiteRootAverage' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.coeff_finiteRootAverage' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finiteRootAverage_eq_cyclicProjector' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.exponentialGeneratingSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.coeff_exponentialGeneratingSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.transferSectionCoeff' does not depend on any axioms
'Komorebi.PaperIV.transferSection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.coeff_transferSection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finiteRootAverage_exp_eq_transferSection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finiteRootAverage_rescale_exp_eq_transferSection' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.derivative_exponentialGeneratingSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.iterate_derivative_exponentialGeneratingSeries' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.transferSectionCoeff_succ_of_pos' depends on axioms: [propext, Quot.sound]
'Komorebi.PaperIV.transferSectionCoeff_succ_zero' depends on axioms: [propext, Quot.sound]
'Komorebi.PaperIV.derivative_transferSection_of_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivative_transferSection_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.transferSectionCoeff_add_period' depends on axioms: [propext]
'Komorebi.PaperIV.iterate_derivative_transferSection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.constantCoeff_iterate_derivative_transferSection' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.signedSectionCoeff' depends on axioms: [propext]
'Komorebi.PaperIV.signedSection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.coeff_signedSection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedSection_eq_inv_pow_mul_transferSection' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.signedSectionCoeff_succ_of_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedSectionCoeff_succ_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivative_signedSection_of_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivative_signedSection_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedSectionCoeff_add_period' depends on axioms: [propext, Quot.sound]
'Komorebi.PaperIV.iterate_derivative_signedSection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.constantCoeff_iterate_derivative_signedSection' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.signedSection_eq_finiteRootAverage_rescale_exp' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.signedSection_zero_eq_finite_exponential_average' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.formalExpFamily' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.formalExpFamily_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.formalExpFamily_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedDenominator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.coeff_reducedDenominator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.constantCoeff_reducedDenominator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedSection_zero_eq_expand_reducedDenominator' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.negativeLogDenominator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.constantCoeff_negativeLogDenominator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.exp_subst_logOf' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.mul_derivative_logOf' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.formalExpFamily_eq_exp_subst' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.constantCoeff_reciprocalSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalSeries_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalSeries_neg_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalSeries_one_eq_inverse' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalOrdCoeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeff_zero_parameter' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeff_zero_parameter_of_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.formalExpFamily_semigroup' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.blockCoeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.blockCoeff_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocal_block_convolution' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalSeries_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeff_addition' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.egfCoeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.egfCoeff_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocal_binomial_type' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivative_rescale_exp' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivative_formalExpFamily' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.formalExpFamily_coefficient_recurrence' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.kappaCoeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedTangentSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.coeff_reducedTangentSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedDenominator_mul_reducedTangentSeries' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.reducedTangent_coefficient_convolution' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivative_reciprocalSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalSeries_coefficient_recurrence' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalOrdCoeff_newton' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.inverse_coefficient_convolution' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.constantCoeff_inverse_of_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.normalizedResidueSection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.coeff_normalizedResidueSection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.constantCoeff_normalizedResidueSection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residueInverseCoeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residueInverseCoeff_triangular' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residueInverseCoeff_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residueInverseCoeff_recurrence' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.appellSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.appellCoeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.egfCoeff_rescale_exp' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.appellCoeff_zero_parameter' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.appell_addition' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.appellCoeff_at_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.appellPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivative_appellPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.formalAppellPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivative_formalAppellPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.eval_formalAppellPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.blockCoefficientSequence' depends on axioms: [propext]
'Komorebi.PaperIV.blockCoefficientSequence_mul' depends on axioms: [propext]
'Komorebi.PaperIV.appellPolynomial_eq_sparse_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.appellPolynomial_eq_block_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residueAppellPolynomial_explicit' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.appellSeries_two_parameter' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.appell_two_parameter_convolution' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.egfConstantCoeffAction' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.egfConstantCoeffAction_X_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.egfConstantCoeffAction_residue_X_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.polynomialDifferentialEval' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.polynomialDifferentialEval_X' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.truncatedDifferentialOperator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.coeff_trunc_mul_trunc_of_lt' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.X_pow_dvd_trunc_mul_trunc_sub_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.truncatedDifferentialOperator_mul_apply_of_natDegree_le' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.truncatedDifferentialOperator_normalizedResidueSection_inverse' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.appellPolynomial_isMonicOfDegree' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.blockAppellPolynomial_isMonicOfDegree' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.eval_appellPolynomial_block_covariance' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residueAppellPolynomial_isMonicOfDegree' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.eval_residueAppellPolynomial_covariance' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.blockCoeff_rescale' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.thetaSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.thetaCoeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.thetaCoeff_reconstruction_unfactored' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.thetaCoeff_reconstruction' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.thetaSeries_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.thetaCoeff_zero_parameter' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.thetaCoeff_zero_parameter_of_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.thetaSeries_neg_one_of_even' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.thetaCoeff_neg_one_of_even_of_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclicProjector_fixed_iff_rescale_covariant' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.cyclicProjector_mem_range_iff_rescale_covariant' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.bivariateExponentialGeneratingSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.coeff_bivariateExponentialGeneratingSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.separatedExponentialGeneratingSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.coeff_separatedExponentialGeneratingSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.transferSection_addition' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residuePochhammerProduct' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.factorial_eq_residuePochhammerProduct' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residueZeroFCoeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residueZeroFSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.coeff_residueZeroFSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residueZeroFCoeff_normalization' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residueParameter_eq_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.omitted_residuePochhammer_eq_factorial' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.transferSection_eq_residueZeroFSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedSection_addition' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedDenominator_rescale_of_pow_eq_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedDenominator_map_conj' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclicAlgebraPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedCyclicAlgebraPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.CyclicAlgebra' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedCyclicAlgebra' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclicGenerator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedCyclicGenerator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclicGenerator_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedCyclicGenerator_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclicGenerator_pow_eq_mod' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedCyclicGenerator_pow_eq_mod' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclicAlgebraPowerBasis' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedCyclicAlgebraPowerBasis' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclicAlgebraPowerBasis_dim' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedCyclicAlgebraPowerBasis_dim' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclicAlgebraExponentialSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedCyclicAlgebraExponentialSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclicAlgebra_exponential_eq_sections' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedCyclicAlgebra_exponential_eq_sections' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.signedShiftPowerMatrix' depends on axioms: [propext]
'Komorebi.PaperIV.signedShiftMatrix' depends on axioms: [propext]
'Komorebi.PaperIV.signedShiftPowerMatrix_apply' depends on axioms: [propext]
'Komorebi.PaperIV.signedShiftPowerMatrix_zero' depends on axioms: [propext, Quot.sound]
'Komorebi.PaperIV.signedShiftPowerMatrix_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedShiftMatrix_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedShiftMatrix_pow_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedShiftMatrix_pow_order' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedFundamentalMatrix' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedFundamentalMatrix_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedFundamentalMatrix_neg' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedFundamentalMatrix_mul_neg' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedFundamentalMatrix_isUnit' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedDenominator_reciprocalSeries_differentialEquation' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.reciprocalOrdCoeff_parameter_equation' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeff_parameter_equation' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeff_parameter_recurrence' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeff_block_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeff_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeff_two_recurrence_form' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeff_three_recurrence_form' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeffPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.X_dvd_reciprocalCoeffPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.coeff_zero_reciprocalCoeffPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeffPolynomialOver' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.eval_reciprocalCoeffPolynomialOver' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.formalTransferTangent' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.transferTangentCoeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.transferTangentCoeff_eq_kappa' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.transferTangentCoeff_convolution' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.transferTangentCoeff_recurrence' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.transferTangentCoeff_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.differentialBellSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.differentialBellSeries_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.differentialBellSeries_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.iterate_derivative_eq_differentialBellSeries_mul' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.derivative_signedSection_zero_eq_neg_formalTransferTangent_mul' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.differentialBellSeries_neg_formalTransferTangent_eq_neg_one' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.normalizedResidueSectionAlg' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.coeff_normalizedResidueSectionAlg' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.constantCoeff_normalizedResidueSectionAlg' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.normalizedResidueSectionAlg_eq_normalizedResidueSection' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.normalizedResidueNegativeLog' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.constantCoeff_normalizedResidueNegativeLog' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residuePowerSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.constantCoeff_residuePowerSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residuePowerSeries_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residuePowerSeries_neg_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residuePowerSeries_one_eq_inverse' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residuePowerCoeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residuePowerCoeff_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residuePowerCoeff_one_eq_residueInverseCoeff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.residuePowerSeries_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residuePowerCoeff_addition' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residuePowerCoeffPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.eval_residuePowerCoeffPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.coeff_residuePowerCoeffPolynomial_parameterDegree' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.natDegree_residuePowerCoeffPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.expandedResidueNegativeLog' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.constantCoeff_expandedResidueNegativeLog' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.expand_residuePowerSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.egfCoeff_expand_residuePowerSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residueAppellPolynomialParam' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residueAppellPolynomialParam_eq_block' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residueAppellPolynomialParam_explicit' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivative_residueAppellPolynomialParam' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.eval_residueAppellPolynomialParam_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.eval_residueAppellPolynomialParam_two_parameter' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.residueAppellPolynomialParam_isMonicOfDegree' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.eval_residueAppellPolynomialParam_covariance' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.egfConstantCoeffAction_residuePowerSeries_X_pow' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.truncatedDifferentialOperator_residuePowerSeries_inverse' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.thetaPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.eval_thetaPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.natDegree_thetaPolynomial_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.X_dvd_thetaPolynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.X_add_one_dvd_thetaPolynomial_of_even' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivative_rescale_series' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.rescale_C_series' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.scaledReciprocalLogDerivative' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivative_rescale_reciprocalSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.thetaLogDerivativeSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivative_thetaSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.coeff_thetaLogDerivativeSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.thetaOrdCoeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.thetaOrdCoeff_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.thetaOrdCoeff_newton' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.factorial_mul_kappaCoeff_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.thetaCoeff_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.bellInput' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.completeExponentialBell' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.constantCoeff_bellInput' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.completeExponentialBell_generating_coefficient' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.completeExponentialBell_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.bellInput_reciprocal' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeff_bell_formula' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.coeff_one_negativeLogDenominator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.coeff_reciprocalCoeffPolynomialOver_parameterDegree' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.natDegree_reciprocalCoeffPolynomialOver' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.X_dvd_reciprocalCoeffPolynomialOver' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.exponentialSumJet' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticAt_exponentialSumJet' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hasDerivAt_exponentialSumJet' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.iteratedDeriv_exponentialSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.exponentialSum_ode' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireTransfer' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticAt_entireTransfer' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireTransfer_eq_exponentialSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hasSum_finiteRootAverage' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hasSum_entireTransfer' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireTransfer_eq_tsum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireTransfer_independent_root' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireTransfer_ode' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireSigned' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticAt_entireSigned' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hasSum_entireSigned' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireSigned_eq_tsum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireSigned_independent_roots' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireSigned_zero_eq_average' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireTransfer_derivative_at_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireTransfer_initial_data' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireSigned_eq_exponentialSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireSigned_ode' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireSigned_derivative_eq_scaled_transfer' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireSigned_initial_data' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.exponentialJetMatrix' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.exponentialJetMatrix_factor' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.det_exponentialJetMatrix' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.det_exponentialJetMatrix_constant' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticWronskian' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.transferWronskian_constant' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.transferWronskian_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedWronskian_constant' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedWronskian_eq_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hasSum_signedFundamentalMatrix_entry' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedFundamentalMatrix_first_column' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedFundamentalMatrix_diagonal' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedFundamentalMatrix_trace' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hasSum_exponentialSumJet' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireSigned_derivative_at_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hasSum_entireSigned_derivative' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedFundamentalMatrix_entry_eq_derivative' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.signedFundamentalMatrix_det' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.companionDisplacement' does not depend on any axioms
'Komorebi.PaperIV.companionDisplacement_lt' depends on axioms: [propext, Quot.sound]
'Komorebi.PaperIV.companionEntrySign' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedShiftMatrix_pow_entry_packet' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedFundamentalMatrix_entry' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.aeval_signedShiftMatrix_first_column' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedShiftMatrix_no_small_annihilator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.aeval_signedShiftMatrix_X_pow_add_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedShiftMatrix_charpoly' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedShiftMatrix_mem_spectrum_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedShiftMatrix_charpoly_separable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedShiftMatrix_charpoly_roots_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedShiftMatrix_charpoly_roots_nodup' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.ode_all_derivatives_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_ode_zero_of_initial_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_ode_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.transferCombination' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticAt_transferCombination' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.transferCombination_derivative' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.transferCombination_ode' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.transferCombination_initial' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireTransfer_solution_expansion' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.transferCombination_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_eq_of_all_derivatives' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_derivative_of_formal' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireTransfer_derivative_of_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireTransfer_derivative_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireSigned_derivative_of_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireSigned_derivative_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalPrimitiveRoot' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedRoot' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalPrimitiveRoot_isPrimitive' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedRoot_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedFundamentalMatrix_det_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.norm_signedRoot' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.norm_entireSigned_zero_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireSigned_two_eq_cos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireSigned_two_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireSigned_two_zero_derivative_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireSigned_two_zero_iff_nat' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireSigned_two_zero_order_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.orderTwo_zero_spacing' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.oddExponentialCenter' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.near_cancellation_exists' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.oddExponentialCenter_separation' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.near_cancellation_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedCombination' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedCombination_eq_transfer' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireSigned_solution_expansion' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedCombination_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.norm_one_add_lower_half' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.log_one_add_lipschitz_half' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.logarithmicZeroMap' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.logarithmicZeroMap_mapsTo' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.logarithmicZeroMap_lipschitz' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.logarithmicZeroMap_fixed_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.perturbed_exponential_unique_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.perturbed_exponential_zero_distance' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.perturbed_exponential_pointwise_distance' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hasDerivAt_perturbed_exponential' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.perturbed_exponential_zero_derivative_lower' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.perturbed_exponential_zero_order_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.perturbed_exponential_derivative_error' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.norm_log_one_add_sub_self_half' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.perturbed_exponential_first_correction' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finiteExponentialRemainder' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticAt_finiteExponentialRemainder' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hasDerivAt_finiteExponentialRemainder' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.iteratedDeriv_finiteExponentialRemainder' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finiteExponentialRemainder_strip_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finite_two_term_normalization' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedExponentialRemainder' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signed_two_term_normalization' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signed_two_term_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedVertex' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedPolygonGap' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedVertex_exp' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedVertex_re' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedVertex_im' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.norm_canonicalSignedVertex' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedVertex_last_angle' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedVertex_last_re' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedVertex_last_im' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedPolygonGap_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedVertex_re_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedRemainder_strip_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedVertex_adjacent_difference' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedZeroFrequency' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedZeroCenter' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signed_sine_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedZeroFrequency_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedZeroCenter_cancellation' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedRemainder_disk_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedRemainder_eventually_small_on_disks' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_conj' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_eventual_local_zero' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_unique_zero_real' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_local_zero_simple' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_eventual_positive_simple_zeros' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_local_zero_exponential_distance' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_local_strings' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_zero_lattice_distance' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.signedRemainderScale' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedRemainderEnvelope' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedRemainderEnvelope_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedRemainderEnvelope_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_first_correction' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.signedRemainderEnvelope_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_normalized_derivative_error' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.signedFundamentalSector' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signed_cosine_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cosine_arc_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedVertex_upper_boundary' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedVertex_upper_projection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedVertex_sector_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finite_one_term_normalization' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finite_exponential_zero_balance' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedSectorWidth' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_upper_sector_zero_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_sector_zero_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.signedSectorWidth_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedRemainder_eventually_small_on_strip' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signed_integer_center' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_sector_exhaustion' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_rotation' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedFundamentalSector_polar' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.exists_signed_sector_rotation' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_global_exhaustion' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.signedZeroFrequency_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_order_rotation' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_derivative_rotation' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.positive_real_rotation_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedZeroCenter_disk_index_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_large_zero_orbits' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.signedNormalizationFactor' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedNormalizationFactor_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_derivative_normalization' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_relative_derivative_error' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.signed_derivative_leading_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_derivative_modulus_error' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.signedFundamentalSector_of_arg' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedRemainder_three_jet_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_two_term_dominance' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_finite_zeros_on_compact' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.onSignedZeroRay' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_eventually_simple_on_rays' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_finite_exceptional_zeros' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedDenominator_coeff_complex' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedDenominator_coeff_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedDenominator_entire_radius' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticAt_entireReducedDenominator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hasSum_entireReducedDenominator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_eq_reduced_power' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_order_eq_reduced' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.exists_complex_nth_root' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_zero_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_finite_zeros_on_compact' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.onSignedZeroRay_power_positive' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_finite_exceptional_zeros' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_eventually_positive_simple' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_two_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_two_zero_order_one' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.isLocalizedPositiveZero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedPositiveZero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedPositiveZero_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedPositiveZero_eq_of_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedPositiveZero_local_strings' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedPositiveZero_global_strings' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedZeroCenter_ge_radius' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedPositiveZero_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedPositiveZero_injective_on_tail' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedPositiveZero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedPositiveZero_global_strings' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedPositiveZero_injective_on_tail' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedPositiveZero_local_strings' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedZeroCenter_tendsto_atTop' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedPositiveZero_sub_center_isBigO_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedPositiveZero_equivalent_center' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedPositiveZero_tendsto_atTop' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedPositiveZero_equivalent_center_power' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.signedPositiveZero_reciprocal_rpow_summable_iff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.reducedPositiveZero_reciprocal_rpow_summable_iff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.reducedPositiveZero_reciprocal_summable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.sequenceCounting' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.lattice_window_counting' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedPositiveZero_lattice_windows' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedPositiveZero_tail_counting' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedTailProduct' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedPositiveZero_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedTail_reciprocal_summable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedTail_factors_norm_summable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedTailProduct_multipliable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedTailProduct_uniform_on_compact' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedTailProduct_locally_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticAt_reducedTailProduct' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedTailProduct_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedTailProduct_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedTailProduct_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finiteWeight' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finiteWeight_of_finite' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finiteWeight_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finiteWeight_union_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finiteWeight_eq_ncard' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finiteWeight_between_tail_and_exceptions' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.zeroDisk' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticZeroCount' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_analyticOrderAt_ne_top' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_order_ne_top' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_order_ne_top' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_zeroDisk_finite' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_zeroDisk_finite' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedZeroEnumeration_exists_ge_three' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedZeroEnumeration_exists_two' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedZeroEnumeration_exists' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalZeroEnumeration' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.orbit' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.orbit_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.orbit_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.orbit_zero_simple' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.orbitDisk' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.exceptions' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.exceptions_finite' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.orbitDisk_finite_card' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.orbitDisk_subset' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.zeroDisk_subset_union' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.weighted_count_bounds' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_zero_counting' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.reducedRoot' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.reducedDisk' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.reducedExceptions' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.reducedRoot_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.reducedRoot_injective' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.reducedRoot_zero_simple' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.reducedExceptions_finite' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.reducedDisk_finite_card' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.reducedDisk_subset' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.reducedZeroDisk_subset_union' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.reduced_weighted_count_bounds' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_zero_counting_power' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_zero_counting' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.ZeroPowerSummable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.summable_iff_comp_of_finite_complement' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.root_equivalent_lattice' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.root_reciprocal_rpow_summable_iff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.reducedRoot_reciprocal_rpow_summable_iff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.orbitZero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.orbitZero_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.orbitZero_finite_complement' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.reducedZero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.reducedZero_injective' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.reducedZero_finite_complement' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_zero_power_summable_iff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_zero_power_summable_iff' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_reciprocal_zeros_summable' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.weightedDirichletTerm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.weightedDirichletTerm_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.weightedDirichletTerm_differentiable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.weightedDirichletTerm_strip_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.weightedDirichlet_locally_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.weightedDirichlet_differentiableOn' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.absoluteZeroZetaTerm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.absoluteZeroZeta' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.zero_norm_pos_of_value_at_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.absoluteZeroZetaTerm_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.absoluteZeroZeta_summable_norm_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.absoluteZeroZeta_locally_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.absoluteZeroZeta_differentiableOn' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_zeta_absolute_convergence' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_zeta_locally_uniform' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_zeta_holomorphic' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_zeta_absolute_convergence' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_zeta_locally_uniform' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_zeta_holomorphic' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedPositiveZero_derivative_asymptotic' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedPositiveZero_unique_global_strings' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedPositiveZero_derivative_rotation' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_large_zero_strings' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.entireSigned_canonical_conj' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireSigned_canonical_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_derivative_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signed_sine_mul_center' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedZeroCenter_positive_phase' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedZeroCenter_negative_phase' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedDerivativeScale' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedDerivativeMainTerm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedDerivativeScale_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedDerivativeMainTerm_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signed_derivative_leading_phase' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedLeadingCorrection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedLeadingCorrection_eq_real_quotient' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedLeadingCorrection_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedRemainderEnvelope_center_tendsto_zero' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.signedPositiveZero_first_correction' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.norm_real_phase_sub_one_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.relative_error_through_unit_phase' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedPositiveZero_signed_derivative_asymptotic' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.signedPositiveZero_eventual_derivative_sign' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.signedPolygonGap_three' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedZeroCenter_three' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedVertex_three_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedVertex_three_two' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedExponentialRemainder_three' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedLeadingCorrection_three' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedPositiveZero_three_correction' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_derivative_lower_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_derivative_power_bound' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.branchedDirichletTerm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.branchedDirichletTerm_differentiable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.branchedDirichletTerm_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.branchedDirichletTerm_strip_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.branchedDirichlet_summable_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.branchedDirichlet_locally_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.branchedDirichlet_entire' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.branchedDirichlet_halfplane' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SimpleZeros' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SimpleZeros.toZero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SimpleZeros.toZero_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SimpleZeros.order_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_simple_zero_power_summable' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.simple_logarithm_re' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivativeZeroWeight' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivativeZeroWeight_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivativeZeroWeight_power_summable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_two_derivative_norm' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.derivativeZeroWeight_two_power_summable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivativeWeightedZeroZetaTerm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivativeWeightedZeroZeta' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivativeWeightedZeroZetaTerm_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivativeWeightedZeroZeta_summable_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivativeWeightedZeroZeta_two_summable_norm' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.derivativeWeightedZeroZeta_entire' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.derivativeWeightedZeroZeta_two_holomorphic' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.positiveZetaTerm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.exponentialZetaDifference' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.positiveZetaTerm_entire' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.exponentialZetaDifference_entire' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.real_log_lipschitz_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.positiveZetaTerm_norm_le_rpow' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.exponentialZetaDifference_factor' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.summable_polynomial_exponential' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.exponentialZetaDifference_majorant' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.exponentialZetaDifference_locally_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.exponentialZetaDifference_sum_entire' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hurwitzRegularPart' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hurwitzRegularPart_entire' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hurwitzZeta_meromorphicAt' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hurwitzLatticeModel' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hurwitzLatticeModel_meromorphicAt' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hurwitzLatticeModel_differentiableAt' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hurwitzLatticeModel_residue' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.meromorphicOrderAt_eq_neg_one_of_residue' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.positiveZetaTerm_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.positiveZetaTerm_eq_cpow' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.positiveZetaTerm_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.positiveZetaTerm_lattice_hasSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedZeroCenter_positive' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedZeroCenter_reciprocal_square_summable' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.root_tendsto_atTop' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.latticeCorrection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.latticeCorrection_locally_uniform' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.latticeCorrection_entire' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.positiveZetaTerm_summable' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.latticePrefix' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.latticePrefix_entire' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.root_zeta_eq_model' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.tsum_injection_add_complement' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finite_subtype_tsum_entire' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.reducedExceptionZeta' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.absoluteExceptionZeta' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.absoluteZeroZetaTerm_entire' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.reducedExceptionZeta_entire' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.absoluteExceptionZeta_entire' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.reducedZetaTerm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.orbitZetaTerm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.reducedZeta_decomposition' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.absoluteZeta_decomposition' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.reducedZetaCorrection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.absoluteZetaCorrection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedZetaCorrection_entire' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.absoluteZetaCorrection_entire' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_zeta_eq_hurwitz' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_zeta_eq_hurwitz' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedZetaContinuation' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.absoluteZetaContinuation' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedZetaContinuation_meromorphic' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.absoluteZetaContinuation_meromorphic' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedZetaContinuation_holomorphic_off_pole' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.absoluteZetaContinuation_holomorphic_off_pole' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.entire_add_preserves_residue' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedZetaContinuation_residue' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.absoluteZetaContinuation_residue' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedZetaContinuation_simple_pole' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.absoluteZetaContinuation_simple_pole' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.branchedZeroZetaTerm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.branchedZeroZeta' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.branchedZeroZetaTerm_entire' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.RealLogOnReducedTail' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedBranchCorrection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedBranchCorrection_entire' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.branchedZeroZetaTerm_eq_absolute_on_tail' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.branchedReducedZeta_summable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.branchedReducedZeta_eq_absolute_add_entire' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.branchedReducedZetaContinuation' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.branchedReducedZetaContinuation_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.branchedReducedZetaContinuation_meromorphic' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.branchedReducedZetaContinuation_holomorphic_off_pole' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.branchedReducedZetaContinuation_residue' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.branchedReducedZetaContinuation_simple_pole' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.branchedReducedZetaContinuation_difference_entire' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.quartic_root_square' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_four_eq_cos_cosh' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.complex_cos_zero_iff_nat' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.quarticPositiveZero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.quarticPositiveZero_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.quarticPositiveZero_div_sqrt' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_four_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.quarticPositiveZero_simple' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_four_zero_order_one' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.exactLatticeEnumeration' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.reducedZero_surjective_of_orbitZero' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.SignedZeroEnumeration.exceptions_zero_of_surjective' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.zero_zeta_exact_of_lattice' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedZeroCenter_four' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.orderTwo_full_lattice' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.orderFour_full_lattice' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.orderTwo_exact_zero_zeta_models' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.orderFour_exact_zero_zeta_models' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_zero_of_halfplane' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.zero_zeta_corrections_of_lattice' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.orderTwo_zeta_corrections_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.orderFour_zeta_corrections_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.ZeroMultiplicityIndex' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.indexedZero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.fullCanonicalProduct' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.zeroMultiplicity_reciprocal_summable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.fullCanonicalProduct_factors_summable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.fullCanonicalProduct_multipliable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.fullCanonicalProduct_uniform_on_compact' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.fullCanonicalProduct_locally_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.fullCanonicalProduct_entire' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.fullCanonicalProduct_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.fullCanonicalProduct_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.fullCanonicalProduct_zero_iff_index' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.indexedZero_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_zero_multiplicity_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.fullCanonicalProduct_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.zeroMultiplicityIndex_countable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_full_product_properties' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.reciprocalProduct' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalProduct_locally_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalProduct_entire' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalProduct_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.zeroIndexFiberEquiv' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.otherZeroProduct' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.otherZeroProduct_entire' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.otherZeroProduct_ne_zero_at_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.fullCanonicalProduct_factor_at_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.linear_zero_factor_order' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.fullCanonicalProduct_order_at_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.fullCanonicalProduct_same_orders' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_full_product_same_orders' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.canonicalProductQuotient' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.rawCanonicalProductQuotient_meromorphic' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.rawCanonicalProductQuotient_order_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalProductQuotient_entire' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalProductQuotient_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalProductQuotient_eq_div' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.fullCanonicalProduct_times_quotient' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalProductQuotient_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_product_quotient' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_normalized_exists_log' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_realPart_sublinear_constant' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_zeroFree_sublinear_logNorm_eq_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_product_quotient_has_log' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.entire_logCounting_poles_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_normalized_proximity_inv_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_eventually_codiscrete_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_quotient_proximity_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_re_le_three_proximity_exp' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_proximity_le_of_growth' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_sublinear_factor_rigidity' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.log_one_add_le_rpow_div' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.zeroMultiplicity_reciprocal_rpow_summable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalPowerMass' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalPowerMass_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.fullCanonicalProduct_growth' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_norm_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_and_product_growth' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_quotient_eq_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_eq_fullCanonicalProduct' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_hadamard_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_hadamard' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.zeroPartialFraction' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.zeroPartialFraction_uniform_majorant' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.zeroPartialFraction_norm_summable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.zeroPartialFraction_uniform_on_compact' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.logDeriv_linear_factor' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.fullCanonicalProduct_logDeriv' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_partialFractions' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.zeroPartialFraction_locally_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTransferTangent' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTransferTangent_eq_reduced_logDeriv' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.analyticTransferTangent_mittagLeffler' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTransferTangent_mittagLeffler_absolute' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.analyticTransferTangent_mittagLeffler_locally_uniform' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.locally_uniform_sum_deriv' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.zeroResolventJet' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.zeroResolventJet_hasDerivAt' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.zeroResolventJet_locally_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.zeroPowerSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.zeroPowerSum_hasSum_from_resolvent' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.zeroPowerSum_resolvent_derivative' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_iteratedDeriv_zero' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.zeroResolvent_analyticAt_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedZeroPowerSum_convolution' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.zeroMomentSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedDenominator_mul_zeroMomentSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.kappaCoeff_eq_zeroPowerSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedZeroPowerSum_newton' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.transferTangentCoeff_zero_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTransferTangent_coefficient_hasSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.bellInput_zero_sums' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeff_zero_sum_bell' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.powerSeries_linear_ode_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.thetaZeroBellInput' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.thetaZeroBellInput_derivative' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.thetaSeries_eq_zero_bell_exp' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.thetaCoeff_zero_sum_bell' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.differentiableOn_ball_taylor_hasSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedZeroPowerSum_logarithm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedZeroPowerSum_resolvent_hasSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finite_positive_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finite_exponential_dominant_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finite_exponential_dominant_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.unit_complex_re_lt_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedVertex_injective' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedVertex_mul_star_self' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_dominant_ray' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diskMaximumModulus' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireGrowthOrder' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireExponentialType' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.norm_le_diskMaximumModulus' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diskMaximumModulus_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.log_growth_ratio_of_exp_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.order_ratio_of_log_growth' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_ray_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_maximum_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_type_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_order_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_order_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_type_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_maximum_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_growth_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_order_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireReducedDenominator_order_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.rayDirection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.norm_rayDirection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedProjection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedIndicator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedProjection_cos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedIndicator_cos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.continuous_signedProjection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.continuous_signedIndicator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedProjection_le_indicator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedVertex_sum_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedIndicator_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedVertex_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signed_root_in_vertices' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.unit_complex_same_real' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signed_maximizer_strict_of_not_tie' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedTieDirection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedTieDirection_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.range_erase_nonempty' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.vertexProjectionGap' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.directionSeparation' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.continuous_vertexProjectionGap' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.continuous_directionSeparation' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.directionSeparation_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.compact_directions_uniform_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_dominant_error' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_compact_dominant_sectors' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.alignedRadii' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.alignedRadii_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.alignedRadii_phase' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.alignedRadii_equal_projection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.alignedRadii_lower_projection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finite_unit_exponential_aligned_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.log_norm_slope_of_normalized_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_indicator_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_log_indicator_upper' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_real_normalization' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_indicator_sequence' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.limsup_eq_of_upper_and_sequence' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_indicator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_indicator_nonzero_radii' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.IsHilbertTraceClass' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalHilbertBasis' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalHilbertBasis_inner' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalHilbertBasis_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalHilbertBasis_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalRankOne' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalRankOne_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalRankOne_summable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalOperator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalOperator_traceClass' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalOperator_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalOperator_apply_basis' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalOperator_pow_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hilbertBasis_hasSum_squared_coordinates' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonal_trace_double_summable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hilbertBasisTrace' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalOperator_trace_in_any_basis' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalOperator_trace_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalOperator_pow_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalOperator_pow_trace' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalCompression' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalCompression_eq_diagonal' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalCompression_determinant' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalFredholmDeterminant' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.diagonalFredholmDeterminant_compression_limit' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.reducedZeroEigenvalue' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedZeroEigenvalue_norm_summable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedZeroOperator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedZeroOperator_traceClass' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedZeroOperator_basis' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedZeroOperator_fredholm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedZeroOperator_trace_power' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reducedZeroOperator_finite_determinants_uniform' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.powerSumLog' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.powerSumLog_constantCoeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.powerSumLog_derivative_coeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.homogeneousSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.homogeneousCoeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.homogeneousSeries_constantCoeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.homogeneousSeries_derivative' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.homogeneousCoeff_recurrence' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.homogeneousGeometric' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.homogeneousGeometric_coeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.homogeneousGeometric_constantCoeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.homogeneousGeometric_inverse' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.homogeneousGeometric_derivative' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finiteHomogeneousSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finiteHomogeneousSeries_constantCoeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finiteHomogeneousSeries_derivative' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finiteHomogeneousSeries_eq_homogeneous' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finiteHomogeneousSeries_monomials' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.summable_norm_positive_powers' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.homogeneousCoeff_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.homogeneousCoeff_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.homogeneousCoeff_continuous' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.homogeneousSeries_congr_positive' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.completeHomogeneous' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finiteHomogeneousSeries_coefficient_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.completeHomogeneous_monomial_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.repeatedEigenvalue' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.repeatedEigenvalue_norm_summable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.repeatedEigenvalue_powerSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalSeries_eq_homogeneous_zero_sums' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeff_completeHomogeneous' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeff_symmetric_polynomial_continuation' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.entireNormalizedSection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.normalizedSection_coeff_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.normalizedSection_entire_radius' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticAt_entireNormalizedSection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hasSum_entireNormalizedSection' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireNormalizedSection_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireNormalizedSection_iteratedDeriv_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireNormalizedSection_transfer' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireTransfer_unit_norm_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finite_sum_le_finsum_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_divisor_eq_orderNat' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_zero_finite_weight_growth' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_zero_subtype_weight_growth' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_zero_bounded_finite' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.weighted_growth_summable_large' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.weighted_growth_summable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_growth_zeroPowerSummable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entire_sublinear_growth_hadamard' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireNormalizedSection_norm_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.normalizedSectionGrowthConstant' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.normalizedSectionGrowthConstant_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireNormalizedSection_disk_growth' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireNormalizedSection_zeroPowerSummable' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireTransfer_positive_ray' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.log_growth_ratio_of_polynomial_exp_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireTransfer_positive_ray_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireNormalizedSection_maximum_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireNormalizedSection_growth_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireNormalizedSection_order_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireNormalizedSection_hadamard' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireNormalizedSection_hadamard_uniform' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries_entireNormalizedSection' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.normalized_zeroMomentSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.normalized_zeroPowerSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.bellInput_normalized_zeros' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residuePowerCoeff_zero_sum_bell' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.powerSeries_eq_of_derivative_constant' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries_log' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries_exp' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.normalizedAnalyticPower' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.normalizedAnalyticPower_taylor' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.normalizedAnalyticPower_zero_sum_bell' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries_coeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries_constantCoeff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries_congr' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries_mul' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries_const' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries_inverse_product' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries_neg' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries_deriv' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries_zeroResolvent' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hadamard_taylor_zeroMoment_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorCoefficient' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorCoefficient_norm_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorCoefficient_isBigO' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorCoefficient_block_error' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.principalPartSeries' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.principalPartSeries_coefficient' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.principalPartSeries_inverse' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.lower_principal_part_choose_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.poleTerm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.polePrincipalPart' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.rawPoleRemainder' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.poleTerm_analyticAt' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.poleTerm_meromorphicAt' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.polePrincipalPart_analyticAt' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.rawPoleRemainder_meromorphic' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.rawPoleRemainder_analyticAt' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.meromorphicOrderAt_nonneg_of_bounded' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.rawPoleRemainder_bounded_at_pole' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.removedPoleRemainder' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.removedPoleRemainder_analyticOnNhd' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.removedPoleRemainder_eq_raw' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries_sub' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries_finsetSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries_id' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries_poleTerm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorCoefficient_principalPart' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries_canonicalSignedDenominator' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'Komorebi.PaperIV.reciprocalSeries_nat' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTaylorSeries_reciprocal_signed' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeff_analyticTaylor' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.poleNumerator' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalPoleCoefficient' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.poleNumerator_analyticAt' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalPoleCoefficient_leading' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.poleNumerator_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.polePrincipalPart_scaled' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalPoleCoefficient_local_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.polePrincipalPart_scaled_general' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.polePrincipalPart_scaled_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.principalPart_leading_coefficient' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.removedPoleRemainder_taylor' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.nearest_pole_taylor_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeff_nearest_pole_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.principalCoefficientSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.leadingPoleCoefficient' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.lowerPrincipalConstant' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.lowerPrincipalConstant_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.lowerPrincipalConstant_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.principalCoefficientSum_split' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.principalCoefficientSum_leading_error' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.principalCoefficientSum_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeff_leading_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.leadingZeroWeight' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.leadingZeroWeight_rotation' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.leadingPoleCoefficient_eq_zero_weights' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.leading_zero_sum_orbit_reduction' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeff_orbit_leading_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cosineNearestZeros' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_two_cos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cosineNearestZeros_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cosineNearestZeros_root' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cosineNearestZeros_simple' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cosine_nearest_zero_exhaustion' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.secant_leading_coefficient' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.secant_coefficient_error' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.secantMainTerm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.secantMainTerm_norm' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.secantMainTerm_ne_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.secant_relative_error' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.secant_coefficient_ratio_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.secant_coefficient_asymptotic' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.pointwiseRootAverage' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.root_weight_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.mapsTo_root_pow' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.pointwiseRootAverage_covariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.pointwiseRootAverage_of_covariant' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.pointwiseRootAverage_projector' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.pointwiseRootAverage_resolution' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.differentiableOn_pointwiseRootAverage' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.pointwiseRootAverage_range_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.pointwiseRootAverage_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.pointwiseRootAverage_product' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.pointwiseRootAverage_hasSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.pointwiseRootAverage_scaled_exp' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireTransfer_addition' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signed_addition_weight' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireSigned_addition' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.IsLogarithmOn' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.logarithmPower' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.logarithmPower_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.IsLogarithmOn.nonzero' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.IsLogarithmOn.deriv' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hasDerivAt_logarithmPower' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocal_fixed_log_derivative' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticDifferentialBell' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticOnNhd_differentialBell' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.iteratedDeriv_eq_analyticDifferentialBell' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analytic_higher_riccati' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.truncatedDifferentialOperator_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.truncatedDifferentialOperator_egfAction' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residueAppell_operator_forward' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residueAppell_operator_inverse' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.canonicalSignedDenominator_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTransferTangent_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.transferTangentCoeff_one_order' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTransferTangent_one_hasSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.analyticTransferTangent_hasSum_all_orders' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeff_two_compact' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalCoeff_three_compact' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.newtonHessenberg' depends on axioms: [propext, Quot.sound]
'Komorebi.PaperIV.newtonHessenberg_det' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.reciprocalOrdCoeff_newton_determinant' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residueHypergeometricParameters' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residueHypergeometricParameters_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residueHypergeometricParameters_re_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.regularized_zeroF_normalization' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residueHypergeometric' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.residueHypergeometric_hasSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.entireTransfer_hypergeometric' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.finiteAlgebraExponential' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hasSum_cyclicAlgebra_exponential' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.hasSum_signedAlgebra_exponential' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclicAlgebraNormedAddCommGroup' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclicAlgebraNormedSpace' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedAlgebraNormedAddCommGroup' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedAlgebraNormedSpace' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.cyclicAlgebra_pointwise_exponential' depends on axioms: [propext, Classical.choice, Quot.sound]
'Komorebi.PaperIV.signedAlgebra_pointwise_exponential' depends on axioms: [propext, Classical.choice, Quot.sound]
FAIL-CLOSED PAPER IV v1.0.0 KERNEL AUDIT PASS: 2234 declarations (1999 theoremInfo); 1164 explicit mapped targets; allowed axioms only: propext, Classical.choice, Quot.sound
