Point at the roadmap before a release, and at mathlib for a hypothesis

[Rafael-SOWNet]

Documentation only. Two additions, both aimed at things being read before they are needed rather than pointed out afterwards.

1. AGENTS.md — read the roadmap before a release

#746 is the ten-year vision, and nothing
pointed at it from the instructions an agent or a new contributor actually reads. Two things in it are
easy to break by accident and impossible to undo:

• Its v1.0–v9.0 are capability tiers, not versions. v1.0 is "a symbolic engine worth building
  on" — polynomial layer, a written canonical-form specification, pattern matching as data, assumptions
  travelling with a node. v2.0 is "the rewrite graph". Choosing a package version spends a label the
  roadmap is using, so it is worth checking the issue first and saying there which tier a release does
  and does not advance.
• Three conditions cut across every tier, and Goal: Math OS — a ten-year vision for AngouriMath as an open mathematical reasoning platform #746 says a tier violating one has failed whatever
  else it delivered: the common case pays for nothing it does not use (package boundaries decided
  early, since a published one cannot move — its item 78), speed and memory measured rather than hoped
  for, and correctness coverage growing with the surface.

With a release checklist that follows from them, including the one thing easiest to get wrong about
the performance table: re-measure the previous column on the same machine and publish the pair,
because columns from different hardware cannot be read as a ratio and a uniform factor across every row
is the machine rather than the code.

CLAUDE.md is added as a pointer to AGENTS.md, so a tool looking for that filename finds its way,
carrying four rules in case nothing else is read.

2. mathlib4, for the hypotheses of an identity

SimplificationContract.md asks a rule to state its assumption set and did not say where to find one.
For classical analysis, mathlib4 has already
stated and machine-checked them — Lean does not accept a lemma otherwise.

The intervals this library guards the inverse-trigonometric cancellations with are the ones mathlib
states, checked against the current docs:

mathlib4	our guard
Real.arcsin_sin (hx₁ : -(π / 2) ≤ x) (hx₂ : x ≤ π / 2) : arcsin (sin x) = x	WithinHalfPi(closed: true)
Real.arccos_cos (hx₁ : 0 ≤ x) (hx₂ : x ≤ π) : arccos (cos x) = x	WithinZeroAndPi(closed: true)
Real.arctan_tan (hx₁ : -(π / 2) < x) (hx₂ : x < π / 2) : arctan (tan x) = x	WithinHalfPi(closed: false)
@[simp] Real.tan_arctan (x : ℝ) : tan (arctan x) = x — no hypothesis	the right-inverse direction, unguarded

Including the open-versus-closed distinction between arctan and arcsin, and the fact that the
right-inverse direction carries no hypothesis at all — §5 of the contract in someone else's notation.

Two warnings go with it, because the lookup is not mechanical. Real.sin_arcsin requires
-1 ≤ x ≤ 1 and we need no such condition, because mathlib's arcsin clamps outside [-1, 1] to stay
a total real function while ours continues into the complex plane — a difference of convention, not of
mathematics. And mathlib has no arccot, which is where this library departs furthest from the
textbooks: its range is (-pi/2, pi/2], so arccotan(-1) is -pi/4
(#887). Where the lookup is empty, measure at
a positive argument, a negative one and zero, and write the three values into the comment.

Why this shape

Leibniz's characteristica universalis wanted three things: a perfectly logical language, an
encyclopedia of verified knowledge, and an engine of reason. #746's v7.0 already plans the bridge to
the first two. The point of this PR is narrower and available now: the encyclopedia is usable today,
with no dependency and no bridge, as a place to look up a side condition — which is the single thing
this library's rules have most often been missing.

No code changes; AGENTS.md, a new CLAUDE.md, and one section in SimplificationContract.md.