refactor(polynomial): make trivariate axes explicit

[alexanderlhicks]

Confirmed defect fixed

• The canonical innermost-variable operation Trivariate.eval_on_Z was opaque, so downstream proofs could not unfold it and Extraction.lean had grown a duplicate pg_eval_on_Z. This replaces it with the transparent, axis-explicit evalAtZ definition and keeps deprecated compatibility aliases.
• The audit confirms that Bivariate.totalDegree on F[Z][X][Y] measures only the structural (X, Y) projection. It is not the (Y, Z) degree and it ignores Z. The asymmetric regression polynomial Z^5 X^7 Y^3 proves the distinction: degreeXY = 10, degreeYZ = 8, and totalDegreeXYZ = 15.

No incorrect mathematical statement on current main was found or changed.

Preventive API hardening

• Add semantic trivariate evaluation operations evalAtX, evalAtY, and evalAtZ.
• Add named degree operations degreeInX, degreeInY, degreeInZ, degreeXY, degreeYZ, and totalDegreeXYZ, with bridge lemmas and docstrings.
• Generalize the existing BCIKS20 D_Y and D_YZ definitions from fields to commutative semirings while preserving their definitions.
• Migrate high-confidence trivariate call sites in BCIKS20 list decoding and the Hensel boundary to the semantic API.
• Reuse the common trivariate total-degree API in Hensel instead of maintaining a local duplicate.
• Add unequal-exponent regression checks for all three evaluation axes and the relevant projected/full degree notions.
• Document the nesting convention and the remaining intentional generic-bivariate uses.

Audit scope

Reviewed trivariate uses of Bivariate.evalX, evalY, degreeX, natDegreeY, totalDegree, swaps, and nested coefficient access across BCIKS20 list decoding, Polishchuk-Spielman and affine-line code, and the rational-function Hensel package. The swap sites inspected are genuinely bivariate. Remaining raw Hensel operations are on actual bivariate coefficients, on results after trivariate specialization, or are definitionally correct middle-X evaluation inside proof-heavy implementation code; the package and wiki documentation record why they are correct.

External finding and remaining obligation

PR #787 at head 54e2e918 adds Claim 5.8 hypotheses of the form Bivariate.totalDegree (R : F[Z][X][Y]) <= D_YZ Q. The asymmetric regression confirms that the left side is the (X, Y) projection, not the intended (Y, Z) projection. This main-based PR deliberately does not mutate #787. After rebasing, #787 should express those hypotheses with Trivariate.degreeYZ R <= D_YZ Q and revalidate the downstream proof obligations.

Validation

• Focused builds: Trivariate, BCIKS20 Agreement, and Hensel Weight dependency closure
• ./scripts/validate.sh
• ./scripts/validate.sh --axioms (fixture matrix passed; 10,479 declarations checked; no new axiom/sorry taint; no non-standard axiom taint)
• ./scripts/validate.sh --docs
• python3 ./scripts/check-docs-integrity.py after staging the new wiki page
• git diff --cached --check

All requested validation passed.

[github-actions]

🤖 PR Summary

The overview is written as a self-contained, objective summary of the PR's changes, organized under relevant headers. It highlights the core refactoring in Trivariate.lean, the mechanical updates across multiple files, the new API definitions, the generalization of degree constants, and the documentation additions. It notes that no sorry or admit instances are introduced, and it mentions the external finding regarding PR #787. The overview avoids critique and speculation, and it is based on the PR body and per-file summaries.

---

Statistics

Metric	Count
📝 Files Changed	9
✅ Lines Added	317
❌ Lines Removed	137

---

Lean Declarations

✏️ Added: 25 declaration(s)

ArkLib/Data/Polynomial/Trivariate.lean (25)

