{
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\Scratch.lean",
  "content": "/- Session 029 axiom audit: LiFEntire.lean (ii\u2032-5e-iv COMPLETE). -/\nimport Mathlib\nimport NguyenRH1.LiFEntire\n\nopen NguyenRH1\n\n#print axioms Fexpr\n#print axioms badPoint\n#print axioms analyticAt_digamma\n#print axioms analyticAt_digamma_div_two\n#print axioms zeta_zero_classification\n#print axioms logDeriv_zeta_sub_mult_div_eventually\n#print axioms logDeriv_zeta_eq_logDeriv_zetaA_sub\n#print axioms Fexpr_eventually_one\n#print axioms digammaSeriesPart\n#print axioms add_nat_add_one_ne_zero_of_mem_ball\n#print axioms digammaSeriesPart_analyticOn\n#print axioms digamma_eq_seriesPart_near_zero\n#print axioms Fexpr_eventually_zero\n#print axioms riemannZeta_neg_two_mul\n#print axioms integerComplement_of_mem_ball_neg_natCast\n#print axioms add_nat_add_one_ne_zero_of_mem_ball_neg\n#print axioms digammaSeriesPartSub\n#print axioms digammaSeriesPartSub_analyticOn\n#print axioms digammaSeriesPart_eq_sub_add_single\n#print axioms Hsub\n#print axioms digamma_eq_neg_inv_add_Hsub\n#print axioms Hsub_analyticAt\n#print axioms Fexpr_eventually_neg_two_mul\n#print axioms Fexpr_eventually_nontrivial\n#print axioms Fexpr_analyticAt_of_not_bad\n#print axioms exists_ball_good_of_not_bad\n#print axioms Gentire\n#print axioms gentire_eq_Fexpr\n#print axioms gentire_eventually_eq_witness\n#print axioms gentire_analyticAt_and_eq\n"
}

