Encyclopedia Masses Masses Mass Genesis T10 Exp Transcendental Prod Icc One Sub C Eval Zero

ARTICLE 2 claims 2 theorems

Masses Mass Genesis T10 Exp Transcendental Prod Icc One Sub C Eval Zero

One line in a chain of reasoning about the number e, and what it does and does not say on its own.

Verify this page

A small lemma in a large proof

The declaration prod_Icc_one_sub_C_eval_zero is a small, precise fact about polynomials. It says that if you take the product of the factors (X - 1), (X - 2), ..., (X - n), and then evaluate that whole product at X = 0, the result is (-1)^n times n factorial. In plainer terms: multiply those n linear factors together, plug in zero, and the answer is the product of the first n integers, with a sign that alternates depending on whether n is even or odd.

This is not a standalone discovery about the universe. It is a lemma, a supporting step inside a larger argument. The larger argument is a proof, in the framework's machine-checked library of formal theorems, that the number e (the base of natural logarithms, about 2.71828) is transcendental. A number is transcendental when it is not the root of any polynomial equation with integer coefficients. The fact that e is transcendental was first proved by Charles Hermite in 1873, and the framework's library reproduces that proof.

In Recognition Science, this proof serves a specific purpose. The framework derives particle masses from a chain of forced mathematical structures. That chain reaches a point where it needs to know that e is transcendental, not merely irrational or algebraic. The lemma about the product evaluated at zero is one of the mechanical ingredients: it helps control the size of a certain integer that appears in the contradiction argument used in Hermite's proof.

What the declaration does not claim is just as important. It does not, by itself, say anything about particle masses, about the golden ratio, or about any physical constant. It is not a statement about physics at all. It is a statement about integer polynomials and their values. Its role is entirely instrumental: it is a gear in a machine that eventually produces a theorem about e, and that theorem is what the mass derivation needs.

In the framework's own accounting, the lemma is tagged as part of a THEOREM: the transcendence of e. The tag means the whole chain, including this lemma, has been checked by a computer and contains no unproven assumptions beyond the standard logical axioms. The lemma itself is a proved fact about polynomials, and its proof is complete. The larger claim it supports, that e is transcendental, is also proved. What remains open is not the mathematics of e, but the physical bridge from that theorem to the mass spectrum, which the framework treats as a separate question.

THEOREM prod_Icc_one_sub_C_eval_zero · IndisputableMonolith/Masses/MassGenesis/T10ExpTranscendental.lean
prod_Icc_one_sub_C_eval_zero · IndisputableMonolith/Masses/MassGenesis/T10ExpTranscendental.lean:123 
/-- `∏_{k=1}^n (X - k)` evaluated at zero is `(-1)^n · n!`. -/
private theorem prod_Icc_one_sub_C_eval_zero (n : ℕ) :
    (∏ k ∈ Finset.Icc 1 n, (X - C (k : ℤ))).eval 0 = (-1 : ℤ) ^ n * (n ! : ℤ) := by
  have hfac : ∀ m : ℕ, (∏ k ∈ Finset.Icc 1 m, (k : ℤ)) = (m ! : ℤ) := by
    intro m
    induction m with
    | zero => simp
    | succ j ih =>
      rw [Finset.prod_Icc_succ_top (Nat.succ_le_succ (Nat.zero_le j)), ih,
        Nat.factorial_succ]
      push_cast
      ring
  rw [Polynomial.eval_prod]
  have hstep : ∀ k ∈ Finset.Icc 1 n, (X - C (k : ℤ)).eval 0 = -(k : ℤ) := by
    intro k _
    rw [Polynomial.eval_sub, Polynomial.eval_X, Polynomial.eval_C, zero_sub]
  rw [Finset.prod_congr rfl hstep]
  have hneg : ∀ k ∈ Finset.Icc 1 n, (-(k : ℤ)) = (-1) * (k : ℤ) := by
    intro k _; rw [neg_one_mul]
  rw [Finset.prod_congr rfl hneg, Finset.prod_mul_distrib, Finset.prod_const,
    Nat.card_Icc, Nat.add_sub_cancel, hfac n]
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 itself says nothing about particle masses or any physical constant. The proof of e's transcendence does not by itself derive any mass value. The declaration does not claim that e is irrational; that is a weaker statement already known before Hermite.

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