MATH, 10 PRIMO, 10 - Vol. 13: The Elimination Formula: From the Sieve of Eratosthenes to a Single Expression Executable by Hand - the Odd-Table Filters k = (d-1)/2 mod d with Activation Embedded at d^2, Four Laws Verified to 1e8 Item-by-Item, a Two-Tier Lean 4 Audit (Numeric Certificates Strictly Zero-Axiom; General Laws Reduced to propext/Quot.sound with No Classical.choice), and a Wheel-Native Deep-Prime Certificate 10,000,000,141 = 1 (mod 30) by a GCD-Gated Kernel Walk

Abstract

This volume executes the author's new directive: not a sweeping procedure over a grid, but a declarative theory of impossibility filters - start from the odd numbers n = 2k+1 (k >= 1) and define exactly what cannot be prime. Main result: each filter d (odd, d >= 3) eliminates exactly the rows k = (d-1)/2 (mod d) - one arithmetic progression per filter, no powers, no modular inverses - and the activation threshold d^2 is EMBEDDED in the progression (first eliminated row k = (d^2-1)/2, where n = d^2). All filters collapse into one self-contained line that never mentions primes: P = {2} union {2k+1 : k >= 1 and for every odd d >= 3 with d^2 <= 2k+1, 2k+1 = 0 (mod d) is impossible}. Four laws: POSITION (one progression per filter), ACTIVATION (embedded), REDUNDANCY (composite filters add nothing: the all-odd-filters elimination equals the primes-only elimination ITEM BY ITEM to 1e8), BOUNDARY (elimination never terminates; no periodic pattern completes it - Lean theorems eliminacao_infinita and fronteira_30_1). Numerical verification (double implementation, element-wise equality) to 1e8: both elimination forms, the wheel-30 eight-column form with the structural law a_p(r) = r*a_p(1) for every p <= 1e4, and the Euler-unified composite-filter form - all equal to the reference sieve (pi(1e8) = 5,761,455 external anchor; product rule 17,076 = 17,076; hand elimination to 1000 gives 167 + 2 = 168 = pi(1000)). Lean 4 audit (v4.33.1, no Mathlib) in two declared tiers: TIER 1 - all numeric certificates (24 block primalities, composites by witness, the author's filter instances, and the deep certificate p = 10,000,000,141 = 30*333,333,338 + 1 = 1 (mod 30), sqrt p = 100,000, 26,665 wheel candidates) are STRICTLY ZERO-AXIOM (#print axioms -> empty; gcd-gated kernel walk sliced into 96 + 100 blocks of 512 steps, constant memory; theorems p_roda_profundo, semSqW_range, semBlkW_range, primoW_range, profW_aux_A/B all 'does not depend on any axioms'; the same theorem links the series' golden number: 161,803,398,871 = 1 (mod 30) - golden_na_roda). TIER 2 - the general laws (filtro_pos, filtro_fileira, filtro_ativa, strike_inv_pos, filtro_fileira_W, eliminacao_infinita, fronteira_30_1, dvd_roda, roda_min, roda_completa, sobrevivente_impar, sobrevivente_roda30, teorema_geral_eliminacao) depend ONLY on propext and Quot.sound with NO Classical.choice: the theory is constructive; we state openly that the Lean core mod/div/dvd/gcd API carries propext (probed lemma by lemma) and register the full zero-axiom reduction as future work in the series' FATIAS style. Engineering record: sandbox reset (Lean reinstalled), monolithic 196-slice build OOM-killed at 4 GB and rebuilt in two sliced stages, Bool-gated walk mirroring the series' Bool discipline. Under the PRIMES-FRONTIER protocol (Rule 1, honesty): the elimination viewpoint is the sieve seen from the complement - classical (Eratosthenes/Legendre; 6k+/-1 is the famous organized case); the contributions are the exact one-line self-contained form, the Position Law with embedded activation, the row-level Redundancy Law, the Boundary formalization, and the wheel-native formal certificate chain. The hand method is included as the deliverable demanded: any person, a pencil, one page (FORMULA_ELIMINACAO.md). Complete sources, captured Lean outputs, the step-by-step reproduction guide and SHA256 manifest included.