{
  "type": "update",
  "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\Scratch.lean",
  "content": "/- Session 029 axiom audit: LiFEntire.lean (ii\u2032-5e-iv COMPLETE). -/\nimport Mathlib\nimport NguyenRH1.LiFEntire\n\nopen NguyenRH1\n\n#print axioms Fexpr\n#print axioms badPoint\n#print axioms analyticAt_digamma\n#print axioms analyticAt_digamma_div_two\n#print axioms zeta_zero_classification\n#print axioms logDeriv_zeta_sub_mult_div_eventually\n#print axioms logDeriv_zeta_eq_logDeriv_zetaA_sub\n#print axioms Fexpr_eventually_one\n#print axioms digammaSeriesPart\n#print axioms add_nat_add_one_ne_zero_of_mem_ball\n#print axioms digammaSeriesPart_analyticOn\n#print axioms digamma_eq_seriesPart_near_zero\n#print axioms Fexpr_eventually_zero\n#print axioms riemannZeta_neg_two_mul\n#print axioms integerComplement_of_mem_ball_neg_natCast\n#print axioms add_nat_add_one_ne_zero_of_mem_ball_neg\n#print axioms digammaSeriesPartSub\n#print axioms digammaSeriesPartSub_analyticOn\n#print axioms digammaSeriesPart_eq_sub_add_single\n#print axioms Hsub\n#print axioms digamma_eq_neg_inv_add_Hsub\n#print axioms Hsub_analyticAt\n#print axioms Fexpr_eventually_neg_two_mul\n#print axioms Fexpr_eventually_nontrivial\n#print axioms Fexpr_analyticAt_of_not_bad\n#print axioms exists_ball_good_of_not_bad\n#print axioms Gentire\n#print axioms gentire_eq_Fexpr\n#print axioms gentire_eventually_eq_witness\n#print axioms gentire_analyticAt_and_eq\n",
  "structuredPatch": [
    {
      "oldStart": 1,
      "oldLines": 29,
      "newStart": 1,
      "newLines": 37,
      "lines": [
        "-/- Session 028 axiom audit: LiSeries.lean (ii\u2032-5e-iii COMPLETE). -/",
        "+/- Session 029 axiom audit: LiFEntire.lean (ii\u2032-5e-iv COMPLETE). -/",
        " import Mathlib",
        "-import NguyenRH1.LiSeries",
        "+import NguyenRH1.LiFEntire",
        " ",
        " open NguyenRH1",
        " ",
        "-#print axioms seriesTerm",
        "-#print axioms seriesFun",
        "-#print axioms one_add_normSq_gammaOf_le",
        "-#print axioms one_div_sub_add_one_div",
        "-#print axioms seriesTerm_norm_le",
        "-#print axioms finite_subtype_norm_lt",
        "-#print axioms seriesTerm_summable_majorant",
        "-#print axioms seriesSummable",
        "-#print axioms exists_ball_avoid_nontrivialZeros",
        "-#print axioms seriesFun_analyticAt",
        "-#print axioms seriesFun_analyticOnNhd",
        "-#print axioms nontrivialZero_isolated",
        "-#print axioms seriesTermSub",
        "-#print axioms seriesFunSub",
        "-#print axioms seriesTermSub_norm_le",
        "-#print axioms seriesTermSub_summable",
        "-#print axioms single_summable",
        "-#print axioms seriesFun_eq_sub_add",
        "-#print axioms seriesFun_sub_term",
        "-#print axioms seriesFunSub_analyticAt",
        "-#print axioms seriesFun_sub_self_term_analyticAt",
        "-#print axioms seriesFun_sub_polar_analyticAt",
        "+#print axioms Fexpr",
        "+#print axioms badPoint",
        "+#print axioms analyticAt_digamma",
        "+#print axioms analyticAt_digamma_div_two",
        "+#print axioms zeta_zero_classification",
        "+#print axioms logDeriv_zeta_sub_mult_div_eventually",
        "+#print axioms logDeriv_zeta_eq_logDeriv_zetaA_sub",
        "+#print axioms Fexpr_eventually_one",
        "+#print axioms digammaSeriesPart",
        "+#print axioms add_nat_add_one_ne_zero_of_mem_ball",
        "+#print axioms digammaSeriesPart_analyticOn",
        "+#print axioms digamma_eq_seriesPart_near_zero",
        "+#print axioms Fexpr_eventually_zero",
        "+#print axioms riemannZeta_neg_two_mul",
        "+#print axioms integerComplement_of_mem_ball_neg_natCast",
        "+#print axioms add_nat_add_one_ne_zero_of_mem_ball_neg",
        "+#print axioms digammaSeriesPartSub",
        "+#print axioms digammaSeriesPartSub_analyticOn",
        "+#print axioms digammaSeriesPart_eq_sub_add_single",
        "+#print axioms Hsub",
        "+#print axioms digamma_eq_neg_inv_add_Hsub",
        "+#print axioms Hsub_analyticAt",
        "+#print axioms Fexpr_eventually_neg_two_mul",
        "+#print axioms Fexpr_eventually_nontrivial",
        "+#print axioms Fexpr_analyticAt_of_not_bad",
        "+#print axioms exists_ball_good_of_not_bad",
        "+#print axioms Gentire",
        "+#print axioms gentire_eq_Fexpr",
        "+#print axioms gentire_eventually_eq_witness",
        "+#print axioms gentire_analyticAt_and_eq",
        " "
      ]
    }
  ],
  "originalFile": "/- Session 028 axiom audit: LiSeries.lean (ii\u2032-5e-iii COMPLETE). -/\nimport Mathlib\nimport NguyenRH1.LiSeries\n\nopen NguyenRH1\n\n#print axioms seriesTerm\n#print axioms seriesFun\n#print axioms one_add_normSq_gammaOf_le\n#print axioms one_div_sub_add_one_div\n#print axioms seriesTerm_norm_le\n#print axioms finite_subtype_norm_lt\n#print axioms seriesTerm_summable_majorant\n#print axioms seriesSummable\n#print axioms exists_ball_avoid_nontrivialZeros\n#print axioms seriesFun_analyticAt\n#print axioms seriesFun_analyticOnNhd\n#print axioms nontrivialZero_isolated\n#print axioms seriesTermSub\n#print axioms seriesFunSub\n#print axioms seriesTermSub_norm_le\n#print axioms seriesTermSub_summable\n#print axioms single_summable\n#print axioms seriesFun_eq_sub_add\n#print axioms seriesFun_sub_term\n#print axioms seriesFunSub_analyticAt\n#print axioms seriesFun_sub_self_term_analyticAt\n#print axioms seriesFun_sub_polar_analyticAt\n",
  "autoRead": false
}