A comprehensive number-theoretic study of the integer sequence Tₖ = 6*2ᵏ + 1 (OEIS A004119). All 28 modules of the OmarwaCore Lean 4 formalization are covered: Core Reduction Theorem P (m) = ord (2, m/gcd (m, 6) ), Fractal Period Laws P (pⁿ) = d₀ * p^ (n-1), Product Theorem via CRT, Super-Period L = 30 with three independent derivations, GCD Law, Palindromic Involution, Pascal-Sierpinski-Fibonacci bridge, and Grand Synthesis five-way theorem. 956 theorems, 0 sorry axioms. 13 pages.
Omer Cetintas (Sun,) studied this question.