audit-session013-axioms.txt
139 declarations audited · 5 sorryAx — intended skeletons · updated 08-20-2026
Raw #print axioms transcript
'NguyenRH1.Bn' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Bn_FAlt_100000_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Bn_FAlt_80000_ge' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Bn_FAlt_80000_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.C0hat' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.FAlt' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.FAlt_psi_neg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Ffactor' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Hhat' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.IIMaj' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.IIMaj_deriv2_lt' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.IIMaj_eq_psiTilde_sqrt' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.IIMaj_le_two_mul' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.IIMaj_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.IsKernelDiagonal' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.LiVerifiedUpTo' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.R003_exact_factorization' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound] 'NguyenRH1.RHUpTo' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.SInfty' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.Sf' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.SfBoundProp' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.bern_term_lower' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.bern_term_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.bern_term_upper' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.block_range_bounds' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.chain_rule_sqrt' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.chain_rule_sqrt_shift' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.chain_rule_sqrt_shift_on' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_FAlt' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_L1' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_L1L2' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_L1sq' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_L2' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_L2sq' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_TL1' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_TL2' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_mFblock' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_mIIM' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_mIdb' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_mL1L2b' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_mL1b' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_mL1sqb' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_mL2b' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_mL2sqb' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_mS' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_mTL1b' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_mTL2b' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_marginExpanded' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.contDiffOn_sqrt_shift' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.continuousOn_marginExpanded' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.deriv2_add' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.deriv2_const_mul' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.deriv2_const_val' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.deriv2_of_hasDerivAt_nhds' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.deriv2_psiTilde' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.deriv_psiTilde' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.exp_eleven' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.exp_five' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.exp_four' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.exp_le_inv_sub_sixteen' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.exp_one_pow_ge' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.exp_one_pow_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.harmonic_lower' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.harmonic_upper' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.hasDerivAt_T_mul_log' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.hasDerivAt_log_log' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.hasDerivAt_log_log_unshifted' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.hasDerivAt_log_shift' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.hasDerivAt_marginS' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.hasDerivAt_psiTilde' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.iim_u2_antitone' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.iimaj_bracket_bound' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.lagariasA1' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.lagariasC1' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.lambda_pos_finite_height' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.lambda_pos_finite_height_verified' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.liCoeff' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.log100000_ge' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.log80000_ge' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.log80000_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.logpi_ge' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.logpi_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.mapsTo_sqrt_shift' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.mapsTo_sqrt_shift_Ici_Ioi1' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.mapsTo_sqrt_shift_Ioi1' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.marginS_deriv2' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.marginTilde' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.marginTilde_FAlt_80000_lt_100000' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.marginTilde_FAlt_80000_pos' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.marginTilde_convex' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.marginTilde_eq_expanded' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.marginTilde_eq_sub' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.oddHarm_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.oddHarm_lower' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.pos_of_convex_of_base' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.pos_of_convex_of_two_points' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_T_mul_log' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_T_mul_log_log_shift' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_T_mul_log_log_shift_neg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_T_mul_log_neg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_T_mul_log_shift' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_T_mul_log_shift_neg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_id' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_log' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_log_log' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_log_log_neg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_log_log_shift' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_log_log_shift_neg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_log_log_sq_shift' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_log_log_sq_shift_neg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_log_mul_log_shift' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_log_mul_log_shift_neg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_log_neg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_log_shift' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_log_shift_neg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_log_sq_shift' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_log_sq_shift_neg' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiOf_sqrt_rel' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.psiTilde_contDiff' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sInf_partial_lower' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sInf_series_summable' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sInftyLower' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sInftyLower_100000_lo' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sInftyLower_80000_lo' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sInftyLower_80000_up' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sInftyLower_eq'' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sInfty_lower_bound' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sineSkeleton' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sqrt100000_ge' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sqrt100000_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sqrt80000_ge' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sqrt80000_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.suzukiW' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.valley_floor_lower_isolated' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound] 'NguyenRH1.valley_floor_upper' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound] 'NguyenRH1.valley_plateau_upper' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound] 'NguyenRH1.valley_profile' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound] 'NguyenRH1.xiFun' depends on axioms: [propext, Classical.choice, Quot.sound]