The allegedly obvious things are the hardest to prove! During the early endgame, consider a local gote endgame with one or both players' simple followups in an ideal environment. These two aspects seem obvious: a) use the gote move value and b) play locally when it is approximately the temperature (largest move value of the environment).
There are four major cases so four theorems occur: 1) one player's followup, the gote move value equals some value of the environment, 2) one player's followup, the gote move value is unequal, 3) both players' followups, the gote move value equals some value of the environment, 4) both players' followups, the gote move value is unequal.
At first, my sketches of proofs covered a few pages (up to 2 pages per proof) and explained why a player must play locally neither prematurely nor too late. However, I overlooked something: taking into account the opponent's decisions leads to minmax decisionmaking. As a consequence, proofreading entered the "whatever it takes..." stage.
Once the "unequal" cases would be done, deriving the "equal" cases would be straightforward. Therefore, first I corrected the former. Each correction of the two "unequal" proofs needed 2.5 weeks and filled 13 to 18 pages. Altogether, I produced 44 pages covering the four proofs.
Afterwards, I have compressed the proofs by excessive use of crossreferences and footnotes. Now, the proofs fill 11+, 9+, 6.5 and 2 pages. Together with a fifth conclusive theorem, 30 pages prove the "obvious".
Needless to say, I must proofread a bit more:)
Why is it so difficult? There are up to 30 cases of starting player, whose / which followup and parities of numbers of intervening moves between / after the local move value and followup move value(s). The small numbers (for 0, 1 or 2 intervening moves) create the trouble. Each case requires a minmax analysis, in which every move demands its own algebraic proof to decide local versus environmental play.
While each small step looks like school mathematics, putting everything together requires great diligence, mathematical experience, structural vision and the right idea exactly what bounds of approximations can be proved.
Why do I invest all this effort? Correct timing in the basic local endgames during the early endgame is of the greatest importance!
Go theory is not selffulfilling. For the late endgame, Bill has taught us that a local gote with one player's followup should be evaluated by its sente(!) move value. Together with a couple of additional theorems, I show that the early endgame is different: we can use the gote move value.
