Partial proof for exists_hensel_numerator_sequence

[aleph-prover]

⚠️ Your proof request could only be partially completed
Some theorems may only have informal proofs available.
Some hard-to-prove facts may have been replaced with axioms.

---

Proven lemmas: 13/16

The current goal is to prove existence of a Hensel numerator sequence βseq for a polynomial relation R at x₀ relative to an irreducible factor H: namely, ∃ βseq : ℕ → 𝒪 H such that βseq gives a genuine Hensel lift and satisfies the weight bound ∀ t, weight(βseq t) ≤ (2t + 1) · natDegreeY(R) · D.

The proof has been decomposed into three main mathematical parts: (1) construct an abstract Hensel coefficient sequence αseq in the function field 𝕃 H, (2) show these coefficients admit regular numerators βseq with the required denominator shape, and (3) prove the coarse weight estimate for those numerators. Around these, several supporting lemmas have already been established: the initial root at x₀, nonvanishing of the derivative term ζ, comparison lemmas showing that a numerator-shaped sequence really gives a Hensel numerator sequence, and degree-control lemmas needed for weights.

Progress is substantial: 13 of the 19 proof components are proved, including the final assembly theorem conditional on its remaining ingredients. In particular, the “outer shell” of the argument is in place: once αseq exists, one can build βseq, transfer the Hensel semantics, and derive the final bound by combining the established lemmas.

What remains are the three deepest pieces: constructing the formal Hensel α-sequence itself, proving the key “cleared residual is regular” lemma that produces the next numerator, and proving the strong successor step for the weight induction. These are exactly the hard recursive core of the paper’s argument.

A notable issue has emerged: there is strong evidence that the present formal statement is using the wrong coordinate system. Mathematically, the paper’s Hensel lift is local in the variable X - x₀, but the current statement appears to encode a global equation in X; a concrete example suggests this global version is false. So the project is at an important checkpoint: either the theorem statement must be corrected to the local-coordinate version, or one should formally record that the current statement is false.

Even with that obstruction, the work done so far is valuable: it has isolated the exact mathematical bottleneck, proved all the surrounding infrastructure, and clarified the intended strategy—simple root ⇒ formal Hensel lift αseq ⇒ regular numerator realization βseq ⇒ induction on weights.

[github-actions]

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: Partial proof for exists_hensel_numerator_sequence

sorry delta: +2 (1 removed, 3 added) — proof obligations increased

Mathematical Framework

Establishes a formal framework for proving the existence of Hensel numerator sequences (exists_hensel_numerator_sequence) for a polynomial relation $R$ at $x_0$ relative to an irreducible factor $H$. The proof structure is decomposed into the construction of an abstract sequence $\alpha_{seq}$, the derivation of regular numerators $\beta_{seq}$, and the establishment of weight bounds.

Key infrastructure established:

• Initial root at $x_0$ and nonvanishing derivative term $\zeta$.
• Comparison lemmas for numerator-shaped sequences.
• Degree-control lemmas for weight estimates.

Proof Status and Admitted Lemmas

• WARNING: This PR is a partial implementation and contains several sorry placeholders for the hard recursive core of the argument.
• Admitted (sorried) items:
  • Construction of the formal Hensel sequence (formalHenselAlphaSequence).
  • The "cleared residual is regular" lemma.
  • The inductive successor step for weight bounds (numerator_shape_weight_succ_le_strong).

Coordinate System Discrepancy

• The PR identifies a significant conceptual discrepancy: the current formal statement uses a global coordinate system in $X$, whereas the mathematical source suggests a local coordinate system in $(X - x_0)$.
• Formal notes indicate the global formulation may be mathematically false, signaling a necessary shift to local coordinates in future iterations.

---

Statistics

Metric	Count
📝 Files Changed	1
✅ Lines Added	420
❌ Lines Removed	1

---

Lean Declarations

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

