docs(ratfunc): organisation, naming and docstring pass

Docstrings: 82 of the 231 declarations had none.  All now do -- every lemma in
the Lemma A.1 resultant chain, the xiPre* decomposition, the bSeq Hensel
iteration, the AllCoeffRegular and RegularWeightLe APIs, and the power-series
helpers.  The docstrings say what the statement is FOR, not just what it says:
e.g. coeff_evalR_split is flagged as the linearity that gives both existence and
uniqueness of the lift, and xiPreTop as the paper's "we can save a little" step.

Umbrella file: replaced the one-line "compatibility umbrella" note with a real
package roadmap -- the variable convention (which of F[X][X][Y]'s three variables
is the paper's X, Y, Z), a per-module map to the paper's sections, the main
results, the axiom-cleanliness claim, and the two documented deviations from
[BCIKS20] with pointers to where each is justified.

Organisation:
- named the six anonymous top-level sections (Monicization, AlgebraicWeights,
  RegularLifts, HenselSetup, HenselLift, HenselNumeratorSequence) and their
  closing `end`s;
- the section variable for R was declared as F[X][X][X] in four files while every
  theorem writes F[X][X][Y] -- same type, inconsistent notation; normalized.

Zero warnings, zero sorries, style-lint clean, and `#print axioms` over the whole
namespace still reports 266 declarations with no sorryAx and no non-standard
axioms.

Author: alexanderlhicks

ArkLib/Data/Polynomial/RationalFunctions.lean

@@ -14,7 +14,72 @@ import ArkLib.Data.Polynomial.RationalFunctions.HenselNumerators.Weight
 import ArkLib.Data.Polynomial.RationalFunctions.HenselNumerators.Sequence
 
 /-!
-# Function Fields and Rings of Regular Functions
+# Appendix A of [BCIKS20]: Function Fields, Weights, and Hensel Lifts
 
-Compatibility umbrella for the modularized BCIKS20 Appendix A development.
+Umbrella import for the `RationalFunctions` package, which formalizes Appendix A of [BCIKS20] —
+the algebraic machinery behind the list-decoding half of the Reed-Solomon proximity-gap proof.
+Import this file for all of it, or an individual module for a narrower dependency.
+
+## Setting
+
+`H : F[X][Y]` plays the role of the paper's `H(Y, Z)`: the outer variable is `Y` and the
+coefficient variable is the paper's `Z`. For the trivariate `R : F[X][X][Y]` the outer variable is
+`Y`, the middle one is the paper's `X` and the innermost is `Z`, so `Bivariate.evalX (C x₀) R` is
+the specialization `R(x₀, Y, Z)`.
+
+## Layout
+
+* `FunctionField` (A.1) — monicization `monicizeRatFunc`/`monicize` (the paper's `H̃`), the
+  function field `𝕃 H = F(Z)[T]/(H̃)`, its ring of regular elements `𝒪 H = F[Z][T]/(H̃)`, the
+  injective embedding `𝒪 H ↪ 𝕃 H`, canonical representatives, and the substitutions `π_z` of A.3.
+* `Lifts` (A.1) — coefficient and bivariate lifts into `𝕃`, the image `T` of the polynomial
+  variable, denominator clearing for `W^k · P(T/W)`, and the extension of `π_z` to quotients
+  `β / C(Z)`.
+* `Weight` (A.2) — the weight `Λ` (`weight`, `regularWeight`) and its calculus: sub-additivity,
+  *full* additivity on `F[Z][T]`, invariance under reduction modulo `H̃`, exact `Λ(H̃)`.
+* `RationalRootVanishing` (A.3) — Lemma A.1: a regular `β` killed by more than `deg_Y H · Λ(β)`
+  substitutions is zero.
+* `HenselNumerators/Setup` (A.4) — hypotheses of the lift, `ζ = ∂R/∂Y(x₀, T/W, Z)`, its cleared
+  form `ξ = W^{d-2}·ζ ∈ 𝒪`, and the bound on `Λ(ξ)`.
+* `HenselNumerators/Hensel` (A.4) — the formal Hensel iteration: existence, uniqueness, and
+  regularity of the numerators.
+* `HenselNumerators/Weight` (A.4) — the quantitative half of Claim A.2: the `RegularWeightLe`
+  calculus and the weight induction.
+* `HenselNumerators/Sequence` (A.4) — Claim A.2 assembled: `betaSeq`, `alpha`, `gamma`, and the
+  weight bounds.
+
+## Main results
+
+* `lemmaA1_embedding_eq_zero_of_many_rational_roots` — Lemma A.1.
+* `HenselNumerators.exists_hensel_numerator_sequence` — the qualitative half of Claim A.2. The data
+  `betaSeq`, `alpha`, `gamma` is defined from this rather than from the bundled statement, so that
+  downstream definitions do not depend on the quantitative argument.
+* `HenselNumerators.IsHenselNumeratorSequence.unique` — uniqueness of the lift, which A.4 asserts
+  and [BCIKS20] §5 invokes in Claim 5.9. It makes `betaSeq` canonical rather than an arbitrary
+  choice.
+* `HenselNumerators.claimA2_exists_numerators_with_weight_bounds` — Claim A.2 as the paper states
+  it: existence together with both weight bounds.
+
+Everything in this package is proved: no `sorry`, and no axioms beyond `propext`,
+`Classical.choice` and `Quot.sound`.
+
+## Deviations from the paper
+
+Two, both recorded in `docs/kb/audits/bciks20-appendix-a-rational-functions.md`.
+
+1. The weight bounds assume `2 ≤ deg_Y R`, which is A.4's own standing assumption — it writes
+   `ξ = W^{d-2}·ζ ∈ 𝒪`, meaningless for `d < 2`. The hypothesis is load-bearing rather than
+   cosmetic: at `deg_Y R = 1` the conclusion of `xi_weight_le` is false. Consumers must case-split;
+   see the docstring of `claimA2_hypotheses` in `BCIKS20/ListDecoding/Agreement.lean`.
+2. `numeratorShapeSharp` carries a correction term relative to the inequality A.4 states, because
+   a factor of `W` that the recursion *saves* is worth only `deg W` while one it *charges* costs
+   the bound `D - dH`. The loose bound `(2t+1)·d·D` that Claim 5.10 consumes is unaffected. See
+   that definition's docstring.
+
+## References
+
+[BCIKS20] Eli Ben-Sasson, Dan Carmon, Yuval Ishai, Swastik Kopparty, and Shubhangi Saraf.
+  Proximity gaps for Reed-Solomon codes. In 2020 IEEE 61st Annual Symposium on Foundations of
+  Computer Science (FOCS), 2020. Full paper: https://eprint.iacr.org/2020/654,
+  version 20210703:203025.
 -/

ArkLib/Data/Polynomial/RationalFunctions/FunctionField.lean

@@ -30,7 +30,7 @@ open Polynomial Polynomial.Bivariate ToRatFunc Ideal
 
 namespace RationalFunctions
 
-section
+section Monicization
 
 variable {F : Type} [CommRing F] [IsDomain F]
 
@@ -49,6 +49,7 @@ section FieldIrreducibility
 
 variable {F : Type} [Field F]
 
+/-- The embedding `F[Z] → F(Z)` of a domain into its fraction field is injective. -/
 lemma univPolyHom_injective :
     Function.Injective (univPolyHom (F := F)) := by
   simpa [ToRatFunc.univPolyHom] using (RatFunc.algebraMap_injective (K := F))
@@ -378,6 +379,9 @@ section FieldEmbedding
 
 variable {F : Type} [Field F]
 
+/-- Divisibility by the monicization descends from `F(Z)[T]` to `F[Z][T]`: if `monicizeRatFunc H`
+divides the image of `p`, then `monicize H` already divides `p`.  This is what makes
+`embeddingOf𝒪Into𝕃` injective. -/
 lemma monicize_dvd_of_map_dvd_monicizeRatFunc {H p : F[X][Y]} (hHdeg : 0 < H.natDegree)
     (hp : monicizeRatFunc H ∣ p.map (univPolyHom (F := F))) :
     monicize H ∣ p := by
@@ -599,5 +603,5 @@ lemma canonicalRepOf𝒪_mk_eq_self_of_degree_lt {H : F[X][Y]} (hH : 0 < H.natDe
   exact (Polynomial.modByMonic_eq_self_iff (monicize_monic H hH)).2 hp
 
 
-end
+end Monicization
 end RationalFunctions