Issues

• FREEZE: daily mathlib bump 2026-09-01 in progress

  freeze:active
  CBirkbeck/AINTLIB#8576 · Filter by author CBirkbeck opened on Sep 1, 2026
  1

• ModularCurves: repair 4 ProjectiveSpaceTwist proofs that run away under the rc2 kernel, then re-wire the subtree (149 modules) into the library root

  CBirkbeck/AINTLIB#8574 · Filter by author CBirkbeck opened on Aug 26, 2026
  2

• decompose: remove maxHeartbeats from PadicLFunctions.seriesEval_mul

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8534 · Filter by author CBirkbeck opened on Jul 17, 2026

• decompose-proof: BernoulliRegular/Reflection/Local/ComponentDimension/CharacterProjectionFinrankOne.lean::completedPrincipalUnitModPEigenspace_mem_filtration_succ_of_exists_pow_ne@L112

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8366 · Filter by author CBirkbeck opened on Jul 16, 2026

• decompose-proof: HasseWeil/Foundation/EC/TranslateValuation.lean::pointValuation_translateAlgEquivOfPoint_of_le_one@L1396

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8364 · Filter by author CBirkbeck opened on Jul 16, 2026

• decompose-proof: HasseWeil/Foundation/EC/MulByIntUnramified.lean::ord_P_mulByInt_y_sub_const_eq_one@L1050

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8363 · Filter by author CBirkbeck opened on Jul 16, 2026

• decompose-proof: DedekindResidue/MainTheorem.lean::zero_sum_le_sq@L47

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8361 · Filter by author CBirkbeck opened on Jul 16, 2026

• decompose-proof: WronskianAux::wronskian_aux_four — fit default maxHeartbeats via the quotient-ring route (from #7205)

  lane:decomposestate:in-progress
  CBirkbeck/AINTLIB#8329 · Filter by author CBirkbeck opened on Jul 16, 2026
  

• decompose-proof: BernoulliRegular/Reflection/WeakSplitting/UniformResidueDegree.lean::idealNormMultiplicity_prime_pow_mul_d_eq_card_sym_of_uniform@L217

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8291 · Filter by author CBirkbeck opened on Jul 16, 2026

• decompose-proof: BernoulliRegular/Reflection/WeakSplitting/MultiGeometric.lean::norm_summable_and_prod_eq@L117

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8289 · Filter by author CBirkbeck opened on Jul 16, 2026

• decompose-proof: BernoulliRegular/Reflection/SingularKummer/LocalizationKernel/LocalToCompletedBridge.lean::fieldUnitToCyclotomicLocalUnitPowerQuotient_equivariant_generator@L704

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8287 · Filter by author CBirkbeck opened on Jul 16, 2026

• decompose-proof: BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/PrincipalUnitFactor/ConjNormSemiPrimaryAndUnitFactorData.lean::dvd_exponent_of_neg_one_pow_mul_zeta_pow_isSemiPrimary@L323

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8278 · Filter by author CBirkbeck opened on Jul 16, 2026

• decompose-proof: BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/KummerFurtwaengler/StickelbergerIdealOrbit.lean::pthSymbolAtPrime_galoisAction_exists_unit@L314

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8275 · Filter by author CBirkbeck opened on Jul 16, 2026

• decompose-proof: BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/IrelandRosen/Theorem1/CanonicalPrimeSourceData.lean::residueCharInt_eq_teichUnitFullOfRootsOfUnityBijective_pow_d@L363

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8274 · Filter by author CBirkbeck opened on Jul 16, 2026

• decompose-proof: BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/IrelandRosen/PrimeSource.lean::reciprocalPrimePhiElement_conj_mul_self_eq_absNorm_pow@L307

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8273 · Filter by author CBirkbeck opened on Jul 16, 2026

• decompose-proof: BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/IrelandRosen/IdealNorm.lean::idealNormReciprocity_of_primePhiFamilyFacts@L113

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8272 · Filter by author CBirkbeck opened on Jul 16, 2026

• decompose-proof: BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/DworkFactorization/WittCarry/TraceCarryTeichmullerExpansion.lean::exists_traceNatCast_sub_teichFrobeniusSum_eq_natCast_ell_mul_wittTheta@L517

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8269 · Filter by author CBirkbeck opened on Jul 16, 2026

• decompose-proof: BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/DworkFactorization/WittCarry/ProductBaseComparison.lean::exists_adjusted_product_teichmuller_series_pow_prime_eq_trace_recursion_of_parameter@L531

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8268 · Filter by author CBirkbeck opened on Jul 16, 2026

• decompose-proof: BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/DworkFactorization/WittCarry/AdjustedProductRecursion.lean::exists_adjusted_product_teichmuller_series_pow_prime_eq_trace_recursion@L70

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8267 · Filter by author CBirkbeck opened on Jul 16, 2026

• decompose-proof: BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/DworkFactorization/Telescope/ZModFold/ZModTraceCarryFold.lean::artinHasseExpTraceCarryZModCorrectionTeichProduct_succ_eq_range_mul_tail@L149

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8266 · Filter by author CBirkbeck opened on Jul 16, 2026

• decompose-proof: BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/DworkFactorization/Telescope/ZModFold/FiniteCharacterFold.lean::artinHasseExpCurrentRootPeelProduct_traceCarry_tail_eq_one_of_factor_pow_prime_eq_one@L331

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8265 · Filter by author CBirkbeck opened on Jul 16, 2026

• decompose-proof: BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/DworkFactorization/Telescope/TraceCarry/ProductIterCorrectionComparison.lean::artinHasseExpFrobeniusProductIterCorrection_succ_eq@L65

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8264 · Filter by author CBirkbeck opened on Jul 16, 2026

• decompose-proof: BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/DworkFactorization/Telescope/TraceCarry/IteratedCorrectionExpansion.lean::exists_traceCarryIterCorrection_eq_teichmuller_series_product_powers_const@L318

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8263 · Filter by author CBirkbeck opened on Jul 16, 2026

• decompose-proof: BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/DworkFactorization/Telescope/TraceCarry/InverseParameterZeroBoundary.lean::artinHasseExp_inverse_adjustedProduct_succ_traceCarry_eq_one_of_le@L167

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8262 · Filter by author CBirkbeck opened on Jul 16, 2026

• decompose-proof: BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/DworkFactorization/Telescope/InversePeel/PrecisionCompatibility.lean::artinHasseExp_inverse_frobenius_product_factor_eq@L304

  lane:decomposestate:todo
  CBirkbeck/AINTLIB#8261 · Filter by author CBirkbeck opened on Jul 16, 2026