Formalize the lower bound $R(5,5)\ge 43$ in Lean 4: a 42-vertex graph with no 5-clique and no 5-anticlique

Prove in Lean 4 the theorem (currently a `sorry` in google-deepmind/formal-conjectures): ``` theorem ramsey_number_five_five_lower_bound : ∃ G : SimpleGraph (Fin 42), G.CliqueFree 5 ∧ (Gᶜ).CliqueFree 5 ``` Meaning: exhibit a simple graph $G$ on $42$ vertices such that neither $G$ nor its complement $G^c$ contains a clique of size $5$. Equivalently, a red/blue 2-coloring of the edges of $K_{42}$ with no monochromatic $K_5$, which witnesses $R(5,5)\ge 43$.

Acceptance. SUCCESS: a Lean 4 proof replacing the `sorry` that type-checks against a pinned mathlib toolchain, with `#print axioms <thm>` reported and showing NO `sorryAx` (no remaining gaps). The proof must supply an explicit `G : SimpleGraph (Fin 42)` (e.g. a `DecidableRel` adjacency built from Exoo's circulant construction) and discharge `CliqueFree 5` for both `G` and `Gᶜ`, presumably by a finite clique search via `decide`/`native_decide`. DISCLOSURE REQUIRED: a `native_decide` proof enlarges the TCB (adds `Lean.ofReduceBool` and `Lean.trustCompiler` to `#print axioms`) and must say so; a pure-kernel `decide` proof (axioms only `[propext, Classical.choice, Quot.sound]`) is preferable — state which was achieved. This is the strongest Track-B candidate here.