• example : Bivariate.totalDegree axisRegressionPolynomial ≠ degreeYZ axisRegressionPolynomial
• example : degreeInX axisRegressionPolynomial = 7
• example : degreeInY axisRegressionPolynomial = 3
• example : degreeInZ axisRegressionPolynomial = 5
• example : degreeXY axisRegressionPolynomial = 10
• example : degreeYZ axisRegressionPolynomial = 8
• example : evalAtX 2 axisRegressionPolynomial =
• example : evalAtY 2 axisRegressionPolynomial =
• example : evalAtZ 2 axisRegressionPolynomial =
• example : totalDegreeXYZ axisRegressionPolynomial = 15
• noncomputable def degreeInX (p : R[Z][X][Y]) : ℕ
• noncomputable def degreeInY (p : R[Z][X][Y]) : ℕ
• noncomputable def degreeInZ (p : R[Z][X][Y]) : ℕ
• noncomputable def degreeXY (p : R[Z][X][Y]) : ℕ
• noncomputable def degreeYZ (p : R[Z][X][Y]) : ℕ
• noncomputable def evalAtX (x : R) (p : R[Z][X][Y]) : Polynomial (Polynomial R)
• noncomputable def evalAtY (y : R) (p : R[Z][X][Y]) : R[Z][X]
• noncomputable def evalAtZ (z : R) (p : R[Z][X][Y]) : R[X][Y]
• noncomputable def totalDegreeXYZ (p : R[Z][X][Y]) : ℕ
• private noncomputable def axisRegressionPolynomial :
• theorem D_YZ_eq_degreeYZ (Q : R[Z][X][Y]) : D_YZ Q = degreeYZ Q
• theorem coeff_totalDegree_add_index_le_totalDegree (p : R[Z][X][Y]) {j : ℕ}
• theorem degreeXY_eq_bivariate_totalDegree (p : R[Z][X][Y]) :
• theorem evalAtX_eq_map_evalRingHom (x : R) (p : R[Z][X][Y]) :
• theorem evalAtZ_eq_map_map_evalRingHom (z : R) (p : R[Z][X][Y]) :

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

• noncomputable abbrev pg_eval_on_Z (p : F[Z][X][Y]) (z : F) : Polynomial (Polynomial F) in ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Extraction.lean moved from L206 to L207
• noncomputable abbrev eval_on_Z (p : R[Z][X][Y]) (z : R) : R[X][Y] in ArkLib/Data/Polynomial/Trivariate.lean moved from L56 to L75
• noncomputable def D_Y (Q : R[Z][X][Y]) : ℕ in ArkLib/Data/Polynomial/Trivariate.lean moved from L66 to L144
• noncomputable def D_YZ (Q : R[Z][X][Y]) : ℕ in ArkLib/Data/Polynomial/Trivariate.lean moved from L74 to L147
• noncomputable def eval_on_Z₀ (p : RatFunc F) (z : F) : F in ArkLib/Data/Polynomial/Trivariate.lean moved from L42 to L208

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📋 **Additional Analysis**

The PR introduces a Trivariate namespace with axis-explicit evaluation and degree functions, migrating calls from Bivariate.evalX/Bivariate.natDegreeY to Trivariate.evalAtX/Trivariate.degreeInY and updating documentation. Several style violations are present, primarily in the use of @[deprecated] attributes and the naming of D_Y/D_YZ. The documentation updates are consistent with the code changes and with the new polynomial-conventions.md file.

---

📄 **Per-File Summaries**

• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Agreement.lean: Refactored multiple lemmas in Agreement.lean to replace Bivariate.evalX, Bivariate.natDegreeY, and Trivariate.eval_on_Z with Trivariate.evalAtX, Trivariate.degreeInY, and Trivariate.evalAtZ respectively. Affected lemmas include exists_factors_with_large_common_root_set, H_dvd_evalX_R, evalX_R_separable, solution_gamma_matches_word_if_subset_large, and exists_points_with_large_matching_subset. These updates align the code with an underlying polynomial representation change from bivariate to trivariate. No new sorry or admit instances were introduced.
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Extraction.lean: This diff replaces the bespoke Bivariate.evalX and Bivariate.natDegreeY notations throughout Extraction.lean with the newly introduced unified Trivariate.evalAtX and Trivariate.degreeInY functions. Concretely, all occurrences of Bivariate.evalX (Polynomial.C x₀) R become Trivariate.evalAtX x₀ R; all occurrences of Bivariate.natDegreeY become Trivariate.degreeInY. The old pg_evalX_eq_map_evalRingHom and pg_eval_on_Z definitions are deprecated and replaced by compatibility aliases that delegate to Trivariate.evalAtX_eq_map_evalRingHom and Trivariate.evalAtZ respectively. The proofs of pg_natDegree_evalX_le_natDegreeY and pg_sum_natDegreeY_Rset_le_natDegreeY_Q are refactored to use the new API, and conversion lemmas (pg_evalX_eq_map_evalRingHom) are replaced by direct calls to Trivariate.evalAtX_eq_map_evalRingHom. No sorry or admit has been added.
• ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/Guruswami.lean: This diff contains three independent changes in Guruswami.lean, all in the ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/ListDecoding/ directory.

