feat: proofs for rational function lemmas

[alexanderlhicks]

replaces #387, addresses some issues in the RationalFunctions file.

[github-actions]

🤖 PR Summary

sorry delta: -3 (5 removed, 2 added) — net proof progress

feat: proofs for rational function lemmas

This PR refactors and extends the rational functions formalization following Appendix A of [BCIKS20]. It modularizes the monolithic RationalFunctions.lean into seven specialized files (FunctionField, Weight, RationalRootVanishing, Lifts, HenselNumerators.Setup, HenselNumerators.Hensel, HenselNumerators.Weight), updates downstream code in the coding theory proximity gap, and adds new theorems and definitions.

Mathematical Formalization

• FunctionField.lean defines the function field 𝕃 H and the ring of regular functions 𝒪 H for a bivariate polynomial H. It introduces monicized polynomials H_tilde and H_tilde', proves irreducibility conditions, constructs field and ring structures, and provides an embedding embeddingOf𝒪Into𝕃 along with rational substitution maps π_z and canonical representatives.
• HenselNumerators/Hensel.lean formalizes the Hensel-lifting construction: defines IsHenselNumeratorSequence, formalHenselAlphaSequence, and exists_hensel_alpha_sequence which constructs a sequence αseq in 𝕃 H satisfying the power series identity evalRAtPowerSeries x₀ H R γ = 0. The file also defines AllCoeffRegular with closure properties and proves the combinatorial clearing denominator theorem henselCoeffResidual_regular_after_clearing (no sorry).
• HenselNumerators/Sequence.lean provides regular_numerator_shape_succ, exists_regular_numerator_shape, and exists_hensel_numerator_sequence for constructing regular numerator sequences βseq, along with packaged definitions βSeq, β, α, α', γ, γ' (no sorry).
• HenselNumerators/Setup.lean formalizes the Hypotheses x₀ R H structure (divisibility and separability conditions), defines ζ, ξ in 𝕃 H, proves regularity lemmas, constructs ξ in 𝒪 H with its representative ξ_pre, and establishes the key identity embeddingOf𝒪Into𝕃_ξ and weight bound ξ_weight_le.
• HenselNumerators/Weight.lean introduces RegularWeightLe and the sharp arithmetic bound numeratorShapeSharp. Proves numerator_shape_weight_sharp by strong induction. Contains two sorry gaps: one in henselClearedTerm_weight for the boundary summand (p.1 = 0, j = d >= 2, p.2 = t+1), and one in numerator_shape_weight_sharp for the degenerate case natDegreeY R = 1.
• Lifts.lean defines liftToFunctionField, liftBivariate, functionFieldT, fieldTo𝕃, and polyToPowerSeries𝕃. Proves regularity conditions for lifts (including liftToFunctionField_ne_zero, regularElementsSet_liftToFunctionField_div_of_dvd, W_pow_mul_eval₂_div_eq_sum, and regularity of evaluations at T/W).
• RationalRootVanishing.lean adds theorems for Lemma A.1: H_tilde_prime_coeff_natDegree_le_of_totalDegree, canonicalRep_coeff_natDegree_le_of_weight_bound, embedding_eq_zero_of_resultant_zero, natDegree_det_le_of_perm_products_le, natDegree_resultant_le_weight_bound, poly_eq_zero_of_ncard_gt_bound_of_subset_roots, resultant_eval_eq_resultant_map_eval_fixed_degrees, resultant_fixed_degree_eq_zero_of_common_root_of_monic_right, Sbeta_subset_resultant_roots, weight_bot_embedding_zero, and the key lemmaA1_embedding_eq_zero_of_many_rational_roots.
• Weight.lean introduces weight_Λ and weight_Λ_over_𝒪, proving algebraic properties (invariance, sub-additivity, monomial bounds). Proves weight_Λ_H_tilde'_le, weight_Λ_sub_leadingCoeff_mul_H_tilde'_le, and weight_Λ_modByMonic_H_tilde'_le. Also defines S_β from Lemma A.1 (no sorry).

Proof Completion (Partial)

• The original RationalFunctions.lean has been stripped to a compatibility umbrella, with all definitions and proofs moved to subfiles.
• Note: Agreement.lean still contains two sorry placeholders in approximate_solution_is_exact_solution_coeffs and approximate_solution_is_exact_solution_coeffs' (marked explicitly).

Protocols / Soundness

• Extraction.lean adds pg_natDegree_pos_of_mem_normalizedFactors_of_separable and pg_candidatePairs_snd_natDegree_pos. Refactors pg_card_normalizedFactors_toFinset_le_natDegree to use the new lemma.

Infrastructure / CI

• ArkLib.lean adds seven new imports (FunctionField, Hensel, Sequence, Setup, Weight, Lifts, RationalRootVanishing) to the top-level re-export.

Documentation

• docs/kb/audits/bciks20-appendix-a-rational-functions.md: Summary unavailable due to parsing error.

Refactoring

• RationalFunctions.lean: Complete restructuring — original content removed, now serves as umbrella re-exporting subfiles.
• Agreement.lean: Updates namespace from BCIKS20AppendixA to RationalFunctions.HenselNumerators, accesses types from new location. Adds natDegree_H_pos and evalX_R_separable lemmas; claimA2_hypotheses bundles properties. All affected lemmas receive new explicit arguments.

Critical sorry / admit note: The file HenselNumerators/Weight.lean contains two sorry placeholders as described above. These must be resolved before merging.

---

Statistics

Metric	Count
📝 Files Changed	17
✅ Lines Added	7345
❌ Lines Removed	1083

---

Lean Declarations

✏️ Removed: 64 declaration(s)

ArkLib/Data/Polynomial/RationalFunctions.lean (64)

