Encyclopedia Masses Masses Mass Genesis T10 Exp Transcendental Tendsto Pow Div Factorial Pred

ARTICLE 3 claims 3 theorems

Masses Mass Genesis T10 Exp Transcendental Tendsto Pow Div Factorial Pred

A small lemma about powers versus factorials is the last step in proving that Euler's number e is transcendental.

Verify this page

The vanishing ratio

The number e, about 2.71828, is the base of natural logarithms and the limit of (1 + 1/n)^n as n grows. A classical theorem, proved by Charles Hermite in 1873, states that e is transcendental: it is not the root of any polynomial with integer coefficients. The proof is a contradiction argument. Assume e is algebraic, build a polynomial relation, then construct an integer that is both nonzero and smaller than 1 in absolute value for infinitely many primes. The contradiction forces the assumption to fail.

The final step of that argument needs a simple analytic fact: for any fixed real number c, the ratio c^m divided by (m-1)! tends to 0 as m tends to infinity. Factorials grow faster than any exponential. The factorial in the denominator eventually dwarfs the power in the numerator, no matter how large c is. This is the lemma named tendsto_pow_div_factorial_pred in the framework's machine-checked library of formal theorems. The declaration proves that the sequence (c^m / (m-1)!) converges to 0 in the real numbers.

In the Hermite proof, this vanishing ratio bounds the size of the constructed integer M_p. The bound shrinks to 0, so for large primes the integer's absolute value is less than 1. Since M_p is a nonzero integer, its absolute value is at least 1. The contradiction proves that e cannot be algebraic, hence e is transcendental. The lemma is the quantitative engine that closes the proof.

Within Recognition Science, this lemma appears in the T10 settlement-cone wall, where the algebraic/transcendental split of memory notes becomes a formal theorem. The declaration itself is a private helper: it does not state the transcendence of e. That conclusion is the separate theorem transcendental_e. The lemma only supplies the limit fact. It does not claim anything about the rate of convergence, nor about any other transcendental numbers, nor about the physical mass spectrum that the T10 wall supports. Its role is narrow and precise: it makes the factorial bound explicit.

The practical consequence is that a reader can trust the Hermite proof's analytic core without hand-waving. The factorial growth argument is checked line by line in the formal library. For the framework, this turns a classical analytical fact into a certified stepping stone toward the e-transcendence theorem, which in turn anchors the algebraic/transcendental split used in the mass-genesis structure.

