Conjectura de MariltonCR dos Primos Encaixados

🇬🇧 English (EN) Primos Encaixados — nine blocks after m^2 (m\ge 10^6): one m-rough per block. This record provides the preprint and supporting materials for the RoughBlocks project. We prove that, for every m\ge 10^6 and each x\in\{0,\dots,8\}, the block K_x=\{m^2+xm+1,\dots,m^2+(x+1)m\} contains at least one m-rough integer (P^-(n)>m). The argument combines Buchstab’s identity/function \omega with an explicit Mertens formula (via Abel summation), yielding a uniform local lemma on short intervals [X,X+Y] with effective constants C_0\le 2, C_1\le 4.4, C_2=100. The range 2\le m<10^6 is covered by a reproducible deterministic sweep; together, both parts settle the statement for all m\ge 2. Formalization (Lean 4). The core result is formalized in rough-blocks-lean (Lake/Mathlib). The Light layer axiom audit shows only system axioms plus a single explicit contract for the computational sweep. See the repository for reproduction (Lake build and scripts/audit.sh). Resources. Preprint (LaTeX/PDF) and technical notes. Lean 4 source (repository): github.com/mariltondev/rough-blocks-lean. Reproducible sweep artifact: DOI 10.5281/zenodo.17137291. Keywords. Buchstab; rough numbers; sieve methods; explicit Mertens; short intervals; formal verification (Lean 4). 🇧🇷 Português (PT-BR) Primos Encaixados — nove blocos após m^2 (m\ge 10^6): um m-áspero por bloco. Este registro disponibiliza o preprint e materiais de apoio do projeto RoughBlocks. Mostramos que, para todo m\ge 10^6 e cada x\in\{0,\dots,8\}, o bloco K_x=\{m^2+xm+1,\dots,m^2+(x+1)m\} contém ao menos um inteiro m-áspero (P^-(n)>m). A prova combina a identidade/função de Buchstab \omega com Mertens explícito (via Abel), resultando em um lema local uniforme em janelas curtas [X,X+Y] com constantes efetivas C_0\le 2, C_1\le 4{,}4, C_2=100. A faixa 2\le m<10^6 é coberta por uma varredura determinística reprodutível; juntas, as duas partes fecham o enunciado para m\ge 2. Formalização (Lean 4). O núcleo do resultado está formalizado em rough-blocks-lean (Lake/Mathlib). A auditoria de axiomas na camada Light aponta apenas axiomas de sistema, e um contrato explícito para a faixa computacional. Veja o repositório para instruções de reprodução (build com lake e script scripts/audit.sh). Recursos. Preprint (LaTeX/PDF) e notas técnicas. Código-fonte Lean 4 (repositório): github.com/mariltondev/rough-blocks-lean. Artefato de varredura (reprodutível): DOI 10.5281/zenodo.17137291. Palavras-chave. Buchstab; números ásperos (rough); crivo; Mertens explícito; intervalos curtos; verificação formal (Lean 4). 🇪🇸 Español (ES) Primos Encaixados — nueve bloques tras m^2 (m\ge 10^6): un m-áspero por bloque. Este registro reúne el preprint y materiales de apoyo del proyecto RoughBlocks. Demostramos que, para todo m\ge 10^6 y cada x\in\{0,\dots,8\}, el bloque K_x=\{m^2+xm+1,\dots,m^2+(x+1)m\} contiene al menos un entero m-áspero (P^-(n)>m). La prueba combina la identidad/función de Buchstab \omega con una versión explícita de Mertens (vía suma de Abel), obteniendo un lema local uniforme en intervalos cortos [X,X+Y] con constantes efectivas C_0\le 2, C_1\le 4{,}4, C_2=100. El rango 2\le m<10^6 se cubre con un barrido determinista reproducible; en conjunto, ambas partes establecen el enunciado para m\ge 2. Formalización (Lean 4). El resultado central está formalizado en rough-blocks-lean (Lake/Mathlib). La auditoría de axiomas en la capa Light muestra sólo axiomas del sistema y un contrato explícito para el tramo computacional. Consulte el repositorio para reproducibilidad (compilación con Lake y scripts/audit.sh). Recursos. Preprint (LaTeX/PDF) y notas técnicas. Código Lean 4 (repositorio): github.com/mariltondev/rough-blocks-lean. Artefacto reproducible del barrido: DOI 10.5281/zenodo.17137291. Palabras clave. Buchstab; números ásperos (rough); métodos de criba; Mertens explícito; intervalos cortos; verificación formal (Lean 4).