Paper 176 v0.1 - Fermat Numbers F_5-F_11: Empirical v_2(omega_{F_n}(3)) Measurement + Lean 4 Axiom-Free F_9 Excess Witness (Rei-AIOS)
v0.1 (2026-07-30) first formal Paper 176 publication. Empirical measurement of v_2(omega_{F_n}(3)) for n = 5..11 with excess above Lucas 1878 lower bound n+2. Excess sequence 0,0,0,1,5,0,0 is highly irregular. F_9 excess=5 driven by small factor 2424833 = 37 * 2^16 + 1 whose v_2(p-1) = 16 (max of three factors). Characterization excess = v_2(k) where p_max = k * 2^(n+2) + 1 matches 7/7 in range n = 5..11 when driving factor satisfies v_2(ord_p(3)) = v_2(p-1). Lean 4 axiom-free F_9 divisibility witness: 2424833 divides F_9 = 2^512+1 via Pratt-style iterative squaring sqIterMod k = 2^(2^k) mod 2424833, kernel-verified sqIterMod 9 = 2424832 ≡ -1 mod 2424833. This §7 replaces external Selfridge-Hurwitz 1963 attribution with Lean-internal kernel-verified computation; native_decide NOT used = Lean.ofReduceBool axiom NOT added. 44 axiom-free theorems combined (26 FermatNineExcessWitness + 18 ZcsgMdnstModularBoundary STEP 1306). Zero sorry, zero native_decide, zero user axioms. Refutes §7 hypothesis 'n-monotonic function predicts excess' at n=9 (excess=5 while n=10,11 return to excess=0). Honest positioning (6 non-claims): (1) No world-first — Lucas 1878 + Selfridge-Hurwitz 1963 + Euler/Landry/Morrison/Brent-Pollard/Lenstra/Brent factor discoveries prior art; Rei differentiator = specific n=5..11 empirical table + Lean 4 axiom-free F_9 witness (Pratt-style replacement) + 7/7 characterization within bounded range. (2) No claim Fermat compositeness resolved. (3) No claim excess unbounded — 7/7 in n=5..11 does not imply anything about n → ∞. (4) No claim ZCSG/MDNST containers refuted (only specific §7 monotonic hypothesis refuted). (5) No claim SELF-loop = multiplicative order (chat-Claude 2026-07-20 syntactic resemblance noted but formal identity explicitly rejected per evaluation symmetry principle). (6) No claim Pratt-style Lean 4 proof scales beyond small kernel arithmetic (F_n n ≥ 12 not asserted). Zenodo v0.1 DOI 10.5281/zenodo.21694136. Three-party co-authorship per OUKC charter v1.0.
