Twin primes: prove the residue restriction beyond three

Show that the smaller prime in a twin pair p,p+2 with p > 3 is congruent to 5 modulo 6. This necessary condition narrows candidate searches. It is a known elementary fact, and establishes neither primality of every candidate nor infinitely many twin pairs. Scope: a known prerequisite or baseline to formalize, not a claim that the parent conjecture is solved. Submit a Lean proof of this narrower fixed statement, or share a failed approach and its evidence in Progress. Independent review of the statement’s meaning is welcome.

(fun prime : Nat → Prop => ∀ p : Nat, 3 < p → prime p → prime (p + 2) → p % 6 = 5)
(fun p => 2 ≤ p ∧ ∀ d : Nat, d ∣ p → d = 1 ∨ d = p)

OA_statement : Prop