Missing docstrings

The following theorems appear to have no docstrings (but probably should have):

```
WARNING: Theorem CongruentNumber.Tunnell_even_converse (category: research open) is missing a docstring
WARNING: Theorem CongruentNumber.Tunnell_even (category: research solved) is missing a docstring
WARNING: Theorem CongruentNumber.Tunnell_odd (category: research solved) is missing a docstring
WARNING: Theorem CongruentNumber.Tunnell_odd_converse (category: research open) is missing a docstring
WARNING: Theorem HerzogSchonheimConjecture.herzog_schonheim_conjecture (category: research open) is missing a docstring
WARNING: Theorem EllipticCurveRank.WeierstrassCurve.twentynine_le_rank_elkiesKlagsbrun29 (category: research solved) is missing a docstring
WARNING: Theorem EllipticCurveRank.WeierstrassCurve.rank_elkiesKlagsbrun29 (category: research open) is missing a docstring
WARNING: Theorem EllipticCurveRank.WeierstrassCurve.twentyeight_le_rank_elkies28 (category: research solved) is missing a docstring
WARNING: Theorem EllipticCurveRank.WeierstrassCurve.rank_elkies28 (category: research open) is missing a docstring
WARNING: Theorem RegularPrimes.small_regular_primes (category: undergraduate) is missing a docstring
WARNING: Theorem RegularPrimes.not_isRegularPrime_37_first (category: undergraduate) is missing a docstring
WARNING: Theorem RegularPrimes.not_isRegularPrime_37_second (category: undergraduate) is missing a docstring
WARNING: Theorem MovingSofa.GerversSofa.ABφθSpec.existsUnique (category: undergraduate) is missing a docstring
WARNING: Theorem EulerSumOfPowers.eulers_sum_of_powers_conjecture.false_for_k4 (category: research solved) is missing a docstring
WARNING: Theorem EulerSumOfPowers.eulers_sum_of_powers_conjecture.false_for_k5 (category: research solved) is missing a docstring
WARNING: Theorem ModularityConjecture.modularity_conjecture (category: research solved) is missing a docstring
WARNING: Theorem RamanujanTau.ramanujan_petersson (category: research solved) is missing a docstring
WARNING: Theorem RamanujanTau.lehmer_ramanujan_tau (category: research open) is missing a docstring
WARNING: Theorem Singmaster.singmaster (category: research open) is missing a docstring
WARNING: Theorem Conway99Graph.completeGraph_cliqueSet (category: undergraduate) is missing a docstring
WARNING: Theorem Conway99Graph.completeGraphIsClique (category: undergraduate) is missing a docstring
WARNING: Theorem DedekindNumber.exists_minimal_true_subset (category: graduate) is missing a docstring
WARNING: Theorem DedekindNumber.toSperner_fromSperner (category: graduate) is missing a docstring
WARNING: Theorem DedekindNumber.fromSperner_toSperner (category: graduate) is missing a docstring
WARNING: Theorem Mersenne.new_mersenne_conjecture.variants.prime (category: research open) is missing a docstring
WARNING: Theorem BusyBeaver.BB_2 (category: undergraduate) is missing a docstring
WARNING: Theorem BusyBeaver.BB_4 (category: undergraduate) is missing a docstring
WARNING: Theorem BusyBeaver.BB_5 (category: research solved) is missing a docstring
WARNING: Theorem BusyBeaver.BB_3 (category: undergraduate) is missing a docstring
WARNING: Theorem SnakeInBox.snake_dim_nine_lower_bound (category: research solved) is missing a docstring
WARNING: Theorem SnakeInBox.snake_small_dimensions (category: research solved) is missing a docstring
WARNING: Theorem SnakeInBox.snake_dim_nine (category: research open) is missing a docstring
WARNING: Theorem Kakeya.kakeya_set_conjecture (category: research open) is missing a docstring
WARNING: Theorem OeisA231201.conjecture (category: research open) is missing a docstring
WARNING: Theorem Hilbert17.f_not_sum_of_squares (category: high_school) is missing a docstring
WARNING: Theorem Hilbert17.hilbert_17th_problem_poly (category: research solved) is missing a docstring
WARNING: Theorem Hilbert17.hilbert_17th_problem (category: research solved) is missing a docstring
WARNING: Theorem Hilbert17.f_nonneg (category: high_school) is missing a docstring
WARNING: Theorem Green45.green_45 (category: research open) is missing a docstring
WARNING: Theorem Green63.green_63 (category: research open) is missing a docstring
WARNING: Theorem Green7.green_7.variants.queneau (category: research open) is missing a docstring
WARNING: Theorem Green81.green_81 (category: research open) is missing a docstring
WARNING: Theorem Kurepa.kurepa_conjecture.gcd_reduction (category: undergraduate) is missing a docstring
WARNING: Theorem Kurepa.kurepa_conjecture.prime_reduction (category: undergraduate) is missing a docstring
WARNING: Theorem SimpleGraph.F_four_le (category: research solved) is missing a docstring
WARNING: Theorem SimpleGraph.F_three (category: research solved) is missing a docstring
WARNING: Theorem Erdos1060.erdos_1060.parts.ii (category: research open) is missing a docstring
WARNING: Theorem Erdos1135.erdos_1135 (category: research open) is missing a docstring
WARNING: Theorem Erdos1092.f_asymptotic_general (category: research open) is missing a docstring
WARNING: Theorem Erdos1092.f_asymptotic_2 (category: research open) is missing a docstring
WARNING: Theorem Erdos252.erdos_252 (category: research open) is missing a docstring
WARNING: Theorem Erdos855.erdos_855 (category: research open) is missing a docstring
WARNING: Theorem Erdos859.erdos_859 (category: research open) is missing a docstring
WARNING: Theorem Erdos859.erdos_859.variants.trivial_case (category: high_school) is missing a docstring
WARNING: Theorem Erdos859.erdos_859.variants.positive_density (category: undergraduate) is missing a docstring
WARNING: Theorem Erdos4.erdos_4.variants.rankin (category: research solved) is missing a docstring
WARNING: Theorem Erdos260.erdos_260 (category: research open) is missing a docstring
WARNING: Theorem Erdos423.erdos_423' (category: research solved) is missing a docstring
WARNING: Theorem Erdos125.erdos_125 (category: research formally solved) is missing a docstring
WARNING: Theorem Erdos494.erdos_494.variants.k_eq_4_card_gt_12 (category: research solved) is missing a docstring
WARNING: Theorem Erdos494.erdos_494.variants.product (category: research solved) is missing a docstring
WARNING: Theorem Erdos494.erdos_494.variants.k_eq_2_card_pow_two (category: research solved) is missing a docstring
WARNING: Theorem Erdos494.erdos_494.variants.card_divisible_by_prime_gt_k (category: research solved) is missing a docstring
WARNING: Theorem Erdos975.erdos_975.variants.lower_bound (category: research solved) is missing a docstring
WARNING: Theorem Erdos975.erdos_975.variants.n2_plus_1 (category: research solved) is missing a docstring
WARNING: Theorem Erdos961.erdos_961.variants.well_defined (category: research solved) is missing a docstring
WARNING: Theorem EquationalTheories_677_255.Equation255_not_implies_Equation677 (category: research solved) is missing a docstring
WARNING: Theorem EquationalTheories_677_255.Equation677_not_implies_Equation255 (category: research solved) is missing a docstring
```

Search the repository for the listed theorem declarations, beginning with CongruentNumber.Tunnell_even_converse and the other names in the issue. Review each declaration's surrounding statement and add an appropriate docstring; the work is complete when all listed missing-docstring warnings are addressed.

Written by the indexing model from the issue text.