• theorem initial_root_at_x0 (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem exists_regular_numerator_shape (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem gammaOfNumerators_eq_gammaFromAlpha (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem formalHenselAlphaSequence (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem zeta_ne_zero_of_Hypotheses (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem hensel_numerator_sequence_of_alpha_shape (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem mk_H_tilde_eq_W_pow_mul_eval2 (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem H_eval2_T_div_W_eq_zero (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean
• def HasNumeratorShape (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem regular_numerator_shape_succ (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem henselCoeffResidual_regular_after_clearing (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean
• noncomputable def gammaFromAlpha (x₀ : F) (H : F[X][Y]) (αseq : ℕ → 𝕃 H) : in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem evalX_totalDegree_le_of_coeff_bound (x₀ : F) (R : F[X][X][Y]) {D : ℕ} in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem beta_zero_eq_X_of_shape (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem numerator_shape_weight_succ_le_strong (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem exists_hensel_alpha_sequence (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean
• theorem numerator_shape_weight_bound (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean
• noncomputable def henselCoeffResidual (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean

---

sorry Tracking

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

• lemma exists_hensel_numerator_sequence (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean (L1760)

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

• theorem formalHenselAlphaSequence (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean (L1836)
• theorem numerator_shape_weight_succ_le_strong (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean (L1994)
• theorem henselCoeffResidual_regular_after_clearing (x₀ : F) (R : F[X][X][Y]) (H : F[X][Y]) in ArkLib/Data/Polynomial/RationalFunctions.lean (L1974)

---

📋 **Additional Analysis**

Style and Naming Guidelines

• Line Length: Several lines exceed the 100-character limit:
  • The change statement in mk_H_tilde_eq_W_pow_mul_eval2 (approx. 265 characters).
  • The hhom definition in mk_H_tilde_eq_W_pow_mul_eval2 (approx. 130 characters).
  • The hprev hypothesis in henselCoeffResidual_regular_after_clearing (approx. 175 characters).
  • The ihAll hypothesis in numerator_shape_weight_succ_le_strong (approx. 115 characters).
  • The exact call in exists_regular_numerator_shape (approx. 108 characters).
• Formatting: The use of spaces around operators and binders generally adheres to the guidelines.
• Naming: The naming of new declarations adheres to the established conventions:
  • Theorems (e.g., evalX_totalDegree_le_of_coeff_bound, beta_zero_eq_X_of_shape) use snake_case.
  • Definitions (e.g., gammaFromAlpha, henselCoeffResidual) use lowerCamelCase.
  • Prop-valued predicates (e.g., HasNumeratorShape) use UpperCamelCase.

Documentation Standards

• Missing Docstrings: All new definitions and theorems (approximately 18 declarations) are missing documentation strings. The guidelines state: "Every definition and major theorem should have a docstring."
• Citations: The implementation notes for formalHenselAlphaSequence and existing docstrings refer to [BCIKS20]. Ensure that the file header contains a ## References section with the corresponding formatted entry and that the BibTeX entry is present in blueprint/src/references.bib.

Progress and Implementation Status

• Admitted Proofs: Three major components of the formalization are currently admitted using sorry:
  • formalHenselAlphaSequence (the core Hensel-lifting existence theorem).
  • henselCoeffResidual_regular_after_clearing (the residual regularity lemma).
  • numerator_shape_weight_succ_le_strong (the inductive step for weight bounds).
• Goal Completion: The pull request successfully provides the structural composition for exists_hensel_numerator_sequence, reducing the primary proof obligation to the three admitted lemmas above.

---

📄 **Per-File Summaries**

• ArkLib/Data/Polynomial/RationalFunctions.lean: This update introduces a comprehensive suite of definitions and theorems to formalize the existence and weight bounds of Hensel numerator sequences. While it provides a high-level proof for exists_hensel_numerator_sequence, several critical technical lemmas and inductive steps, such as formalHenselAlphaSequence and numerator_shape_weight_succ_le_strong, currently contain sorry placeholders.

---

Last updated: 2026-06-07 01:10 UTC.

[alexanderlhicks]

PR #540 is stacked on #497, so its base is the relevant bridge.

The current #497 head (73d346a9) already contains the Claim A.2 developments introduced by this PR, including formalHenselAlphaSequence, henselCoeffResidual_regular_after_clearing, and the numerator-shape/weight scaffolding. #497 now also modularizes them under RationalFunctions.HenselNumerators.

Because #540 is based on the older #497 state and is now divergent, it should be treated as superseded rather than rebased and merged separately.