Bring the simplification contract up to date, and measure the rule it still names

[Rafael-SOWNet]

Documentation only. Two halves: what #916 made stale, and a measurement of the one rule boundcheck still reports.

Stale after #916

• The DomainCondition table still gave the logarithm's real condition (ln(x) → x > 0). It is now the complex one, with a note that WithCodomain(Domain.Real) gives the other and that which you get is the reading.
• §7's first inconsistency — "ln and sqrt disagree about which reading their domain describes" — was fixed by Let the logarithm's domain follow the reading (#721, #890) #916. Struck, with the reason it is worth remembering: the condition cannot be read off evaluation, because ln(0) is -oo and -oo is not a complex number.
• §8 ended "It does not exist yet" about a harness built from the rules rather than from a grammar. boundcheck is that harness and was built in the same PR that wrote this file.

§11 — new, and a measurement rather than a plan

ln(a) + ln(b) -> ln(a*b) is boundcheck's last disagreement: at x = -3, ln(x) + ln(x+1) is 1.7918 + 6.2832i and ln(x*(1+x)) is 1.7918, differing by the 2*pi*i the principal branch discards. The rule carries no condition, so by O2 it asserts there is nothing to assume, and that is false.

I guarded it with the file's own IsPositiveReal idiom and ran the suite. work/TRIAGE.md records the cost as "the log-equation solver loses coverage". That is not what it is.

• Three failures: SimplifyTest.PowerRulesTest for ln(a) + ln(b) and ln(a) - ln(b) — the rules' own tests — and OneSidedLimitTest.ADifferenceOfReciprocalLogarithms(Left).
• And a hang. The run does not finish. Left alone it passed three and a half hours against a normal five minutes. Under --blame-hang the host is killed with the offending test among RemarkableLimitAfterSimplificationTest, RealCodomainLimitTest.AgreeingOneSidedLimitsArePromoted, StirlingFactorialLimitTest, PowerQuotientGatheringTest and SolveOneEquation.LinearTrigRoots. Four of those five are limit tests.

The dependency is termination, not coverage: the limit machinery expands logarithms (LogarithmExpanded) and relies on the simplifier to gather them back.

Why this is documented rather than fixed here

The precedent is eight rules up in the same file. a^n / b^n -> (a/b)^n was guarded for exactly this reason, cost (x^2 + 1)^x / (x^2)^x its limit, and was repaired by teaching the limit reader to recognise the quotient itself — where IsEventuallyPositive can require the bases to be positive on the approach. See ApplySecondRemarkable.

That repair also needed a thread-static re-read bound (MaxSecondRemarkableRereads), because the rewrite feeds itself indirectly and every level asks for limits of its own. The logarithm path has no such bound, which is the likeliest reason its symptom is a hang rather than a lost answer. Landing the same move for logarithms is a real change to the limit machinery and wants its own PR with its own measurements, not a guard bolted onto this one.

§11 states the acceptance for it: guard in place, boundcheck at 0 disagreements, those three tests passing, the suite finishing in its usual five minutes, and no limit answer lost.

§10 gains the caution that follows. This rule was the standing example of what per-symbol assumptions (#721's second half) would rescue — and no assumption on a and b discharges a termination dependency, because the limit machinery's own expansion is what creates the operands. Assumptions are still worth having; this consumer is not the argument for them.

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