feat: proofs for rational functions

[alexanderlhicks]

Replaces #304 to make it easier to commit straight to this branch rather than on the fork's branch.

[github-actions]

🤖 Gemini PR Summary

Summary

Advances the formalization of polynomial constructions for Hensel lifting, focusing on monisization and structural properties.

Note: The PR title refers to "rational functions," while the draft summary describes polynomial monisization and lifting procedures.

Mathematical Formalization

• Polynomial Monisization: Defines the monisized polynomial $\tilde{H}$ and its bivariate counterpart $\tilde{H}'$.
• Hensel Lifting Support: Defines coefficients $\alpha, \gamma, \zeta$ required for Hensel lifting procedures.
• Structural Properties: Establishes the monic property of the bivariate polynomial $\tilde{H}'$ and provides equivalence proofs between its univariate and bivariate forms.
• Irreducibility: Provides initial formalizations regarding the irreducibility of the monisized construction $\tilde{H}$.

Incomplete Proofs

CRITICAL: This PR contains several sorry placeholders and is not yet fully proved. The following items remain incomplete:

• Lemma_A_1: Primary proof is omitted.
• ξ_regular: Regularity proof for the coefficient $\xi$ is incomplete.
• bivPolyHom_HTilde'_eq_HTilde: Zero-degree case for the homomorphism equivalence remains unproven.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	533
❌ Lines Removed	73

---

Lean Declarations

✏️ **Removed:** 7 declaration(s)

