Encyclopedia Masses Masses Mass Genesis T10 Exp Transcendental Complex Exp Nat Cast Eq E C Pow

ARTICLE 2 claims 2 theorems

Masses Mass Genesis T10 Exp Transcendental Complex Exp Nat Cast Eq E C Pow

A small formal lemma connects the complex exponential at whole numbers to powers of e, a step toward proving e is transcendental.

Verify this page

A bridge for the exponential

The exponential function is one of the most important functions in mathematics. For any complex number z, the exponential exp(z) is defined by the infinite series 1 + z + z²/2! + z³/3! + ..., which converges for every z. A fundamental property is that exp(z+w) = exp(z)exp(w), and in particular exp(n) = eⁿ for any natural number n, where e = exp(1) ≈ 2.71828. This identity is so basic that it is often taken for granted, but in a formal proof system, every such step must be derived from definitions.

The declaration complexExp_natCast_eq_eC_pow is a machine-checked theorem in the framework's library of formal mathematics. It states precisely that for any natural number k, the complex exponential of k equals e raised to the k-th power. Here eC is the complex number corresponding to the real number e. The proof is short: it uses the fact that the complex exponential of a sum is the product of exponentials, and applies this k times. This is not a new mathematical discovery; it is a formal verification of a standard identity.

The theorem matters because it is a bridge between two ways of writing the same thing. In the proof of Hermite's theorem, which shows that e is transcendental (not a root of any polynomial with integer coefficients), the argument needs to manipulate expressions like e^k. This lemma allows the proof to replace those expressions with powers of eC, making the algebraic structure explicit. Without this bridge, the proof would have to handle the exponential function directly at every step, which is more cumbersome.

In Recognition Science, this lemma is part of the T10 settlement-cone wall, a step toward establishing the algebraic/transcendental split that the framework's mass-genesis story requires. The framework models particle masses on a ladder of powers of the golden ratio, and the transcendence of e is a technical ingredient in that larger argument. The lemma itself is a small, fully verified piece of that machinery.

What this declaration does not claim is important to state plainly. It does not prove that e is transcendental; that is a separate theorem, transcendental_e, which is also in the library. It does not say anything about the golden ratio, particle masses, or any physical quantity. It is purely a statement about the complex exponential and natural numbers. It also does not claim that the exponential function is defined by this property; the series definition is the starting point, and this identity is a consequence.

THEOREM complexExp_natCast_eq_eC_pow · IndisputableMonolith/Masses/MassGenesis/T10ExpTranscendental.lean
complexExp_natCast_eq_eC_pow · IndisputableMonolith/Masses/MassGenesis/T10ExpTranscendental.lean:57 
/-- `Complex.exp` at a natural index is a power of the complex `e`. -/
private theorem complexExp_natCast_eq_eC_pow (k : ℕ) :
    Complex.exp (k : ℂ) = eC ^ k := by
  have h1 : ((k : ℂ)) = k • (1 : ℂ) := by simp [nsmul_eq_mul]
  rw [h1, Complex.exp_nsmul]
  congr 1
  rw [show (1 : ℂ) = ((1 : ℝ) : ℂ) from (map_one (algebraMap ℝ ℂ)).symm]
  exact (Complex.ofReal_exp 1).symm
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

This declaration does not prove that e is transcendental, which is a separate theorem. It does not state anything about the golden ratio or particle masses. It does not define the exponential function; it derives a property from the series definition.

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