Encyclopedia Masses Masses Mass Genesis T10 Exp Transcendental

ARTICLE 3 claims 2 theorems 1 measured

Masses Mass Genesis T10 Exp Transcendental

A machine-checked proof that Euler's number e is transcendental, a fact that anchors a key boundary in the framework's account of particle masses.

Verify this page

The transcendental wall

Euler's number e, approximately 2.71828, is the base of natural logarithms and the limit of (1 + 1/n)^n as n grows. A transcendental number is one that is not the root of any polynomial with integer coefficients; π and e are the famous examples, while √2, being a root of x² − 2, is merely irrational. Charles Hermite proved in 1873 that e is transcendental, settling a question that had resisted earlier mathematicians including Euler and Liouville.

The proof runs by contradiction. Suppose e were algebraic, meaning it satisfied some integer polynomial equation. Hermite constructed a specific integer combination M_p, depending on a prime p, that is forced to be both a nonzero integer and, for large enough p, smaller than 1 in absolute value. The contradiction shows no such polynomial can exist. A key ingredient is the approximation of powers of e by rational numbers with error that shrinks faster than any factorial grows.

In Recognition Science, this classical result becomes a load-bearing wall. The framework models physical reality as a discrete ledger of recognition events, where recognition is the act of matching an input against a stored pattern. The framework's account of particle masses, called mass genesis, requires a clean split between algebraic and transcendental numbers to define a boundary in its settlement cone, a geometric region of possible mass values. The module T10ExpTranscendental closes exactly this gap.

The module contains a machine-checked proof of the theorem transcendental_e: the real number e is transcendental over the rationals. The proof follows Hermite's 1873 argument as presented in Jacobson's Basic Algebra I, formalized in the framework's library of formal theorems. The library verifies every step with no gaps and no added axioms, making the algebraic/transcendental split a proved theorem rather than an assumption.

What this establishes in plain language: the framework does not merely assume that e sits on the transcendental side of a dividing line. It proves that fact from first principles, using only the standard axioms of logic. That proof then supports the mass-genesis construction, which uses the split to define which mass values are allowed. The result is that a classical theorem from 1873, long known to mathematicians, becomes a verified pillar in a physical theory of particle masses.

MEASURED 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
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
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 page does not claim that the framework derives the numerical value of any particle mass. This page does not claim that the transcendence of e is a new mathematical result. This page does not claim that the settlement cone's boundary is physically observable.

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