fix(BCIKS20): repair separability, Claim A.2, and §5 hypotheses

[alexanderlhicks]

Summary

This PR repairs two genuine defects in the BCIKS20 formalization and cleans up the surrounding
§5 statement interfaces after a line-by-line review against BCIKS20, ePrint
2020/654 and the downstream ABF26/EF-Millenium usage.

1. The separability needed by Appendix A is separability of R(x₀, Y, Z) as a polynomial in Y
   over F(Z), not over F[Z].
2. The literal Claim A.2 bound on ξ omits the cost of clearing content introduced by
   specialization. The corrected formal bound includes contentWeight.

The review also found that several §5 statements had silently omitted load-bearing hypotheses or
bridges. Those are now explicit instead of being hidden behind too-weak theorem interfaces.

What changed

Separability and Appendix A

• State the Hensel separability hypothesis over RatFunc F and prove the required map from the
  polynomial-ring specialization.
• Add an exact 𝔽₅ counterexample to the paper's literal ξ weight bound:
  R = ZY² + ZY + (Z + X), x₀ = 0, H = Y² + Y + 1, D = 3.
• Account for specialization content with contentWeight and prove the resulting sharp and loose
  numerator bounds.
• Use (2t+1)(dY+1)D only as a conservative proved bound. The PR no longer claims that the extra
  +1 is necessary or that an actual numerator attains the arithmetic budget; the invalid
  numerical witness for that claim was removed.

Section 5 statement repair

• Add Section5Regime, recording the standing assumptions used by §5: m ≥ 3, k+1 < n, the
  permitted δ range, D_Y Q > 0, and the content-aware cardinality bound.
• Use real-valued division/cardinality comparisons in Proposition 5.5 and Claim 5.7 rather than
  truncated natural-number division.
• Give Claim 5.6 the finite-field discriminant-degree premise needed to choose a good x₀.
• Count only positive-Y-degree factors in Claim 5.7. Claim57Assumptions explicitly records the
  remaining content/exceptions bridge and specialization separability until the paper's finite
  exceptional-set argument is formalized.
• Restrict the Appendix A weight path to the 2 ≤ natDegreeY R branch and expose its factor-degree
  premises. A degree-one factor should instead use its rational root directly; that branch remains
  a separate proof obligation.
• Thread the corrected D_YZ Q and content-aware bounds through Claims 5.10 and 5.11.

API and scope cleanup

• Retain the existing ring-level separability helper theorems that were valid; add filtered and
  fraction-field APIs instead of deleting sound statements.
• Remove the unrelated Bivariate.rootMultiplicity₀ proof rewrite from the final PR diff.
• Rebase onto current main; the already-merged Proposition 5.5 / D_YZ repair from fix(BCIKS20): repair D_YZ index order and two Prop 5.5 defects #772 is no
  longer duplicated here.
• Update the Appendix A audit to distinguish proved corrections, conservative bounds, and open
  proof obligations.

Verification

• ./scripts/validate.sh
• lake exe axiomsweep --check — no new sorryAx or non-standard-axiom taint
• Full lake build ArkLib
• Targeted compilation of the modified BCIKS20 and rational-function modules
• Existing sorry counts in the touched §5 modules are unchanged

Scope note

This PR fixes the statements and proved Appendix A support it touches. It does not claim to have
completed the existing sorry proofs for the Claim 5.7 exceptional-set/content bridge or the
degree-one direct-root branch; those obligations are now visible in the APIs and documentation.

[github-actions]

🤖 PR Summary

Summary

Mathematical Formalization

• Ring-level Separable → fraction-field separability. The previous Polynomial.Separable condition, used throughout the §5 chain and the Hensel setup, forced the discriminant to be a unit over the coefficient ring. Over F[Z] or F[Z][X] this is far too strong, rejecting legitimate inputs where the specialization acquires a non‑unit content (e.g. Z in R = Z·Y² + Z·Y + (Z + X) over 𝔽₅). All uses are now retargeted to separability over the fraction field F(Z).

  • Eq 5.12 (irreducible_factorization_of_gs_solution): ∀ Rᵢ ∈ R, Rᵢ.Separable → ∀ Rᵢ ∈ R, Bivariate.discr_y Rᵢ ≠ 0.
  • Claim 5.7 (exists_factors_with_large_common_root_set): The conjunct is now separability of R(x₀,·,Z) over F(Z), i.e. ((Bivariate.evalX (C x₀) R).map (ToRatFunc.univPolyHom (F := F))).Separable. evalX_R_separable → evalX_R_separable_over_ratFunc.
  • Hensel setup (Hypotheses): The field separable_evalX now requires separability over F(Z). Docstrings explain the defect.

