feat(NumberTheory): non-vanishing derivative and algebraic lower bound for Gelfond-Schneider

[mkaratarakis]

This PR continues the formalization of the Gelfond-Schneider Theorem (Hilbert's Seventh Problem). It establishes the critical algebraic lower bound for the auxiliary function's evaluation by isolating its first non-vanishing derivative and scaling it to a non-zero algebraic integer.

Following the contradiction argument in Loo-Keng Hua's Introduction to Number Theory (Chapter 17.9, Equation 5), we extract the minimal non-vanishing derivative order $r$ and prove the integrality of its scaled evaluation to establish a strict analytical lower bound.

1. Confirms that by our previous choice of coefficients $\eta$, the first $n$ derivatives of the auxiliary function $R(x)$ vanish at the evaluation points $1, \dots, m$.
2. Extracts the exact minimal order of vanishing $r$ among all points $l_0 + 1$, explicitly proving the textbook assertion that $n \le r$.
3. Defines the non-zero algebraic number $\rho = (\log \alpha)^{-r} R^{(r)}(l_0)$.
4. Formalizes the crucial algebraic step that scaling the evaluated system coefficients by $c_1^{r+2mq}$ (formalized here as cρ) clears all denominators, resulting in an algebraic integer strictly within $\mathcal{O}_K$.
5. Concludes that because the scaled $\rho$ is a non-zero algebraic integer, its absolute norm is strictly bounded below by $1$. This establishes the algebraic foundation for the absolute lower bound $|N(\rho)| > c_5^{-r}$, which will directly oppose the complex analytic upper bound via Cauchy's integral formula in the final contradiction step.

---

• depends on: feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem (Part 4/5) #35316
• depends on: feat(NumberTheory): non-vanishing derivative and norm lower bounds for Gelfond-Schneider #35743
• depends on: [Merged by Bors] - feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem (Part 3/5) #35315

[github-actions]

PR summary 8f07524533

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.NumberTheory.Transcendental.GelfondSchneider.MainAlg (new file)	2917
Mathlib.NumberTheory.Transcendental.GelfondSchneider.MainAlgSetup (new file)	3127
Mathlib.NumberTheory.Transcendental.GelfondSchneider.MainOrder (new file)	3133
Mathlib.NumberTheory.Transcendental.GelfondSchneider.MainAnalytic (new file)	3134
Mathlib.NumberTheory.Transcendental.GelfondSchneider.MainPostAnalytic (new file)	3136

---

Declarations diff

+ A
+ IsIntegral.Cast
+ IsIntegral.Nat
+ IsIntegral_assoc
+ R
+ R_ne_zero
+ R_order
+ R_order_eq
+ R_order_prop
+ Rorder_exists
+ Setup
+ V
+ a
+ abs_crho_le_norm_crho
+ abs_q_pow_mul_house_le_c₃_pow
+ alpha'_beta'_gamma'_ne_zero
+ alpha'_ne_one
+ alpha_gamma_pow_beta_ne_zero
+ b
+ b_sum_ne_zero
+ beta'_ne_zero
+ beta_ne_zero
+ bound_c₁β
+ c1rho_neq_0
+ c1ρ
+ c5nonneg
+ c_coeffs
+ c_coeffs0
+ c_coeffs_neq_zero
+ c_coeffspow_r
+ cexp_mul
+ coeffs_mulVec_A_eq
+ coeffs_mul_deriv_eq_zero
+ crho_le_abs_crho
+ cρ
+ cρ_ne_zero
+ c₀
+ c₀Coeff
+ c₀Coeff_ne_zero
+ c₁
+ c₁IsInt
+ c₁_ne_zero
+ c₁_pow_sub_one_mul_c₁_pow_mul_c₁_pow_eq
+ c₁α_ne_zero
+ c₁γ_ne_zero
+ c₂
+ c₃
+ c₃_pow
+ c₄
+ c₅
+ deriv_R_k_eval_at_l0'
+ eq5
+ eq5zero
+ eq_iff_finProdFinEquiv_symm_ext
+ exists_common_field_of_isAlgebraic
+ exists_int_smul_isIntegral
+ exists_min_analyticOrderAt
+ exists_nonzero_iteratedFDeriv
+ h
+ h1
+ hM_ne_zero
+ hbound_sigma
+ house_add_mul_le
+ house_bound_c₁α
+ house_eta_le_c₄_pow
+ house_geq_1
+ house_matrixA_le
+ isInt_β_bound
+ isInt_β_bound_low
+ isIntegral_c₁_pow_smul_add_smul_pow
+ isIntegral_c₁_pow_smul_pow
+ isIntegral_c₁_pow_smul_α'_pow
+ isIntegral_c₁_pow_smul_α'_pow'
+ isIntegral_c₁_pow_smul_γ'_pow
+ isIntegral_c₁_pow_smul_γ'_pow'
+ isIntegral_c₁α
+ isIntegral_c₁β
+ isIntegral_c₁γ
+ isNumberField_adjoin_of_isAlgebraic
+ iteratedDeriv_R
+ iteratedDeriv_R_eq_zero
+ iteratedkDeriv_R_eq_zero
+ k
+ l
+ log_α_ne_zero
+ l₀'
+ l₀_prop
+ m
+ m_mul_n_lt_q_mul_q
+ m_mul_n_pos
+ mul_div_sub_eq_one
+ mul_rpow_sub_one_div_two
+ n
+ n_le_r
+ norm_Algebra_norm_rho_nonzero
+ norm_crho_le_house_crho
+ norm_cρ_pos
+ one_le_abs_c₁
+ one_le_c1rho
+ one_le_c₁
+ one_le_c₂
+ one_le_c₃
+ one_le_house_c₁γ
+ one_le_m
+ one_le_n
+ one_le_norm_c1rho
+ order_geq_n
+ order_geq_n_foo
+ order_neq_top
+ order_neq_top_min_one
+ q_eq_n_etc
+ q_le_two_mn
+ q_sq_eq_two_mn
+ q_sq_le_two_mn
+ r
+ r'
+ r'_spec
+ r_div_q_geq_0
+ r_exists
+ r_ne_zero
+ r_prop
+ r_spec
+ rho
+ rho_eq_ρᵣ
+ rho_injective
+ rho_nonzero
+ systemCoeffs
+ systemCoeffs_deriv
+ systemCoeffs_deriv_r
+ systemCoeffs_map_eq_exp_mul
+ systemCoeffs_map_eq_exp_mul_r
+ systemCoeffs_ne_zero_r
+ systemCoeffs_r
+ vandermonde_det_ne_zero
+ vecMul_V_eq_zero
+ zero_le_c1rho
+ zsmul_mul_mul_distrib
+ β'_ne_zero
+ η
+ ηvec_eq_zero
+ ρ
+ ρ_is_int
+ ρᵣ
+ ρᵣ_nonzero

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for scripts/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem (Part 4/5) #35316
• feat(NumberTheory): non-vanishing derivative and norm lower bounds for Gelfond-Schneider #35743
• [Merged by Bors] - feat: lemmas for the analytic part of the proof of the Gelfond–Schneider theorem (Part 3/5) #35315
  By Dependent Issues (🤖). Happy coding!