Experiment: encode the five-vertex Erdős 23 case

[DomTheDeveloper]

Current finding

The direct decide +kernel attempt does not elaborate because Lean cannot synthesize reducible Decidable instances for the quantified SimpleGraph propositions:

Decidable (∀ G : SimpleGraph (Fin 5), ...)
Decidable (∃ G : SimpleGraph (Fin 5), ...)

Focused run 30212114859 reached the exact module and failed on those two instance-synthesis errors. No theorem from this PR is green, and the failed declarations expose sorryAx; they must not be used.

Next proof architecture

A valid kernel proof needs an explicit finite encoding of the ten possible edges, together with:

• decoding from edge bit-vectors to simple graphs;
• a verified triangle-free test;
• a verified bipartite-subgraph/deletion certificate;
• exhaustive kernel checking over the encoded finite space;
• a bridge back to the canonical SimpleGraph (Fin 5) statements.

This remains a draft experiment and is not queued for GDM promotion.

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.