• def β (R : F[X][X][Y]) (t : ℕ) : 𝒪 H in ArkLib/Data/Polynomial/RationalFunctions.lean
• def γ (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [φ : Fact (Irreducible H)] : PowerSeries (𝕃 H) in ArkLib/Data/Polynomial/RationalFunctions.lean
• def α (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [φ : Fact (Irreducible H)] (t : ℕ) : 𝕃 H in ArkLib/Data/Polynomial/RationalFunctions.lean
• def ζ (R : F[X][X][Y]) (x₀ : F) (H : F[X][Y]) [H_irreducible : Fact (Irreducible H)] : 𝕃 H in ArkLib/Data/Polynomial/RationalFunctions.lean
• def α' (x₀ : F) (R : F[X][X][Y]) (H_irreducible : Irreducible H) (t : ℕ) : 𝕃 H in ArkLib/Data/Polynomial/RationalFunctions.lean
• def γ' (x₀ : F) (R : F[X][X][Y]) (H_irreducible : Irreducible H) : PowerSeries (𝕃 H) in ArkLib/Data/Polynomial/RationalFunctions.lean
• def ξ (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) [φ : Fact (Irreducible H)] : 𝒪 H in ArkLib/Data/Polynomial/RationalFunctions.lean

✏️ **Added:** 13 declaration(s)

• theorem univPolyHom_injective : in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem canonicalRepOf𝒪_zero in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem H_tilde_eq_sum_range (H : F[X][Y]) : in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem C_mul_X_div_C {w : RatFunc F} (hw : w ≠ 0) : in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem H_tilde'_tail_degree_lt (H : F[X][Y]) : in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem H_tilde_eq_explicit_forward (H : F[X][Y]) (hdeg : 0 < H.natDegree) : in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem H_tilde'_map_explicit (H : F[X][Y]) : in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem H_tilde_eq_explicit (H : F[X][Y]) (hdeg : 0 < H.natDegree) : in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem embeddingOf𝒪Into𝕃_ideal_le (H : F[X][Y]) : in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem irreducible_comp_C_mul_X_iff {K : Type} [Field K] (a : K) (ha : a ≠ 0) (p : K[X]) : in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem bivPolyHom_HTilde'_eq_HTilde (H : F[X][Y]) : in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem H_tilde'_monic (H : F[X][Y]) : in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem irreducible_map_univPolyHom_of_irreducible in ArkLib/Data/Polynomial/RationalFunctions.lean

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

• theorem β_regular in ArkLib/Data/Polynomial/RationalFunctions.lean moved from L242 to L493
• theorem irreducibleHTildeOfIrreducible {H : Polynomial (Polynomial F)} in ArkLib/Data/Polynomial/RationalFunctions.lean moved from L57 to L550
• lemma ξ_regular (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean moved from L222 to L684
• lemma isField_of_irreducible {H : F[X][Y]} (hdeg : H.natDegree ≠ 0) : in ArkLib/Data/Polynomial/RationalFunctions.lean moved from L67 to L648
• theorem H_tilde_equiv_H_tilde' (H : F[X][Y]) (hdeg : 0 < H.natDegree) : in ArkLib/Data/Polynomial/RationalFunctions.lean moved from L91 to L348

---

sorry Tracking

✅ **Removed:** 3 `sorry`(s)

• lemma β_regular (R : F[X][X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean (L246)
• lemma irreducibleHTildeOfIrreducible {H : Polynomial (Polynomial F)} : in ArkLib/Data/Polynomial/RationalFunctions.lean (L59)
• lemma H_tilde_equiv_H_tilde' (H : F[X][Y]) : (H_tilde' H).map univPolyHom = H_tilde H in ArkLib/Data/Polynomial/RationalFunctions.lean (L92)

❌ **Added:** 1 `sorry`(s)

• theorem bivPolyHom_HTilde'_eq_HTilde (H : F[X][Y]) : in ArkLib/Data/Polynomial/RationalFunctions.lean (L366)

✏️ **Affected:** 1 `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 L178 to L469

---

🎨 **Style Guide Adherence**

There are more than 20 violations of the style guide. They are grouped by rule below:

Documentation Standards

• Module and Declaration Docstrings: "Each file should start with a /-! ... -/ block containing a title, summary, notation, and references" and "Every definition and major theorem should have a docstring... Use /-- ... -/ above definitions."
  • Violation Count: 18
  • Examples:
    • The file starts with a copyright block but is missing the mandatory /-! ... -/ module docstring.
    • theorem H_tilde'_monic (Line 150) is missing a docstring.
    • theorem isField_of_irreducible (Line 550) is missing a docstring.

Naming Conventions

• Theorems and Proofs in snake_case: "Theorems and Proofs: snake_case (e.g., add_comm, list_reverse_id)."
  • Violation Count: 5
  • Examples:
    • theorem bivPolyHom_HTilde'_eq_HTilde (Line 361) uses CamelCase and acronyms incorrectly.
    • theorem irreducibleHTildeOfIrreducible (Line 534) uses CamelCase.
    • lemma Lemma_A_1 (Line 466) uses improper capitalization.
• Functions and Terms in lowerCamelCase: "Functions and Terms: lowerCamelCase (e.g., binarySearch, isPrime)."
  • Violation Count: 1
  • Example: def Polynomial.Bivariate.Y (Line 30) uses UpperCamelCase.

Syntax and Formatting

• Line Length: "Keep lines under 100 characters."
  • Violation Count: 6
  • Examples: Line 115 (106 chars), Line 247 (122 chars), and Line 318 (106 chars).
• Indentation: "Use 2 spaces for indentation."
  • Violation Count: 8
  • Examples: Lines 118-121 (4+ spaces), and the tactic block for irreducible_comp_C_mul_X_iff (Line 515).
• Functions and Binders: "Prefer fun x ↦ ... over λ x, ...."
  • Violation Count: 3
  • Examples: Line 124 uses fun x => and Line 410 uses fun n =>.
• Instances: "Use the where syntax for defining instances and structures."
  • Violation Count: 1
  • Example: The Field (𝕃 H) instance (Line 566) uses :=.
• Operators: "Place [operators] before a line break rather than at the start of the next line."
  • Violation Count: 1
  • Example: Line 458 places the : operator at the start of a new line.

Normal Forms

• Standard Inequalities: "Avoid ≥ (ge) and > (gt) in theorem statements unless necessary for argument ordering."
  • Violation Count: 4
  • Examples: hD : D ≥ Bivariate.totalDegree H (Line 466) and S_β_card : Set.ncard (S_β β) > ... (Line 467).

Dot Notation

• Manual Dot Notation: "Use manual dot notation for logical connectives and equality (e.g., And.intro, Eq.refl, Iff.mp)."
  • Violation Count: 3
  • Examples: Lines 229, 290, and 302 use .symm on equality proofs instead of the manual Eq.symm.

---

📄 **Per-File Summaries**

• ArkLib/Data/Polynomial/RationalFunctions.lean: This update formalizes the construction and properties of the monisized polynomial $\tilde{H}$ and its bivariate counterpart $\tilde{H}'$, providing proofs for their equivalence and the irreducibility of $\tilde{H}$. It introduces several new definitions for Hensel lifting coefficients ($\alpha, \gamma, \zeta$) and establishes the monic property of $\tilde{H}'$. However, sorry placeholders remain in the proofs of Lemma_A_1, ξ_regular, and the zero-degree case of bivPolyHom_HTilde'_eq_HTilde.

---

Last updated: 2026-03-17 07:03 UTC.

[github-actions]

Build Timing Report

• Commit: f5d9faf
• Message: Merge ef21ebd into e862b6c
• Ref: update-rational-functions
• Comparison baseline: 01d3253 from the latest successful main run.
• 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	639.70	638.06	-1.64	exit 1
Warm rebuild	6.13	-	-	-
Validation wrapper	4.12	-	-	-

Incremental Rebuild Signal

• Clean:warm comparison is unavailable because one of the build measurements is missing.

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
100.00	85.00	+15.00	ArkLib/ProofSystem/Fri/Spec/SingleRound.lean
83.00	86.00	-3.00	ArkLib/Data/CodingTheory/JohnsonBound/Lemmas.lean
62.00	58.00	+4.00	ArkLib/Data/CodingTheory/Basic.lean
61.00	63.00	-2.00	ArkLib/Data/CodingTheory/GuruswamiSudan/Basic.lean
51.00	60.00	-9.00	ArkLib/Data/CodingTheory/ProximityGap/BCIKS20/AffineLines/BWMatrix.lean
49.00	49.00	+0.00	ArkLib/Data/CodingTheory/BerlekampWelch/Condition.lean
46.00	44.00	+2.00	ArkLib/ProofSystem/Binius/BinaryBasefold/Prelude.lean
45.00	43.00	+2.00	ArkLib/Data/CodingTheory/JohnsonBound/Basic.lean
44.00	49.00	-5.00	ArkLib/OracleReduction/LiftContext/Reduction.lean
40.00	41.00	-1.00	ArkLib/OracleReduction/Security/RoundByRound.lean
34.00	41.00	-7.00	ArkLib/Data/CodingTheory/ProximityGap/DG25.lean
32.00	31.00	+1.00	ArkLib/Data/CodingTheory/DivergenceOfSets.lean
27.00	26.00	+1.00	ArkLib/OracleReduction/ProtocolSpec/Basic.lean
27.00	29.00	-2.00	ArkLib/Data/CodingTheory/PolishchukSpielman/Resultant.lean
27.00	24.00	+3.00	ArkLib/ProofSystem/Component/RandomQuery.lean
26.00	29.00	-3.00	ArkLib/ProofSystem/Fri/Domain.lean
24.00	31.00	-7.00	ArkLib/OracleReduction/Composition/Sequential/Append.lean
23.00	24.00	-1.00	ArkLib/ProofSystem/Binius/BinaryBasefold/Steps.lean
22.00	25.00	-3.00	ArkLib/Data/Hash/Poseidon2.lean
22.00	17.00	+5.00	ArkLib/ProofSystem/Component/ReduceClaim.lean