ErdosProblems/1175: `variants.shelah_consistency` asserts the counterexample outright, not its consistency

`Erdos1175.erdos_1175.variants.shelah_consistency` asks, via `answer(sorry) ↔ ...`, whether an ℵ₁-chromatic graph all of whose triangle-free subgraphs have chromatic number below ℵ₁ exists in the ambient universe, whereas Shelah's result states only that the existence of such a graph is consistent with ZFC.

https://tadamcz.com/fc-review-results/c90271f0fa/#/f/ErdosProblems/1175

- 1 misformalization
- 2 minor
- trivial proof: bailed out
- fix compiles

_{Found by a language-model audit of the repository at c90271f0fa. Not reviewed by a human. This issue's title and description were written by a language model as well.}

Start at Erdos1175.erdos_1175.variants.shelah_consistency and read the linked review to compare the formal statement with Shelah's consistency result. Adjust the assertion so it represents consistency rather than outright existence, then run the relevant Lean checks; done means the corrected declaration compiles.

Written by the indexing model from the issue text.