• Two proved helpers that were false under the corrected hypothesis. pg_natDegree_pos_of_mem_normalizedFactors_of_separable and pg_card_normalizedFactors_toFinset_le_natDegree used ring‑Separable to exclude constant factors. Constant primes (e.g. Z) are legitimate normalized factors of p : F[Z][X] with natDegree 0, so the count is not bounded by p.natDegree. They are replaced by pg_natDegree_pos_of_mem_positiveDegreeFactors and pg_card_positiveDegreeFactors_toFinset_le_natDegree which filter to factors of positive natDegree and require no hypothesis at all (covering p = 0 directly).

  • New definitions: pg_positiveDegreeFactors, pg_positiveDegreePairs (analogue of pg_candidatePairs). pg_card_positiveDegreePairs_le_natDegreeY replaces pg_card_candidatePairs_le_natDegreeY as the primary bound.
  • pg_candidatePairs is left unfiltered and pg_positiveDegreePairs added alongside; bridging them is an explicit obligation (part of Claim 5.7's counting argument).

• [BCIKS20] Claim A.2 missing a hypothesis. The lemma xiPreTop_coeff_natDegree_zero_of_H_natDegree_eq_R_natDegree (which claimed the top coefficient's natDegree is 0 when dH = d) is false. The paper’s bound Λ(ξ) ≤ (d-1)(D-dH+1) is not provable without an extra Λ(W) term; a concrete counterexample over 𝔽₅ is given.

  • New definition: contentWeight x₀ R H computes the Z-degree of the quotient (coeff of R.derivative at (natDegree-1)) / H.leadingCoeff.
  • contentWeight_le (replaces the old lemma): contentWeight ≤ D - R.natDegree using the total‑degree hypothesis.
  • xiPreTop_weight_over_𝒪_le gains + contentWeight in the dH = d branch; both branches need no separability at all.
  • xi_weight_le gains + contentWeight x₀ R H.
  • numeratorShapeSharp → numeratorShapeSharpContent which adds the contentWeight term. The loose bound becomes (2t+1)·(dY+1)·D (previously (2t+1)·dY·D). All theorems in Weight.lean are updated accordingly.
  • Affected §5 statements: solution_gamma_matches_word_if_subset_large (Claim 5.10) and exists_points_with_large_matching_subset (Claim 5.11) carry dY + 1 in their thresholds.

Proof Completion (sorries removed)

• 17 sorry in the §5 chain, 17 after – this PR does not remove sorries but repairs statements so the existing sorries are reachable under correct hypotheses. ./scripts/validate.sh green, zero non‑sorry warnings under ArkLib/Data.

Protocols / Soundness

• Section5Regime structure introduced in Guruswami.lean to formalize the standing numerical hypotheses of §5.2 (including a strengthened lower bound on the size of coeffs_of_close_proximity). The lemma exists_a_set_and_a_matching_polynomial (Prop 5.5) now takes a Section5Regime argument, fixing the defect where the conclusion #S' > #S / (2·D_Y Q) was false at empty S. The hypothesis hS : 0 < #(coeffs_of_close_proximity …) is added (the weakest form that restores provability), threaded through matching_set, matching_set_is_a_sub_of_coeffs_of_close_proximity, matching_set_at_x, and Claims 5.10/5.11.

Infrastructure / CI

• None.

Documentation

• docs/kb/audits/bciks20-appendix-a-rational-functions.md: Updated audit table – 'Claim A.2 bound for ξ' marked 'corrected', referencing contentWeight, contentWeight_le, xi_weight_le. The two 'Claim A.2 sharp weight bound' rows and the 'loose weight bound' row marked 'corrected', now referencing numeratorShapeSharpContent, numeratorShapeSharpContent_le_loose. Finding 3 renamed and updated with concrete counterexample.
• Docstrings expanded throughout Agreement.lean, Setup.lean, Sequence.lean, Weight.lean, RationalFunctions.lean explaining the error in the paper and how the code corrects it.
• RationalFunctions.lean module docstring revised; Hypotheses now documented as requiring fraction‑field separability.
• Extraction.lean: discr_of_irred_components_nonzero docstring updated with explicit hdegree hypothesis.

Refactoring

• Agreement.lean: Introduced Claim57Assumptions structure bundling hypotheses needed for Claim 5.7. All downstream lemmas (irreducible_H, natDegree_H_pos, H_dvd_evalX_R, hensel_lift_hypotheses, approximate_solution_is_exact_solution_coeffs, solution_gamma_is_linear_in_Z, gamma_eq_P, matching_set_at_x, solution_gamma_matches_word_if_subset_large, exists_points_with_large_matching_subset) now take an explicit h57 : Claim57Assumptions … argument.
• Hensel.lean: zeta_ne_zero_of_hypotheses proof refactored to explicitly factor through RatFunc F via an auxiliary ring homomorphism ψ.
• Setup.lean: xiPreTop_coeff_natDegree_zero_of_H_natDegree_eq_R_natDegree deleted; contentWeight, contentWeight_le added.
• Extraction.lean: pg_positiveDegreeFactors, pg_positiveDegreePairs added; pg_natDegree_pos_of_mem_normalizedFactors_of_separable and pg_card_normalizedFactors_toFinset_le_natDegree deprecated (still present for callers with the stricter Separable hypothesis).
• Guruswami.lean: Section5Regime added; matching_set, matching_set_is_a_sub_of_coeffs_of_close_proximity, exists_a_set_and_a_matching_polynomial now take a regime argument.

Salvaged from #773

• le_rootMultiplicity_of_coeff_shift_eq_zero: collapses symbolicGSPolyMultiplicityBridge from a 16‑line body to a single exact.
• rootMultiplicity₀_ne_none: 8 lines against the previous 32, running rootMultiplicity₀_ge_iff backwards.

Audit notes

• Curves.lean (3 sorries): Clean – regime hypotheses explicit, n * l < card present, conjuncts correctly parenthesized, card ≤ δ * n coercion lands in ℝ≥0.
• Index-order convention checked repo‑wide: Bivariate.coeff f i j = (f.coeff j).coeff i (X‑index first); natWeightedDegree f u v weights X by u, Y by v; evalX substitutes inner variable, evalY outer. All call sites agree, including PolishchukSpielman.
• Footgun: evalX and evalY have the same return type Polynomial F, so nothing type‑distinguishes 'polynomial in X' from 'polynomial in Y'.

No new sorry or admit are introduced anywhere.

---

Statistics

Metric	Count
📝 Files Changed	10
✅ Lines Added	779
❌ Lines Removed	296

---

Lean Declarations

✏️ Removed: 2 declaration(s)

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

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

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

• theorem xiPreTop_coeff_natDegree_zero_of_H_natDegree_eq_R_natDegree (x₀ : F) (hH : 0 < H.natDegree)

✏️ Added: 11 declaration(s)

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

• lemma evalX_R_separable_over_ratFunc (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁)

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

• noncomputable def pg_positiveDegreeFactors (p : F[Z][X]) : Multiset F[Z][X]
• noncomputable def pg_positiveDegreePairs
• theorem pg_card_positiveDegreeFactors_toFinset_le_natDegree (p : F[Z][X]) :
• theorem pg_card_positiveDegreePairs_le_natDegreeY (x₀ : F)
• theorem pg_natDegree_pos_of_mem_positiveDegreeFactors {p : F[Z][X]} {H : F[Z][X]}
• theorem pg_positiveDegreePairs_snd_natDegree_pos (x₀ : F)

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

• noncomputable def contentWeight (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) : ℕ
• theorem contentWeight_le (x₀ : F) (hH : 0 < H.natDegree) (hHyp : Hypotheses x₀ R H)

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

• def numeratorShapeSharpContent (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) (D t : ℕ) : ℕ
• lemma numeratorShapeSharpContent_le_loose (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y])

✏️ Affected: 10 declaration(s) (line number changed)

• lemma H_dvd_evalX_R (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean moved from L62 to L112
• lemma gamma_eq_P (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean moved from L163 to L248
• lemma hensel_lift_hypotheses (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean moved from L91 to L149
• lemma irreducible_H (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean moved from L52 to L94
• lemma natDegree_H_pos (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean moved from L57 to L105
• noncomputable def H (δ : ℚ) (x₀ : F) (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean moved from L47 to L88
• noncomputable def P (δ : ℚ) (x₀ : F) (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean moved from L152 to L229
• noncomputable def R (δ : ℚ) (x₀ : F) (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean moved from L42 to L83
• lemma discr_of_irred_components_nonzero (_h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Extraction.lean moved from L74 to L87
• theorem pg_card_candidatePairs_le_natDegreeY (x₀ : F) (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Extraction.lean moved from L509 to L722

---

sorry Tracking

✏️ Affected: 2 `sorry`(s) (line number changed)

• lemma exists_factors_with_large_common_root_set (δ : ℚ) (x₀ : F) in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean moved from L39 to L80
• lemma exists_points_with_large_matching_subset in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean moved from L218 to L322

---

📋 **Additional Analysis**

The diff contains several violations of the project's style and naming guidelines. The most pervasive issues are naming conventions (camelCase used where snake_case is required for theorems, and snake_case used where lowerCamelCase is required for functions) and excessive line length (many lines exceed the 100-character limit). A few minor formatting points (e.g., spacing) appear acceptable. No violations were found for documentation, citation, or header requirements within the scope of the diff, though some aspects (deprecation, imports, file headers) are not visible in the diff and cannot be assessed. The sorry blocks themselves are not style violations, but the presence of unproven statements does not violate the guidelines. The findings are detailed below by category.

---

📄 **Per-File Summaries**

• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean: The diff refactors the file to introduce a Claim57Assumptions structure that bundles three hypotheses (regime, specializations_separable, positive_pair_for_every_z) needed for Claim 5.7. The main lemma exists_factors_with_large_common_root_set and all downstream definitions (R, H, P) and lemmas (irreducible_H, natDegree_H_pos, H_dvd_evalX_R, evalX_R_separable_over_ratFunc, hensel_lift_hypotheses, approximate_solution_is_exact_solution_coeffs, approximate_solution_is_exact_solution_coeffs', solution_gamma_is_linear_in_Z, gamma_eq_P, matching_set_at_x, solution_gamma_matches_word_if_subset_large, exists_points_with_large_matching_subset) are updated to take an explicit h57 : Claim57Assumptions k x₀ δ h_gs argument. The separability condition is changed from Polynomial.Separable over the ring to Separable over the fraction field F(Z) (((Bivariate.evalX (Polynomial.C x₀) R).map (ToRatFunc.univPolyHom (F := F))).Separable). irreducible_H is now proven by deducing Irreducible from membership in pg_positiveDegreeFactors. natDegree_H_pos is proved via pg_natDegree_pos_of_mem_positiveDegreeFactors. H_dvd_evalX_R is proved via UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors. The cardinality inequality in exists_factors_with_large_common_root_set now uses ℝ comparisons (via : ℝ casts) and includes a changed bound: 2 * D_Y Q * (D_Y Q + 1) * D_X ... * D_YZ Q (previously 2 * D_Y Q ^ 2 * D_X ... * D_YZ Q). Several lemmas acquire extra hypotheses: _hR_degree_at_least_two : 2 ≤ Bivariate.natDegreeY (R ...), _hR_totalDegree_le : Bivariate.totalDegree (R ...) ≤ D_YZ Q, _hH_totalDegree_le : Bivariate.totalDegree (H ...) ≤ D_YZ Q. The statement of solution_gamma_matches_word_if_subset_large uses Bivariate.natDegreeY (R ...) + 1 and D_YZ Q where previously it used a generic D and Bivariate.natDegreeY R * D. The proof of solution_gamma_is_linear_in_Z and the helper matching_set_at_x now depend on h57.regime. The docstrings are expanded to explain the motivation for the refactor and the precise meaning of the separability condition.
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Extraction.lean: This diff makes several related changes to Extraction.lean. In irreducible_factorization_of_gs_solution, the condition (∀ Rᵢ ∈ R, Rᵢ.Separable) is replaced by (∀ Rᵢ ∈ R, Bivariate.discr_y Rᵢ ≠ 0), and the docstring for discr_of_irred_components_nonzero is updated to add an explicit hdegree hypothesis. A new noncomputable def pg_positiveDegreeFactors filters UniqueFactorizationMonoid.normalizedFactors to those factors of positive natDegree; a new noncomputable def pg_positiveDegreePairs is defined analogously to pg_candidatePairs but using pg_positiveDegreeFactors. New theorems pg_natDegree_pos_of_mem_positiveDegreeFactors and pg_positiveDegreePairs_snd_natDegree_pos provide the positive-degree property without a separability hypothesis. A new theorem pg_card_positiveDegreeFactors_toFinset_le_natDegree gives the cardinality bound directly, and pg_card_positiveDegreePairs_le_natDegreeY replaces pg_card_candidatePairs_le_natDegreeY as the primary bound, not requiring Separable. The existing pg_card_normalizedFactors_toFinset_le_natDegree and pg_candidatePairs_snd_natDegree_pos and pg_card_candidatePairs_le_natDegreeY are retained for callers with the stricter Separable hypothesis.
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Guruswami.lean: Introduces the Section5Regime structure to formalize the standing numerical hypotheses of [BCIKS20] §5.2 (including 3 ≤ m, rate strictly below one, δ in the list-decoding radius, D_Y Q > 0, and a strengthened lower bound on the size of coeffs_of_close_proximity). Adds Section5Regime as a new hypothesis to exists_a_set_and_a_matching_polynomial, whose docstring is updated to explain that this regime is load-bearing for the counting inequalities and the factor/Hensel argument. matching_set and matching_set_is_a_sub_of_coeffs_of_close_proximity likewise now take a Section5Regime argument. The lemma exists_a_set_and_a_matching_polynomial remains sorry.
• ArkLib/Data/Polynomial/RationalFunctions.lean: The module documentation for RationalFunctions.lean was revised to reflect corrections in the formalization. The description of exists_hensel_numerators_with_weight_bounds now states it provides the corrected Claim A.2 package with content-aware sharp and conservative loose bounds. A new item documents that xi_weight_le carries a content‑weight summand omitted in the paper, raising the uniform loose bound from (2t+1)·d·D to (2t+1)·(d+1)·D; the affected §5 statements and largeness assumptions have been adjusted. Finally, Hypotheses now requires separability over F(Z) (the paper’s actual meaning) instead of ring‑level separability, which excluded valid instances. No code or proofs were changed; the diff is exclusively documentation.
• ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Hensel.lean: The theorem zeta_ne_zero_of_hypotheses was refactored to prove the final hne statement via an auxiliary ring homomorphism ψ : RatFunc F →+* 𝕃 H that factors through the fraction field. The proof now constructs ψ and establishes hfactor (relating liftToFunctionField to ψ ∘ univPolyHom) and hroot' (an evaluation condition using ψ), then uses the separable hypothesis hHyp.separable_evalX.eval₂_derivative_ne_zero with ψ before rewriting back to the original term. This change makes the separability argument explicit at the fraction-field level rather than relying solely on liftToFunctionField.
• ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Sequence.lean: The diff updates four lemmas (betaSeq_weight_sharp_le, betaSeq_weight_le, betaSeq_weight_sharp_le_defaultDegreeBound, betaSeq_weight_le_defaultDegreeBound) and the theorem exists_hensel_numerators_with_weight_bounds, as well as their docstrings, to replace the previously used numeratorShapeSharp R H D t and Bivariate.natDegreeY R * D bounds with corrected sharper and looser bounds: for the sharp bound, the term numeratorShapeSharp R H D t is replaced by numeratorShapeSharpContent x₀ R H D t, which now explicitly depends on x₀; for the loose bound, the factor Bivariate.natDegreeY R * D is replaced by (Bivariate.natDegreeY R + 1) * D. The docstrings are updated accordingly to reflect the new form of the bounds and to note that xi_regular and xi_weight_le now refer to content-aware bounds rather than an explicit formula.
• ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Setup.lean: This diff modifies Setup.lean to fix a gap in the weight bound for the Hensel numerator lift. It does several things as a single unit:

1. Changes the separable_evalX field of Hypotheses so that separability of the specialized polynomial R(x₀,·,Z) is required over the fraction field F(Z) (by mapping to F(Z)[Y]) rather than over the coefficient ring F[X]. The docstring explains why the old ring-level Polynomial.Separable was too strong, ruling out legitimate inputs where the specialization acquires a non-unit content.

2. Updates the lemma evalX_ne_zero_of_hypotheses to use the new separable_evalX condition; its proof now factors through the map to F(Z)[Y].

3. Adds the new noncomputable def contentWeight: it computes the Z-degree of the quotient (coeff of R.derivative at (natDegree-1)) / H.leadingCoeff. The extensive docstring explains that Claim A.2 of [BCIKS20] is missing this term, which is needed when the leading coefficient W of H has Λ(W) < D - dH, and gives an explicit counterexample over 𝔽₅.

4. Replaces the old theorem xiPreTop_coeff_natDegree_zero_of_H_natDegree_eq_R_natDegree (which claimed the top coefficient's natDegree is 0 when dH = d) with contentWeight_le, a more general bound contentWeight ≤ D - R.natDegree using the total-degree hypothesis on R(x₀,·,Z).

5. Changes xiPreTop_weight_over_𝒪_le (the weight bound for the top term) to include the contentWeight summand: R.natDegree - 1)*(D - H.natDegree + 1) + contentWeight. Both its call to the dH < d case and the dH = d case are updated: the dH = d case now uses contentWeight directly instead of the deleted xiPreTop_coeff_natDegree_zero lemma.

6. Updates the top-level lemma xi_weight_le and xiPreTop_weight_over_𝒪_le_of_H_natDegree_lt_R_natDegree similarly: xi_weight_le's conclusion gains the + contentWeight x₀ R H term, and the xiPreLower branch in its proof also adds contentWeight via Nat.le_add_right. The xiPreTop_weight_over_𝒪_le_of_H_natDegree_lt_R_natDegree lemma is now used and its call includes an additional Nat.le_add_right in xiPreTop_weight_over_𝒪_le.

7. Adds/updates extensive long-form docstrings on Hypotheses, contentWeight, xiPreTop_weight_over_𝒪_le, and xi_weight_le that explain the error in the paper and how the code corrects it.

There are no sorry or admit introduced.

• ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Weight.lean: The file introduces a new definition numeratorShapeSharpContent that adds a contentWeight term to the previous sharp budget numeratorShapeSharp, together with a lemma numeratorShapeSharpContent_le_loose showing it weakens to (2t+1)·(dY+1)·D. All existing theorems that previously used numeratorShapeSharp as the weight bound—namely henselClearedTerm_weight, henselClearedResidual_weight, numerator_shape_weight_sharp, numerator_shape_weight_bound, hensel_numerator_weight_sharp_le, and hensel_numerator_weight_le—now use numeratorShapeSharpContent. Consequently the loose bound reported in numerator_shape_weight_bound and hensel_numerator_weight_le becomes (2t+1)·(dY+1)·D instead of (2t+1)·dY·D. The module-level docstring is updated to explain that the content charge is required because the paper’s Λ(ξ) bound is false without it.
• docs/kb/audits/bciks20-appendix-a-rational-functions.md: This file documents the audit of the formalization of BCIKS20 Appendix A.4 (rational functions). The table tracking which claims are formalized is updated: the 'Claim A.2 bound for ξ' row is marked 'corrected' and now references new definitions contentWeight,contentWeight_le, and xi_weight_le to account for specialization content omitted by the paper. The two 'Claim A.2 sharp weight bound' rows and the 'loose weight bound' row are also marked 'corrected', now referencing new content-aware theorems (numeratorShapeSharpContent, numeratorShapeSharpContent_le_loose) that include both the recursion correction and the specialization-content charge; the loose bound is documented as Λ(βₜ) ≤ (2t+1)(dY+1)D. The 'Corrected Claim A.2 package' row is newly added as 'present'. The 'Three findings on Appendix A.4' section is revised: finding 2 no longer claims that simply raising the ξ-charge breaks the paper's loose bound, and now notes that the arithmetic theorem numeratorShapeSharp_le_loose still yields (2t+1)·dY·D for the defined budget but must not be confused with the bound after finding 3. Finding 3 is renamed from 'The paper's sharper Λ(ξ) bound also assumes Λ(W)=D-dH' to 'The paper's Λ(ξ) bound omits specialization content', and now provides a concrete counterexample over 𝔽₅ where the proved bound is 3 but the paper's bound is 2; it also notes that the safe loose bound (2t+1)(dY+1)D does not prove an actual numerator attains that budget, so the paper's smaller bound is not disproved. The 'Near-Term Work' section is updated: item 1 now references completing the degree-one/direct-root branch, item 2 is new (formalizing the finite exceptional-set argument), and item 3 is renumbered. The concluding statement about the appendix being 'otherwise complete' now reads 'including Lemma A.1 and the corrected Claim A.2 package'.
• 1 file(s) filtered as noise (lockfiles, generated, or trivial): scripts/axiom_baseline.json

---

Last updated: 2026-08-21 15:33 UTC.

[aryaethn]

Stepping back from BCIKS20 §5 for now — you're working through it actively (#733, #777, #787) and
I'd rather not create collisions. Happy to pick something up if it's ever useful to hand off a
specific piece.

Thanks for carrying the two Bivariate.lean lemmas forward with attribution.

One item still open, for your list rather than as a request: ModifiedGuruswami permits
D_Y Q = 0, and then 2 * D_Y Q = 0 makes (5.9)'s right-hand side 0 rather than the paper's
+∞, so the bound reads #S' > 0. Downstream that is worse than a weak bound — with no Y,
Y - Pz(X) ∣ Q forces Q = 0 and §5.2.2 collapses. hS doesn't reach it; the note is in the
Prop 5.5 docstring on main.

[github-actions]

Build Timing Report

• Commit: 54e2e91
• Message: fix(BCIKS20): repair separability, Claim A.2, and §5 hypotheses
• Ref: alh/bciks20-separable-repairs
• Comparison baseline: df2339f from current base of main.
• 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	1199.10	652.94	-546.16	ok
Warm rebuild	2.91	2.19	-0.72	ok
Validation wrapper	17.23	10.34	-6.89	ok

Incremental Rebuild Signal

• Warm rebuild saved 650.75s vs clean (298.15x 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
61.00	124.00	-63.00	ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Weight.lean
45.00	95.00	-50.00	ArkLib/ProofSystem/Stir/Combine.lean
40.00	69.00	-29.00	ArkLib/Data/CodingTheory/ListDecodability/Bounds/KKH26Asymptotic.lean
34.00	67.00	-33.00	ArkLib/Data/CodingTheory/SubspaceDesign.lean
31.00	77.00	-46.00	ArkLib/Data/CodingTheory/ProximityGap/CapacityBounds/UniqueDecoding.lean
30.00	61.00	-31.00	ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
30.00	71.00	-41.00	ArkLib/Data/CodingTheory/ProximityGap/DG25/MainResults.lean
29.00	66.00	-37.00	ArkLib/Data/CodingTheory/JohnsonBound/Family.lean
29.00	62.00	-33.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/BWMatrix.lean
28.00	65.00	-37.00	ArkLib/Data/CodingTheory/ProximityGap/Folding.lean
28.00	56.00	-28.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean
24.00	73.00	-49.00	ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean
24.00	51.00	-27.00	ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean
24.00	42.00	-18.00	ArkLib/Data/CodingTheory/ProximityGap/AHIV22.lean
24.00	52.00	-28.00	ArkLib/Data/CodingTheory/ProximityGap/CapacityBounds/Frs.lean
23.00	57.00	-34.00	ArkLib/Data/CodingTheory/ListDecodability/Bounds/LargeAlphabet/Pigeonhole.lean
23.00	43.00	-20.00	ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean
22.00	38.00	-16.00	ArkLib/Data/CodingTheory/ProximityGap/CapacityBounds/Entropy.lean
22.00	45.00	-23.00	ArkLib/Data/MvPolynomial/EvenAndOdd.lean
21.00	36.00	-15.00	ArkLib/Data/CodingTheory/ListDecodability/Bounds/LargeAlphabet/Centers.lean

[dtumad]

Independent confirmation of the §5 half of this PR, from an external audit of the BCIKS20
chain: exists_factors_with_large_common_root_set (Claim 5.7) has the same missing eq. (5.3)
largeness premise on #S that exists_a_set_and_a_matching_polynomial (Prop 5.5) documents in
its docstring, and on main @ 14a4b351d154 Claim 5.7 carries no warning at all — so one of
the two reads as sound and the other as flagged. Six .choose extractors in Agreement.lean
(R, H, irreducible_H, natDegree_H_pos, and the two following) sit on top of it.

Section5Regime with S_large, Claim57Assumptions, and the move from truncated ℕ division
to real division all look like the right shape to me. Filed #799 as a tracker so the Claim 5.7
side is visible on main while this is in review; happy to close it as soon as this lands.

One small thing that might reduce review surface if this PR is feeling large: mirroring Prop
5.5's existing docstring warning onto Claim 5.7 is a one-line, zero-risk interim change that
removes the asymmetry independently of the rest of the repair.

[quangvdao]

Thanks for the careful repair here, Alexander. I reviewed head 54e2e918740738125de3c062a5bae5f1f8187981 against BCIKS20 and the current ArkLib degree/Hensel APIs. I agree with the two headline diagnoses: separability belongs over F(Z), and the literal Claim A.2 bound omits the specialization-content charge. The 𝔽₅ example checks out, and Section5Regime, real-valued cardinality division, positive-Y factor filtering, and the explicit degree-one/content obligations are all good improvements.

A few findings to address while rebasing:

1. [P1] The Claim 5.8 R premise measures the wrong axes. In Agreement.lean, every _hR_totalDegree_le : Bivariate.totalDegree (R ...) ≤ D_YZ Q measures the structural (X,Y) projection and ignores Z; it is not the intended (Y,Z) degree. After refactor(polynomial): make trivariate axes explicit #790 lands, these seven propagated premises should use Trivariate.degreeYZ R ≤ Trivariate.D_YZ Q.

   There is a related lower-layer obligation: the quantitative Hensel API currently asks for ∀ j ∈ R.support, Bivariate.totalDegree (R.coeff j) + j ≤ D, which charges full (X,Y,Z) degree. That also cannot generally be derived from the paper-facing D_YZ bound. The robust fix is to add a degreeYZ coefficient-bound bridge and weaken the Hensel coefficient-weight argument to charge only coefficient Z degree plus the outer Y exponent, leaving the middle X exponent uncharged. Merely renaming the Agreement premise will not be enough for the eventual Claim 5.8 proof.

2. [P2] specializations_separable ranges over content factors. pg_Rset contains all normalized factors of Q, including irreducible factors of the content C(X,Z), while Claim 5.6 only chooses x₀ to make the positive-Y factors Rᵢ good. If a content factor vanishes at x₀, the current Claim57Assumptions field is not constructible even for a source-valid instance. I suggest restricting separability to positive-Y/admissible candidate factors, or bundling it into the positive-degree pair predicate. It would also help to state explicitly that this interface covers the separable-factor branch and leaves the Appendix C inseparable branch out of scope.

3. [P3] Regression hardening: the 𝔽₅ counterexample is currently prose-only. An executable Lean example computing the specialization and the contentWeight/ξ discrepancy would give durable evidence for changing a published bound.

Current merge mechanics: this branch conflicts with current main in HenselNumerators/Weight.lean. The resolution should retain the bounded-arithmetic/performance refactor now on main rather than reintroducing the old large-heartbeat proof. The existing sorry counts in the touched §5 modules are unchanged, and no new sorry was added. The old red Pages job is the unrelated AxiomSweepTestFixtures issue already fixed on main; a fresh Lean 4.33.1 full/axiom/docs validation after rebase is the meaningful gate.

Overall, this is an important and well-motivated correction. #790 should land first, then this PR can adopt the semantic trivariate API and close the degree-bound mismatch cleanly.