twenty6390_factorization
plain-language theorem explainer
26390 factors as 2 × 5 × 7 × 13 × 29. Analysts of Ramanujan's 1/π series cite the result when confirming the numerator coefficient in the term (1103 + 26390n). The proof reduces the equality to a direct numerical check.
Claim. $26390 = 2 × 5 × 7 × 13 × 29$
background
The module examines Ramanujan's 1914 series 1/π = (2√2/9801) Σ (4n)!(1103 + 26390n) / ((n!)^4 396^{4n}), which converges at roughly eight digits per term. RS interprets the denominators via the passive edge integer 11: 396 = 2² × 3² × 11 and 9801 = (9 × 11)². The integer 26390 appears only in the numerator and is shown here to carry none of the RS topological factors.
proof idea
The proof is a one-line wrapper that applies norm_num to the natural-number equality.
why it matters
The result supplies a verified coefficient for the Ramanujan series inside the RS framework, where π arises from the eight-tick octave and recognition-circle geometry. It sits alongside sibling factorizations of 396 and 9801 that isolate the factor 11. No downstream theorems yet invoke it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.