Encyclopedia Masses Masses Mass Genesis T10 Exp Transcendental Nat Cast Mem Aroots Prod Icc

ARTICLE 2 claims 2 theorems

Masses Mass Genesis T10 Exp Transcendental Nat Cast Mem Aroots Prod Icc

A small lemma about polynomial roots that becomes the final step in proving the number e is transcendental.

Verify this page

A root among the integers

In the classical theory of polynomials, a root of a polynomial is a number that makes the polynomial equal zero. The declaration natCast_mem_aroots_prod_Icc establishes a specific instance of this idea. It says that for any natural number n, and for any k between 1 and n inclusive, the complex number k is a root of the polynomial that is the product of (X - j) for all j from 1 to n. In plainer terms, if you build a polynomial by multiplying together factors that each vanish at one of the integers 1 through n, then every one of those integers is indeed a root of the resulting product.

This fact is not deep on its own. It is a routine consequence of the definition of a root and the behavior of products. The declaration's role in the framework is as a supporting lemma, not a headline result. It appears inside a machine-checked proof of a much larger theorem: that the number e, the base of natural logarithms, is transcendental over the rational numbers. Transcendental means that e is not the root of any nonzero polynomial with integer coefficients. This was first proved by Charles Hermite in 1873, and the framework's library reproduces that proof in a form verified by a computer.

In Recognition Science, this lemma serves a specific structural purpose. The framework models physical mass values as lying on a ladder of powers of the golden ratio. The transcendence of e is needed to establish a clean split between algebraic and transcendental numbers in the settlement cone, a discrete record of allowed recognition events. The lemma about roots of products of linear factors is one of the mechanical steps that make the larger proof go through. It does not by itself say anything about physics, mass, or the golden ratio.

What the declaration does not claim is equally important. It does not assert that the polynomial has no other roots, nor that the roots are simple. It does not say anything about the values of the polynomial at other points. It does not establish that e is transcendental; that is the job of the theorem transcendental_e, which uses this lemma as one ingredient. The lemma is a small, precise statement about a specific polynomial construction, and its value lies entirely in supporting the larger result.

THEOREM natCast_mem_aroots_prod_Icc · IndisputableMonolith/Masses/MassGenesis/T10ExpTranscendental.lean
natCast_mem_aroots_prod_Icc · IndisputableMonolith/Masses/MassGenesis/T10ExpTranscendental.lean:145 
/-- Every `k ∈ {1, …, n}` is a complex root of `∏_{j=1}^n (X - j)`. -/
private theorem natCast_mem_aroots_prod_Icc (n : ℕ) (k : ℕ) (hk : k ∈ Finset.Icc 1 n) :
    ((k : ℂ)) ∈ (∏ j ∈ Finset.Icc 1 n, (X - C (j : ℤ))).aroots ℂ := by
  rw [Polynomial.mem_aroots']
  constructor
  · rw [Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective ℤ ℂ)]
    apply Finset.prod_ne_zero_iff.mpr
    intro j _
    exact Polynomial.X_sub_C_ne_zero (j : ℤ)
  · rw [map_prod]
    apply Finset.prod_eq_zero hk
    rw [map_sub, aeval_X, aeval_C, map_natCast, sub_self]
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 by itself establish the transcendence of e. The lemma does not describe any physical property of mass or the golden ratio. The lemma does not claim the constructed polynomial has no other roots.

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