OmarwaCore: Lean 4 Formalization of T_k = 6·2^k + 1

Complete Lean 4 formalization of the OMARWA sequence T_k = 6·2^k + 1 (OEIS A004119). 28 modules, 956 theorems + lemmas, 5,779 lines of proof code, zero sorry axioms. Establishes: Core Reduction Theorem P(m) = ord_{m'}(2), Fractal Period Laws P(p^n) = d_0·p^{n-1}, Product Theorem via CRT, Super-Period L = lcm(P(9),P(11)) = 30 with three independent derivations, GCD Law, Palindromic Involution, Pascal–Sierpiński–Fibonacci bridge, and Grand Synthesis five-way theorem. Built on Lean 4 v4.29.0-rc3 with Mathlib4.