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

AGENTS.md

@@ -283,6 +283,11 @@ a procedure, find out whether it has a name:
   new symbolic-computation algorithms appear.
 - **Gruntz's thesis** for limits, **Bronstein's _Symbolic Integration I_** for integration,
   **_Modern Computer Algebra_** (von zur Gathen & Gerhard) for the polynomial layer.
+- **[mathlib4](https://leanprover-community.github.io/mathlib4_docs/)** — for the *hypotheses* of an
+  identity. Every lemma there carries its side conditions explicitly and machine-checked, which is
+  exactly what a rewrite rule needs and exactly what our rules have repeatedly been missing. See
+  [`Contributing/SimplificationContract.md`](Sources/AngouriMath/Docs/Contributing/SimplificationContract.md)
+  for how to use it and where it does not help.
 
 Branch cuts deserve a specific warning: `arcsin`, `log`, and fractional powers disagree between
 conventions, and C99, .NET, Python and Mathematica do not all agree. Decide deliberately, cite the
@@ -374,6 +379,39 @@ checks that any more: the `PublicApiAnalyzers` package that required every publi
 listed in a `PublicApi.*.txt` is gone from the tree, so it is a rule to follow rather than one to
 be caught by.
 
+## Read the roadmap before you release anything
+
+[#746](https://github.com/asc-community/AngouriMath/issues/746) is the ten-year technical vision, and
+it is **not optional reading before a release, a version number, or anything that lands in the kernel
+package**. It was written to be argued with, not obeyed — but it has to be read first, because two
+things in it are easy to break by accident and impossible to undo afterwards.
+
+**Its `v1.0`–`v9.0` are capability tiers, not versions.** `v1.0` is "a symbolic engine worth building
+on" — a real polynomial layer, a *written* canonical-form specification, pattern matching as data
+rather than a `switch`, and assumptions that travel with a node. `v2.0` is "the rewrite graph". A
+published package version does **not** mean the tier of the same name has been reached, and choosing
+one spends a label the roadmap is using: check #746 before picking a number, and say on the issue
+which tier the release does and does not advance.
+
+**Three conditions cut across every tier**, and #746 says a tier that violates one has failed
+whatever else it delivered:
+
+1. **The common case pays for nothing it does not use.** Package boundaries are decided deliberately
+   and early, because a published one cannot be moved. Anything large landing in the kernel wants that
+   decision first — #746's item 78.
+2. **Speed and memory on popular use cases are measured, not hoped for.** Parse, `Simplify`, `Solve`
+   and `Differentiate` on textbook-sized input, recorded in
+   [`WhatsNew/version_performance_control.md`](Sources/AngouriMath/Docs/WhatsNew/version_performance_control.md).
+   Measure the previous column again on the same machine and publish the pair: columns taken on
+   different hardware cannot be read as a ratio, and a uniform factor across every row is the machine
+   rather than the code.
+3. **Correctness coverage grows with the surface.** Each new layer adds ways to be wrong that the one
+   below could not express.
+
+So the release checklist is: the suite and the harnesses in `work/` green, a `BREAKING-CHANGES.md`
+entry for every changed answer measured on real builds, **a performance column measured against the
+previous one on the same machine**, and a version number that does not contradict #746.
+
 ## Where the work is
 
 Good entry points, roughly by depth. **Checked against the tracker on 2026-08-08** — the list this

CLAUDE.md

@@ -0,0 +1,25 @@
+# CLAUDE.md
+
+The instructions for this repository are in **[AGENTS.md](AGENTS.md)**. Read it before doing
+anything else here; this file exists only so that tools looking for `CLAUDE.md` find their way there.
+
+Four things from it that are most often learned the hard way, so that they are visible even if
+nothing else is read:
+
+1. **Be a mathematician first.** When correctness and backward compatibility disagree, correctness
+   wins — and every changed answer is recorded in [BREAKING-CHANGES.md](BREAKING-CHANGES.md), measured
+   on a build of each version rather than read off a diff.
+2. **Not answering is a legitimate answer; answering wrongly is not.** Unevaluated means "I could not
+   settle this", `NaN` means "this does not exist", and confusing them ships a wrong answer.
+3. **Read [#746](https://github.com/asc-community/AngouriMath/issues/746) before a release or a
+   version number.** Its `v1.0`–`v9.0` are capability tiers, not shipping versions, and it names
+   conditions — measured performance, deliberate package boundaries — that a release has to meet. See
+   *Read the roadmap before you release anything* in AGENTS.md.
+4. **Before adding or changing a simplification rule**, read
+   [`Contributing/SimplificationContract.md`](Sources/AngouriMath/Docs/Contributing/SimplificationContract.md).
+   A rule states the assumptions under which it holds, or it is asserting there are none.
+
+The measurement harnesses live outside this repository, in the analysis workspace one directory up
+(`work/`): a self-verifying solver corpus, a property checker, root-completeness and
+simplification sweeps, a boundary checker, a crash harness that survives a stack overflow, and a
+checker for the documentation's code samples. Run them before claiming anything is fixed.

Sources/AngouriMath/Docs/Contributing/SimplificationContract.md

@@ -275,7 +275,46 @@ grammar.** For each rewrite, construct the set where its assumption fails and te
 and compare `L` against `R` numerically at each, counting **both undefined** as agreement, per O4.
 Such a harness would have found all four rules of #884 immediately. It does not exist yet.
 
-## 9. What this does not settle
+## 9. Where to look an assumption set up
+
+Obligation O2 says to state the assumption set. For a large part of classical mathematics somebody has
+already stated it, machine-checked it, and published it:
+**[mathlib4](https://leanprover-community.github.io/mathlib4_docs/)**. Every lemma carries its
+hypotheses explicitly, because Lean will not accept it otherwise — which is the discipline a rewrite
+rule needs, already applied to most of classical analysis.
+
+The intervals this library guards the inverse-trigonometric cancellations with are the ones mathlib
+states:
+
+| mathlib4 | our guard |
+|---|---|
+| `Real.arcsin_sin {x : ℝ} (hx₁ : -(π / 2) ≤ x) (hx₂ : x ≤ π / 2) : arcsin (sin x) = x` | `WithinHalfPi(closed: true)` |
+| `Real.arccos_cos {x : ℝ} (hx₁ : 0 ≤ x) (hx₂ : x ≤ π) : arccos (cos x) = x` | `WithinZeroAndPi(closed: true)` |
+| `Real.arctan_tan {x : ℝ} (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 |
+
+Note the open-versus-closed distinction that separates `arctan` from `arcsin`, and that
+`Real.tan_arctan` is a `@[simp]` lemma with no hypothesis at all — the right-inverse direction needs
+none, which is §5's point in someone else's notation. This is the first place to look when writing a
+guard.
+
+**Two warnings.**
+
+**A hypothesis can differ because the convention differs, not because the mathematics does.**
+`Real.sin_arcsin` requires `-1 ≤ x ≤ 1`, and this library needs no such condition — because mathlib's
+`Real.arcsin` clamps outside `[-1, 1]` to stay a total real function, while ours goes into the complex
+plane. Both are right about their own `arcsin`. Copying a hypothesis without checking which convention
+it belongs to is the same error as reading a branch cut off memory, so §6 applies: measure what *this*
+library does.
+
+**And it does not cover everything.** mathlib has no `arccot`, and `arccot` is the case where this
+library's convention departs furthest from the textbooks: its range is `(-pi/2, pi/2]` rather than
+`(0, pi)`, so `arccotan(-1)` is `-pi/4`
+([#887](https://github.com/asc-community/AngouriMath/issues/887)). Where the lookup is empty there is
+no substitute for measuring the function at a positive argument, a negative one, and zero, and writing
+the three values into the comment.
+
+## 10. What this does not settle
 
 - **Per-symbol assumptions.** SymPy carries them on the symbol (`Symbol('x', positive=True)`) with
   `refine`/`ask` to query, and an explicit `force=True` escape where the user accepts the risk. This