1. In the ModifiedGuruswami structure, the field Q_deg_X was changed from degreeX Q < D_X ((k + 1) / (n : ℚ)) n m to Trivariate.degreeInX Q < D_X ((k + 1) / (n : ℚ)) n m, reflecting a rename or migration to a more explicit Trivariate.degreeInX API.

2. In the proof of private theorem symbolicGSPoly_DYZ_le, the unfold call was updated from Trivariate.D_YZ to Trivariate.D_YZ Trivariate.degreeYZ, adding Trivariate.degreeYZ to the unfolding to expose a composed definition.

3. In the proof of private theorem modified_guruswami_has_a_solution_core, two simpa lines were adjusted: the first changed by exact_mod_cast hx to by simpa [Trivariate.degreeInX] using hx, and the second changed simpa only [Trivariate.D_Y] using hy to simpa only [Trivariate.D_Y, Trivariate.degreeInY] using hy. These now use Trivariate.degreeInX and Trivariate.degreeInY respectively, presumably to align with the renamed structured fields and maintain coherence with the change in the ModifiedGuruswami structure.

• ArkLib/Data/Polynomial/RationalFunctions.lean: The comment block in the documentation was updated to clarify that Trivariate.evalAtX x₀ R is definitionally the same as the existing Bivariate.evalX (C x₀) R expressions used elsewhere in the package, and to note that generic bivariate operations on R.coeff i are deliberate because that coefficient is genuinely bivariate in (Z, X). This improves the orientation for readers understanding the polynomial variable encodings.
• ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Hensel.lean: The definition trivariateTotalDegree is reimplemented in terms of Trivariate.totalDegreeXYZ instead of a manual support.sup over bivariate degree plus index. The lemma coeff_totalDegree_add_index_le_trivariateTotalDegree now delegates to Trivariate.coeff_totalDegree_add_index_le_totalDegree. The theorem evalX_totalDegree_le_of_coeff_bound now uses Trivariate.evalAtX instead of Bivariate.evalX, and its statement and proof are updated accordingly. A new import ArkLib.Data.Polynomial.Trivariate is added to support these changes.
• ArkLib/Data/Polynomial/Trivariate.lean: This diff refactors ArkLib/Data/Polynomial/Trivariate.lean to introduce explicit axis‑oriented evaluation and degree operations for trivariate polynomials (F[Z][X][Y] with Y outermost, X middle, Z innermost). New definitions include evalAtX, evalAtY, evalAtZ (the latter replacing the previously opaque eval_on_Z with a @[deprecated] abbreviation), degree projections degreeInX, degreeInY, degreeInZ, degreeXY, degreeYZ, totalDegreeXYZ, and theorems such as degreeXY_eq_bivariate_totalDegree, evalAtX_eq_map_evalRingHom, evalAtZ_eq_map_map_evalRingHom, and coeff_totalDegree_add_index_le_totalDegree. The paper‑facing constants D_Y and D_YZ are redefined to use these new projections, and a private axisRegressionPolynomial is added with concrete example checks verifying the degree and evaluation computations. The code is reorganized into a Semiring section (generic over R) and a Field section (field‑specific definitions eval_on_Z₀ and toRatFuncPoly), and the module docstring is expanded to clarify the variable ordering and the semantic distinction between Bivariate and Trivariate operations.
• docs/wiki/README.md: Added references to a new polynomial-conventions.md in two sections of docs/wiki/README.md: once in the list of reusable cross‑cutting workflow documents (describing semantic axes for nested bivariate and trivariate polynomial representations) and once in the agent‑consultation list (describing nested polynomial axes and semantic evaluation/degree APIs).
• docs/wiki/polynomial-conventions.md: This new wiki page documents ArkLib's nested polynomial axis convention for trivariate polynomials F[Z][X][Y], explicitly mapping semantic variables Y, X, Z to structural positions. It introduces the dedicated Trivariate operations (evalAtX/Y/Z, degreeInX/Y/Z, degreeXY, degreeYZ, totalDegreeXYZ) and the paper-facing wrappers D_Y and D_YZ. The page warns against deducing axis semantics from type arguments alone, explaining that direct Bivariate operations on a trivariate value treat it as bivariate over F[Z] and thus yield different degree measures (e.g., Bivariate.totalDegree only covers the (X,Y) projection, not the full totalDegreeXYZ). Concrete examples illustrate correct usage after specialization (e.g., Bivariate.totalDegree (p.coeff j)) and a testing heuristic using unequal exponents to detect accidental permutation errors.
• docs/wiki/repo-map.md: The documentation for trivariate polynomial utilities (ArkLib/Data/Polynomial/Trivariate.lean) is corrected: the old entry eval_on_Z is replaced with the current names evalAtX, evalAtY, evalAtZ, and the phrase “the named degree projections” is added before D_Y, D_YZ. A cross-reference to polynomial-conventions.md is also added, warning readers to consult those conventions before applying generic bivariate operations to a trivariate value.

