@yellowchesstiger: Congratulations! With Lemmas 9 and 10 (which relate to the position's "theme"), the proof is now rock solid.
As this position was a lot more complicated than the first one I posted here, it doesn't surprise me that no one else attempted a proof of illegality for it. If I do submit another position in the near future (which I may or may not ), I'll try to make it a little less complicated, but (hopefully) just as interesting.
@Cobra91: I think I have found a corrected proof this time:
Lemma 4,5,6 of my first (wrong) "proof" still hold.
With slight adjustments one can also proof Lemma 7 to be correct (modifications are italic):
Lemma 7: The black pawn that promoted captured 4 or 5 white figures, but not white's a-pawn. White's a-pawn was captured by another black figure.
Proof: One of black's f,g,h pawns must have promoted on a light square to a LSB. As a bishop cannot reach f3 from the fields h1 and f1 (due to being blocked by white pawns), it is clear that a black pawns must have promoted to a LSB either on b1 or on d1. Either way, it must have captured at least 4 white pieces/pawns on its march to promotion.
Because the White a-pawn never left the a-file (Lemma 5), if the Black pawn that promoted would have captured the a-pawn, it would have had to capture another white figure to get back onto the b-file to become a LSB. Hence, it would have captured at least 6 white figures. The only way for a black f,g,h pawn to capture 6 white figures to reach one of the two possible promotion squares b1 or d1 is if the black f or h pawn captured 6 white figures on ligth squares, specifically not the white DSB.
In P, there are 9 white figures left. If one also considers the White LSB which was on f1 and the white DSB and the 6 captures by the black pawn that promoted, we obtain 9+6+1+1=17>16 White figures, contradicition.
Hence, the black pawn that promoted didn't capture the white a-pawn, and therefore captured 4 or 5 white figures different from the a-pawn.
Because White has no a-pawn in position P, the white a-pawn must have been captured by another black figure. This ends the proof of Lemma 7. qed
It is obvious that Lemma 8 then also holds.
Now, we also prove the following new Lemma:
Lemma 9: If the black pawn that promoted to a LSB on squares b1 or d1 captured the white b-pawn, it didn't capture the white DSB.
Proof: The only squares a black f,g or h pawn could have captured a white b-pawn on the b-file (Lemma 5), the capture must have happened either on b3 or on b2.
If it happened on b2, there is no way for the white DSB on c1 to leave the pawn chain before the capture, and it also wasn't capture after the capture because it is still sitting on c1 (dark square).
If the capture happened on b3, however, it is only possible if the black f-pawn captured e6,d5,c4,b3 in a row. Then, again, it is impossible for the black f-pawn to capture the white DSB because then it would be required to capture the white DSB either on a1 or on c1. qed
Now, we can count white's pieces:
- In position P, white has 9 figures.
- White LSB on f1 (Lemma 4)
- 4 or 5 white figures captured by the black pawn that promoted to LSB (Lemma 7)
- white figure captured by h-pawn (Lemma 6, this figure wasn't counted yet (Lemma 8))
- white a-pawn (Lemma 7)
This alone adds up to 16 or 17 white figures. Therefore, the black pawn that has promoted must have captured exactly 4 white figures. The only possible candidates are the white DSB, b-pawn, Queen, two rooks. Lemma 9 now ensures us that it either didn't capture the DSB or the b-pawn.
The figure that was not captured by the black pawn that promoted must therefore have been captured by the black h-pawn, and because the white h-pawn never left its file, we obtain:
Lemma 10: The black h-pawn captured the white DSB.
Proof: see above. qed
This specific capture hxwhite DSB can however only occured on the squares g5, g3 or g1.
As the white c-pawn can never reach any of these squares, it never captured the black h-pawn.
In position P, black has still got 11 figures. Black also had a LSB on c8 when the game started, and four more black figures where captured by the white c-pawn (Lemma 5). This adds up to 16 figures in total. Hence, white captured no more figures and as such didn't capture the black h-pawn (or a piece resulting from promoting it.
Again by observing the white piece count as above, we obtain that the black h-pawn must have captured exactly one white figure and as such, didn't promote. As it wasn't captured either, it staid on the g-file.
Therefore, the black g-pawn in position P must result from the black h-pawn capturing the white DSB on g5.
This, however, now obviously prohibits case 2 of Lemma 3 of my first "proof" and therefore closes this hole.
Hence, now the proof should be complete (unless I again messed up somewhere).