• abbrev 𝒪 (H : F[X][Y]) : Type
• abbrev 𝕃 (H : F[X][Y]) : Type
• def rationalRoot (H : F[X][Y]) (z : F) : Type
• def regularElms (H : F[X][Y]) : Type
• def regularElms_set (H : F[X][Y]) : Set (𝕃 H)
• def α (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [φ : Fact (Irreducible H)] (t : ℕ) : 𝕃 H
• def α' (x₀ : F) (R : F[X][X][Y]) (H_irreducible : Irreducible H) (t : ℕ) : 𝕃 H
• def β (R : F[X][X][Y]) (t : ℕ) : 𝒪 H
• def γ (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [φ : Fact (Irreducible H)] : PowerSeries (𝕃 H)
• def γ' (x₀ : F) (R : F[X][X][Y]) (H_irreducible : Irreducible H) : PowerSeries (𝕃 H)
• def ζ (R : F[X][X][Y]) (x₀ : F) (H : F[X][Y]) [H_irreducible : Fact (Irreducible H)] : 𝕃 H
• def ξ (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [φ : Fact (Irreducible H)] : 𝒪 H
• lemma H_tilde'_monic (H : F[X][Y]) (hH : 0 < H.natDegree) :
• lemma H_tilde_equiv_H_tilde' (H : F[X][Y]) : (H_tilde' H).map univPolyHom = H_tilde H
• lemma Lemma_A_1 {H : F[X][Y]} (hH : 0 < H.natDegree) (β : 𝒪 H) (D : ℕ)
• lemma canonicalRepOf𝒪_degree_lt {H : F[X][Y]} (hH : 0 < H.natDegree) (β : 𝒪 H) :
• lemma canonicalRepOf𝒪_mk {H : F[X][Y]} (hH : 0 < H.natDegree) (p : F[X][Y]) :
• lemma canonicalRepOf𝒪_mk_eq_self_of_degree_lt {H : F[X][Y]} (hH : 0 < H.natDegree)
• lemma canonicalRepOf𝒪_natDegree_le {H : F[X][Y]} (hH : 0 < H.natDegree) (β : 𝒪 H) :
• lemma canonicalRepOf𝒪_zero {H : F[X][Y]} (hH : 0 < H.natDegree) :
• lemma embeddingOf𝒪Into𝕃_mk (H : F[X][Y]) (p : F[X][Y]) :
• lemma irreducibleHTildeOfIrreducible {H : Polynomial (Polynomial F)} :
• lemma isField_of_irreducible {H : F[X][Y]} : Irreducible H → IsField (𝕃 H)
• lemma liftBivariate_C {H : F[X][Y]} (p : F[X]) :
• lemma liftBivariate_X {H : F[X][Y]} :
• lemma mk_canonicalRepOf𝒪 {H : F[X][Y]} (hH : 0 < H.natDegree) (β : 𝒪 H) :
• lemma regularElms_set_add {H : F[X][Y]} {a b : 𝕃 H}
• lemma regularElms_set_functionFieldT (H : F[X][Y]) :
• lemma regularElms_set_liftBivariate (H : F[X][Y]) (p : F[X][Y]) :
• lemma regularElms_set_liftToFunctionField (H : F[X][Y]) (p : F[X]) :
• lemma regularElms_set_mul {H : F[X][Y]} {a b : 𝕃 H}
• lemma regularElms_set_neg {H : F[X][Y]} {a : 𝕃 H}
• lemma regularElms_set_one (H : F[X][Y]) : (1 : 𝕃 H) ∈ regularElms_set H
• lemma regularElms_set_pow {H : F[X][Y]} {a : 𝕃 H}
• lemma regularElms_set_sub {H : F[X][Y]} {a b : 𝕃 H}
• lemma regularElms_set_zero (H : F[X][Y]) : (0 : 𝕃 H) ∈ regularElms_set H
• lemma regular_liftBivariate (H : F[X][Y]) (p : F[X][Y]) :
• lemma regular_liftToFunctionField (H : F[X][Y]) (p : F[X]) :
• lemma weight_Λ_over_𝒪_mk {H : F[X][Y]} (hH : 0 < H.natDegree) (p : F[X][Y])
• lemma weight_Λ_over_𝒪_mk_eq_self_of_degree_lt {H : F[X][Y]} (hH : 0 < H.natDegree)
• lemma weight_Λ_over_𝒪_zero {H : F[X][Y]} (hH : 0 < H.natDegree) (D : ℕ) :
• lemma weight_Λ_zero (H : F[X][Y]) (D : ℕ) :
• lemma weight_ξ_bound (x₀ : F) (hH : 0 < H.natDegree) {D : ℕ}
• lemma β_regular (R : F[X][X][Y])
• lemma ζ_regular_of_derivative_evalX_eq_C (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• lemma ξ_regular (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [H_irreducible : Fact (Irreducible H)] :
• lemma ξ_regular_of_derivative_evalX_eq_C_of_natDegree_le_one
• noncomputable def H_tilde (H : F[X][Y]) : Polynomial (RatFunc F)
• noncomputable def H_tilde' (H : F[X][Y]) : F[X][Y]
• noncomputable def S_β {H : F[X][Y]} (β : 𝒪 H) : Set F
• noncomputable def canonicalRepOf𝒪 {H : F[X][Y]} (hH : 0 < H.natDegree) (β : 𝒪 H) : F[X][Y]
• noncomputable def coeffAsRatFunc : F[X] →+* Polynomial (RatFunc F)
• noncomputable def embeddingOf𝒪Into𝕃 (H : F[X][Y]) : 𝒪 H →+* 𝕃 H
• noncomputable def fieldTo𝕃 {H : F[X][Y]} : F →+* 𝕃 H
• noncomputable def functionFieldT {H : F[X][Y]} : 𝕃 H
• noncomputable def liftBivariate {H : F[X][Y]} : F[X][Y] →+* 𝕃 H
• noncomputable def liftToFunctionField {H : F[X][Y]} : F[X] →+* 𝕃 H
• noncomputable def polyToPowerSeries𝕃 (H : F[X][Y]) (P : F[X][Y]) : PowerSeries (𝕃 H)
• noncomputable def weight_Λ (f H : F[X][Y]) (D : ℕ) : WithBot ℕ
• noncomputable def weight_Λ_over_𝒪 {H : F[X][Y]} (hH : 0 < H.natDegree) (f : 𝒪 H) (D : ℕ) :
• noncomputable def π_z {H : F[X][Y]} (z : F) (root : rationalRoot (H_tilde' H) z) : 𝒪 H →+* F
• noncomputable def π_z_lift {H : F[X][Y]} (z : F) (root : rationalRoot (H_tilde' H) z) :
• private lemma monicize_leading_term {K : Type} [Field K] (a : K) (d : ℕ)
• private lemma monicize_term {K : Type} [Field K] (a b : K) (i d : ℕ)

✏️ Added: 234 declaration(s)

ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean (4)

• lemma H_dvd_evalX_R (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :
• lemma claimA2_hypotheses (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :
• lemma evalX_R_separable (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :
• lemma natDegree_H_pos (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :

ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Extraction.lean (2)

• theorem pg_candidatePairs_snd_natDegree_pos (x₀ : F)
• theorem pg_natDegree_pos_of_mem_normalizedFactors_of_separable (p : F[Z][X])

ArkLib/Data/Polynomial/RationalFunctions/FunctionField.lean (41)

• abbrev 𝒪 (H : F[X][Y]) : Type
• abbrev 𝕃 (H : F[X][Y]) : Type
• def rationalRoot (H : F[X][Y]) (z : F) : Type
• def regularElements (H : F[X][Y]) : Type
• def regularElementsSet (H : F[X][Y]) : Set (𝕃 H)
• lemma H_tilde'_dvd_of_map_dvd_H_tilde {H p : F[X][Y]} (hHdeg : 0 < H.natDegree)
• lemma H_tilde'_monic (H : F[X][Y]) (hH : 0 < H.natDegree) :
• lemma canonicalRepOf𝒪_degree_lt {H : F[X][Y]} (hH : 0 < H.natDegree) (β : 𝒪 H) :
• lemma canonicalRepOf𝒪_mk {H : F[X][Y]} (hH : 0 < H.natDegree) (p : F[X][Y]) :
• lemma canonicalRepOf𝒪_mk_eq_self_of_degree_lt {H : F[X][Y]} (hH : 0 < H.natDegree)
• lemma canonicalRepOf𝒪_natDegree_le {H : F[X][Y]} (hH : 0 < H.natDegree) (β : 𝒪 H) :
• lemma canonicalRepOf𝒪_zero {H : F[X][Y]} (hH : 0 < H.natDegree) :
• lemma embeddingOf𝒪Into𝕃_injective {H : F[X][Y]} (hHdeg : 0 < H.natDegree) :
• lemma irreducibleHTilde'OfIrreducible {H : F[X][Y]} (hHdeg : 0 < H.natDegree)
• lemma irreducibleHTildeOfIrreducible {F : Type} [Field F] {H : Polynomial (Polynomial F)}
• lemma irreducibleHTildeOfIrreducible_of_natDegree_pos
• lemma isField_of_irreducible {F : Type} [Field F] {H : F[X][Y]} (hHdeg : 0 < H.natDegree) :
• lemma isField_of_irreducible_of_natDegree_pos {F : Type} [Field F] {H : F[X][Y]}
• lemma map_H_tilde'_eq_H_tilde (H : F[X][Y]) : (H_tilde' H).map univPolyHom = H_tilde H
• lemma mk_canonicalRepOf𝒪 {H : F[X][Y]} (hH : 0 < H.natDegree) (β : 𝒪 H) :
• lemma regularElementsSet_add {H : F[X][Y]} {a b : 𝕃 H}
• lemma regularElementsSet_mul {H : F[X][Y]} {a b : 𝕃 H}
• lemma regularElementsSet_neg {H : F[X][Y]} {a : 𝕃 H}
• lemma regularElementsSet_one (H : F[X][Y]) : (1 : 𝕃 H) ∈ regularElementsSet H
• lemma regularElementsSet_pow {H : F[X][Y]} {a : 𝕃 H}
• lemma regularElementsSet_prod {ι : Type} {H : F[X][Y]} (s : Finset ι) {f : ι → 𝕃 H}
• lemma regularElementsSet_sub {H : F[X][Y]} {a b : 𝕃 H}
• lemma regularElementsSet_sum {ι : Type} {H : F[X][Y]} (s : Finset ι) {f : ι → 𝕃 H}
• lemma regularElementsSet_zero (H : F[X][Y]) : (0 : 𝕃 H) ∈ regularElementsSet H
• lemma univPolyHom_injective :
• noncomputable def H_tilde (H : F[X][Y]) : Polynomial (RatFunc F)
• noncomputable def H_tilde' (H : F[X][Y]) : F[X][Y]
• noncomputable def canonicalRepOf𝒪 {H : F[X][Y]} (hH : 0 < H.natDegree) (β : 𝒪 H) : F[X][Y]
• noncomputable def embeddingOf𝒪Into𝕃 (H : F[X][Y]) : 𝒪 H →+* 𝕃 H
• noncomputable def π_z {H : F[X][Y]} (z : F) (root : rationalRoot (H_tilde' H) z) :
• noncomputable def π_z_lift {H : F[X][Y]} (z : F) (root : rationalRoot (H_tilde' H) z) :
• private lemma irreducible_comp_C_mul_X_iff {K : Type} [Field K] (a : K) (ha : a ≠ 0)
• private lemma irreducible_map_univPolyHom_of_irreducible
• private lemma mem_span_H_tilde'_of_bivPolyHom_mem_span_H_tilde {H p : F[X][Y]}
• private lemma monicize_leading_term {K : Type} [Field K] (a : K) (d : ℕ)
• private lemma monicize_term {K : Type} [Field K] (a b : K) (i d : ℕ)

ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Hensel.lean (57)

• def AllCoeffRegular (H : F[X][Y]) (φ : PowerSeries (𝕃 H)) : Prop
• def HasNumeratorShape (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• def IsHenselNumeratorSequence (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• def defaultDegreeBound (R : F[X][X][Y]) (H : F[X][Y]) : ℕ
• def henselDenominatorExponent (t : ℕ) : ℕ
• def trivariateTotalDegree (R : F[X][X][Y]) : ℕ
• lemma coeff_totalDegree_add_index_le_trivariateTotalDegree (R : F[X][X][Y]) {i : ℕ}
• lemma defaultDegreeBound_ge_H (R : F[X][X][Y]) (H : F[X][Y]) :
• lemma defaultDegreeBound_ge_R_coeff (R : F[X][X][Y]) (H : F[X][Y]) {i : ℕ}
• lemma henselDenominatorExponent_succ (t : ℕ) :
• lemma henselDenominatorExponent_zero : henselDenominatorExponent 0 = 0
• noncomputable def alphaOfNumerators (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• noncomputable def alphaSeq (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• noncomputable def bSeq (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• noncomputable def evalRAtPowerSeries (x₀ : F) (H : F[X][Y]) (R : F[X][X][Y])
• noncomputable def gammaFromAlpha (H : F[X][Y]) (αseq : ℕ → 𝕃 H) :
• noncomputable def gammaOfNumerators (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• noncomputable def henselCoeffResidual (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• noncomputable def liftCoeffToPowerSeries (x₀ : F) (H : F[X][Y]) :
• theorem AllCoeffRegular.X {H : F[X][Y]} : AllCoeffRegular H (PowerSeries.X)
• theorem AllCoeffRegular.add {H : F[X][Y]} {φ ψ : PowerSeries (𝕃 H)}
• theorem AllCoeffRegular.const {H : F[X][Y]} {c : 𝕃 H} (hc : c ∈ regularElementsSet H) :
• theorem AllCoeffRegular.mul {H : F[X][Y]} {φ ψ : PowerSeries (𝕃 H)}
• theorem AllCoeffRegular.pow {H : F[X][Y]} {φ : PowerSeries (𝕃 H)}
• theorem AllCoeffRegular.zero {H : F[X][Y]} :
• theorem H_eval2_T_div_W_eq_zero (H : F[X][Y])
• theorem bSeq_eq_zero_of_gt (x₀ : F) (R : F[X][X][Y]) (N j : ℕ) (hj : N < j) :
• theorem bSeq_stable (x₀ : F) (R : F[X][X][Y]) (N i : ℕ) (hi : i ≤ N) :
• theorem bSeq_succ_def (x₀ : F) (R : F[X][X][Y]) (N : ℕ) :
• theorem bSeq_succ_eq_below (x₀ : F) (R : F[X][X][Y]) (N i : ℕ) (hi : i < N + 1) :
• theorem bSeq_zero (x₀ : F) (R : F[X][X][Y]) (N : ℕ) :
• theorem beta_zero_eq_X_of_shape (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem coeff_delta_below (x₀ : F) (R : F[X][X][Y]) (N i : ℕ) (hi : i < N + 1) :
• theorem coeff_evalR_split (x₀ : F) (R : F[X][X][Y]) (n : ℕ) (hn : 1 ≤ n)
• theorem coeff_evalR_stable (x₀ : F) (R : F[X][X][Y]) (n m : ℕ) (hm : m < n)
• theorem coeff_liftCoeff_regular (x₀ : F) (H : F[X][Y]) (p : F[X][X]) :
• theorem coeff_mul_eq_zero_of_orders {A : Type} [CommRing A] {m : ℕ}
• theorem coeff_mul_of_low_order {A : Type} [CommRing A] (n : ℕ) (P δ : PowerSeries A)
• theorem coeff_zero_evalR (x₀ : F) (R : F[X][X][Y]) (Γ : PowerSeries (𝕃 H)) :
• theorem constantCoeff_eval₂_derivative_eq_zeta (x₀ : F) (R : F[X][X][Y])
• theorem constantCoeff_eval₂_liftCoeff (x₀ : F) (q : F[X][X][Y]) (Γ : PowerSeries (𝕃 H)) :
• theorem constantCoeff_liftCoeffToPowerSeries (x₀ : F) (p : F[X][X]) :
• theorem evalX_totalDegree_le_of_coeff_bound (x₀ : F) (R : F[X][X][Y]) {D : ℕ}
• theorem exists_hensel_alpha_sequence (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem fieldTo𝕃_regular (x₀ : F) (H : F[X][Y]) :
• theorem formalHenselAlphaSequence (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem gammaOfNumerators_eq_gammaFromAlpha (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem henselClearedTerm_regular (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem henselCoeffResidual_eq_trunc (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem henselCoeffResidual_regular_after_clearing (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem hensel_numerator_sequence_of_alpha_shape (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem initial_root_at_x0 (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem mk_H_tilde_eq_W_pow_mul_eval2 (H : F[X][Y])
• theorem mk_bSeq_coeff_eq (x₀ : F) (R : F[X][X][Y]) (N i : ℕ) (hi : i ≤ N) :
• theorem remainder_low_order {A B : Type} [CommRing A] [CommRing B] (n : ℕ)
• theorem root_bSeq (x₀ : F) (R : F[X][X][Y])
• theorem zeta_ne_zero_of_Hypotheses (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])

ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Sequence.lean (10)

• def α (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [φ : Fact (Irreducible H)]
• def α' (x₀ : F) (R : F[X][X][Y]) (H_irreducible : Irreducible H)
• def γ (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [φ : Fact (Irreducible H)]
• def γ' (x₀ : F) (R : F[X][X][Y]) (H_irreducible : Irreducible H)
• lemma exists_hensel_numerator_sequence (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• lemma βSeq_spec (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• noncomputable def β (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• noncomputable def βSeq (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem exists_regular_numerator_shape (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem regular_numerator_shape_succ (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])

ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Setup.lean (35)

• def ζ (R : F[X][X][Y]) (x₀ : F) (H : F[X][Y]) [H_irreducible : Fact (Irreducible H)]
• lemma H_natDegree_le_R_natDegree_of_Hypotheses {x₀ : F} {R : F[X][X][Y]} {H : F[X][Y]}
• lemma derivative_evalX_coeff (x₀ : F) (R : F[X][X][Y]) (i : ℕ) :
• lemma derivative_evalX_eq_C_of_natDegree_le_one
• lemma embeddingOf𝒪Into𝕃_mk_ξ_pre (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• lemma embeddingOf𝒪Into𝕃_ξ (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• lemma evalX_ne_zero_of_Hypotheses {x₀ : F} {R : F[X][X][Y]} {H : F[X][Y]}
• lemma leadingCoeff_dvd_evalX_coeff_natDegree {x₀ : F} {R : F[X][X][Y]} {H : F[X][Y]}
• lemma leadingCoeff_dvd_evalX_derivative_coeff_pred {x₀ : F} {R : F[X][X][Y]} {H : F[X][Y]}
• lemma leadingCoeff_dvd_evalX_leadingCoeff {x₀ : F} {R : F[X][X][Y]} {H : F[X][Y]}
• lemma natDegree_derivative_evalX_coeff_le (x₀ : F) (R : F[X][X][Y]) {D i : ℕ}
• lemma ζ_regular_of_derivative_evalX_eq_C (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• lemma ξ_regular (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [H_irreducible : Fact (Irreducible H)]
• lemma ξ_regular_of_derivative_evalX_eq_C_of_natDegree_le_one
• lemma ξ_regular_of_natDegree_eq_two
• lemma ξ_regular_of_natDegree_le_one
• lemma ξ_weight_le (x₀ : F) (hH : 0 < H.natDegree) (hHyp : Hypotheses x₀ R H)
• noncomputable def xiPreLower (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) : F[X][Y]
• noncomputable def xiPreTop (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) : F[X][Y]
• noncomputable def ξ (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [_φ : Fact (Irreducible H)]
• noncomputable def ξ_pre (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) : F[X][Y]
• private lemma evalX_natDegree_le {K : Type} [CommSemiring K] (x : K) (P : K[X][Y]) :
• theorem cofactor_top_reduction_weight_le {H : F[X][Y]} (hH : 0 < H.natDegree) {Q : F[X][Y]} {d D : ℕ}
• theorem leadingCoeff_natDegree_le_of_totalDegree_le {D : ℕ} (hD_H : Bivariate.totalDegree H ≤ D) :
• theorem weight_Λ_over_𝒪_add_le {H : F[X][Y]} {D : ℕ} (hD_H : Bivariate.totalDegree H ≤ D)
• theorem xiPreLower_coeff_natDegree_le (x₀ : F) {D i : ℕ}
• theorem xiPreLower_term_weight_le (x₀ : F) (hHyp : Hypotheses x₀ R H) (hRdeg : 2 ≤ R.natDegree)
• theorem xiPreLower_weight_le (x₀ : F) (hHyp : Hypotheses x₀ R H) (hRdeg : 2 ≤ R.natDegree)
• theorem xiPreTop_coeff_natDegree_zero_of_H_natDegree_eq_R_natDegree (x₀ : F) (hH : 0 < H.natDegree) (hHyp : Hypotheses x₀ R H)
• theorem xiPreTop_modByMonic_coeff_natDegree_le (x₀ : F) (hH : 0 < H.natDegree) (hHyp : Hypotheses x₀ R H)
• theorem xiPreTop_modByMonic_weight_le (x₀ : F) (hH : 0 < H.natDegree) (hHyp : Hypotheses x₀ R H)
• theorem xiPreTop_topCoeff_mul_natDegree_le (x₀ : F) (hH : 0 < H.natDegree) (hHyp : Hypotheses x₀ R H)
• theorem xiPreTop_weight_over_𝒪_le (x₀ : F) (hH : 0 < H.natDegree) (hHyp : Hypotheses x₀ R H)
• theorem xiPreTop_weight_over_𝒪_le_of_H_natDegree_lt_R_natDegree (x₀ : F) (hH : 0 < H.natDegree) (hHyp : Hypotheses x₀ R H)
• theorem xiPre_eq_lower_add_top (x₀ : F) (hRdeg : 2 ≤ R.natDegree) :

ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Weight.lean (26)

• def RegularWeightLe {H : F[X][Y]} (hH : 0 < H.natDegree) (a : 𝕃 H) (D B : ℕ) : Prop

…and 84 more not listed.

---

sorry Tracking

✅ Removed: 5 `sorry`(s)

ArkLib/Data/Polynomial/RationalFunctions.lean (5)

• lemma Lemma_A_1 {H : F[X][Y]} (hH : 0 < H.natDegree) (β : 𝒪 H) (D : ℕ) (L471)
• lemma irreducibleHTildeOfIrreducible {H : Polynomial (Polynomial F)} : (L52)
• lemma weight_ξ_bound (x₀ : F) (hH : 0 < H.natDegree) {D : ℕ} (L603)
• lemma β_regular (R : F[X][X][Y]) (L613)
• lemma ξ_regular (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [H_irreducible : Fact (Irreducible H)] : (L591)

❌ Added: 2 `sorry`(s)

ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Weight.lean (2)

• lemma henselClearedTerm_weight (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) (L570)
• theorem numerator_shape_weight_sharp (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) (L779)

---

Coverage Notes

• Additional-instructions analysis was skipped because the full diff exceeded the analysis size budget, and partial results would be misleading.

---

📄 **Per-File Summaries**

• ArkLib.lean: Added seven new imports to ArkLib.lean from ArkLib.Data.Polynomial.RationalFunctions, specifically FunctionField, HenselNumerators (including Hensel, Sequence, Setup, Weight), Lifts, RationalRootVanishing, and Weight. This extends the top-level re‑export for the polynomial rational‑functions module, making those theorems, definitions, and structures available to any code that imports ArkLib.

• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean: This diff updates Agreement.lean to align it with a refactored framework: the previous BCIKS20AppendixA namespace has been replaced by RationalFunctions.HenselNumerators, and the 𝕃 type, polyToPowerSeries𝕃, γ', and the Hypotheses structure are now accessed from the new location. The lemma exists_factors_with_large_common_root_set gains two new conjuncts in its existential conclusion: the irreducible factor H has 0 < H.natDegree and R(x₀, Y, Z) is separable. Two new lemmas, natDegree_H_pos and evalX_R_separable, extract these properties, and a new lemma claimA2_hypotheses bundles H_dvd_evalX_R and evalX_R_separable into the Hypotheses record for Claim A.2. Consequently, approximate_solution_is_exact_solution_coeffs, approximate_solution_is_exact_solution_coeffs', solution_gamma_is_linear_in_Z, and gamma_eq_P all receive additional explicit arguments (the natDegree positivity and the claimA2_hypotheses proof), and approximate_solution_is_exact_solution_coeffs and approximate_solution_is_exact_solution_coeffs' are still marked sorry.

• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Extraction.lean: This diff extracts the proof that any normalized factor of a separable polynomial has positive degree into a separate lemma, pg_natDegree_pos_of_mem_normalizedFactors_of_separable (new), and then adds a new theorem pg_candidatePairs_snd_natDegree_pos which uses that lemma to show that for any pair (R, H) in pg_candidatePairs, the second component H has positive natDegree. The existing theorem pg_card_normalizedFactors_toFinset_le_natDegree is refactored to replace its inlined proof of positivity with a call to the new pg_natDegree_pos_of_mem_normalizedFactors_of_separable.

• ArkLib/Data/Polynomial/RationalFunctions.lean: This file has been completely restructured: it now serves as an umbrella module that re-exports the content of seven new sub-files (FunctionField, Weight, RationalRootVanishing, Lifts, HenselNumerators.Setup, HenselNumerators.Hensel, HenselNumerators.Weight). All of the original definitions, lemmas, and instances (including H_tilde, H_tilde', 𝕃, 𝒪, embeddingOf𝒪Into𝕃, regularElms_set, π_z, canonicalRepOf𝒪, weight_Λ, weight_Λ_over_𝒪, S_β, Lemma_A_1, liftToFunctionField, liftBivariate, functionFieldT, ζ, ξ, β, α, γ, and the ClaimA2 namespace) have been removed from this file, as have the dependencies on Mathlib and ArkLib imports that were previously here. The only remaining content is a module header and a comment indicating that this file now acts as a 'Compatibility umbrella' for the modularized development.

• ArkLib/Data/Polynomial/RationalFunctions/FunctionField.lean: This new file defines the function field 𝕃 and the ring of regular functions 𝒪 for a bivariate polynomial H over a field, following Appendix A of [BCIKS20]. It introduces the monicized polynomial H_tilde and its integral version H_tilde', proves irreducibility conditions under positive Y-degree (irreducibleHTildeOfIrreducible, irreducibleHTilde'OfIrreducible), and constructs field and ring structures (isField_of_irreducible, Field instance). The file also provides an embedding of 𝒪 into 𝕃 (embeddingOf𝒪Into𝕃) and proves its injectivity, defines the set of regular elements (regularElementsSet) with closure properties, defines rational substitution maps π_z, and develops canonical representatives (canonicalRepOf𝒪) with associated lemmas.

• ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Hensel.lean: This file, Hensel.lean, adds the definitions and main theorems implementing the Hensel-lifting construction of Appendix A of [BCIKS20] for trivariate polynomials over a field, formalising the notions of Hensel coefficients, residuals, and a Hensel numerator sequence for a trivariate polynomial R(X,Y,Z) ∈ F[Z][X][Y] with respect to an irreducible bivariate polynomial H ∈ F[X][Y] and a root x₀ of the resultant. The file defines henselDenominatorExponent, trivariateTotalDegree, defaultDegreeBound, the power-series lifting homomorphism liftCoeffToPowerSeries, the evaluation map evalRAtPowerSeries, the function-field element alphaOfNumerators, the power series gammaOfNumerators, the predicate IsHenselNumeratorSequence, and a construction gammaFromAlpha. The central result formalHenselAlphaSequence (line ~520) constructs, under the assumptions hinit (initial root condition) and hzeta (non‑zero derivative ζ), an αseq : ℕ → 𝕃 H such that αseq 0 = T/W and the power series γ = ∑ αᵗ Sᵗ (where S = X - x₀) satisfies evalRAtPowerSeries x₀ H R γ = 0 — this formalises the formal‑Hensel/Newton iteration over the residue field. The file further proves exists_hensel_alpha_sequence (line ~620) that, given Hypotheses x₀ R H, provides the same α‑sequence using initial_root_at_x0 and zeta_ne_zero_of_Hypotheses. The second major block defines AllCoeffRegular (a predicate that all coefficients of a power series are in the regular‑elements set) and proves closure properties (add, mul, pow, const, X, zero, and coeff_liftCoeff_regular). The key combinatorial lemmas henselCoeffResidual_eq_trunc (line ~660) and henselClearedTerm_regular (line ~720) and the final theorem henselCoeffResidual_regular_after_clearing (line ~830) establish that, after multiplying the Hensel residual at step t by a global clearing denominator Ddiv = W^{t+2} · η^{E-1} · W^{d-2} (where W = lifting of the leading coefficient, η = ξ), the result is a regular element — this is the combinatorial heart of clearing denominators (paper A.4, pp. 52–53). No sorry or admit appear in the diff.

• ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Sequence.lean: This new file adds the theory of Hensel numerator sequences for rational functions over a field, following Appendix A of [BCIKS20]. It defines the theorem regular_numerator_shape_succ giving an inductive step for constructing numerators, and exists_regular_numerator_shape which produces a sequence of regular numerators βseq from an alpha sequence. The lemma exists_hensel_numerator_sequence then provides a sequence βseq satisfying the IsHenselNumeratorSequence property and a weight bound. Finally, noncomputable definitions βSeq, β, α, α', γ, γ' package the chosen sequences and their induced power series, with βSeq_spec stating the specification. No sorry or admit are present.

• ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Setup.lean: This file adds a new module RationalFunctions.HenselNumerators.Setup that formalises the algebraic setup for Claim A.2 of [BCIKS20]. It introduces:

• The structure Hypotheses x₀ R H, which states that H divides R(x₀,Y,Z) and that the specialization R(x₀,Y,Z) is separable; it comes with supporting lemmas such as evalX_ne_zero_of_Hypotheses, H_natDegree_le_R_natDegree_of_Hypotheses, leadingCoeff_dvd_evalX_leadingCoeff, leadingCoeff_dvd_evalX_coeff_natDegree, and leadingCoeff_dvd_evalX_derivative_coeff_pred.

• The definition ζ R x₀ H : 𝕃 H as the evaluation of the derivative specialization R'(x₀, Y, Z) in the function field, together with regularity lemmas ζ_regular_of_derivative_evalX_eq_C, derivative_evalX_eq_C_of_natDegree_le_one, ξ_regular_of_derivative_evalX_eq_C_of_natDegree_le_one, ξ_regular_of_natDegree_le_one, and ξ_regular_of_natDegree_eq_two that produce a preimage in the integral closure 𝒪 H for low-degree cases.

• The regular element ξ x₀ R H hHyp : 𝒪 H and its explicit polynomial representative ξ_pre (constructed via xiPreLower and xiPreTop), and the key identity embeddingOf𝒪Into𝕃_ξ which shows embedding(ξ) = W^(d-2)·ζ (the algebraic identity of Claim A.2).

• The bound ξ_weight_le which states that, under a Hypotheses assumption and 2 ≤ natDegreeY R, the weight weight_Λ_over_𝒪 of ξ is ≤ (deg_Y R - 1) * (D - deg_Y H + 1). This is derived from weight_Λ_over_𝒪_add_le, xiPreLower_weight_le, xiPreTop_weight_over_𝒪_le, and a suite of supporting lemmas (xiPreLower_coeff_natDegree_le, xiPreLower_term_weight_le, xiPreTop_modByMonic_weight_le, xiPreTop_modByMonic_coeff_natDegree_le, xiPreTop_coeff_natDegree_zero_of_H_natDegree_eq_R_natDegree, xiPreTop_topCoeff_mul_natDegree_le).

• ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Weight.lean: This file introduces the concept of RegularWeightLe (a Prop bundling regularity in the image of 𝒪 H with a Λ-weight certificate) and proves sharp per-step Λ-weight bounds for Hensel numerators, following Appendix A of [BCIKS20]. Key definitions include RegularWeightLe, numeratorShapeSharp (a sharp arithmetic bound 1 + (t+1)*(D-dH) + eₜ*((dY-1)*(D-dH+1))), and numeratorShapeSharp_le_loose (showing it weakens to (2t+1)*dY*D). The central theorem is numerator_shape_weight_sharp, which proves by strong induction that Λ(βₜ) ≤ numeratorShapeSharp R H D t, with its successor step relying on the weight-tracking lemma henselClearedResidual_weight (itself using henselClearedTerm_weight). Auxiliary lemmas provide RegularWeightLe instances for common 𝕃 H elements (e.g., RWL_lift, RWL_W, RWL_X, RWL_fieldTo, RWL_binom_coeff, RWL_coeff_liftCoeff, RWL_W_sharp) and algebraic identities (betaSucc_eq_neg_clearedResidual). The proof contains two sorry gaps: one in henselClearedTerm_weight for the boundary summand (where p.1 = 0, j = d = R.natDegree >= 2, p.2 = t+1), and one in numerator_shape_weight_sharp for the degenerate case natDegreeY R = 1.

• ArkLib/Data/Polynomial/RationalFunctions/Lifts.lean: This new file introduces the notions of regular lifts into function fields from Appendix A of [BCIKS20]. It defines liftToFunctionField and liftBivariate as ring homomorphisms from coefficient polynomials and bivariate polynomials, respectively, into the function field 𝕃 H; functionFieldT as the image of the polynomial variable; fieldTo𝕃 as the scalar embedding; and polyToPowerSeries𝕃 as a power series via lifted coefficients. Key lemmas establish that images of these lifts are regular elements of the function field under various conditions: liftToFunctionField_ne_zero shows nonzero coefficient polynomials remain nonzero assuming H is irreducible of positive Y-degree; regularElementsSet_liftToFunctionField_div_of_dvd and regularElementsSet_liftToFunctionField_div_leadingCoeff_of_dvd handle divisibility by the leading coefficient; W_pow_mul_eval₂_div_eq_sum gives a sum decomposition for clearing denominators; and regularElementsSet_eval₂_linear_of_coeff_one_dvd and regularElementsSet_mul_pow_eval₂_div_of_natDegree_le_succ_of_coeff_succ_dvd provide sufficient conditions for regularity of evaluations at T / W.

• ArkLib/Data/Polynomial/RationalFunctions/RationalRootVanishing.lean: This new file adds definitions and theorems for Appendix A of the BCIKS20 paper on rational-root vanishing. It defines H_tilde_prime_coeff_natDegree_le_of_totalDegree bounding coefficients of H_tilde' H, canonicalRep_coeff_natDegree_le_of_weight_bound bounding coefficients of the canonical representation via weight, embedding_eq_zero_of_resultant_zero showing the embedding vanishes when the resultant of the canonical representation and H_tilde' H is zero, natDegree_det_le_of_perm_products_le bounding the determinant's degree by the product degrees, natDegree_resultant_le_weight_bound bounding the resultant's degree, poly_eq_zero_of_ncard_gt_bound_of_subset_roots that a polynomial is zero if it has too many roots, resultant_eval_eq_resultant_map_eval_fixed_degrees relating evaluation of resultant to resultant of maps, resultant_fixed_degree_eq_zero_of_common_root_of_monic_right giving a condition for zero resultant, Sbeta_subset_resultant_roots embedding the set S_β β into roots of the resultant, weight_bot_embedding_zero that embedding is zero when the weight is ⊥, and the key lemma lemmaA1_embedding_eq_zero_of_many_rational_roots (Lemma A.1) establishing that the embedding is zero when the set S_β β has cardinality exceeding the weight times H.natDegree. The file also imports several Mathlib modules for polynomials, resultants, and principal ideal domains, and opens Polynomial, Polynomial.Bivariate, ToRatFunc, and Ideal.

• ArkLib/Data/Polynomial/RationalFunctions/Weight.lean: This file introduces the Λ-weight function weight_Λ on bivariate polynomials F[X][Y] over a domain F, along with its extension weight_Λ_over_𝒪 to the quotient ring 𝒪 H = F[X][Y]/(H_tilde' H). It proves basic algebraic properties of weight_Λ (invariance under negation, sub-additivity for sum/subtraction/finite sums, bounds for monomials/C c/C c*X^k, and a sub-additivity lemma weight_Λ_C_mul_X_pow_mul_le for multiplication by C c * X^k). It also proves key lemmas about the monic associate H_tilde' H: that weight_Λ of H_tilde' H is bounded by H.natDegree * (D+1-natDegreeY H) (Lemma weight_Λ_H_tilde'_le), that subtracting a suitable multiple of H_tilde' H from a polynomial does not increase its Λ-weight (weight_Λ_sub_leadingCoeff_mul_H_tilde'_le), and that reduction modulo H_tilde' H (p %ₘ H_tilde' H) is Λ-weight non-increasing (weight_Λ_modByMonic_H_tilde'_le). The file then defines the set S_β from Lemma A.1 of [BCIKS20] and provides auxiliary lemmas natDegree_H_tilde', canonicalRepOf𝒪_natDegree_lt_H, and π_z_eq_eval_canonicalRepOf𝒪. No sorry or admit are present.

• docs/kb/audits/bciks20-appendix-a-rational-functions.md: Summary unavailable — error: 1 validation error for _ProseSummary
  Invalid JSON: expected value at line 1 column 1 [type=json_invalid, input_value='The documentation was up...e of the formalization.', input_type=str]
  For further information visit https://errors.pydantic.dev/2.13/v/json_invalid

• 4 file(s) filtered as noise (lockfiles, generated, or trivial): docs/kb/_generated/declarations.json, docs/kb/_generated/dedup-report.md, docs/kb/_generated/lean-citations.json, docs/kb/log.md

---

Last updated: 2026-07-14 13:35 UTC.

[github-actions]

🤖 AI Review

Overall Summary:
TL;DR: The PR successfully introduces the positive Y-degree requirement for the extracted polynomial H across the function field construction, but it requires changes due to unresolved sorrys and a critical underspecification of the Hensel lift numerator β.

Mechanical Pre-Check Results: Mechanical pre-checks reveal numerous sorry escape hatches remaining in RationalFunctions.lean, Extraction.lean, and Agreement.lean, which violate the strict kernel verification policy.

Checklist Coverage: No explicit checklist was provided for this PR.

Cross-File Issues: The degree constraint on H is excellently threaded across the PR via typeclasses ([Fact (0 < H.natDegree)]). However, cross-file analysis reveals that the existential witness for β_regular was trivialized to 0, decoupling the extracted β from its true mathematical definition and breaking downstream algebraic composition.

Critical Misformalizations:

• Underspecification of β due to a trivialized existential witness. β_regular only asserts the existence of an element satisfying a weight bound, and the PR replaces the sorry here with a trivial proof (fun _ => ⟨0, by simp⟩). Consequently, β R t (defined via .choose) evaluates to an arbitrary value instead of the required Hensel lift numerator, breaking theorems like approximate_solution_is_exact_solution_coeffs. (ArkLib/Data/Polynomial/RationalFunctions.lean:783-799)

Key Lean 4 / Mathlib Issues:

• The PR contains unresolved sorry escape hatches, which bypass the Lean kernel and leave the formal verification incomplete. All proofs must be completed. (ArkLib/Data/Polynomial/RationalFunctions.lean, ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Extraction.lean, ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean)

Overall Verdict: Changes Requested

---

🔍 **Mechanical Pre-Check Results**

Pre-existing escape hatches in touched files (context only, does not affect verdict):

• sorry in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean line 35: (Bivariate.evalX z.1 H).eval (Pz.eval x₀) = 0} sorry)
• sorry in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean line 38: 2 * D_Y Q ^ 2 * (D_X ((k + 1 : ℚ) / n) n m) * D_YZ Q := by sorry
• sorry in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean line 68: := by sorry
• sorry in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean line 87: sorry
• sorry in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean line 101: ) := by sorry
• sorry in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean line 130: (Pz (matching_set_is_a_sub_of_coeffs_of_close_proximity k h_gs h)).eval (ωs x)} sorry
• sorry in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean line 148: := by sorry
• sorry in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean line 167: * D := by sorry
• sorry in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Extraction.lean line 38: := sorry
• sorry in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Extraction.lean line 45: Bivariate.evalX x₀ (Bivariate.discr_y R) ≠ 0 := by sorry
• sorry in ArkLib/Data/Polynomial/RationalFunctions.lean line 136: sorry
• sorry in ArkLib/Data/Polynomial/RationalFunctions.lean line 567: embeddingOf𝒪Into𝕃 _ β = 0 := by sorry
• sorry in ArkLib/Data/Polynomial/RationalFunctions.lean line 687: sorry
• sorry in ArkLib/Data/Polynomial/RationalFunctions.lean line 699: sorry

🔗 **Cross-File Analysis**

Cross-File Analysis:

1. Composition Chains: The PR successfully fixes a mathematical gap in the function field construction by requiring the extracted polynomial H to have a strictly positive Y-degree. This constraint is correctly threaded across files: Extraction.lean provides the foundational lemma pg_candidatePairs_snd_natDegree_pos showing valid factors have positive degree. RationalFunctions.lean updates the Field instance for 𝕃 H to demand [Fact (0 < H.natDegree)], propagating this down to Hensel lifting primitives like α and γ. Finally, Agreement.lean stitches these together by extracting natDegree_H_pos and correctly passing it into the evaluations of α' and γ'. The interface composition here is structurally excellent.

2. Type-Flow: Typeclass instances flow properly. The explicit parameter hHdeg passed to α' and γ' is correctly repackaged into the [Fact (0 < H.natDegree)] instance required by the section variables in ClaimA2.

3. Axiom Impact & Issues: The PR admirably removes critical sorrys in the RationalFunctions.lean algebraic proofs. However, it replaces the sorry for β_regular with a trivial dummy proof (fun _ => ⟨0, by simp⟩). Because β is defined as the Classical.choose of β_regular, and β_regular only constrains the weight (which 0 trivially satisfies), β becomes completely decoupled from its true mathematical definition (the Hensel lift numerators). This underspecification breaks downstream proofs that rely on β behaving like the actual algorithm.

4. External Dependencies: Usage of Mathlib.RingTheory and FieldTheory (e.g., algEquivCMulXAddC, Polynomial.IsPrimitive) is entirely sound.

Cross-File Composition Issues:

• Underspecification of β due to a trivialized existential witness. β_regular only asserts the existence of an element satisfying a weight bound inequality. The PR replaces the sorry here with a trivial proof fun _ => ⟨0, by simp⟩ because 0 naturally has a minimal weight (⊥). Consequently, β R t (defined as the .choose of this lemma) evaluates to an arbitrary/trivial value instead of the required Hensel lift numerator. Downstream uses of α and γ will evaluate to mathematically meaningless values, breaking the composition chain for theorems like approximate_solution_is_exact_solution_coeffs which expect α to hold exact polynomial approximations. (ArkLib/Data/Polynomial/RationalFunctions.lean:783-799)
  • Suggested fix: Define β R t explicitly via its structural recurrence / algebraic identity (similar to how ξ is uniquely specified by its mapping equation). The weight bound should be formulated as a separate theorem about this explicitly defined β, rather than defining β as the arbitrary witness of the weight bound.

Axiom/Escape Hatch Impact: None

External Dependency Issues: None

Missing Cross-File Verification: None

Cluster: Function Field Y-Degree Fix (critical)

Are the new hypotheses 0 < H.natDegree correctly propagated from the polynomial factorization in Extraction.lean through the list decoding agreement in Agreement.lean to ensure the irreducibility of H_tilde and construction of the function field in RationalFunctions.lean?

📄 **Review for `ArkLib/Data/Polynomial/RationalFunctions.lean`**

Analysis:
VERDICT: Changes Requested. The PR introduces mathematical fixes for the function field construction but leaves several 'sorry' stubs, violating the strict escape hatch policy.

Context validation: The introduction of the positive Y-degree requirement (0 < H.natDegree) correctly resolves the irreducibility issue over the function field. The structural changes to definitions like H_tilde, isField_of_irreducible, and the ClaimA2 embeddings cleanly propagate this constraint via [Fact (0 < H.natDegree)].

Resolution leap: Despite the valid mathematical updates, the file retains unresolved sorry instances (e.g., Lemma_A_1, ξ_regular, weight_ξ_bound). These bypass the Lean kernel and immediately force a rejection under the escape hatch guidelines.

Verdict: Changes Requested

Critical Misformalizations: None

Lean 4 / Mathlib Issues:

• The file contains unresolved sorry escape hatches, which bypass the Lean kernel. All proofs must be completed, as sorry is strictly prohibited under the hard rules. (ArkLib/Data/Polynomial/RationalFunctions.lean)
  • Suggested fix: Replace sorry with fully verified proofs for Lemma_A_1, ξ_regular, and weight_ξ_bound.

Nitpicks: None

📄 **Review for `ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Extraction.lean`**

Analysis:
The pull request modifies Extraction.lean to explicitly prove that the natDegree of normalized factors of separable polynomials is strictly positive (> 0).

1. Mathematical Logic:

   • The lemma pg_natDegree_pos_of_mem_normalizedFactors_of_separable extracts a previously inline block of proof that shows if a polynomial H is an irreducible factor of a separable polynomial p, its degree must be strictly positive.
   • The proof goes by contradiction: If H.natDegree = 0, then H is a constant polynomial C (H.coeff 0). Since H must be separable (dividing a separable polynomial p), H.coeff 0 must be a unit in the base ring (here F[Z]). That implies H itself is a unit. However, H is irreducible and therefore cannot be a unit, resulting in a contradiction.
   • The lemma pg_candidatePairs_snd_natDegree_pos directly uses this property to show that the H component of any extracted pair (R, H) has positive degree. This neatly ties up the hypothesis required for H being non-trivial, which cascades into the function field constructions elsewhere (such as in RationalFunctions.lean where H_tilde irreducibility depends on 0 < H.natDegree).

2. Lean / Mathlib Validation:

   • The types match up perfectly. R : F[Z][X][Y] evaluated at x₀ yields an element of F[Z][X], and extracting factors yields H : F[Z][X].
   • Substitution of 1 ≤ q.natDegree with 0 < q.natDegree works definitionally in Lean for Nat type, ensuring a smooth refactor in pg_card_normalizedFactors_toFinset_le_natDegree.
   • The omit context bounds and type variables are consistent and properly managed.
   • No escape hatches (like sorry or axiom) have been introduced.

Everything is well-typed, mathematically sound, and properly integrated.

Verdict: Approved

Critical Misformalizations: None

Lean 4 / Mathlib Issues: None

Nitpicks: None

📄 **Review for `ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean`**

Analysis:
Verdict: Changes Requested.
Initial logic and parameters are validated. Standard processing applied to the mathematical updates regarding the positive degree requirement (0 < H.natDegree) for the function field construction. Final evaluation indicates the presence of sorry blocks in the modified declarations, which strictly violates kernel verification requirements.

Verdict: Changes Requested

Critical Misformalizations: None

Lean 4 / Mathlib Issues:

• The file contains sorry in multiple proofs, which acts as a kernel bypass and leaves the formal verification incomplete. (ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean:93)
  • Suggested fix: Complete the formal proofs and remove all instances of sorry.

Nitpicks: None

[github-actions]

🤖 PR Summary

sorry delta: -7 (7 removed) — net proof progress

The PR completes the formalization of Appendix A of BCIKS20 in the RationalFunctions module, which is now a directory of seven submodules. The core additions are complete proofs for Lemma A.1 (rational root vanishing) and Claim A.2 (Hensel numerator existence, uniqueness, and weight bounds). All previously sorry-marked declarations have been resolved and moved into their respective submodules; no sorry or admit remain in any file. The modularization also resolves several technical discrepancies with the paper (documented in the audit file). Downstream consumers in BCIKS20 list-decoding proofs have been updated to use the new module structure and renamed declarations, with minor adjustments to statement forms (e.g., coefficient conditions).

---

Statistics

Metric	Count
📝 Files Changed	14
✅ Lines Added	6062
❌ Lines Removed	698

---

Lean Declarations

✏️ Removed: 64 declaration(s)

ArkLib/Data/Polynomial/RationalFunctions.lean (64)

• abbrev 𝒪 (H : F[X][Y]) : Type
• abbrev 𝕃 (H : F[X][Y]) : Type
• def rationalRoot (H : F[X][Y]) (z : F) : Type
• def regularElms (H : F[X][Y]) : Type
• def regularElms_set (H : F[X][Y]) : Set (𝕃 H)
• def α (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [φ : Fact (Irreducible H)] (t : ℕ) : 𝕃 H
• def α' (x₀ : F) (R : F[X][X][Y]) (H_irreducible : Irreducible H) (t : ℕ) : 𝕃 H
• def β (R : F[X][X][Y]) (t : ℕ) : 𝒪 H
• def γ (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [φ : Fact (Irreducible H)] : PowerSeries (𝕃 H)
• def γ' (x₀ : F) (R : F[X][X][Y]) (H_irreducible : Irreducible H) : PowerSeries (𝕃 H)
• def ζ (R : F[X][X][Y]) (x₀ : F) (H : F[X][Y]) [H_irreducible : Fact (Irreducible H)] : 𝕃 H
• def ξ (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [φ : Fact (Irreducible H)] : 𝒪 H
• lemma H_tilde'_monic (H : F[X][Y]) (hH : 0 < H.natDegree) :
• lemma H_tilde_equiv_H_tilde' (H : F[X][Y]) : (H_tilde' H).map univPolyHom = H_tilde H
• lemma Lemma_A_1 {H : F[X][Y]} (hH : 0 < H.natDegree) (β : 𝒪 H) (D : ℕ)
• lemma canonicalRepOf𝒪_degree_lt {H : F[X][Y]} (hH : 0 < H.natDegree) (β : 𝒪 H) :
• lemma canonicalRepOf𝒪_mk {H : F[X][Y]} (hH : 0 < H.natDegree) (p : F[X][Y]) :
• lemma canonicalRepOf𝒪_mk_eq_self_of_degree_lt {H : F[X][Y]} (hH : 0 < H.natDegree)
• lemma canonicalRepOf𝒪_natDegree_le {H : F[X][Y]} (hH : 0 < H.natDegree) (β : 𝒪 H) :
• lemma canonicalRepOf𝒪_zero {H : F[X][Y]} (hH : 0 < H.natDegree) :
• lemma embeddingOf𝒪Into𝕃_mk (H : F[X][Y]) (p : F[X][Y]) :
• lemma irreducibleHTildeOfIrreducible {H : Polynomial (Polynomial F)} :
• lemma isField_of_irreducible {H : F[X][Y]} : Irreducible H → IsField (𝕃 H)
• lemma liftBivariate_C {H : F[X][Y]} (p : F[X]) :
• lemma liftBivariate_X {H : F[X][Y]} :
• lemma mk_canonicalRepOf𝒪 {H : F[X][Y]} (hH : 0 < H.natDegree) (β : 𝒪 H) :
• lemma regularElms_set_add {H : F[X][Y]} {a b : 𝕃 H}
• lemma regularElms_set_functionFieldT (H : F[X][Y]) :
• lemma regularElms_set_liftBivariate (H : F[X][Y]) (p : F[X][Y]) :
• lemma regularElms_set_liftToFunctionField (H : F[X][Y]) (p : F[X]) :
• lemma regularElms_set_mul {H : F[X][Y]} {a b : 𝕃 H}
• lemma regularElms_set_neg {H : F[X][Y]} {a : 𝕃 H}
• lemma regularElms_set_one (H : F[X][Y]) : (1 : 𝕃 H) ∈ regularElms_set H
• lemma regularElms_set_pow {H : F[X][Y]} {a : 𝕃 H}
• lemma regularElms_set_sub {H : F[X][Y]} {a b : 𝕃 H}
• lemma regularElms_set_zero (H : F[X][Y]) : (0 : 𝕃 H) ∈ regularElms_set H
• lemma regular_liftBivariate (H : F[X][Y]) (p : F[X][Y]) :
• lemma regular_liftToFunctionField (H : F[X][Y]) (p : F[X]) :
• lemma weight_Λ_over_𝒪_mk {H : F[X][Y]} (hH : 0 < H.natDegree) (p : F[X][Y])
• lemma weight_Λ_over_𝒪_mk_eq_self_of_degree_lt {H : F[X][Y]} (hH : 0 < H.natDegree)
• lemma weight_Λ_over_𝒪_zero {H : F[X][Y]} (hH : 0 < H.natDegree) (D : ℕ) :
• lemma weight_Λ_zero (H : F[X][Y]) (D : ℕ) :
• lemma weight_ξ_bound (x₀ : F) (hH : 0 < H.natDegree) {D : ℕ}
• lemma β_regular (R : F[X][X][Y])
• lemma ζ_regular_of_derivative_evalX_eq_C (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• lemma ξ_regular (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [H_irreducible : Fact (Irreducible H)] :
• lemma ξ_regular_of_derivative_evalX_eq_C_of_natDegree_le_one
• noncomputable def H_tilde (H : F[X][Y]) : Polynomial (RatFunc F)
• noncomputable def H_tilde' (H : F[X][Y]) : F[X][Y]
• noncomputable def S_β {H : F[X][Y]} (β : 𝒪 H) : Set F
• noncomputable def canonicalRepOf𝒪 {H : F[X][Y]} (hH : 0 < H.natDegree) (β : 𝒪 H) : F[X][Y]
• noncomputable def coeffAsRatFunc : F[X] →+* Polynomial (RatFunc F)
• noncomputable def embeddingOf𝒪Into𝕃 (H : F[X][Y]) : 𝒪 H →+* 𝕃 H
• noncomputable def fieldTo𝕃 {H : F[X][Y]} : F →+* 𝕃 H
• noncomputable def functionFieldT {H : F[X][Y]} : 𝕃 H
• noncomputable def liftBivariate {H : F[X][Y]} : F[X][Y] →+* 𝕃 H
• noncomputable def liftToFunctionField {H : F[X][Y]} : F[X] →+* 𝕃 H
• noncomputable def polyToPowerSeries𝕃 (H : F[X][Y]) (P : F[X][Y]) : PowerSeries (𝕃 H)
• noncomputable def weight_Λ (f H : F[X][Y]) (D : ℕ) : WithBot ℕ
• noncomputable def weight_Λ_over_𝒪 {H : F[X][Y]} (hH : 0 < H.natDegree) (f : 𝒪 H) (D : ℕ) :
• noncomputable def π_z {H : F[X][Y]} (z : F) (root : rationalRoot (H_tilde' H) z) : 𝒪 H →+* F
• noncomputable def π_z_lift {H : F[X][Y]} (z : F) (root : rationalRoot (H_tilde' H) z) :
• private lemma monicize_leading_term {K : Type} [Field K] (a : K) (d : ℕ)
• private lemma monicize_term {K : Type} [Field K] (a b : K) (i d : ℕ)

✏️ Added: 245 declaration(s)

ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean (4)

• lemma H_dvd_evalX_R (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :
• lemma claimA2_hypotheses (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :
• lemma evalX_R_separable (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :
• lemma natDegree_H_pos (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :

ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Extraction.lean (2)

• theorem pg_candidatePairs_snd_natDegree_pos (x₀ : F)
• theorem pg_natDegree_pos_of_mem_normalizedFactors_of_separable (p : F[Z][X])

ArkLib/Data/Polynomial/RationalFunctions/FunctionField.lean (39)

• abbrev 𝒪 (H : F[X][Y]) : Type
• abbrev 𝕃 (H : F[X][Y]) : Type
• def rationalRoot (H : F[X][Y]) (z : F) : Type
• def regularElementsSet (H : F[X][Y]) : Set (𝕃 H)
• lemma canonicalRepOf𝒪_degree_lt {H : F[X][Y]} (hH : 0 < H.natDegree) (β : 𝒪 H) :
• lemma canonicalRepOf𝒪_mk {H : F[X][Y]} (hH : 0 < H.natDegree) (p : F[X][Y]) :
• lemma canonicalRepOf𝒪_mk_eq_self_of_degree_lt {H : F[X][Y]} (hH : 0 < H.natDegree)
• lemma canonicalRepOf𝒪_zero {H : F[X][Y]} (hH : 0 < H.natDegree) :
• lemma embeddingOf𝒪Into𝕃_injective {H : F[X][Y]} (hHdeg : 0 < H.natDegree) :
• lemma irreducible_monicize {H : F[X][Y]} (hHdeg : 0 < H.natDegree)
• lemma irreducible_monicizeRatFunc {F : Type} [Field F] {H : Polynomial (Polynomial F)}
• lemma irreducible_monicizeRatFunc_of_natDegree_pos
• lemma isField_of_irreducible {F : Type} [Field F] {H : F[X][Y]} (hHdeg : 0 < H.natDegree) :
• lemma isField_of_irreducible_of_natDegree_pos {F : Type} [Field F] {H : F[X][Y]}
• lemma map_monicize_eq_monicizeRatFunc (H : F[X][Y]) : (monicize H).map univPolyHom = monicizeRatFunc
• lemma mk_canonicalRepOf𝒪 {H : F[X][Y]} (hH : 0 < H.natDegree) (β : 𝒪 H) :
• lemma monicize_dvd_of_map_dvd_monicizeRatFunc {H p : F[X][Y]} (hHdeg : 0 < H.natDegree)
• lemma monicize_monic (H : F[X][Y]) (hH : 0 < H.natDegree) :
• lemma regularElementsSet_add {H : F[X][Y]} {a b : 𝕃 H}
• lemma regularElementsSet_mul {H : F[X][Y]} {a b : 𝕃 H}
• lemma regularElementsSet_neg {H : F[X][Y]} {a : 𝕃 H}
• lemma regularElementsSet_one (H : F[X][Y]) : (1 : 𝕃 H) ∈ regularElementsSet H
• lemma regularElementsSet_pow {H : F[X][Y]} {a : 𝕃 H}
• lemma regularElementsSet_prod {ι : Type} {H : F[X][Y]} (s : Finset ι) {f : ι → 𝕃 H}
• lemma regularElementsSet_sub {H : F[X][Y]} {a b : 𝕃 H}
• lemma regularElementsSet_sum {ι : Type} {H : F[X][Y]} (s : Finset ι) {f : ι → 𝕃 H}
• lemma regularElementsSet_zero (H : F[X][Y]) : (0 : 𝕃 H) ∈ regularElementsSet H
• lemma univPolyHom_injective :
• noncomputable def canonicalRepOf𝒪 {H : F[X][Y]} (hH : 0 < H.natDegree) (β : 𝒪 H) : F[X][Y]
• noncomputable def embeddingOf𝒪Into𝕃 (H : F[X][Y]) : 𝒪 H →+* 𝕃 H
• noncomputable def monicize (H : F[X][Y]) : F[X][Y]
• noncomputable def monicizeRatFunc (H : F[X][Y]) : Polynomial (RatFunc F)
• noncomputable def piZ {H : F[X][Y]} (z : F) (root : rationalRoot (monicize H) z) :
• noncomputable def piZLift {H : F[X][Y]} (z : F) (root : rationalRoot (monicize H) z) :
• private lemma irreducible_comp_C_mul_X_iff {K : Type} [Field K] (a : K) (ha : a ≠ 0)
• private lemma irreducible_map_univPolyHom_of_irreducible
• private lemma mem_span_monicize_of_bivPolyHom_mem_span_monicizeRatFunc {H p : F[X][Y]}
• private lemma monicize_leading_term {K : Type} [Field K] (a : K) (d : ℕ)
• private lemma monicize_term {K : Type} [Field K] (a b : K) (i d : ℕ)

ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Hensel.lean (58)

• def AllCoeffRegular (H : F[X][Y]) (φ : PowerSeries (𝕃 H)) : Prop
• def HasNumeratorShape (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• def IsHenselNumeratorSequence (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• def defaultDegreeBound (R : F[X][X][Y]) (H : F[X][Y]) : ℕ
• def henselDenominatorExponent (t : ℕ) : ℕ
• def trivariateTotalDegree (R : F[X][X][Y]) : ℕ
• lemma coeff_totalDegree_add_index_le_trivariateTotalDegree (R : F[X][X][Y]) {i : ℕ}
• lemma defaultDegreeBound_ge_H (R : F[X][X][Y]) (H : F[X][Y]) :
• lemma defaultDegreeBound_ge_R_coeff (R : F[X][X][Y]) (H : F[X][Y]) {i : ℕ}
• lemma henselDenominatorExponent_succ (t : ℕ) :
• lemma henselDenominatorExponent_zero : henselDenominatorExponent 0 = 0
• noncomputable def alphaOfNumerators (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• noncomputable def alphaSeq (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• noncomputable def bSeq (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• noncomputable def evalRAtPowerSeries (x₀ : F) (H : F[X][Y]) (R : F[X][X][Y])
• noncomputable def gammaFromAlpha (H : F[X][Y]) (αseq : ℕ → 𝕃 H) :
• noncomputable def gammaOfNumerators (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• noncomputable def henselCoeffResidual (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• noncomputable def liftCoeffToPowerSeries (x₀ : F) (H : F[X][Y]) :
• theorem AllCoeffRegular.X {H : F[X][Y]} : AllCoeffRegular H (PowerSeries.X)
• theorem AllCoeffRegular.add {H : F[X][Y]} {φ ψ : PowerSeries (𝕃 H)}
• theorem AllCoeffRegular.const {H : F[X][Y]} {c : 𝕃 H} (hc : c ∈ regularElementsSet H) :
• theorem AllCoeffRegular.mul {H : F[X][Y]} {φ ψ : PowerSeries (𝕃 H)}
• theorem AllCoeffRegular.pow {H : F[X][Y]} {φ : PowerSeries (𝕃 H)}
• theorem AllCoeffRegular.zero {H : F[X][Y]} :
• theorem H_eval2_T_div_W_eq_zero (H : F[X][Y])
• theorem bSeq_eq_zero_of_gt (x₀ : F) (R : F[X][X][Y]) (N j : ℕ) (hj : N < j) :
• theorem bSeq_stable (x₀ : F) (R : F[X][X][Y]) (N i : ℕ) (hi : i ≤ N) :
• theorem bSeq_succ_def (x₀ : F) (R : F[X][X][Y]) (N : ℕ) :
• theorem bSeq_succ_eq_below (x₀ : F) (R : F[X][X][Y]) (N i : ℕ) (hi : i < N + 1) :
• theorem bSeq_zero (x₀ : F) (R : F[X][X][Y]) (N : ℕ) :
• theorem beta_zero_eq_X_of_shape (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem coeff_delta_below (x₀ : F) (R : F[X][X][Y]) (N i : ℕ) (hi : i < N + 1) :
• theorem coeff_evalR_split (x₀ : F) (R : F[X][X][Y]) (n : ℕ) (hn : 1 ≤ n)
• theorem coeff_evalR_stable (x₀ : F) (R : F[X][X][Y]) (n m : ℕ) (hm : m < n)
• theorem coeff_liftCoeff_regular (x₀ : F) (H : F[X][Y]) (p : F[X][X]) :
• theorem coeff_mul_eq_zero_of_orders {A : Type} [CommRing A] {m : ℕ}
• theorem coeff_mul_of_low_order {A : Type} [CommRing A] (n : ℕ) (P δ : PowerSeries A)
• theorem coeff_zero_evalR (x₀ : F) (R : F[X][X][Y]) (Γ : PowerSeries (𝕃 H)) :
• theorem constantCoeff_eval₂_derivative_eq_zeta (x₀ : F) (R : F[X][X][Y])
• theorem constantCoeff_eval₂_liftCoeff (x₀ : F) (q : F[X][X][Y]) (Γ : PowerSeries (𝕃 H)) :
• theorem constantCoeff_liftCoeffToPowerSeries (x₀ : F) (p : F[X][X]) :
• theorem evalX_totalDegree_le_of_coeff_bound (x₀ : F) (R : F[X][X][Y]) {D : ℕ}
• theorem exists_hensel_alpha_sequence (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem fieldTo𝕃_regular (x₀ : F) (H : F[X][Y]) :
• theorem formalHenselAlphaSequence (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem gammaOfNumerators_eq_gammaFromAlpha (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem henselClearedTerm_regular (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem henselCoeffResidual_eq_trunc (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem henselCoeffResidual_regular_after_clearing (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem hensel_alpha_sequence_unique (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem hensel_numerator_sequence_of_alpha_shape (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem initial_root_at_x0 (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem mk_bSeq_coeff_eq (x₀ : F) (R : F[X][X][Y]) (N i : ℕ) (hi : i ≤ N) :
• theorem mk_monicizeRatFunc_eq_leadingCoeff_pow_mul_eval₂ (H : F[X][Y])
• theorem remainder_low_order {A B : Type} [CommRing A] [CommRing B] (n : ℕ)
• theorem root_bSeq (x₀ : F) (R : F[X][X][Y])
• theorem zeta_ne_zero_of_hypotheses (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])

ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Sequence.lean (16)

• def alpha (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [φ : Fact (Irreducible H)]
• def alpha' (x₀ : F) (R : F[X][X][Y]) (H_irreducible : Irreducible H)
• def gamma (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [φ : Fact (Irreducible H)]
• def gamma' (x₀ : F) (R : F[X][X][Y]) (H_irreducible : Irreducible H)
• lemma betaSeq_spec (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• lemma betaSeq_weight_le (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• lemma betaSeq_weight_le_defaultDegreeBound (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• lemma betaSeq_weight_sharp_le (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• lemma betaSeq_weight_sharp_le_defaultDegreeBound (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• lemma exists_hensel_numerator_sequence (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• noncomputable def betaSeq (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem IsHenselNumeratorSequence.eq_betaSeq (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem IsHenselNumeratorSequence.unique (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem claimA2_exists_numerators_with_weight_bounds (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem exists_regular_numerator_shape (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• theorem regular_numerator_shape_succ (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])

ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Setup.lean (30)

• def zeta (R : F[X][X][Y]) (x₀ : F) (H : F[X][Y]) [H_irreducible : Fact (Irreducible H)]
• lemma derivative_evalX_coeff (x₀ : F) (R : F[X][X][Y]) (i : ℕ) :
• lemma derivative_evalX_eq_C_of_natDegree_le_one
• lemma embeddingOf𝒪Into𝕃_mk_xiPre (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• lemma embeddingOf𝒪Into𝕃_xi (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])
• lemma evalX_ne_zero_of_hypotheses {x₀ : F} {R : F[X][X][Y]} {H : F[X][Y]}
• lemma leadingCoeff_dvd_evalX_coeff_natDegree {x₀ : F} {R : F[X][X][Y]} {H : F[X][Y]}
• lemma leadingCoeff_dvd_evalX_derivative_coeff_pred {x₀ : F} {R : F[X][X][Y]} {H : F[X][Y]}
• lemma leadingCoeff_dvd_evalX_leadingCoeff {x₀ : F} {R : F[X][X][Y]} {H : F[X][Y]}
• lemma natDegree_H_le_natDegree_R_of_hypotheses {x₀ : F} {R : F[X][X][Y]} {H : F[X][Y]}
• lemma natDegree_derivative_evalX_coeff_le (x₀ : F) (R : F[X][X][Y]) {D i : ℕ}
• lemma xi_regular (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [H_irreducible : Fact (Irreducible H)]
• lemma xi_weight_le (x₀ : F) (hH : 0 < H.natDegree) (hHyp : Hypotheses x₀ R H)
• noncomputable def xi (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [_φ : Fact (Irreducible H)]
• noncomputable def xiPre (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) : F[X][Y]
• noncomputable def xiPreLower (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) : F[X][Y]
• noncomputable def xiPreTop (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) : F[X][Y]
• private lemma evalX_natDegree_le {K : Type} [CommSemiring K] (x : K) (P : K[X][Y]) :
• theorem cofactor_top_reduction_weight_le {H : F[X][Y]} (hH : 0 < H.natDegree) {Q : F[X][Y]}
• theorem leadingCoeff_natDegree_le_of_totalDegree_le {D : ℕ} (hD_H : Bivariate.totalDegree H ≤ D) :
• theorem regularWeight_add_le {H : F[X][Y]} {D : ℕ} (hD_H : Bivariate.totalDegree H ≤ D)
• theorem xiPreLower_coeff_natDegree_le (x₀ : F) {D i : ℕ}
• theorem xiPreLower_term_weight_le (x₀ : F) (hHyp : Hypotheses x₀ R H) (hH : 0 < H.natDegree)
• theorem xiPreLower_weight_le (x₀ : F) (hHyp : Hypotheses x₀ R H) (hH : 0 < H.natDegree)
• theorem xiPreTop_coeff_natDegree_zero_of_H_natDegree_eq_R_natDegree (x₀ : F) (hH : 0 < H.natDegree)
• theorem xiPreTop_modByMonic_coeff_natDegree_le (x₀ : F) (hH : 0 < H.natDegree)
• theorem xiPreTop_modByMonic_weight_le (x₀ : F) (hH : 0 < H.natDegree) (hHyp : Hypotheses x₀ R H)
• theorem xiPreTop_weight_over_𝒪_le (x₀ : F) (hH : 0 < H.natDegree) (hHyp : Hypotheses x₀ R H)
• theorem xiPreTop_weight_over_𝒪_le_of_H_natDegree_lt_R_natDegree (x₀ : F) (hH : 0 < H.natDegree)
• theorem xiPre_eq_lower_add_top (x₀ : F) (hRdeg : 2 ≤ R.natDegree) :

ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Weight.lean (28)

• def RegularWeightLe {H : F[X][Y]} (hH : 0 < H.natDegree) (a : 𝕃 H) (D B : ℕ) : Prop

…and 95 more not listed.

---

sorry Tracking

✅ Removed: 7 `sorry`(s)

ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean (2)

• lemma exists_factors_with_large_common_root_set (δ : ℚ) (x₀ : F) (L35)
• noncomputable def matching_set_at_x (L130)

ArkLib/Data/Polynomial/RationalFunctions.lean (5)

• lemma Lemma_A_1 {H : F[X][Y]} (hH : 0 < H.natDegree) (β : 𝒪 H) (D : ℕ) (L471)
• lemma irreducibleHTildeOfIrreducible {H : Polynomial (Polynomial F)} : (L52)
• lemma weight_ξ_bound (x₀ : F) (hH : 0 < H.natDegree) {D : ℕ} (L604)
• lemma β_regular (R : F[X][X][Y]) (L614)
• lemma ξ_regular (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [H_irreducible : Fact (Irreducible H)] : (L592)

---

📋 **Additional Analysis**

The diff appears to be a substantial contribution of a new Appendix A package for BCIKS20. The code adheres to the project's naming and style conventions (UpperCamelCase files, lowerCamelCase functions, snake_case theorems, proper headers, consistent indentation). The commit message format cannot be verified from the raw diff. There are no obvious violations of the provided guidelines. Since the deployment-supplied instructions are generic contribution guidelines rather than a specific review framework, no actionable findings are identified.

---

📄 **Per-File Summaries**

• ArkLib.lean: The file now imports seven new modules under ArkLib.Data.Polynomial.RationalFunctions: FunctionField, HenselNumerators.Hensel, HenselNumerators.Sequence, HenselNumerators.Setup, HenselNumerators.Weight, Lifts, RationalRootVanishing, and Weight. These imports make available additional definitions, theorems, and structures related to rational functions, Hensel lifting, and weight computations, expanding the project’s polynomial and rational‑function infrastructure.
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean: The Agreement.lean file undergoes several interrelated changes to adapt the BCIKS20 list-decoding proofs to the refactored RationalFunctions module structure, replacing the previous BCIKS20AppendixA namespace. The exists_factors_with_large_common_root_set lemma gains two new conclusion fields: 0 < H.natDegree and (Bivariate.evalX (Polynomial.C x₀) R).Separable (the Fintype.ofFinite _ argument replaces the former sorry in the cardinality set). Two new lemmas natDegree_H_pos, H_dvd_evalX_R, and evalX_R_separable extract these fields, and a new lemma claimA2_hypotheses bundles them into the Hypotheses type from RationalFunctions.HenselNumerators. All open imports switch from BCIKS20AppendixA.ClaimA2 to RationalFunctions.HenselNumerators; correspondingly, calls to α', γ', 𝕃, and polyToPowerSeries𝕃 are now qualified under RationalFunctions instead of BCIKS20AppendixA. The statements of approximate_solution_is_exact_solution_coeffs and approximate_solution_is_exact_solution_coeffs' change their coefficient condition from ∀ t ≥ k / if t ≥ k to ∀ t > k / if t > k, and their hypotheses now include (natDegree_H_pos k h_gs) and (claimA2_hypotheses k h_gs). The solution_gamma_is_linear_in_Z and gamma_eq_P lemmas similarly acquire the two new arguments. The matching_set_at_x definition replaces its final sorry with (Fintype.ofFinite _). A large docstring on claimA2_hypotheses explains that the deg_Y R ≥ 2 weight bounds (needed for the Hensel machinery) are not derivable from Claim 5.7 and must be handled by a case split in §5.
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Extraction.lean: Two new theorems are added: pg_natDegree_pos_of_mem_normalizedFactors_of_separable (proves any normalized factor of a separable polynomial has positive natDegree) and pg_candidatePairs_snd_natDegree_pos (derives the same positivity for the second component of pg_candidatePairs under the given separability hypothesis). The existing pg_card_normalizedFactors_toFinset_le_natDegree is refactored to use the first new lemma instead of inlining the same argument, removing code duplication. Both new theorems carry the omit [DecidableEq (RatFunc F)] [Finite F] that was already present on the existing theorem. No sorry or admit are introduced.
• ArkLib/Data/Polynomial/RationalFunctions.lean: The file has been completely rewritten from a monolithic module containing all definitions and proofs relating to Appendix A of [BCIKS20] into a lightweight umbrella import that re‑exports seven submodules (FunctionField, Weight, RationalRootVanishing, Lifts, HenselNumerators/Setup, HenselNumerators/Hensel, HenselNumerators/Weight, HenselNumerators/Sequence). The new file adds a comprehensive module‑level docstring that describes the setting, layout, main results (notably lemmaA1_embedding_eq_zero_of_many_rational_roots, the HenselNumerators existence/uniqueness/weight‑bound theorems), and two documented deviations from the paper. All previously sorry‑marked declarations (irreducibleHTildeOfIrreducible, Lemma_A_1, ξ_regular, weight_ξ_bound, β_regular) have been removed from this file; the corresponding definitions and proofs now live in the respective submodules. This reorganization modularizes the formalization and provides a central orientation point for reviewers and downstream users.
• ArkLib/Data/Polynomial/RationalFunctions/FunctionField.lean: This 607-line file ArkLib/Data/Polynomial/RationalFunctions/FunctionField.lean is a new addition implementing the algebraic construction from Appendix A.1 and A.3 of the BCIKS20 paper. It defines:

monicizeRatFunc H as a monic polynomial in (RatFunc F)[T] from a bivariate polynomial H ∈ F[Z][Y], and proves its irreducibility when H is irreducible with positive Y-degree via irreducible_monicizeRatFunc_of_natDegree_pos and irreducible_monicizeRatFunc. The function field 𝕃 H = (RatFunc F)[T]/(monicizeRatFunc H) is defined as an abbrev, and it is shown to be a field when H is irreducible and has positive Y-degree via isField_of_irreducible_of_natDegree_pos and isField_of_irreducible, with a corresponding noncomputable instance.

The integral monicization monicize H ∈ F[Z][Y] is defined and proven monic via monicize_monic. The file establishes that map_monicize_eq_monicizeRatFunc ensures compatibility under the embedding to (RatFunc F)[T], and uses this to prove irreducible_monicize descends irreducibility to F[Z][Y].

The ring of regular elements 𝒪 H = F[Z][Y]/(monicize H) is introduced as an abbrev with a ring instance. The embedding embeddingOf𝒪Into𝕃 H : 𝒪 H →+* 𝕃 H is defined, and its injectivity is proven (embeddingOf𝒪Into𝕃_injective) under the positive-degree hypothesis using the divisibility lemma monicize_dvd_of_map_dvd_monicizeRatFunc.

The set regularElementsSet H is defined as the image of 𝒪 H in 𝕃 H, and lemmas regularElementsSet_zero, regularElementsSet_one, regularElementsSet_add, regularElementsSet_neg, regularElementsSet_sub, regularElementsSet_mul, regularElementsSet_pow, regularElementsSet_sum, regularElementsSet_prod show it is closed under all ring operations.

Finally, the rational substitution piZ : 𝒪 H →+* F is defined (for a rationalRoot of monicize H at z), and the canonicalRepOf𝒪 function gives a degree-reduced representative with associated lemmas canonicalRepOf𝒪_degree_lt, mk_canonicalRepOf𝒪, canonicalRepOf𝒪_mk, canonicalRepOf𝒪_zero, and canonicalRepOf𝒪_mk_eq_self_of_degree_lt.

The diff contains no sorry or admit statements.

• ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Hensel.lean: This new file (1137 lines) formalizes the Hensel/Newton iteration for the bivariate rational function setting of [BCIKS20] Appendix A.4. It defines the exponent pattern henselDenominatorExponent, the degree bounds trivariateTotalDegree and defaultDegreeBound, the power-series evaluation evalRAtPowerSeries (with the shift X ↦ x₀ + S), and constructs coefficient sequences alphaOfNumerators/gammaOfNumerators from regular numerators. Key theorems establish existence and uniqueness of the Hensel lift (formalHenselAlphaSequence, hensel_alpha_sequence_unique), the splitting of the residual (coeff_evalR_split), the base-case numerator identity (beta_zero_eq_X_of_shape), first-order Taylor expansion in power series (remainder_low_order), and the regularity half of Claim A.2 (henselCoeffResidual_regular_after_clearing). The file is complete (no sorry/admit) and depends on earlier imports (Bivariate, Prelims, Setup).

• ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Sequence.lean: This new file formalizes the Hensel numerator sequence (Claim A.2 of [BCIKS20]) in Lean 4. It provides two core theorems: regular_numerator_shape_succ (one-step numerator recursion) and exists_regular_numerator_shape (existence of a sequence βseq satisfying the shape condition). Using these, exists_hensel_numerator_sequence delivers the existence of a sequence of regular numerators βseq with the Hensel-lift semantics, and the noncomputable definition betaSeq selects a canonical such sequence via betaSeq_spec. Uniqueness is proved in IsHenselNumeratorSequence.unique and IsHenselNumeratorSequence.eq_betaSeq. Weight bounds (sharp and loose) for the chosen sequence are then stated as lemmas betaSeq_weight_sharp_le and betaSeq_weight_le, with specialized versions using defaultDegreeBound. The theorem claimA2_exists_numerators_with_weight_bounds bundles existence and both weight estimates. Finally, convenience definitions alpha, alpha', gamma, gamma' expose the induced Hensel-lift coefficients and power series. No sorry or admit appears in the diff.

• ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Setup.lean: This new file, ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Setup.lean, formalizes the setup for Claim A.2 of [BCIKS20], introducing the Hypotheses structure (requiring H ∣ R(x₀,·,Z) and separability of R(x₀,·,Z) in Y) and the key objects zeta (the specialized derivative ∂R/∂Y evaluated at T/W in the function field 𝕃 H) and xi (a quotient representative of W^(d-2)·ζ in 𝒪 H). It proves the algebraic identity embeddingOf𝒪Into𝕃_xi linking these, establishes several divisibility and degree-bound lemmas for the leading coefficient W = H.leadingCoeff (e.g., leadingCoeff_dvd_evalX_leadingCoeff, leadingCoeff_dvd_evalX_derivative_coeff_pred, leadingCoeff_natDegree_le_of_totalDegree_le), and provides the main weight bound xi_weight_le stating Λ(ξ) ≤ (d-1)(D - dH + 1) under the assumption 2 ≤ R.natDegree. The proof of this bound decomposes xiPre into a low part (xiPreLower) and a top term (xiPreTop), proving weight bounds for each via auxiliary results like xiPreLower_weight_le, xiPreTop_weight_over_𝒪_le, cofactor_top_reduction_weight_le, and regularWeight_add_le. The file contains no sorry or admit.

• ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Weight.lean: This new file (Weight.lean) introduces a RegularWeightLe certificate predicate and a large collection of supporting lemmas that track the Λ-weight (regular weight) of elements in the field 𝕃 H during Hensel-clearing expansions. It defines the sharp per‑step budget numeratorShapeSharp and proves it weakens to the loose paper bound (2t+1)·natDegreeY(R)·D. The main theorem numerator_shape_weight_sharp (proved by strong induction using henselClearedResidual_weight) establishes that every Hensel numerator βₜ has a RegularWeightLe certificate with budget numeratorShapeSharp R H D t, and the wrapping theorems hensel_numerator_weight_sharp_le and hensel_numerator_weight_le state the corresponding weight inequalities for an arbitrary Hensel numerator sequence. All proofs are complete (no sorry or admit).

• ArkLib/Data/Polynomial/RationalFunctions/Lifts.lean: This new file adds the coefficient and bivariate lifts into the function field 𝕃 H (liftToFunctionField, liftBivariate, functionFieldT) and proves that these lifts send polynomials to regular elements (regularElementsSet_liftBivariate, regularElementsSet_liftToFunctionField, liftToFunctionField_ne_zero, etc.). It establishes denominator‑clearing identities (leadingCoeff_pow_mul_eval₂_div_eq_sum, regularElementsSet_mul_pow_eval₂_div_of_natDegree_le_succ_of_coeff_succ_dvd) that are used to keep Hensel‑lift coefficients inside 𝒪. Finally, it extends the substitution π_z to quotients β/C via piZOfDiv, proves well‑definedness (piZOfDiv_congr), and provides a vanishing criterion (piZOfDiv_eq_zero_iff), which are used in §5 of BCIKS20. No sorry or admit appear.

• ArkLib/Data/Polynomial/RationalFunctions/RationalRootVanishing.lean: This single-file addition proves Lemma A.1 of [BCIKS20]. Nine new theorems are introduced:

• natDegree_coeff_monicize_le_of_totalDegree_le and canonicalRep_coeff_natDegree_le_of_weight_bound — weight bounds on monomials of H̃ and of the canonical representative of β.

• embedding_eq_zero_of_resultant_zero — vanishing resultant forces β = 0 in 𝕃.

• natDegree_det_le_of_perm_products_le — degree bound for a determinant from its Leibniz expansion.

• natDegree_resultant_le_weight_bound — deg_Z res_T(β, H̃) ≤ Λ(β)·dH.

• poly_eq_zero_of_ncard_gt_bound_of_subset_roots — a polynomial with too many roots is zero.

• resultant_eval_eq_resultant_map_eval_fixed_degrees — evaluation and fixed-degree resultant commute.

• resultant_fixed_degree_eq_zero_of_common_root_of_monic_right — common root forces resultant zero.

• rationalVanishingSet_subset_resultant_roots — each rational vanishing point is a root of the resultant.

• embedding_eq_zero_of_weight_eq_bot — weight ⊥ forces β = 0.

The main lemma lemmaA1_embedding_eq_zero_of_many_rational_roots assembles them: given enough rational roots, the resultant is zero, hence β embeds to zero.

No sorry or admit are present.

• ArkLib/Data/Polynomial/RationalFunctions/Weight.lean: This new file defines the algebraic weight function Λ (as weight) for bivariate polynomials F[X][Y], associates regularWeight for the quotient ring 𝒪 H, and proves a suite of lemmas establishing its algebraic properties (invariance under negation, sub-additivity for addition/subtraction/sums/multiplication, exact additivity via weight_mul, and bounds for special monomials). It also proves that reduction modulo monicize H does not increase weight (weight_modByMonic_monicize_le and related lemmas), derives exact weight formulas for monicize H (weight_monicize), and introduces rationalVanishingSet with a lemma evaluating piZ on canonical representatives. No sorry or admit appear in the diff.
• docs/kb/audits/bciks20-appendix-a-rational-functions.md: The diff updates docs/kb/audits/bciks20-appendix-a-rational-functions.md to reflect that the formalization of Appendix A is now largely complete. The 'Scope' section revises the Lean surface from a single file to a directory RationalFunctions/ listing five sub-files (FunctionField.lean, Lifts.lean, Weight.lean, RationalRootVanishing.lean, HenselNumerators/) and notes downstream consumers. The 'Status' table is rewritten: definitions are renamed (e.g., monicizeRatFunc replaces H_tilde, monicize replaces H_tilde'), Lemma A.1 is upgraded from 'present-but-incomplete' to 'present' with a proof reference, Claim A.2 entries now detail Hensel-lift existence, uniqueness, regularity and multiple weight bounds (including a sharp bound with a correction term), and new infrastructure entries (weight additivity, regular-weight calculus, A.3 rational substitutions) appear. A new 'Three findings on Appendix A.4' section documents three technical discrepancies relative to the paper (the 2 ≤ degY R precondition, a correction term in the sharp weight bound, and a hidden assumption in the Λ(ξ) bound) that affect downstream consumers. The 'Near-Term Work' section is replaced with two specific tasks (case-split on deg_Y R in §5, optional fidelity improvement) and a closing statement that the appendix is otherwise axiom-clean (zero sorryAx).
• docs/kb/log.md: The changelog received new entries recording the completion of Appendix A (axiom-clean, all sorries closed), the restructuring and renaming of declarations for Mathlib style, the correction of an off-by-one in Claim 5.8, and removal of statement-level sorries; earlier recommendations about 2 ≤ deg_Y R and Λ(ξ) bounds were corrected, and a target reference in the [2026-06-16] entry was updated from ClaimA2.ξ_regular to RationalFunctions.HenselNumerators.xi_regular.

---

Last updated: 2026-08-05 03:53 UTC.

[github-actions]

Build Timing Report

• Commit: 6c28870
• Message: feat: proofs for rational function lemmas
• Ref: rational-functions-positive-degree
• Comparison baseline: 3768409 from the previous successful PR update.
• Measured on ubuntu-latest with /usr/bin/time -p.
• Commands: clean build rm -rf .lake/build && lake build; warm rebuild lake build; validation wrapper ./scripts/validate.sh.

Measurement	Baseline (s)	Current (s)	Delta (s)	Status
Clean build	807.01	715.92	-91.09	ok
Warm rebuild	2.47	1.91	-0.56	ok
Validation wrapper	2.53	1.95	-0.58	ok

Incremental Rebuild Signal

• Warm rebuild saved 714.01s vs clean (374.83x faster).

This compares a clean project build against an incremental rebuild in the same CI job; it is a lightweight variability signal, not a full cross-run benchmark.

Slowest Current Clean-Build Files

Showing 20 slowest current targets, with comparison against the selected baseline when available.

Current (s)	Baseline (s)	Delta (s)	Path
107.00	108.00	-1.00	ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Weight.lean
60.00	67.00	-7.00	ArkLib/ProofSystem/Stir/Combine.lean
59.00	55.00	+4.00	ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
53.00	56.00	-3.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean
52.00	51.00	+1.00	ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean
45.00	48.00	-3.00	ArkLib/Data/CodingTheory/ProximityGap/DG25/MainResults.lean
42.00	38.00	+4.00	ArkLib/Data/CodingTheory/BerlekampWelch/Condition.lean
39.00	40.00	-1.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/BWMatrix.lean
38.00	46.00	-8.00	ArkLib/Data/CodingTheory/ProximityGap/AHIV22.lean
37.00	39.00	-2.00	ArkLib/Data/CodingTheory/ProximityGap/Folding.lean
34.00	36.00	-2.00	ArkLib/OracleReduction/LiftContext/Reduction.lean
31.00	28.00	+3.00	ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean
31.00	37.00	-6.00	ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean
29.00	17.00	+12.00	ArkLib/Commitments/Functional/KZG/Binding.lean
29.00	32.00	-3.00	ArkLib/ProofSystem/Sumcheck/Spec/SingleRound.lean
28.00	34.00	-6.00	ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Hensel.lean
27.00	24.00	+3.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/JointAgreement.lean
26.00	27.00	-1.00	ArkLib/OracleReduction/Security/RoundByRound.lean
24.00	24.00	+0.00	ArkLib/Data/CodingTheory/DivergenceOfSets.lean
23.00	24.00	-1.00	ArkLib/Data/Polynomial/FoldingPolynomial.lean