THEOREM tendsto_pow_div_factorial_pred · IndisputableMonolith/Masses/MassGenesis/T10ExpTranscendental.lean
tendsto_pow_div_factorial_pred · IndisputableMonolith/Masses/MassGenesis/T10ExpTranscendental.lean:160 
private theorem tendsto_pow_div_factorial_pred (c : ℝ) :
    Filter.Tendsto (fun m : ℕ => c ^ m / ((m - 1)! : ℝ)) Filter.atTop (nhds 0) := by
  have h0 : Filter.Tendsto (fun m : ℕ => c ^ m / (m ! : ℝ)) Filter.atTop (nhds 0) :=
    (Real.summable_pow_div_factorial c).tendsto_atTop_zero
  have h1 : Filter.Tendsto (fun m : ℕ => c ^ (m - 1) / ((m - 1)! : ℝ))
      Filter.atTop (nhds 0) := by
    simpa only [Function.comp_apply] using h0.comp (Filter.tendsto_sub_atTop_nat 1)
  have hev : (fun m : ℕ => c ^ m / ((m - 1)! : ℝ)) =ᶠ[Filter.atTop]
      (fun m : ℕ => c * (c ^ (m - 1) / ((m - 1)! : ℝ))) := by
    filter_upwards [Filter.eventually_ge_atTop 1] with m hm
    have hm' : m = (m - 1) + 1 := (Nat.succ_pred_eq_of_pos hm).symm
    conv_lhs => rw [hm']
    rw [pow_succ', Nat.add_sub_cancel]
    ring
  have h2 : Filter.Tendsto (fun m : ℕ => c * (c ^ (m - 1) / ((m - 1)! : ℝ)))
      Filter.atTop (nhds (c * 0)) := h1.const_mul c
  rw [mul_zero] at h2
  exact Filter.Tendsto.congr' hev.symm h2
THEOREM tendsto_pow_div_factorial_pred · IndisputableMonolith/Masses/MassGenesis/T10ExpTranscendental.lean
tendsto_pow_div_factorial_pred · IndisputableMonolith/Masses/MassGenesis/T10ExpTranscendental.lean:160 
private theorem tendsto_pow_div_factorial_pred (c : ℝ) :
    Filter.Tendsto (fun m : ℕ => c ^ m / ((m - 1)! : ℝ)) Filter.atTop (nhds 0) := by
  have h0 : Filter.Tendsto (fun m : ℕ => c ^ m / (m ! : ℝ)) Filter.atTop (nhds 0) :=
    (Real.summable_pow_div_factorial c).tendsto_atTop_zero
  have h1 : Filter.Tendsto (fun m : ℕ => c ^ (m - 1) / ((m - 1)! : ℝ))
      Filter.atTop (nhds 0) := by
    simpa only [Function.comp_apply] using h0.comp (Filter.tendsto_sub_atTop_nat 1)
  have hev : (fun m : ℕ => c ^ m / ((m - 1)! : ℝ)) =ᶠ[Filter.atTop]
      (fun m : ℕ => c * (c ^ (m - 1) / ((m - 1)! : ℝ))) := by
    filter_upwards [Filter.eventually_ge_atTop 1] with m hm
    have hm' : m = (m - 1) + 1 := (Nat.succ_pred_eq_of_pos hm).symm
    conv_lhs => rw [hm']
    rw [pow_succ', Nat.add_sub_cancel]
    ring
  have h2 : Filter.Tendsto (fun m : ℕ => c * (c ^ (m - 1) / ((m - 1)! : ℝ)))
      Filter.atTop (nhds (c * 0)) := h1.const_mul c
  rw [mul_zero] at h2
  exact Filter.Tendsto.congr' hev.symm h2
THEOREM transcendental_e · IndisputableMonolith/Masses/MassGenesis/T10ExpTranscendental.lean
transcendental_e · IndisputableMonolith/Masses/MassGenesis/T10ExpTranscendental.lean:181 
/-- Hermite's theorem: `e` is transcendental over ℚ. -/
theorem transcendental_e : Transcendental ℚ (Real.exp 1) := by
  intro h_alg
  obtain ⟨f, hf_ne, hf_eval0_ne, hf_aeval⟩ := exists_int_poly_rel h_alg
  classical
  set n := f.natDegree with hn
  -- The degree is positive: a constant relation would contradict `f.eval 0 ≠ 0`.
  have hn1 : 1 ≤ n := by
    by_contra hlt
    push_neg at hlt
    have hn0 : f.natDegree = 0 := by
      rw [← hn]
      exact Nat.lt_one_iff.mp hlt
    have hC : f = C (f.coeff 0) := Polynomial.eq_C_of_natDegree_eq_zero hn0
    rw [hC, aeval_C] at hf_aeval
    apply hf_eval0_ne
    rw [← coeff_zero_eq_eval_zero]
    have h1 : ((f.coeff 0 : ℤ) : ℝ) = 0 := by
      rw [← eq_intCast (algebraMap ℤ ℝ)]
      exact hf_aeval
    exact_mod_cast h1
  -- The root polynomial `G = ∏_{k=1}^n (X - k)`.
  set G : ℤ[X] := ∏ k ∈ Finset.Icc 1 n, (X - C (k : ℤ)) with hG
  have hG_eval0 : G.eval 0 = (-1 : ℤ) ^ n * (n ! : ℤ) := prod_Icc_one_sub_C_eval_zero n
  have hG0 : G.eval 0 ≠ 0 := by
    rw [hG_eval0]
    refine mul_ne_zero (pow_ne_zero _ (by norm_num)) ?_
    exact_mod_cast Nat.factorial_ne_zero n
  have hG_natAbs : (G.eval 0).natAbs = n ! := by
    rw [hG_eval0, Int.natAbs_mul, Int.natAbs_pow, Int.natAbs_neg, Int.natAbs_one,
      one_pow, one_mul, Int.natAbs_natCast]
  -- The analytic engine.
  obtain ⟨c, hc⟩ := LindemannWeierstrass.exp_polynomial_approx G hG0
  -- The coefficient bound.
  set C0 : ℝ := ∑ k ∈ Finset.Icc 1 n, |(f.coeff k : ℝ)| with hC0
  -- Eventual smallness.
  have hsmall : Filter.Tendsto (fun m : ℕ => C0 * (c ^ m / ((m - 1)! : ℝ)))
      Filter.atTop (nhds 0) := by
    have h1 := tendsto_pow_div_factorial_pred c
    simpa using h1.const_mul C0
  obtain ⟨N, hN⟩ := Filter.eventually_atTop.mp
    (hsmall.eventually_lt_const (by norm_num : (0 : ℝ) < 1))
  -- A sufficiently large prime.
  obtain ⟨pp, hpp_ge, hpp_prime⟩ :=
    Nat.exists_infinite_primes (max N (max n ! (f.eval 0).natAbs) + 1)
  have hppN : N ≤ pp := le_trans (le_max_left _ _) (le_trans (Nat.le_succ _) hpp_ge)
  have hpp_gt_G : (G.eval 0).natAbs < pp := by
    rw [hG_natAbs]
    exact lt_of_le_of_lt
      (le_trans (le_max_left _ _) (le_max_right _ _)) (Nat.lt_of_succ_le hpp_ge)
  have hpp_gt_f : (f.eval 0).natAbs < pp :=
    lt_of_le_of_lt
      (le_trans (le_max_right _ _) (le_max_right _ _)) (Nat.lt_of_succ_le hpp_ge)
  have hppNat : pp.Prime := hpp_prime
  obtain ⟨npp, hndvd, gp, _hdeg, happrox⟩ := hc pp hpp_gt_G hppNat
  -- The integer `M`.
  set M : ℤ := npp * f.eval 0 + pp * ∑ k ∈ Finset.Icc 1 n, (f.coeff k) * gp.eval (k : ℤ)
    with hM
  -- `p ∤ M`.
  have hp_not_dvd_f0 : ¬ (pp : ℤ) ∣ f.eval 0 := by
    intro hdvd
    have h1 : pp ∣ (f.eval 0).natAbs := by
      have h2 := Int.natAbs_dvd_natAbs.mpr hdvd
      rwa [Int.natAbs_natCast] at h2
    have h3 := Nat.le_of_dvd (Int.natAbs_pos.mpr hf_eval0_ne) h1
    exact (not_le_of_gt hpp_gt_f) h3
  have hp_not_dvd_M : ¬ (pp : ℤ) ∣ M := by
    intro hdvd
    have hsub : (pp : ℤ) ∣ npp * f.eval 0 := by
      have h1 : (pp : ℤ) ∣ pp * ∑ k ∈ Finset.Icc 1 n, (f.coeff k) * gp.eval (k : ℤ) :=
        dvd_mul_right _ _
      have h2 := dvd_sub hdvd h1
      rwa [hM, add_sub_cancel_right] at h2
    have hnat : pp ∣ npp.natAbs * (f.eval 0).natAbs := by
      have h3 : ((pp : ℤ)).natAbs ∣ (npp * f.eval 0).natAbs :=
        Int.natAbs_dvd_natAbs.mpr hsub
      rwa [Int.natAbs_natCast, Int.natAbs_mul] at h3
    rcases (Nat.Prime.dvd_mul hppNat).mp hnat with hd | hd
    · have h3 : (pp : ℤ) ∣ npp := by
        have h4 : ((pp : ℤ)).natAbs ∣ npp.natAbs := by
          rwa [Int.natAbs_natCast]
        exact Int.natAbs_dvd_natAbs.mp h4
      exact hndvd h3
    · have h3 : (pp : ℤ) ∣ f.eval 0 := by
        have h4 : ((pp : ℤ)).natAbs ∣ (f.eval 0).natAbs := by
          rwa [Int.natAbs_natCast]
        exact Int.natAbs_dvd_natAbs.mp h4
      exact hp_not_dvd_f0 h3
  have hM_ne : M ≠ 0 := fun h0 => hp_not_dvd_M (h0.symm ▸ dvd_zero _)
  have hM_one : (1 : ℝ) ≤ ‖(M : ℂ)‖ := by
    rw [Complex.norm_intCast, ← Int.cast_abs]
    exact_mod_cast Int.one_le_abs hM_ne
  -- The master relation in ℂ.
  have hrel : ∑ i ∈ Finset.range (n + 1), ((f.coeff i : ℤ) : ℂ) * eC ^ i = 0 := by
    have hstep : aeval eC f = 0 := by
      have hR : aeval (Real.exp 1) f = 0 := hf_aeval
      have hh : algebraMap ℝ ℂ (aeval (Real.exp 1) f) =
          aeval (algebraMap ℝ ℂ (Real.exp 1)) (f.map (algebraMap ℤ ℝ)) := by
        refine Polynomial.map_aeval_eq_aeval_map ?hcomm f (Real.exp 1)
        case hcomm => rfl
      rw [hR, map_zero] at hh
      rw [Polynomial.aeval_def, Polynomial.eval₂_map,
        ← IsScalarTower.algebraMap_eq ℤ ℝ ℂ, ← Polynomial.aeval_def] at hh
      exact hh.symm
    rw [Polynomial.aeval_eq_sum_range, ← hn] at hstep
    exact (Finset.sum_congr rfl fun i _ => by rw [zsmul_eq_mul]).trans hstep
  -- The complex representation of `M`.
  have hsplit : ∑ i ∈ Finset.range (n + 1), ((f.coeff i : ℤ) : ℂ) * eC ^ i =
      ((f.eval 0 : ℤ) : ℂ) +
        ∑ k ∈ Finset.Icc 1 n, ((f.coeff k : ℤ) : ℂ) * eC ^ k := by
    rw [← coeff_zero_eq_eval_zero]
    have hrw : Finset.range (n + 1) = insert 0 (Finset.Icc 1 n) := by
      ext i
      simp [Finset.mem_range, Finset.mem_Icc]
      omega
    rw [hrw, Finset.sum_insert (by simp)]
    simp
  -- `M` as a cast to ℂ.
  have hM_cast : ((M : ℤ) : ℂ) =
      (npp : ℂ) * ((f.eval 0 : ℤ) : ℂ) +
        (pp : ℂ) *
          ∑ k ∈ Finset.Icc 1 n, ((f.coeff k : ℤ) : ℂ) * ((gp.eval (k : ℤ) : ℤ) : ℂ) := by
    rw [hM]
    push_cast [map_sum]
    rfl
  have hM_repr : ((M : ℤ) : ℂ) =
      -∑ k ∈ Finset.Icc 1 n, ((f.coeff k : ℤ) : ℂ) *
        (npp • Complex.exp (k : ℂ) - pp • aeval (k : ℂ) gp) := by
    have hf0 : ((f.eval 0 : ℤ) : ℂ) =
        -∑ k ∈ Finset.Icc 1 n, ((f.coeff k : ℤ) : ℂ) * eC ^ k := by
      have h0 : ((f.eval 0 : ℤ) : ℂ) +
          ∑ k ∈ Finset.Icc 1 n, ((f.coeff k : ℤ) : ℂ) * eC ^ k = 0 := hsplit ▸ hrel
      exact eq_neg_of_add_eq_zero_left h0
    rw [hM_cast, hf0, mul_neg, Finset.mul_sum, Finset.mul_sum,
      ← Finset.sum_neg_distrib, ← Finset.sum_add_distrib, ← Finset.sum_neg_distrib]
    apply Finset.sum_congr rfl
    intro k hk
    rw [complexExp_natCast_eq_eC_pow k, aeval_int_natCast gp k]
    push_cast [nsmul_eq_mul, zsmul_eq_mul]
    ring
  -- The upper bound.
  have hupper : ‖((M : ℤ) : ℂ)‖ ≤ C0 * (c ^ pp / ((pp - 1)! : ℝ)) := by
    rw [hM_repr, norm_neg]
    refine (norm_sum_le _ _).trans ?_
    rw [hC0, Finset.sum_mul]
    apply Finset.sum_le_sum
    intro k hk
    rw [norm_mul, Complex.norm_intCast]
    exact mul_le_mul_of_nonneg_left
      (happrox (natCast_mem_aroots_prod_Icc n k hk)) (abs_nonneg _)
  -- The contradiction.
  have hlt : C0 * (c ^ pp / ((pp - 1)! : ℝ)) < 1 := hN pp hppN
  have : (1 : ℝ) < 1 := lt_of_le_of_lt hM_one (lt_of_le_of_lt hupper hlt)
  exact lt_irrefl 1 this

What this page does not claim

The lemma does not state that e is transcendental. It does not claim any specific rate of convergence for the ratio. It does not assert anything about the physical mass spectrum.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Masses/MassGenesis/T10ExpTranscendental.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND