feat(Arxiv): update 2107.00295 Conjecture 1.6 status

[dawsonamf]

Conjecture 1.6 of Cho–Choi–Park (arxiv/2107.00295), formalized in this file as independentDominationEven and independentDominationOdd, has been proved in the literature.

Eun-Kyung Cho, Jinha Kim, Minki Kim and Sang-il Oum, Independent domination of graphs with bounded maximum degree, J. Combin. Theory Ser. B 158 (2023), 341–352 (arxiv/2202.09594, doi:10.1016/j.jctb.2022.10.004) prove, as Corollary 1.3: every graph $G$ with maximum degree at most $\Delta$ and no isolated vertices has an independent dominating set of size at most $\left(1 - \frac{\Delta}{\lfloor (\Delta+2)^2/4 \rfloor}\right)\lvert V(G)\rvert$. The paper states that this corollary "was conjectured by Cho, Choi, and Park".

Expanding the floor by parity: for even $\Delta = D$, $\lfloor (D+2)^2/4 \rfloor = (D+2)^2/4$, and the bound becomes $(D+2)^2 \cdot i(G) \le (D^2+4) \cdot n$; for odd $\Delta = D$, $\lfloor (D+2)^2/4 \rfloor = (D+1)(D+3)/4$, and it becomes $(D+1)(D+3) \cdot i(G) \le (D^2+3) \cdot n$ — exactly the two statements in this file.

This PR flips both tags to research solved and records the reference in the module and declaration docstrings, following the pattern of #4628. Proof bodies are left as sorry (no formalization of the proof is claimed).

[google-cla]

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

[dawsonamf]

CLA signed.

[mo271]

@guelmi94 could you review this? (Adding you because you originally added this conjecture..)