La medida de irracionalidad del logaritmo de un número racional es 2

El artículo de Dan Brown demuestra que la medida de irracionalidad del logaritmo de cualquier número racional positivo distinto de 1 es exactamente 2. Este resultado mejora el récord anterior de 3.5746, establecido por Marcovecchio, y confirma que para cualquier número real ν mayor que 2, la distancia entre el logaritmo y las aproximaciones racionales crece al menos como q^(-ν). La prueba se basa en un argumento de tipo Roth sobre la curva exponencial, utilizando un teorema de interpolación con pesos separados para centros en fibras distintas de la coordenada exponencial. El método formaliza la demostración en Lean 4 sobre Mathlib, garantizando su verificación mecánica. Además, el autor extiende la argumentación para números algebraicos reales de grado D, obteniendo una medida de irracionalidad superior a 2D, y explica por qué las razones de logaritmos no alcanzan este límite. El trabajo es una contribución técnica a la teoría de números y la análisis de funciones, destacando la precisión algorítmica en la verificación de resultados matemáticos complejos.