Record the logarithm gathering as fixed, in the section that said it was not

[Rafael-SOWNet]

Documentation only, following #922.

§11 of SimplificationContract.md was written while ln(a) + ln(b) -> ln(a*b) was still unsound, and it ended with acceptance criteria for whoever took it on. #922 met them, so the section now records what closed it rather than what was owed. §8 no longer says boundcheck reports one disagreement, because it reports none.

Three things are kept rather than dropped, because they generalise past this rule:

• Withdrawing a rewrite can break termination, not merely coverage. The limit machinery expands logarithms and relied on the simplifier to gather them back, so guarding the rule hung the suite where it was expected to cost answers. Worth asking of any rule being withdrawn: not only what answers it produced, but what machinery relied on it to close a loop.
• The identity moves to where it is checkable rather than being deleted — a^n / b^n is gathered into (a/b)^n unconditionally, which is wrong for bases of opposite sign #802's rule, and §3's third row in practice.
• Withdrawing a rewrite has a cost in search, invisible until something is timed. Stating the approach too narrowly left the answer correct and 6× slower.

It also records the four placements it took to find where the identity had to be stated, each ruled out by measurement rather than argument: a limit solver never fires, a rewrite in the limit pipeline is reached zero times, stating the approach around one Simplify leaves the rule reached 192 times with nothing to check against, and stating it only at the +oo-normalised entries is correct but slow.

No code changed, so the suite is master's.