---

Last updated: 2026-09-01 02:06 UTC.

[github-actions]

Build Timing Report

• Commit: fe1a3f9
• Message: refactor(polynomial): make trivariate axes explicit
• Ref: harden-trivariate-axis-api
• 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	1229.08	+29.98	ok
Warm rebuild	2.91	2.79	-0.12	ok
Validation wrapper	17.23	16.95	-0.28	ok

Incremental Rebuild Signal

• Warm rebuild saved 1226.29s vs clean (440.53x 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
135.00	124.00	+11.00	ArkLib/Data/Polynomial/RationalFunctions/HenselNumerators/Weight.lean
100.00	95.00	+5.00	ArkLib/ProofSystem/Stir/Combine.lean
80.00	69.00	+11.00	ArkLib/Data/CodingTheory/ListDecodability/Bounds/KKH26Asymptotic.lean
80.00	66.00	+14.00	ArkLib/Data/CodingTheory/JohnsonBound/Family.lean
75.00	77.00	-2.00	ArkLib/Data/CodingTheory/ProximityGap/CapacityBounds/UniqueDecoding.lean
68.00	71.00	-3.00	ArkLib/Data/CodingTheory/ProximityGap/DG25/MainResults.lean
66.00	67.00	-1.00	ArkLib/Data/CodingTheory/SubspaceDesign.lean
64.00	65.00	-1.00	ArkLib/Data/CodingTheory/ProximityGap/Folding.lean
62.00	62.00	+0.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/BWMatrix.lean
60.00	61.00	-1.00	ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
58.00	56.00	+2.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineSpaces.lean
57.00	52.00	+5.00	ArkLib/Data/CodingTheory/ProximityGap/CapacityBounds/Frs.lean
54.00	73.00	-19.00	ArkLib/Data/Domain/CosetFftDomain/Subdomain.lean
50.00	45.00	+5.00	ArkLib/Data/MvPolynomial/EvenAndOdd.lean
49.00	57.00	-8.00	ArkLib/Data/CodingTheory/ListDecodability/Bounds/LargeAlphabet/Pigeonhole.lean
46.00	51.00	-5.00	ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean
46.00	43.00	+3.00	ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean
45.00	36.00	+9.00	ArkLib/Data/CodingTheory/ListDecodability/Bounds/ReedSolomon.lean
44.00	36.00	+8.00	ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean
44.00	42.00	+2.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/WeightedAgreement.lean

[quangvdao]

Thanks, Alexander — I reviewed the axis semantics and the downstream migrations, rebased this onto current main, and validated the rebased head locally. Making the trivariate axes explicit removes a real ambiguity in degree reasoning, and the compatibility bridge plus migrated call sites look coherent. Approved.