docs(autodiff): state the expansion contract a backend must satisfy

[AlekseiChirkovVention]

Pin the public expansion surface in the extension-contract test, and document what adopting an
expanded artifact actually costs a backend.

Goal

The twelve public names already existed but were asserted by nothing: a name dropped from the
package's lazy export chain, or leaked into the top-level package, would have gone unnoticed.
And a backend author had no written statement of which handlers an expanded artifact requires.

What this changes

• The extension-contract test gains a fourth export set beside the dependency, lowering, and
  training sets it already pins, checked the same way — declared in __all__, reachable,
  identical to the module's own object, and absent from the top-level package. The three
  existing sets are byte-unmodified.
• The module docstring gains the full contract per the specification's documentation
  requirement.
• The package README gains a short subsection under the autodiff surface.

No behaviour changed. Every edit to the module is inside its docstring; no function body,
control flow, emitted value, or exported binding moved.

The correction worth reading

The specification's required-handler table says the rank-reducing tier needs a trivial reshape
handler. It does not say where. The answer is both artifacts: the gradient path's own
leading seed reshape survives expansion untouched, so a backend that registers a reshape
handler for the forward graph alone still fails closed on the derivative program.

An author following the table as written would hit that rejection with no idea why. The
documentation now states it explicitly, and names the reduction written with kept dimensions as
the recommended lower-cost form, since that tier needs no reshape handler at all.

Two further points the documentation is careful about:

• The exact-divisor clause is described as a scope guard, not a correctness guard. The
  rewrite preserves value for any divisor; the clause confines the pass to the reduction case
  and keeps the one inexact substitution on an exact integer element count. Implying more would
  promise a safety the code does not provide.
• The source-first differentiation contract is stated without claiming that differentiating
  an expanded graph must fail. That claim was withdrawn from the specification deliberately:
  reverse traversal skips a node whose inputs contain no requested differentiation target
  before looking up a rule, so a zero-operand constant guarantees no such failure.

One note records that both emitters derive the terminal node's declared type from its
operands rather than copying it, while the specification words that as "verbatim". They agree
for every artifact this framework produces, and deriving is the correct reading of the
truthful-types invariant — it is what makes truthfulness structural rather than incidental. The
note exists so a later reader does not turn it back into a copy and quietly reintroduce the
defect the design exists to prevent.

Test evidence

The new export test passes on its first run, because the surface it pins was built by the
branches below this one. That is a regression guard, not a driver of new behaviour, so its
value depends entirely on being falsifiable — which was checked rather than assumed. Dropping a
name from the declared exports fails the subset assertion; dropping it from the routing set
fails the reachability assertion; a name leaked into the top-level package fails the absence
loop.

5 cases in the contract test, 889 in the focused autodiff suite — unchanged, since
documentation adds no test. Broad non-integration suite: 1140 passed, 9 failed, 1 skipped, the
9 pre-existing and unrelated.

The documentation criteria are verified by review rather than by test. Unit and contract levels
are exhausted by the export test; integration and smoke are inapplicable because no runtime
behaviour or entry point is added. Tests that grep prose were deliberately not written — they
pin wording rather than meaning and break on every edit.

Stack position

Stack position 7 of 8 — based on fix/fail-closed-lowering-diagnostics.

Cannot merge into main before the six branches below it in the series.