finish proximitygap, do bivariate

[Ferinko]

ArkLib/Data/Polynomial/RationalFunctions.lean:81 - What is H_tilde' supposed to be?

[github-actions]

🤖 Gemini PR Summary

Error generating summary:
No API_KEY or ADC found. Please either:
- Set the GOOGLE_API_KEY environment variable.
- Manually pass the key with genai.configure(api_key=my_api_key).
- Or set up Application Default Credentials, see https://ai.google.dev/gemini-api/docs/oauth for more information.

---

Analysis of Changes

Metric	Count
📝 Files Changed	8
✅ Lines Added	239
❌ Lines Removed	518

---

sorry Tracking

• ✅ Removed: 1 sorry(s)
  • def H_tilde' (H : F[X][Y]) : F[X][Y] in ArkLib/Data/Polynomial/RationalFunctions.lean
• ❌ Added: 4 sorry(s)
  • lemma rank_eq_iff_subUpFull_eq (h : n ≤ m) : in ArkLib/Data/CodingTheory/Prelims.lean
  • lemma rank_eq_min_row_col_rank : U.rank = min (rowRank U) (colRank U) in ArkLib/Data/CodingTheory/Prelims.lean
  • lemma H_tilde_equiv_H_tilde' (H : F[X][Y]) : (H_tilde' H).map univPolyHom = H_tilde H in ArkLib/Data/Polynomial/RationalFunctions.lean
  • lemma rank_eq_iff_det_ne_zero {U : Matrix (Fin n) (Fin n) F} : in ArkLib/Data/CodingTheory/Prelims.lean
• ✏️ Affected: 2 sorry(s) (line number changed)
  • lemma Lemma_A_1 {H : F[X][Y]} (β : 𝒪 H) (D : ℕ) (hD : D ≥ Bivariate.totalDegree H) in ArkLib/Data/Polynomial/RationalFunctions.lean moved from L157 to L165
  • lemma ξ_regular (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [H_irreducible : Fact (Irreducible H)] : in ArkLib/Data/Polynomial/RationalFunctions.lean moved from L208 to L214

---

Last updated: 2025-10-27 21:12 UTC. See the main CI run for build status.