symplex 0.9.0

# Changelog

All notable changes to this project are documented in this file.

The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/),
and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
Until 1.0, minor releases may contain breaking changes; they are listed first.

## [0.9.0] - 2026-09-19

A **comprehensiveness** release: the first pass over the gaps a SymPy user
hits in the first hour, taken from a module-by-module survey against
SymPy 1.14 (reference values from that SymPy are cited in the tests).
Additive over 0.8.2.

### Added

- **Algebraic numbers and polynomial algebra on `Ex`**
  (`api::expr_algebraic_ext`): `minimal_polynomial(&var)` (`√2 + √3` →
  `x⁴ − 10x² + 1`; `∛2`, `(1 + √2)⁻¹`, `√(3 + 2√2)`, the golden ratio),
  `gcd_all` / `lcm_all` (multivariate over ℚ, no variable named),
  `Ex::groebner(&polys, &vars, order)` and `reduce_modulo` with
  `MonomialOrder::{Lex, GrevLex}` (in the prelude), `real_roots(&var)` /
  `root_of(&var, k)` (rational roots exact, the others as ordered
  `RootOf` nodes), `factor_mod(&var, p)` (factorisation over GF(p), odd
  prime `p`), and `resultant_symbolic` / `discriminant_symbolic` for
  polynomials whose other coefficients are symbolic (Sylvester
  determinant: `disc(ax² + bx + c) = b² − 4ac`).
- **24 special functions**, each with constructor, exact special values,
  derivative, arbitrary-precision `evalf` (verified at 40 digits against
  mpmath on every branch), `Display`, LaTeX and `parse` support:
  `erfi`, `erfinv`, `erfcinv`, `expint(n, x)` / `E1`, `Shi`, `Chi`,
  `fresnels`, `fresnelc`, `lowergamma`, `uppergamma`, `polylog` (with
  `Li₂(½)` and the `s ≤ 0` rational values), `dirichlet_eta`, `airyai`,
  `airybi`, `airyaiprime`, `airybiprime`, `elliptic_k`, `elliptic_e`,
  `elliptic_f`, `elliptic_pi` (Carlson forms), `gegenbauer`, `jacobi`,
  `assoc_legendre`, `assoc_laguerre` (polynomial expansion for integer
  degree).  `integrate` now reaches `∫e^{ax²+bx+c}` for `a > 0` (`erfi`),
  `∫sinh(x)/x = Shi(x)` and `∫cosh(x)/x = Chi(x)`.  `expr!` accepts all
  of them (multi-argument ones in SymPy's `f(params…, x)` order).  Lean
  rendering of these is `NotImplemented` (no Mathlib spelling); codegen
  likewise.
- **Function analysis on `Ex`** (`api::expr_calculus_util_ext`, SymPy's
  `calculus.util`): `singularities`, `stationary_points`, `maximum` /
  `minimum` on a union of intervals (stationary points, endpoints,
  one-sided limits; `±∞` allowed), `is_increasing` / `is_decreasing` /
  `is_strictly_*` / `is_monotonic` / `is_convex` (exact Sturm route for
  polynomial and rational derivatives; three-valued, never a guess),
  `periodicity` (`sin(2x) + cos(3x)` → `2π`), `function_range`.
- **Matrices**: `singular_values`, `condition_number`, `rank_decomposition`
  (`A = C·F`), `hessenberg` (`(H, P)` by Gaussian similarity, exact over
  ℚ), `companion`, `jordan_block`, `permanent` (Ryser / subset DP),
  `row_insert` / `col_insert` / `row_del` / `col_del` / `permute_rows` /
  `permute_cols`, `inv_mod`, `matrix_log` (Jordan form, defective blocks
  included), `casoratian`; `ZMatrix::{lll, lll_default,
  lll_with_transform}` with exact rational Gram–Schmidt
  (`normalforms::lll`), `QMatrix::{rank_decomposition, pinv, hessenberg}`,
  `ExactMatrix::permanent`.

### Changed

- `Matrix::pinv` is defined for **every** matrix: a rank-deficient input
  goes through the full-rank factorisation `Fᵀ(FFᵀ)⁻¹(CᵀC)⁻¹Cᵀ` (SymPy:
  `[[1,2],[2,4]].pinv() = (1/25)·[[1,2],[2,4]]`) instead of returning
  `ComputationFailed`.
- `∫e^{x²}` and friends are no longer unevaluated `Integral` nodes (see
  `erfi` above).

### Fixed

- A random-LP property test boxed the variables at a fixed `±50`, which
  one seed showed can exclude the whole feasible region (`x₃ ≥ 52`); the
  box is now placed around a feasible vertex.  The solver's verdicts were
  correct.

### Infrastructure

- `symplex` and `symplex-build` at 0.9.0; `symplex-macros` at 0.3.2
  (new function names for `expr!`; the unreachable arm is a compile
  error).  New test group `tests/v09/` (algebraic, calculus_util, matrix,
  special; `ntheory_discrete` and `output` reserved for the next pass).

## [0.8.2] - 2026-09-19

### Changed

- `prove_sos` prunes its Gram basis by the **Newton polytope**: a monomial
  is kept only if its doubled exponent lies in the convex hull of the
  goal's support (one small exact LP per candidate), which is exactly the
  set of monomials that can occur in a sum-of-squares decomposition
  (Reznick) — so nothing provable is lost, and sparse goals fit the
  `max_basis` budget: `x⁸ + y⁸ + 1` needs 6 basis monomials instead of 45.
  Dense goals are unchanged (the eight pinned Mathlib shapes are
  byte-identical; the 120-case random stress is still 119 proved, the
  same one unknown).

## [0.8.1] - 2026-09-19

### Changed

- **`symplex-macros` 0.3.1.**  `syn` is now depended on with an explicit,
  minimal feature set (`parsing`, `printing`, `proc-macro`, `derive`,
  `full`; `default-features = false`): `full` — which the `rule!` macro's
  `if <closure>` condition needs — was previously enabled only
  transitively through `tracing-attributes`, and `extra-traits` /
  `clone-impls` were unused.  `matrix!` rejects an empty literal at
  compile time (a ragged one already was) and its expansion no longer
  contains an `.expect(...)`: the shape is checked by the parser, so the
  matrix is built infallibly.  The doc examples of `expr!`, `matrix!` and
  `eq!` show the actual `ctx,` first argument.  Two new `trybuild`
  snapshots (`tests/ui/matrix_{empty,ragged}.rs`).

## [0.8.0] - 2026-09-19

### Added

- **Structured Lean proofs: `lean::{Block, Tactic, Proof, Decl,
  DeclKind}`.**  A small model of a tactic proof — `Tactic::have(name,
  ty, Proof::term(…) | Proof::by(block))`, `Tactic::bullet(block)`,
  `Tactic::raw(text)` — whose `Block::render(indent)` places every line
  from its *tactic column* (a `· ` bullet moves it by two; a `by` block
  sits two further in) and wraps long lines past it, so a generator that
  stitches many certificates into one lemma no longer counts spaces or
  risks a tactic silently joining the wrong block.  `Decl` renders a
  `theorem`/`lemma`/`example` header in Mathlib's style (binders packed,
  ` :` closing the binder lines, statement on its own line, ` := by`) with
  an optional doc comment.  `PolyhedronLeanSteps::block()` returns a
  certificate's closing steps as a `Block` (its `have hg : … := by` with
  the `linarith` inside the `by`), and `to_block` is now that block
  rendered — byte-identical to before.  The renderer's output for a
  downstream generator's leaf shape (a `refine … ?_` call, bullets of
  wrapped `have hg` certificates) is pinned to text that compiled against
  Mathlib.
- `lean::lean_ident` is public: a plain identifier when the name is one,
  `«…»`-quoted otherwise.
- `Tactic::introduced_names()`: the `have` names a tactic introduces,
  recursively.

### Infrastructure

- `symplex` and `symplex-build` at 0.8.0; `symplex-macros` unchanged at
  0.3.0.  Additive over 0.7.2.

## [0.7.2] - 2026-09-19

### Changed

- `PolyhedronProver` runs its cheapest LP stage **before** the exact
  refutation (ten sampled parameter values, one small LP each), so the
  majority of goals — true ones certified at the first stage — never pay
  for refutation; a certified goal has no counterexample, so outcomes are
  exactly those of "refute first".  Refutation itself now evaluates the
  goal and hypotheses through exact `MultiPoly` arithmetic instead of the
  expression arena.  n = 5 floor generator: 25 s → 21 s, output identical
  to the Mathlib-compiled 0.7.1 file (cumulative since 0.6.0: 103 s →
  21 s).

## [0.7.1] - 2026-09-19

### Changed

- **Hybrid arithmetic in the exact simplex.**  The fraction-free tableau
  is generic over its cell type and runs on `i64` cells first, then `i128`
  cells with exact 256-bit intermediates (a hand-rolled 128×128→256
  multiply, Jebelean exact division by the modular inverse, 256-bit
  comparison), and only on the first value that does not fit does it
  solve the problem again on `BigInt` cells.  Every decision is a sign
  test or an exact comparison of products, so all three take the same
  pivot path and give the same answer — verified byte-for-byte on 4,000
  random LPs and on the pinned Mathlib fixtures.  Measured on a
  downstream generator: the entries of its final tableaux have median
  67 bits and p90 99, so `i64` alone fit 38% of its 18,000 LPs and `i128`
  fits 99%; certificate LP time 8.3 s → 2.3 s, the whole run 33 s → 25 s.
- **Anti-cycling policy.**  Bland's rule used to take over permanently
  after the *first* degenerate pivot; the certificate LPs are degenerate
  from the start (zero right-hand sides), so they walked Bland's slow
  path throughout.  Dantzig's rule now stays in force until twelve
  consecutive degenerate pivots, then Bland's rule runs until the next
  improving pivot — still provably finite.  Handelman degree 8 on a
  2-variable box: 34,763 pivots / 92 s → 3,683 pivots / 11 s.  Optimal
  objectives and statuses are unchanged on the 4,000-LP check; 24 of them
  now report a different (equally optimal) vertex or a different (equally
  valid) Farkas vector, and one facet of the n = 5 floor generator's
  output uses a different hypothesis set — the generated file compiles
  against Mathlib.
- `PolyhedronProver` emits a `tracing::debug!` event per stage LP
  (`symplex::certificates::polyhedron`: degree, rows, cols, status,
  microseconds); `linprog` reports fallbacks to `BigInt` at `debug` and
  final tableau growth at `trace` under `symplex::linprog::growth`.

## [0.7.0] - 2026-09-19

### Breaking

- **One `certificates::Outcome<C, U>` for every prover.**  `BoxOutcome`,
  `HalfLineOutcome`, `PolyhedronOutcome` and `SosOutcome` are now type
  aliases of it (`Proved(C)` / `Refuted { point, value, param_value }` /
  `Unknown(U)`), so `PolyhedronOutcome::Proved(c)` still reads as before.
  What changes: `Refuted.point` is `Vec<(Ex, Q)>` everywhere (was
  `Vec<Q>` for boxes and `Q` for half-lines) and the variant is
  `#[non_exhaustive]` — patterns need `..`; the `Unknown` payloads are the
  structs `BoxUnknown { farkas, degree }`, `HalfLineUnknown {
  max_polya_power }`, `PolyhedronUnknown { degree, lambda_degree, pairwise
  }`, `SosUnknown { reason }` (all `#[non_exhaustive]`, all `Display`) —
  patterns become `Unknown(u)`.
- The Handelman box certificate struct `certificates::Certificate` is
  renamed **`BoxCertificate`** (`CertificateData` → `BoxCertificateData`);
  `certificates::Certificate` is now the **trait** (`goal`, `verify`,
  `to_lean`, `to_lean_with`, `to_json`, `from_json`) implemented by all
  five certificate types.  Inherent methods are unchanged.
- `lean::LeanOpts`, `certificates::PolyhedronOpts` and
  `certificates::SosOpts` are `#[non_exhaustive]`: struct literals
  (including `..Default::default()`) no longer compile outside the crate;
  use `::default()` with the `with_*` builders or assign fields on a `mut`
  default.  Adding an option is no longer a breaking change.
- Functions that could panic on their arguments now return `Result`
  (found by the panic audit below): `StateSpace::{controllability_matrix,
  observability_matrix, discretize_zoh}` (were infallible),
  `StateSpace::{riccati_residual, ackermann}` (were `Option`),
  `robotics::homogeneous`, and `dynamics::{total_time_derivative,
  euler_lagrange, mass_matrix, christoffel_symbols, coriolis_matrix,
  manipulator_equation}`.  `StateSpace::char_poly` and
  `matrix_decomp::wronskian` return NaN instead of panicking on an
  ill-shaped model / empty list (new `try_char_poly`, `try_wronskian`
  return the error); `is_controllable` / `is_observable` are `false` for an
  ill-shaped model; `ode::solve_ode_system{,_nonhomogeneous}` return `None`
  where they could panic.

See `book/src/reference/migrating-0.7.md` for the one-line fix to each.

### Added

- `Outcome::{is_refuted, is_unknown, into_certificate, refutation, unknown,
  map_certificate}`; `Display` for outcomes.
- `RealLineCertificate::{goal, to_data, from_data, to_json, from_json}`,
  `RealLineCertificateData`, and `Display`.
- Builders `PolyhedronOpts::{with_max_degree, with_max_lambda_degree,
  with_pairwise, with_staged}` and `SosOpts::{with_max_basis,
  with_max_iterations, with_rounding_digits, with_max_facial_reductions}`.
- **No-panic policy and ratchet.**  `CONTRIBUTING.md` spells out the
  practical policy (validate at the boundary, `Result` for failure, `Option`
  for absence, `debug_assert!` for invariants, `std`-style `try_` siblings
  for indexing; error plumbing measured at zero cost);
  `tests/unit/test_no_panics.rs` counts `unwrap`/`expect`/`panic!`/
  `unreachable!` in library code and fails on any increase — or on an
  allowlist that is no longer tight.  108 sites removed; the allowlist is
  the two documented logic errors, the arena's `u32` index conversion and
  the compile-time `const_assert_dim!`.

### Fixed

- `matrix_decomp::wronskian` panicked when the derivatives exceeded the
  expression budget (reachable from user input); it now returns NaN and
  `try_wronskian` reports the error.

### Infrastructure

- `symplex` and `symplex-build` at 0.7.0; `symplex-macros` unchanged at
  0.3.0.  Pinned Mathlib-compiled fixtures byte-identical to 0.6.1.

## [0.6.1] - 2026-09-19

### Added

- `PolyhedronCertificate::used_hyps()`: the indices of the hypotheses the
  identity actually uses, so a generated lemma can list exactly those in
  its signature (previously recoverable only by scanning the emitted Lean
  for hypothesis names).
- `PolyhedronProver::prove_poly(&Poly)`: prove a goal that is already an
  exact polynomial, skipping the expression round trip; its generators may
  be any subset of the prover's in any order (a tool's `(j, r, t)` against
  the prover's sorted `(r, t, j)`).
- `MultiPoly::{as_constant, affine_form, eval_var, to_ex}`: the value of a
  constant polynomial; a degree-≤ 1 polynomial as `(coefficients,
  constant)`; substitution of a value for one variable that **keeps** the
  variable count (unlike `substitute`, which drops the variable and shifts
  the indices — the natural operation for instantiating a parameter); and
  the bridge to an `Ex` over named symbols.  `MultiPoly` and the rational
  type `Q` are re-exported from the prelude.
- `Polytope::is_full_dimensional()` and `Polytope::interior_point()`: one
  exact LP (the largest common slack), instead of testing `volume() > 0`;
  defined for unbounded polyhedra too.  `HalfSpace::{value_sign, is_tight,
  is_trivial, normalized, same_hyperplane}` — gcd-free sign tests and the
  canonical hyperplane key that identifies a cut with its flip and its
  rescalings.

### Changed

- **`Polytope::vertices` is 10× faster and cached.**  The enumeration runs
  in integer arithmetic throughout: half-spaces are scaled to integers
  once, only *distinct* hyperplanes are combined, each `n × n` system is
  solved by the fraction-free kernel (which yields the point as `X / D`
  directly) and containment is the sign of `a·X + b·D` — no rational
  reduction until the accepted vertices are returned.  The vertex list is
  cached on the polytope (`Clone` carries it; `PartialEq`/`Debug` ignore
  it).  `Polytope::volume` enumerates vertices once and hands each facet
  its own vertices (those on its hyperplane, projected) instead of
  re-enumerating at every level of the recursion; `is_bounded` recognises a
  description with axis-parallel bounds on every coordinate without LPs.
  `HalfSpace::contains` / `Polytope::contains` use the gcd-free sign test.
  Profiled on a downstream decision-tree generator (three free
  coordinates, 49 leaves): 103 s → 34 s with byte-identical output; the
  remaining time is the certificate LPs.
- `ParametricPolytope::at` instantiates through exact `MultiPoly`
  arithmetic rather than the expression arena (identical results; verified
  against the symbolic route on random families).

### Fixed

- `lean::wrap_lean` measures its continuation indent from the line's
  *tactic column* (past `· ` / `. ` bullets), not from the leading spaces.
  A bullet's tactics sit two columns right of the `·`, so the old `+2`
  put a wrapped `· have … := by tac` continuation at the same column as
  the following tactic — Lean then swallowed that tactic into the inner
  `by` block (`expected '{' or indented tactic sequence`), or rejected a
  wrapped application argument (`unknown tactic`).  Both shapes were
  compiled against Mathlib before and after; plain (non-bullet) lines and
  the pinned certificate fixtures are unchanged.

### Infrastructure

- `symplex` and `symplex-build` at 0.6.1; `symplex-macros` unchanged at
  0.3.0.  Additive over 0.6.0 (`cargo semver-checks`: no semver update
  required).  End-to-end check: a downstream Lean generator built against
  this tree reproduces its 0.6.0 output byte-for-byte apart from the
  `wrap_lean` bullet fix, and the generated file compiles against Mathlib.
- `CONTRIBUTING.md`: no Cargo feature flags by design; the explicit
  context argument of `expr!` and friends is deliberate.

## [0.6.0] - 2026-09-18

### Added

- **Sums-of-squares certificates** (`certificates::prove_sos(goal, &vars,
  &SosOpts)`, `is_sos`): prove `g ≥ 0` on all of ℝⁿ by an exact
  decomposition `g = Σₖ dₖ·pₖ²` with rational `dₖ > 0` and
  rational-coefficient `pₖ` — the class of goals the box, half-line and
  polyhedron certificates could not reach (`(x − 1)² + (y − 1)²`, the
  AM–GM form `x⁴ + y⁴ + z⁴ + 1 − 4xyz`, …).  Outcomes
  `Proved(SosCertificate)` / `Refuted { point, value }` (exact rational
  point, found by a grid and a rationalised numerical minimiser) /
  `Unknown { reason }` (Motzkin's polynomial, odd degree, or a search that
  did not converge — never a wrong `Proved`).
  - The pipeline is Peyrl–Parrilo made exact: the Gram SDP `g = mᵀQm`,
    `Q ⪰ 0` is solved numerically by a small dense primal–dual
    interior-point method (HKM direction, Mehrotra predictor–corrector,
    exact-to-the-boundary steps; no external solver) whose zero objective
    makes it converge to the analytic centre; the solution is rounded,
    projected back onto the coefficient constraints exactly (rational
    least-norm correction) and tested for positive semidefiniteness with
    the rational `QMatrix::ldl_psd`, whose factorisation *is* the
    decomposition.
  - Goals with real zeros have only singular Gram matrices; the search then
    performs **facial reduction**: the numerical kernel is made exact
    either directly (rational kernel) or through its integer relations
    (LLL on the kernel lattice, with Newton-refined zeros of the goal
    providing a double-precision kernel), the problem is restricted to the
    face `Q = B Q' Bᵀ` and re-solved, up to three times.  Sums of two or
    three random squares with irrational common zeros are recovered
    exactly (119 of 120 random cases through degree 6 in two and three
    variables).
  - `SosCertificate::{goal, vars, basis, gram, squares, rank, identity,
    verify, lean_hints, to_lean, to_lean_with, to_data, from_data,
    to_json, from_json}` (`from_*` re-verify), `Display` as
    `goal = d₁·(p₁)² + …`.
  - Lean export: `have h : goal = d₁ * (p₁) ^ 2 + … := by ring` then
    `rw [h]; positivity` — two deterministic steps, no search.  Eight
    shapes (squares with a common zero, positive definite quadratics and
    quartics, a perfect square, a product of squares, univariate, three
    variables, AM–GM) compile against Mathlib (Lean 4.30.0) with
    `linter.style.longLine` on; the emitted text is pinned to that file
    (`tests/fixtures/sos_certificates.lean`).
- `lean::wrap_lean` never breaks between `^` and its exponent.
- `Poly::new` docs point to `try_new` for the failure reason.

### Infrastructure

- `symplex` and `symplex-build` at 0.6.0; `symplex-macros` unchanged at
  0.3.0.  Additive over 0.5.0.

## [0.5.0] - 2026-09-18

### Breaking

- `certificates::PolyhedronOutcome::Refuted` gained the field
  `param_value: Option<Q>` (the sampled parameter value at which the
  counterexample was found).  Patterns must add `..` or bind it.
- `lean::LeanOpts` gained the fields `single_fraction` and `symbol_text`
  (as announced in 0.4.0: use `..Default::default()` or the `with_*`
  builders; literals naming every field break).

### Added

- **`certificates::PolyhedronProver`**: `PolyhedronProver::new(&hyps,
  param, &opts)?` parses the hypotheses and builds every stage's product
  basis once; `.prove(&goal)` / `.prove_empty()` then certify any number
  of goals against them (accessors `hyps`, `gens`, `parameter`, `opts`).
  `prove_nonnegative_on_polyhedron` and `prove_polyhedron_empty` are now
  one-line wrappers over it.  A goal mentioning a symbol absent from the
  hypotheses is an `InvalidArgument`.
- `LeanOpts::symbol_text` (+ `with_symbol_text(name, text)`): render a
  symbol as given Lean text everywhere it occurs — `("J", "(j : ℝ)")` for
  a parameter that is a cast natural in the surrounding proof.  Applied
  by `Ex::to_lean_with` and therefore by every certificate emitter
  (goals, hypotheses, `λ`, `hg`); hypothesis *names* such as `e1J` are
  untouched.  In a full theorem the binder keeps the plain identifier.
- `LeanOpts::single_fraction` (+ `with_single_fraction`): combine over a
  common denominator before rendering, so an `expand`ed rational function
  prints as `(-(8 * j) - 2) / (7 * j + 4)` instead of
  `-(8 * j / (7 * j + 4)) - 2 / (7 * j + 4)`.
- `PolyhedronLeanSteps::to_block(indent)` now re-flows its lines to
  Mathlib's width (indent included) and `to_block_width(indent, width)`
  takes an explicit width; `lean::wrap_lean` never starts a continuation
  line with `:=`, so `have hg : … := by` keeps its `:= by`.
- **`polytope::ParametricPolytope`**: a family `{x : hₖ(j, x) ≥ 0}` with
  half-spaces affine in `x` and polynomial in one parameter.  `at(&j)`
  instantiates exactly; `polytope_at` / `vertices_at` / `volume_at` /
  `is_empty_at` / `contains_at` cache per sample; `clear_cache`.
- `Polytope::volume` works in **any dimension** (was `≤ 3`): exact facet
  decomposition around the vertex centroid, recursing on each facet's
  exact `(n − 1)`-dimensional H-representation; duplicate or rescaled
  facets are counted once.  Verified on hypercubes and simplices up to
  dimension 5 and the 4-D cross-polytope.
- `QMatrix::ldl_psd()` (exact `L·D·Lᵀ` of a PSD matrix, `None` if not
  PSD), `QMatrix::is_positive_semidefinite()`, `QMatrix::is_symmetric()`.

### Infrastructure

- `symplex` and `symplex-build` at 0.5.0; `symplex-macros` unchanged at
  0.3.0.  The three new `lean_steps` skeleton shapes (cast parameter with
  long names and a wrapped `have hg`, emptiness with `K` chains,
  `prefer_subtraction`) compile against Mathlib.

## [0.4.0] - 2026-09-18

### Breaking

- `Ex::roots_count_real` (the 0.3 alias) is removed; call
  `count_real_roots_in` on `Ex` or `Poly`.
- `lean::LeanOpts` gained the field `prefer_subtraction`.  Struct literals
  must add `..Default::default()` (`LeanOpts { real_type: "ℚ".into(),
  ..Default::default() }`) or use the new builders
  `with_real_type` / `with_ascribe_integers` / `with_prefer_subtraction`.
  Further fields may be added in minor releases.

### Added

- **Certificates on a parametric polyhedron**
  (`certificates::prove_nonnegative_on_polyhedron(goal, hyps, Some((&j,
  &j0)), &PolyhedronOpts)` and `prove_polyhedron_empty`): prove `g ≥ 0`
  on `{hₖ(j, x) ≥ 0}` for every real `j ≥ j₀` — or that the set is empty
  — by the exact identity `λ(j)·g = Σ μ·jᵃ(j − j₀)ᵇ·hₖ + Σ μ·jᵃ(j − j₀)ᵇ
  + μ₀` (optionally `+ Σ μ·hₖhₗ`), `λ(j) = 1 + Σ νₐ jᵃ`, all `μ, ν ≥ 0`.
  The polynomial multiplier `λ` on the goal is what makes `j`-dependent
  facets certifiable (their Farkas multipliers are rational functions of
  `j`).  Outcomes `Proved(PolyhedronCertificate)` / `Refuted { point,
  value }` (an exact point of the set, found by sampling `j` and
  minimising an affine goal with the exact LP) / `Unknown { degree,
  lambda_degree, pairwise }`.  The search is **staged** (degree-1
  multipliers with `λ = 1` first, then higher degrees, pairwise products
  last; `PolyhedronOpts::single` for one LP) and every certificate is
  re-verified with exact polynomial arithmetic.  `param = None` gives a
  plain Farkas / pairwise certificate on a fixed polyhedron.
  - `PolyhedronCertificate::{goal, hyps, parameter, terms, lambda,
    lambda_coeffs, lambda_is_one, degree, uses_pairwise,
    proves_emptiness, product_expr, identity, verify}`, `Display` with
    the hypotheses abbreviated `hₖ`.
  - Lean export in the shape a hand-written proof uses: `to_lean(name)`
    emits a theorem with `hj : j₀ ≤ j`, `h0 : 0 ≤ h₀`, …, derives `hJ0`
    / `hK0` when needed, one `have … := mul_nonneg …` per product
    (`h0K`, `h0JK`, `h0xh1`, `pJJ`), and closes with `linarith only […]`
    — through `have hg : 0 ≤ λ * g` and `nonneg_of_mul_nonneg_right`
    when `λ ≠ 1`; emptiness certificates conclude `False`.
    `lean_steps(&PolyhedronLeanNames { hyps, param_nonneg, shift_nonneg },
    &opts)` returns the same `have` lines, hint names and closing block
    (`PolyhedronLeanSteps`, `to_block(indent)`) for an existing proof
    skeleton.  Fifteen shapes (λ = 1; λ of degree 1 and 2 on `j` or on
    `j − j₀`; `j₀ > 0`, `j₀ = 0`, `j₀ < 0`; mixed `J`/`K` chains; pairwise
    products with and without a parameter; emptiness with and without `λ`;
    pure parameter powers `pJJ`, `pJK`, `pKK`; no parameter) compile
    against Mathlib (Lean 4.30.0) with
    `linter.style.longLine` on; the emitted text is pinned to that compiled
    file (`tests/fixtures/polyhedron_certificates.lean`).
- **`symplex::polytope`**: exact convex polyhedra in ℚⁿ from half-spaces
  `a·x + b ≥ 0`.  `Polytope::{new, from_rows, from_exprs, to_exprs,
  halfspaces, contains, with_halfspace, split, is_empty, any_point,
  bounding_box, is_bounded, vertices, irredundant, vertex_centroid,
  volume}` (vertices by `QMatrix::solve` over `n`-subsets, emptiness and
  bounds by the exact LP, volume for `n ≤ 3`); `HalfSpace::{value,
  contains, flipped}`.  Meant for the geometry around certificate
  searches (cells of a decision tree, cuts, containment), not for large
  polyhedra.
- `Poly::try_new(expr, gens) -> Result<Poly, SymplexError>`: `Poly::new`
  with the reason for failure — which generator sits inside a function,
  under a negative power (a rational function), under a fractional or
  symbolic power, or in an exponent.
- `Poly::terms_iter()` (borrowed `(&[u32], &Ex)` pairs, no allocation) and
  `Poly::coeffs_rational() -> Option<Vec<Ratio<BigInt>>>`.
- `LeanOpts::prefer_subtraction`: a sum with exactly one negated term is
  printed as a subtraction with that term last (`(1 / 2 : ℝ) - r` instead
  of `-r + (1 / 2 : ℝ)`), so generated hypotheses match hand-written ones
  syntactically; `with_real_type` / `with_ascribe_integers` /
  `with_prefer_subtraction` builders.
- `HalfLineCertificate::lean_hints(hk, &opts)`: the hint list of the Lean
  proof (`hk`, `pow_nonneg hk n`, `mul_nonneg (sq_nonneg g) (…)`) for a
  caller's proof skeleton, with the caller's name for `0 ≤ k`.
- Certificates cross trust boundaries: `Certificate`,
  `HalfLineCertificate` and `PolyhedronCertificate` have `to_data()` /
  `from_data(&ctx, &data)` (plain serde-derived structs
  `CertificateData`, `HalfLineCertificateData`,
  `PolyhedronCertificateData` built from `ExprTree`s and `"p/q"`
  rationals) and `to_json()` / `from_json(&ctx, json)`.  `from_*`
  **re-verifies** the identity with exact polynomial arithmetic and
  rejects data that does not hold, so a checker can accept a certificate
  produced elsewhere without trusting the producer.
- `linsolve` docs state explicitly that an over-determined but consistent
  system is `Unique` (with an example), a contradictory one
  `Inconsistent`.
- `examples/polyhedron_certificates.rs`; test group `tests/v04.rs`
  (`v04_polyhedron`, `v04_polytope`); book: "What's New in 0.4",
  "Migrating from 0.3 to 0.4", a parametric-polyhedra section in the
  certificates cookbook and a polytope section in the LP guide.

### Infrastructure

- `symplex` and `symplex-build` at 0.4.0; `symplex-macros` unchanged at
  0.3.0.  `cargo-semver-checks --release-type minor` against 0.3.5 reports
  exactly the two breaking changes listed above.

## [0.3.5] - 2026-09-18

### Added

- **Exact matrix core.**  `matrix::{QMatrix, ZMatrix}` (aliases of
  `ExactMatrix<Ratio<BigInt>>` / `ExactMatrix<BigInt>`, both in the
  prelude): dense row-major matrices with no expression arena behind
  them.  Construction (`new`, `from_i64`, `from_fn`, `from_flat`, `zeros`,
  `identity`, `diag`, `row_vector`, `col_vector`), access (`get`,
  `try_get`, `row`, `col`, `diagonal`, `rows`, `iter`, `as_slice`,
  `to_rows`, `into_flat`, indexing), shape ops (`transpose`, `submatrix`,
  `hstack`, `vstack`, `map`), arithmetic (`add`, `sub`, `neg`, `scale`,
  `matmul`, `trace`, operators `+ − *`), `is_zero`, `is_identity`, and
  `Display`/`Debug` in the `Matrix` layout.
  - `QMatrix`: `rref`, `rank`, `nullspace`, `columnspace`, `rowspace`,
    `det`, `inv`, `solve` (square, multiple right-hand sides),
    `clear_denominators`, `to_zmatrix`, `is_integer`, `to_matrix`.  Every
    elimination is **fraction-free** (Bareiss Gauss–Jordan on the
    row-wise integerised matrix): intermediate entries are minors of the
    input, all divisions are exact, and no gcd runs in the inner loop.
  - `ZMatrix`: Bareiss `det`, `rank`, `content`,
    `hermite_normal_form[_with_transform]`, `column_hermite_normal_form`,
    `smith_normal_form[_with_transforms]`, `integer_nullspace`,
    `is_unimodular`, `lattice_determinant`, `to_qmatrix`, `to_matrix`.
  - Conversions: `TryFrom<&Matrix>` for both (constant arithmetic is
    folded first; a symbolic entry is `InvalidArgument`), `From<ZMatrix>
    for QMatrix`.
- `examples/exact_matrices.rs`, `benches/exact_matrix.rs`; book: a
  "0.3.5: the exact matrix core" section on the What's New page, a new
  section in the Matrices guide, performance notes in the LP and lattice
  guides.

### Changed

- `Matrix::{rref, rank, nullspace, columnspace, rowspace, left_nullspace,
  det, inv, solve, solve_least_squares, pinv}`, `linsolve`,
  `linsolve_matrix` and every function in `normalforms` now detect
  all-rational input and run on `QMatrix`/`ZMatrix`, converting back at
  the end.  Results are unchanged (the RREF is unique; parametric
  `linsolve` solutions go through the same `tidy` step and print
  identically); a 30×30 rational `inv` drops from 470 ms to 10 ms, `rref`
  of a 30×36 from 208 ms to 4 ms, `linsolve_matrix` 30×30 from 135 ms to
  1.5 ms.  The `Ex`-based Bareiss determinant that only served numeric
  matrices is gone; symbolic matrices take the same paths as before.
- `linprog`: the simplex tableau pivots on **integers with a common
  denominator** (Bareiss/Edmonds integer pivoting).  Each constraint row
  is scaled once to clear denominators (its artificial gets phase-1 cost
  `1/sᵢ` and the scale is divided back out of the duals and Farkas
  vectors); every pivot keeps the tableau integral; ratio and sign tests
  are cross-multiplied integer comparisons with no gcd in the loop.  The
  entering/leaving choices are made on the same rational values as
  before, so the pivot sequence is the same: on 4,000 random LPs with
  fractional data, degenerate rows, all three relations, free and
  two-sided-bounded variables, `x`, objective, duals and Farkas vectors
  are byte-identical to 0.3.4.  A 40-row × 100-variable program goes from
  1.1 s to 40 ms, 60 × 160 from 2.8 s to 80 ms, and Handelman certificate
  searches run 4–7× faster.
- `normalforms` is now a thin wrapper over `ZMatrix`; error messages and
  conventions are unchanged.

### Infrastructure

- Decision recorded after benchmarking `num-bigint 0.4` against `dashu
  0.6` on the exact-linear-algebra kernels: dashu is ~9× faster on
  Gauss–Jordan over `Ratio` but only 1.2–2× on integer kernels — the gap
  is `Ratio`'s per-operation gcd, not bignum speed.  Fraction-free
  elimination on `num-bigint` beats dashu's rational elimination by 5×
  and the previous code by 40×, so `num-bigint` stays and the public
  `Ratio<BigInt>` types are untouched.
- `tests/v03/v03_exact_matrix.rs`: the exact core against textbook
  Gauss–Jordan, the `Matrix` fast paths against the core, the numeric
  `linsolve` route against the symbolic one, random fractional LPs against
  the exact KKT conditions, Farkas certificates on fractional data, and a
  40×40 rational inverse.  A white-box `linprog` unit test covers the
  tableau's negative common denominator after an artificial is driven out
  on a negative pivot.
- `symplex` and `symplex-build` at 0.3.5; `symplex-macros` unchanged at
  0.3.0.  Additive over 0.3.4.

## [0.3.4] - 2026-09-18

### Added

- Sign facts for univariate polynomials with rational coefficients in a
  real-assumed symbol are now decided exactly (square-free factoring +
  Sturm sequences) when the structural assumption rules are silent:
  `(3u² + 2u + 1).is_positive()` is `Some(true)` for `u ≥ 0`,
  `(x² − 2x + 2).is_positive()` is `Some(true)` for real `x`,
  `(x − 1)²` is `is_nonnegative() == Some(true)` but `is_positive() ==
  None`, `x² − 1` stays `None`.  The symbol's own sign assumptions
  (`Positive`, `NonNegative`, `Negative`, `NonPositive`) restrict the
  domain; an excluded endpoint may be a root (`p² + p > 0` for `p > 0`).
  Everything downstream benefits: `simplify` drops `abs(·)` and folds
  `sqrt(p²)`/`sign(p)`, `ln(p).is_real()`, `compare_numeric`, `BoolEx::eval`
  of `p > 0`.  Guarded to degree ≤ 24; symbols without a `Real` assumption
  (possibly complex) are untouched.
- `lean::wrap_lean(text, width)` and `lean::MATHLIB_LINE_WIDTH`: re-flow
  Lean source at spaces, preferring breaks after commas (hint lists) and
  between binders (signatures), with Lean-compatible continuation
  indentation.  All certificate emitters (`Certificate`,
  `HalfLineCertificate`, `RealLineCertificate`) now produce output that
  passes Mathlib's `linter.style.longLine` — verified by compiling the
  wrapped output with the linter enabled.  `Ex::to_lean` stays single-line
  for embedding.

### Infrastructure

- `symplex` and `symplex-build` at 0.3.4; `symplex-macros` unchanged at
  0.3.0.  Additive over 0.3.3.

## [0.3.3] - 2026-09-18

### Added

- `certificates::prove_nonnegative_on_halfline(goal, var, a, Ray::{AtLeast,
  AtMost}, max_polya_power)`: exact certificates for univariate `goal ≥ 0`
  on `x ≥ a` / `x ≤ a`.  With `k = x − a` the identity is
  `(1 + k)^N · goal = g² · Σ cᵢ kⁱ` with `cᵢ ≥ 0`: `N = 0` is the
  shift-and-read-off-coefficients certificate, `N > 0` a Pólya multiplier
  (always exists for a strictly positive goal), and `g` collects
  even-multiplicity zeros.  Outcomes: `Proved(HalfLineCertificate)`,
  `Refuted { point, value }` (exact, found via root isolation), or
  `Unknown { max_polya_power }`.  `HalfLineCertificate::{verify, identity,
  coefficients, polya_power, square, to_lean}`.
- `certificates::prove_nonnegative_on_reals(goal, var, split, max_polya)`
  → `RealLineCertificate` (two half-lines; Lean proof by
  `rcases le_total split x`).
- Box certificates now handle interior even-multiplicity zeros: when the
  plain Handelman search fails, the goal is factored as `g²·h` (exact
  factoring over ℤ) and `h` is certified; `Certificate::square()` exposes
  `g` and the Lean hints become `mul_nonneg (sq_nonneg g) (…)`.
  `(x − 1/2)²·(1 − xy)` on the unit square is now `Proved`.
- Every Lean theorem emitted by `examples/certificates_to_lean.rs`
  (9 theorems: boxes, half-lines both directions, Pólya exponents 1 and
  12, square factors, the real line) was compiled against Mathlib
  (Lean 4.30.0) with no errors or warnings; the texts are pinned in
  `tests/v03/v03_certificates.rs`.

### Fixed

- `(c·m)^n` with a numeric coefficient `c` and `|n| > 10` was left as an
  opaque power by canonicalisation (the product-power distribution has a
  swell guard at 10), so `(-x)^11` did not become `-x^11`,
  `expand((2 - x)^11)` lost its leading term and `Poly::new` rejected the
  result.  A numeric coefficient is now always pulled out (`(-x)^11 →
  -x^11`, `(2x)^13 → 8192*x^13`); products of symbols keep the guard
  (`(x*y)^12` stays as is) but the polynomial view now recognises such
  powers as monomials (`Poly::new((x*y)^12 + 1)` works).

### Infrastructure

- `symplex` and `symplex-build` at 0.3.3; `symplex-macros` unchanged at
  0.3.0.

## [0.3.2] - 2026-09-18

### Added

- `symplex::certificates` — exact, machine-checkable non-negativity
  certificates on a box.  `prove_nonnegative_on_box(goal, &[(var, lo, hi)],
  degree)` searches for a Handelman certificate
  `goal = Σ λₖ · Π (xᵢ − lᵢ)^a (uᵢ − xᵢ)^b`, `λ ≥ 0`, by exact LP (weighted to
  prefer few, low-degree products), **re-verifies the identity with exact
  `Poly` arithmetic** before returning, and otherwise either refutes the
  claim with an exact counterexample (`BoxOutcome::Refuted { point, value }`)
  or reports `BoxOutcome::Unknown { farkas, degree }` (e.g. when the goal
  touches zero inside the box, where no Handelman certificate exists).
  `Certificate::{terms, product, product_expr, identity, verify, degree}`,
  `is_nonnegative_on_box` (three-valued convenience),
  `Poly::express_as_nonneg_combination(basis)` (the LP step alone), and
  `Ex::prove_nonnegative_on_box`.
- `Certificate::to_lean(name)` / `to_lean_with`: a Lean 4 / Mathlib theorem
  `theorem name (x y : ℝ) (h_x_lo : …) … : 0 ≤ goal := by nlinarith […]`
  whose hints are exactly the certificate's products (`mul_nonneg
  (sub_nonneg.mpr h_x_lo) (sub_nonneg.mpr h_y_hi)`, …); linear certificates
  use `linarith`; unused bounds are underscored for the linter.  Every
  theorem produced by `examples/certificates_to_lean.rs` was compiled
  against Mathlib (Lean 4.30.0) with no errors or warnings.

### Infrastructure

- `symplex` and `symplex-build` at 0.3.2; `symplex-macros` unchanged at
  0.3.0.  Additive over 0.3.1 (`cargo-semver-checks`: 223/223).

## [0.3.1] - 2026-09-18

Driven by field notes from downstream tools built on 0.3.0.  Additive only
(verified with `cargo-semver-checks` against 0.3.0).

### Added

- The exact-arithmetic crates are re-exported — `symplex::num_bigint`,
  `num_rational`, `num_integer`, `num_traits` — so a downstream crate can
  name `Ratio<BigInt>` (from `as_rational`, `linprog::Q`, `Matrix::from_ratio`,
  …) without adding and version-matching those crates itself.
- `Ex::as_ratio_parts() -> Option<(BigInt, BigInt)>` and
  `Ex::as_ratio_i128() -> Option<(i128, i128)>`: numerator and denominator of
  a rational literal (SymPy's `Rational.p` / `.q`).
- `Poly::{count_real_roots, count_real_roots_in(lo, hi), real_roots_isolate,
  is_nonnegative_on(lo, hi), is_positive_on(lo, hi)}` — the Sturm-based
  primitives that were only reachable through `Ex` — and `Poly::shift(gen, a)`
  (Taylor shift; "all coefficients of `p(k + a)` are `≥ 0`" is the
  certificate-style sufficient condition for `p ≥ 0` on `[a, ∞)`).
- `Ex::count_real_roots_in(var, lo, hi)`; the old name `roots_count_real`
  stays as an alias (no deprecation warning in a patch release) and is
  removed in 0.4.
- `Ex::to_lean()` / `to_lean_with(&LeanOpts)` (`symplex::lean`): Lean 4 /
  Mathlib rendering with Mathlib spacing (`2 * j + 1`, `j ^ 2`), ascribed
  rational literals (`(3 / 31 : ℝ)`), single-fraction division
  (`(j - 1) / (2 * j)`), `⁻¹` for negative powers, `Real.sin`/`Real.exp`/
  `Real.sqrt`/`Real.pi`/`|x|`/`⌊x⌋`, relations and connectives for `BoolEx`
  (`0 < x ∧ x < 1`), `if … then … else` for `Piecewise`.  Nodes without a
  standard Mathlib spelling are `Err(NotImplemented)`.

### Behaviour changes

- `Ex::as_numer_denom` follows SymPy: a rational literal splits into
  integers (`3/31` → `(3, 31)`), a rational coefficient splits
  (`2/3·x` → `(2*x, 3)`), and sums are combined over a common denominator at
  every depth (`x/2 + 1/3` → `(3*x + 2, 6)`, `1/x + 1/y` → `(x + y, x*y)`).
  Previously a rational literal was an atom (`(3/31, 1)`) and a sum was
  returned whole.  Still no cancellation (`ratsimp` does that).
- `Ex::together` is deep: fractions nested inside numerators, denominators,
  products and integer powers are flattened into one quotient.  Previously
  only a top-level sum was combined, so `Poly::new` on the numerator of a
  `together()` result could silently see a rational function.

### Fixed

- `eval` was not idempotent on `exp(f)^g`: `(1/exp(-1)).eval()` gave
  `exp(1)`, and only a second `eval` gave `E`.  The rewritten exponent is
  now evaluated in the same pass.
- `laplace_final_value` located poles of `s·F(s)` without cancelling the
  factor `s`, which with the deep `together` would have reported a spurious
  pole at the origin for `F(s) = 3/s − 2/(s + 1)`; it now uses `ratsimp`.

### Infrastructure

- The ~275 integration-test source files are compiled into nine test
  binaries (`tests/{v03,v03_oracle,v02,v02_oracle,unit,legacy,proptests,
  perf}.rs` plus `ui_tests`); every test keeps its name as
  `<module>::<test>`.  Linking dropped from ~6.5 min / 13 GB to seconds, and
  the CI disk-space workaround is gone.  See `tests/README.md` for the
  layout and the `cargo test --test <group> <module>::` / `cargo nextest run
  -E …` invocations.
- `.config/nextest.toml`: `cargo nextest run` executes one process per test
  with per-test wall-clock limits (`default` and `ci` profiles).
- `deny.toml` + a `cargo deny check` CI job enforce the pure-Rust dependency
  policy (no C/C++ or system libraries), a licence allow-list, advisories and
  registry sources.
- Removed the assertion-free `tests/zz_probe_tmp.rs` left over from 0.2.
- `symplex-wasm`: dropped the unused `web-sys` dependency.
- `symplex` and `symplex-build` at 0.3.1; `symplex-macros` is unchanged at
  0.3.0.

## [0.3.0] - 2026-09-18

**Polynomials as data, exact certificates.**  This release makes the
polynomial structure of an expression a first-class object (`Poly`: sparse
terms over explicit generators with symbolic coefficients), gives rational
functions a real normal form (`ratsimp`), and adds three exact
certificate-producing domains: linear programming over ℚ with shadow prices
and Farkas infeasibility vectors, Hermite/Smith normal forms of integer
matrices with unimodular transforms and ℤ-bases of integer kernels, and
Sturm-verified polynomial signs on intervals.  A deterministic `f64`
optimisation toolbox (Brent, Nelder–Mead, differential evolution,
least-squares fits) rounds out the numeric side.  There are no
signature-breaking changes; the behaviour changes below alter the *form* of
some results, never their value.

Measured at release: 92 `ExprNode` variants (unchanged), ~11,000 `#[test]`
functions (~154K lines of tests, 273 integration-test files), ~174K lines in
`src/`, ~600 doctests in the main crate, and a SymPy 1.14 oracle extended
with 455 fixtures for the 0.3 features
(`tests/fixtures/v03_cross_validation.json`).

### Behaviour changes

Not breaking — no signature changed — but results may print differently.

- `Ex::{degree, coeffs, coeff, leading_coeff, is_polynomial}` accept
  symbolic, variable-free coefficients: `(a·x² + x).degree(&x)` is `Some(2)`
  and `coeffs` is `[0, 1, a]` where 0.2 returned `None`.  Rational-coefficient
  results are byte-for-byte unchanged.
- `Ex::solve` on linear and quadratic equations with parametric coefficients
  puts the root (and the quadratic discriminant) into rational normal form:
  `((3r−1)/(j+1) − (r+1)/(2j)).solve(&r)` is `(3*j + 1)/(5*j - 1)` instead of
  a fraction of fractions.
- `Ex::simplify_rational` is now `ratsimp` (one fraction over all variables
  at once, integer-primitive numerator and denominator, positive leading
  denominator coefficient) instead of `together` followed by a per-symbol
  `cancel`.  Same value; nested fractions that 0.2 left uncancelled are
  now cancelled.
- `Display`: a product with a rational coefficient *and* inverse factors is
  printed as one fraction.  `1/2*1/j*(j - 1)` is now `(j - 1)/(2*j)`,
  `4/3*1/pi*sin(3*x)` is `4*sin(3*x)/(3*pi)`, `-1/2*1/(x + 1)` is
  `-1/(2*(x + 1))`, and `x - 3*y*1/z` is `x - 3*y/z`.  Products without an
  inverse factor are unchanged (`1/2*x`), as is `x^(-2)`.

### Added

**Polynomials**

- `poly_ex::Poly` (also `prelude::Poly`) and `Ex::as_poly(&[&gens])`: an
  expression as a sparse polynomial in explicit generators with exact
  rational *or* symbolic coefficients; terms in SymPy's lex-descending
  order.  `Poly::{new, from_terms, zero, one, constant, from_multipoly}`;
  queries `gens`, `num_gens`, `is_zero/is_ground/is_univariate/is_linear/
  is_homogeneous`, `has_rational_coeffs`, `num_terms`, `terms`, `monoms`,
  `coeffs`, `coeff_monomial`, `total_degree`, `degree_in`, `degree_list`,
  `leading_term/leading_coeff/leading_monomial`, `all_coeffs`, `equals`;
  conversion `to_ex`, `to_multipoly`; evaluation `eval` (all generators)
  and `eval_gen` (partial, generator removed); arithmetic `add`, `sub`,
  `mul`, `neg`, `scale`, `pow`, `derivative`, `content_and_primitive`,
  `monic`; `nroots`; `Poly::monomial_basis` and `Poly::coefficient_matrix`
  for turning "goal = Σ λᵢ pᵢ" into an exact linear system; `Display` as
  `Poly(expr, gens…)`.
- `Ex::poly_is_nonnegative_on` / `poly_is_positive_on(var, lo, hi)`: exact
  three-valued sign of a rational-coefficient polynomial on a closed
  interval (square-free part isolates odd-multiplicity roots, Sturm count,
  one sign sample); endpoints may be `±∞`.
- `MultiPoly::{gcd, lcm}` (heuristic GCD, GCDHEU, verified by exact
  division), `integer_content`, `clear_denominators`, `from_terms`,
  `coeff`, `map_coeffs`.

**Simplification**

- `Ex::ratsimp`: rational-function normal form.  `P/Q` over the free
  symbols with every maximal non-rational subexpression (`sin x`, `π`,
  `√x`) treated as an independent indeterminate, `gcd(P, Q)` divided out,
  denominators cleared to integer-primitive parts, leading coefficient of
  `Q` positive.  Idempotent; expressions with `±∞`, `NaN` or unevaluated
  nodes are returned unchanged.

**Linear programming** (`symplex::linprog`)

- `LpProblem` builder (`minimize`/`maximize`, `le`/`ge`/`eq` rows,
  per-variable `bounds`, `free`) and `LpProblem::solve` → `LpSolution
  { status, x, objective, duals, farkas }` with `LpStatus::{Optimal,
  Infeasible, Unbounded}`; `LpSolution::{is_optimal, x_ex}`.  Two-phase
  dense simplex over `Ratio<BigInt>`, Dantzig pivots switching to Bland's
  rule at the first degenerate step (no cycling), pivot cap reported as
  `ComputationFailed`.
- Exact **shadow prices** (`duals`, one per constraint in insertion order,
  `yᵢ = ∂ optimum / ∂ bᵢ`) and exact **Farkas certificates** (`farkas`,
  `Aᵀy`-based inequality proving infeasibility; `None` only when the bounds
  alone are contradictory).  Sign conventions documented in the module docs.
- `linprog(c, A_ub, b_ub, A_eq, b_eq, bounds)` (SciPy-shaped),
  `feasible_nonneg(A, b)` ("is there `x ≥ 0` with `Ax = b`?", exactly),
  `feasible_nonneg_certified` and the column-oriented `nonneg_combination
  (vectors, target)` returning `Feasibility::{Feasible(x), Infeasible {
  farkas }}`, `linprog_matrix(Objective, &c, A_ub, b_ub, A_eq, b_eq)` on
  `Matrix` data with numeric-literal entries, `LpSolution::duals_ex`, a
  one-line `Display` for `LpSolution`, and the literal helpers `q(n, d)`,
  `qi(n)`.
- `prelude` re-exports `LpProblem`, `LpSolution`, `LpStatus`.

**Integer normal forms** (`symplex::normalforms`)

- `hermite_normal_form` (row style, `H = U·A`, unique: positive pivots,
  entries above pivots reduced into `[0, pivot)`, zero rows last),
  `hermite_normal_form_with_transform` → `(H, U)`,
  `column_hermite_normal_form` (`H = A·V`, SymPy / Cohen 2.4.5 convention,
  leading zero columns kept).
- `smith_normal_form` (`diag(d₁, …, dᵣ, 0, …)`, `dᵢ | dᵢ₊₁`) and
  `smith_normal_form_with_transforms` → `(S, U, V)`.
- `integer_nullspace` (a ℤ-basis of `{x ∈ ℤⁿ : Ax = 0}` — generates every
  integer solution, unlike a scaled rational nullspace), `is_unimodular`,
  `lattice_determinant` (index of the column lattice in `ℤᵐ`).
- `Matrix::{hermite_normal_form, smith_normal_form, integer_nullspace}`
  method forms.  Non-integer entries are `InvalidArgument`.

**Matrices**

- Selection: `extract(rows, cols)`, `select_rows`, `select_cols`,
  `delete_row`, `delete_col` (index lists may repeat or reorder; empty or
  out-of-range is `InvalidArgument`).
- Three-valued structure test `is_integer_matrix` (alongside the existing
  `is_zero`).
- Exact numeric conversion: `to_rational_rows`, `to_bigint_rows`,
  `Matrix::from_ratio`, `Matrix::from_bigint`, `Matrix::from_f64_rows`
  (exact dyadic; `NaN`/`∞` rejected).
- `subs_map(&[(&from, &to)])` (simultaneous substitution in every entry),
  `nnz`.

**Number theory**

- `ntheory::{gcd_many, lcm_many}` on `&[BigInt]` (empty list: `0` / `1`;
  early exit at gcd 1; any zero makes the lcm 0), generic `igcd` / `ilcm`
  for any `Into<BigInt>`, and `rational_lcm_of_denominators`.

**Numerical optimisation** (`symplex::optimize`)

- Root finding: `brent_root` (Brent–Dekker), `bisect`, `newton_root`, with
  `RootOpts { xtol, rtol, max_iter }`.
- Minimisation: `nelder_mead`, `minimize_scalar` (Brent), `golden_section`,
  `differential_evolution` (DE/rand/1/bin, Latin-hypercube start,
  Nelder–Mead polish, SplitMix64 seeded by `DeOpts::seed` — fully
  deterministic), with `MinimizeOpts`, `DeOpts` and `MinimizeResult { x,
  fun, iterations, evaluations, converged }`.  An exhausted budget is
  reported through `converged = false`, never by discarding the best point.
- Fitting and helpers: `poly_fit` (column-scaled Householder QR, ascending
  coefficients), `poly_fit_exact` (rational normal equations),
  `linear_fit`, `trapezoid`, `eval_poly`.
- On `Ex`, compiling first: `find_root_bracket[_with]`,
  `minimize_numeric[_with]`, `minimize_scalar_numeric`,
  `minimize_global_numeric`, and `Ex::poly_fit_points` (exact least-squares
  polynomial through rational points).  A stray free symbol is
  `FreeSymbol`, not a silent `NaN`.
- `prelude` re-exports `RootOpts`, `MinimizeOpts`, `MinimizeResult`.

**Examples and tests**

- New examples `polynomials`, `exact_lp`, `integer_lattices`,
  `numeric_optimization`; `readme_snippets` mirrors the new README sections.
- The crate docs list the new modules (`poly_ex`, `linprog`,
  `normalforms`, `optimize`) in the module map.

### Fixed

- `simplify_rational` could not cancel common factors that only appear
  after combining (`(x² − y²)/(x − y)` was returned unchanged) or
  fractions nested inside fractions (`1/(x + 1/y) + 1/(1/x + y)` became
  `(x + 1/x + y + 1/y)/((x + 1/y)*(1/x + y))`); it now returns `x + y` and
  `(x + y)/(x*y + 1)`.
- `solve` returned unsimplified nested fractions for linear and quadratic
  equations whose coefficients are themselves parametric fractions
  (`(1/2*1/j + 1/(j + 1))/(-1/2*1/j + 3/(j + 1))` for the example above).
- `degree`/`coeffs`/`coeff`/`leading_coeff`/`is_polynomial` reported
  "not a polynomial" (`None`/`false`) for polynomials with symbolic
  parameter coefficients such as `a·x² + (a + 1)·x + 3`.

### Infrastructure

- `tests/v03_*` integration suites, one concept per test: `v03_poly_view`,
  `v03_poly_symbolic_coeffs`, `v03_ratsimp`, `v03_linprog` (every `Optimal`
  result checked against the full KKT conditions exactly, every
  `Infeasible` result's Farkas vector verified), `v03_normalforms` (defining
  invariants `H = U·A`, `|det U| = 1`, `S = U·A·V`, divisibility chain,
  `A·k = 0` checked rather than pinned answers), `v03_matrix_ergonomics`,
  `v03_optimize`.
- SymPy 1.14 oracle extended to the 0.3 features (`Poly.terms`/`coeffs`,
  `cancel`/`ratsimp`, `sympy.solvers.simplex`, `hermite_normal_form`,
  `smith_normal_form`) via `tests/fixtures/v03_cross_validation.json`;
  as before, comparisons are numeric or structural, never by printed form.
- Crate, `symplex-macros`, `symplex-build` and `symplex-wasm` at 0.3.0.

## [0.2.0] - 2026-09-18

A large release: complex analysis, definite/improper/numeric integration,
symbolic summation, a public rewrite-rule engine, sets and logic, a C99
backend, linear-system and general solvers, ODE initial-value problems,
recurrences, Berlekamp–Zassenhaus factoring, and a new `factorint`.  The
guiding rule for every change below is *never silently wrong*: operations
that used to guess now return `Err`, an unevaluated node, or `None`.

Measured at release: 91 `ExprNode` variants, ~10,600 `#[test]` functions
(~148K lines of tests), ~167K lines in `src/`, 520 doctests, and a
1,400-fixture SymPy 1.14 oracle with zero numerical disagreements.

### Breaking

**Core / API model**

- `Ex::compile(&[&str])` returns `Result<CompiledFn, SymplexError>` instead of
  `Option`.  `CompiledFn` is `Clone + Send + Sync`, callable as a closure,
  and has `arity()` and `try_call()` (arity-checked).
- `Ex::definite_integral` is replaced by `Ex::integrate_definite` (returns a
  bounded, unevaluated `DefiniteIntegral` node — displayed
  `Integral(f, x, a, b)` — when it cannot decide) and
  `Ex::try_integrate_definite` (`Err(Divergent)` / `Err(ComputationFailed)`).
  The old method could return a wrong finite number for `∫₋₁¹ dx/x²`.
- `Ex::solve` semantics: identities (`x − x = 0`) return
  `Err(InfiniteSolutions)`; contradictions and range violations (`sin x = 2`,
  `eˣ = −1`, `|x| = −1`) return `Err(NoSolution)`.  Results are `eval`'d
  (`asin(1/2)` → `π/6`).
- `Context::solve_system` returns `Result<LinearSolution>` with
  `Unique` / `Parametric { solution, free }` / `Inconsistent` instead of a
  flat vector.
- `polysys::solve_system_ex` returns algebraic (radical) solutions, not only
  rational ones, and `Err(InfiniteSolutions)` for positive-dimensional systems.
- `has_unevaluated()` no longer counts `RootOf` / `RootSum`: they are complete
  algebraic answers.  `try_*` methods therefore succeed on degree ≥ 5 roots.
- `Ex::equals` may now return `Some(false)` (previously only `Some(true)`/`None`).
- `Debug for Ex` prints the expression (`Ex(x^2 + 1)`) instead of internal ids.
- `re`, `im`, `conjugate`, `arg` of a symbol without a realness assumption
  return unevaluated `re(z)`, `im(z)`, `conjugate(z)`, `arg(z)` nodes.  0.1
  silently assumed every symbol real.
- `Digamma(n)` folds for positive integers and half-integers
  (`ψ(1) = −γ`); `d/dx digamma(x)` is `polygamma(1, x)` (was a formal
  derivative).
- `expand()` no longer splits `(x·y)^a` for symbols of unknown sign (unsound
  over ℂ).  Use `expand_power_base(force)` to opt in.
- `Ex::differentiate_finite(var, points, order)` replaces the previous
  finite-difference signature; `finite_diff::{finite_diff_weights,
  apply_finite_diff, …}` are `Ex`-based.
- `FormalPowerSeries` is `Ex`-based (`from_coefficients`, `coefficient`,
  `general_term`, arithmetic) instead of `Ratio`-based.
- `std::iter::Sum` / `Product` for `Ex` **panic on an empty iterator** (there
  is no context to build `0`/`1` in).  Use `Context::sum` / `Context::product`
  or collect into `Option<Ex>`.
- Plotting methods (`plot_data`, `textplot`, `to_svg`, `to_tikz`, `eval_table`)
  return `Result` instead of panicking or producing empty output.
- `SimplifyOpts::trace` is honoured; use `Ex::simplify_traced` to obtain the
  steps.
- `Assumption` gained `ExtendedReal` and the negated variants (`NotPositive`,
  `NotZero`, …); `match` statements on it need updating.

**Matrices**

- `Matrix::{eigenvals, eigenvects, diagonalize, jordan_form, matrix_exp}` take
  no dummy variable; the eigenvalue symbol is internal.  Use `char_poly(&λ)`
  when you want a named variable.
- `Matrix::is_diagonalizable` and `Matrix::is_symmetric` return `Option<bool>`.
- `Matrix::cholesky` and `Matrix::lu` return `Result` (`InvalidArgument` for a
  non-symmetric / non-square matrix, `ComputationFailed` when not positive
  definite).
- `Matrix::minor(i, j)` returns `Result<Ex>` (the determinant of the minor);
  the sub-matrix is `Matrix::minor_matrix(i, j)`.
- `Matrix::from_i64(ctx, rows)` returns `Result` (ragged rows are an error).
- Removed: `add_elementwise`, `sub_elementwise`, `try_identity`, `try_zeros`
  (use `add`/`sub`/`identity`/`zeros`).
- `StateSpace::poles()` takes no variable.
- `vector::{is_conservative, is_irrotational, is_solenoidal}` return
  `Option<bool>` (three-valued) instead of `bool`.

**Sets & logic**

- `SetEx::contains(&elem)` is set membership returning `Option<bool>`
  (previously structural containment).
- `BoolEx::eval` folds relations through the assumption system
  (`pos > 0` → `True` for a positive-assumed symbol).

**Fixed behaviour that may change results**

- `fourier_series` (and the new `fourier_series_on`) returns correct closed
  forms for `|x|`, `sign(x)` and piecewise inputs (coefficients are exact
  definite integrals).
- One-sided limits fall back to a two-sided `Limit` node when unevaluated.
- Factoring is no longer limited by `MAX_KRONECKER_DEGREE`: `factor` uses
  Berlekamp–Zassenhaus and handles any degree.
- `OdeType` gained `NthOrderLinearConstCoeff`, `Clairaut`, `Riccati`,
  `HomogeneousCoefficient`, `IntegratingFactor` (exhaustive matches break).

### Added

**Core nodes and constants**

- Complex analysis: `Re`, `Im`, `Conjugate`, `Arg` nodes with
  `Ex::{re, im, conjugate, arg, as_real_imag, expand_complex, polar,
  abs_squared, is_real_valued}`; conjugation distributes over `Add`/`Mul`/
  integer powers and commutes with real-analytic functions at construction.
- Constants `EulerGamma`, `Catalan`, `GoldenRatio`
  (`Context::{euler_gamma, catalan, golden_ratio}`) and
  `Context::complex_infinity()` (`zoo`; `1/0` evaluates to it).
- Special functions `si`, `ci`, `ei`, `li`, `zeta`, `polygamma(n, x)`,
  `kronecker_delta(i, j)` with exact values (`ζ(2m)`, `ζ(0)`, `ζ(−n)`,
  `ψ⁽ⁿ⁾(1)`, `Si(∞)`), derivative rules and arbitrary-precision `evalf`.
- `evalf` for `besseli` / `besselk` and orthogonal polynomials of any degree;
  derivative rules for Bessel functions and orthogonal polynomials.
- The parser accepts the new names (`re`, `im`, `conjugate`/`conj`, `arg`,
  `si`, `ci`, `ei`, `li`, `zeta`, `polygamma`, `kronecker`, `zoo`).
- `ExprNode::DefiniteIntegral(body, var, lo, hi)`: a bounded unevaluated
  integral (`Integral(f, x, a, b)`, LaTeX `\int_a^b f\,dx`).  It round-trips
  through Display/parse/JSON, binds its variable for `free_symbols`/`subs`,
  differentiates by the Leibniz rule, evaluates numerically via Gauss–Kronrod
  quadrature in `eval_f64`, and is resolved innermost-out by
  `integrate_definite` / `Ex::eval_integrals`.  Also `Ex::definite_integral_node`,
  `Ex::is_definite_integral`.

**Numeric backends**

- `compile()` covers every numerically evaluable node: Γ, lnΓ, ψ, erf/erfc,
  Lambert W, Beta, factorials and binomials, Bessel J/Y/I/K, orthogonal
  polynomials, integer sequences (`fibonacci`, `lucas`, `harmonic`, …),
  `min`/`max`/`floor`/`ceiling`/`sign`/`heaviside`/`atan2`, piecewise and
  boolean conditions.
- `Ex::compile_many` → `CompiledFnVec` (shared CSE across outputs;
  `call`, `call_vec`, `try_call`, `arity`, `len`).
- `to_rust_fn` embeds a self-contained `mod symplex_rt` runtime with only the
  special-function helpers the expression uses.
- `CodegenOptions::{use_mul_add, checked_domain, emit_runtime}` and
  `CodegenOptions::{runtime_module, c_runtime}` for multi-function files.
- **C99 backend**: `Ex::to_c_fn` / `to_c_fn_with_options`: `#include <math.h>`,
  `static inline symplex_*` helpers, `fma`, `float` precision with
  `f`-suffixed calls, `assert` domain checks, piecewise → ternary chains.
- Deterministic CSE (post-order numbering, cheap-node threshold, no boolean
  temporaries) and `Ex::cse_many`.

**Integration**

- `Ex::integrate_definite` / `try_integrate_definite`: interior
  singularities, infinite bounds, endpoint singularities via one-sided
  limits, symmetry shortcuts, `Piecewise` / `Abs` / `Sign` / `Heaviside` /
  `DiracDelta` integrands, and a ~30-entry table of classical improper
  integrals (Gaussian, Dirichlet, Fresnel, `x/(eˣ−1)`, `ln x`, Γ, …) with
  symbolic parameters under assumptions.
- `Ex::integrate_numeric` / `integrate_numeric_with` (adaptive Gauss–Kronrod
  G7/K15, `QuadOpts`, infinite bounds); `definite::quadrature` for plain
  `Fn(f64) -> f64`.
- Residues at poles of any order; `Ex::residue_at_infinity`.
- ~20 new indefinite-integration families.

**Summation and series**

- `Ex::summation` / `try_summation`, `product_over` / `try_product_over`,
  `hypergeometric_ratio`: Faulhaber sums of any degree, telescoping,
  binomial sums (`Σ P(k)·C(n,k)·xᵏ`), p-series (`ζ(2m)` exact, `zeta(p)` for
  odd `p`, Catalan's constant), power-series recognition (`Σ xᵏ/k! = eˣ`),
  Gosper with a polynomial-time normal form, infinite products.
- `Ex::is_convergent` / `is_absolutely_convergent` (decisive answers only).
- `Ex::series_at_infinity` / `series_at_neg_infinity`.
- `FormalPowerSeries`: lazy exact coefficients, `general_term`, `add`, `mul`,
  `compose`, `inverse`, `reversion`, `derivative`, `integral`.
- `Ex`-based finite differences (`finite_diff_weights`, `apply_finite_diff`,
  `equispaced_grid`, `Ex::differentiate_finite`).

**Solving**

- `Ex::solve_general` → `GeneralSolution` (periodic families with a fresh
  integer parameter, `instance(k)`).
- `linsolve`, `linsolve_matrix`, `LinearSolution`, `ZeroForm` (accepts `Ex`
  or `Equation`), symbolic coefficients, parametric solutions.
- Algebraic solutions in `polysys::solve_system_ex`.
- `solve_numeric_system` / `solve_numeric_system_with` (damped Newton,
  `NewtonOpts`).
- `Ex::solve_ode_ivp`, nth-order constant-coefficient ODEs, Clairaut,
  Riccati (`Ex::solve_riccati`), `ode::solve_ode_system_ivp`.
- `rsolve::rsolve_linear` / `rsolve_first_order` for recurrences.
- Inequalities with absolute values (`|x − 1| < 2`).

**Sets and logic**

- `SetEx::{simplify, eval, difference, symmetric_difference,
  absolute_complement, contains, is_subset, is_superset, is_disjoint,
  is_empty, inf, sup, measure, boundary, closure, interior, is_open,
  is_closed, as_intervals, as_finite_set, to_condition}`; `Ex::is_in`.
- `reduce_inequalities(&[BoolEx], &x) -> Result<SetEx>` and
  `BoolEx::solve_for`.
- `BoolEx::{simplify, to_nnf, to_cnf, to_dnf, is_tautology,
  is_contradiction, satisfiable, atoms, truth_table}` (DPLL with unit
  propagation; declared assumptions respected).
- `Ex::piecewise_simplify`.
- `Props::EXTENDED_REAL`, `Assumptions::implies`, `Assumption::negate`,
  `Display for Assumptions`.

**Matrices, vectors, quaternions, control**

- Eigen family without a dummy variable; `eigenvals_with_multiplicity`,
  `char_poly_coeffs`, `matrix_exp_t`, `matrix_pow_symbolic`, `matrix_sqrt`.
- `RootOf` eigenvalues for irreducible cubics/quartics without a compact
  radical form (exact, numerically evaluable, no Cardano swell);
  `EXPRESSION_BUDGET` swell guard.
- `qr`, `gram_schmidt`, `ldl`, `hessian`, `wronskian`, `adjoint`,
  `is_hermitian`, `is_orthogonal`, `is_unitary`, `is_positive_definite`,
  `is_positive_semidefinite`, `is_nilpotent`, `is_skew_symmetric`,
  `is_upper_triangular`, `is_lower_triangular`, `is_diagonal`, `is_identity`,
  `is_zero`, `norm_1`, `norm_inf`, `norm_p`, `solve_least_squares`,
  `rowspace`, `left_nullspace`.
- Ergonomics: `Index<(usize, usize)>` / `IndexMut`, `TryFrom<Vec<Vec<Ex>>>`,
  scalar operators on both sides (`2 * &m`, `&m * 2`, `m / 2`), `Neg`,
  `col`, `diagonal`, `submatrix`, `set`, `iter`, `to_vec`, `vec`, `eval_f64`,
  `equals`, `map_indexed`, `block_diag`, `hadamard`.
- `Quaternion`: arithmetic operators, `slerp`, `exp`/`ln`/`pow`,
  `rotate_vector`, `to_euler`/`from_euler`, `from_rotation_matrix`,
  `to_axis_angle`.
- `vector::CoordinateSystem` with cylindrical/spherical `gradient_in`,
  `divergence_in`, `curl_in`, `laplacian_in`; `directional_derivative`,
  `line_integral_scalar`, `line_integral_vector`, `scalar_potential`.
- `TransferFunction::to_state_space`, `StateSpace::to_transfer_function`.

**Number theory and polynomials**

- Berlekamp–Zassenhaus `factor` for any degree; multivariate `factor_all`
  (Kronecker substitution); `factor_list`, `factor_list_all`.
- `Ex` polynomial algebra: `resultant`, `discriminant`, `sqf_list`,
  `square_free_part`, `is_squarefree`, `is_irreducible`, `poly_div`,
  `poly_quo`, `poly_rem`, `poly_gcdex`, `decompose`, `content_primitive`,
  `leading_coeff`, `monic`, `poly_compose`, `poly_shift`, `poly_reverse`,
  `poly_interpolate`, `count_real_roots`, `roots_count_real`,
  `real_roots_isolate`, `nroots`.
- `ntheory::factorint` (Pollard–Brent rho with Montgomery `u128` arithmetic
  + ECM for `BigInt`), BPSW `isprime`, `is_probable_prime`,
  `jacobi_symbol`, `kronecker_symbol`, `is_quad_residue`, `sqrt_mod`,
  `sqrt_mod_all`, `discrete_log`, `n_order`/`multiplicative_order`,
  `primitive_root`, `is_primitive_root`, `primepi`, `prime`, `primerange`,
  `carmichael_lambda`, `perfect_power`, `is_mersenne_prime`,
  `continued_fraction`, `continued_fraction_periodic`,
  `continued_fraction_convergents`, `egyptian_fraction`, `digits`,
  `is_palindromic`.
- Sequences: `fibonacci`, `lucas`, `bernoulli`, `euler_number`, `harmonic`
  (ntheory); `bell`, `catalan`, `derangements`, `partitions` iterator
  (combinatorics); symbolic `Ex::{fibonacci, lucas, bell, catalan_number,
  bernoulli_number, euler_number, harmonic, partition_count}`.
- `diophantine::{linear_diophantine, linear_diophantine_n, pell,
  pell_solutions, pell_negative, sum_of_two_squares, sum_of_four_squares,
  pythagorean_triples, frobenius_number}`.

**Simplification and rules**

- Public rewrite-rule engine: `Rule` (template, guarded, closure RHS),
  `RuleSet`, `Bindings`, `RewriteOpts`, `RewriteStrategy`, `Step`;
  `Ex::{rewrite, rewrite_once, rewrite_traced, rewrite_with,
  rewrite_with_traced, simplify_with_rules, simplify_traced}`;
  `RuleSet::standard(&ctx)`.
- AC matching for `Add`/`Mul` with `rest__` sequence wildcards and a
  bounded backtracking budget; `rule!` macro rules usable via
  `Rule::from_macro_rule` / `RuleSet::from_macro_rules`.
- `sqrtdenest`, `signsimp`, `powdenest(force)`, `expand_with(ExpandOpts)`,
  `expand_power_base`, `expand_power_exp`, `expand_multinomial`,
  `log_combine_with`, `expand_log_with`, `nsimplify`,
  `nsimplify_with_constants`, `rcollect`, `collect_const`,
  `separate_vars_additive`, `separate_vars_dict`, `subs_algebraic`.
- 15 trig/hyperbolic identity rules; `vars!` macro (alias of `syms!`).

**Transforms and limits**

- `Ex::{limit_dir, limit_left, limit_right}` + `try_` twins and
  `Direction`; Gruntz work budget; many limits fixed or newly solved.
- `fourier_transform` / `fourier_transform_with` /
  `inverse_fourier_transform[_with]` with `FourierConvention`
  (non-unitary angular, unitary angular, ordinary).
- `mellin_transform` (returns the fundamental strip as a `BoolEx`) and
  `inverse_mellin_transform`.
- Laplace table extensions (`f(t)/t`, Bessel, `t^n e^{−at}`, …), inverse
  extensions (`1/√s`, shifted `e^{−as}F(s)`), `laplace_initial_value`,
  `laplace_final_value` (`Err(Divergent)` for unstable poles).
- `FourierSeries` with `fourier_series_on(var, lower, upper, n)`,
  `coefficient_a/b/c`, `truncate`, `omega0`.
- Z-transform table and inverse extensions.

**Ergonomics**

- `Context::{from_f64 (exact dyadic), from_f64_approx, from_f64_nice,
  from_bigint, from_ratio, from_i128, from_u64, rational_str, decimal_str,
  complex, symbols, symbols_indexed, apply, sum, product}`.
- Operators with `f64`, `i32`, `u32`, `u64`, `i128`, `BigInt`, `Ratio`;
  compound assignment (`+=`, `*=`, …); `ToEx` and `Scalar` traits.
- `Ex::{as_rational, as_bigint, as_i64, compare_numeric, is_less_than,
  is_greater_than, probably_equal, eval_at, subs_map_with}`.
- `Equation` accessors (`lhs`, `rhs`, `swap`, `to_zero_equation`, `to_expr`),
  arithmetic with scalars and equations, `solve` / `solve_for` /
  `solve_or_empty`, `subs`, `is_satisfied`, `is_identity`, `apply`.
- `base::numeric::{f64_to_ratio_exact, f64_to_ratio_approx}`.
- `symplex-wasm`: `Session` (persistent context with `define`) and a full
  stateless API (`integrate_definite`, `to_c_fn`, `eval_decimal`, …).
- `symplex-build`: exact DH parameters via `from_f64_approx`,
  `RobotArmBuilder::generate_fk_matrix`, `"fk_matrix"` in TOML configs.

### Fixed

**Found by the new SymPy oracle and fixed before release**

- Inequality solver: poles are now sign-change points, both-negative
  branches are kept, and the natural domain is intersected in
  (`1/x > 2` → `(0, 1/2)`, `(x−1)/(x+1) ≥ 0` → `(−∞,−1) ∪ [1,∞)`,
  `√x < 2` → `[0, 4)`).  Undecidable cases return `ConditionSet`, never a
  guess.
- `solve_system_ex` returned non-solutions (Cardano emitted `cbrt` of a
  negative radicand, evaluated on the principal branch) and `Ok([])` for
  biquadratic eliminants (Ferrari `0/0`).  Every returned tuple is now
  verified against all equations at 30 digits.
- `rsolve_linear` hung on irrational cubic characteristic roots; roots are
  now `RootOf` values and constant fitting is budgeted.
- `series_at_infinity(atan x)` returned the garbage `atan(zoo)`; constant
  terms are now limits, and unevaluable results are formal `Series` nodes.
- `evalf` Bessel `J`/`Y` were wrong for `x ≳ 12` (doubled leading Hankel
  term, sign error in the recurrence, premature series→asymptotic switch);
  now 25+ digits at any `x`.
- `eval()` of `Piecewise` selected a later `True` branch over an earlier
  undecided one.
- `0 · oo` / `0 · zoo` were order-dependent (`nan` vs `0`).
- Debug-build panic (nested `Mul`) when multiplying numeric radicals such as
  `(√6/3)·(√3/3)`.
- Display of rational/negative bases: `(2/3)^x` printed as `2/3^x`.
- `free_symbols` counted bound index variables of `Sum`/`Product`/`RootOf`/
  `RootSum`/`ConditionSet`/`DefiniteIntegral` as free.
- `eval_decimal` truncated instead of rounding the last digit.
- `eval_f64` on compound expressions with free symbols reported a cache
  miss instead of `FreeSymbol { name }`.
- Assumption lattice: `oo` is positive, extended-real and infinite but not
  real/finite; queries are order-independent; contradictory declarations
  panic with a clear message.
- `nroots` missed real roots of odd/even polynomials (mirror-symmetric Aberth
  start points); real roots are snapped only after an exact Sturm count.
- Expression construction was proportional to tree size (sort keys
  concatenated whole subtrees); keys are now bounded and hashed, and the
  debug canonical-form verifier is iterative (deep expressions no longer
  overflow the stack).
- `sqrt(<large integer>).eval()` trial-divided to `√n` (14 s); square factors
  are now found via bounded `factorint`.  Radical normal form unified:
  `√(1/2) = 1/√2 = √2/2`, `√(4/9) = 2/3`, `∛54 = 3∛2`.
- `Context::rational(p, 0)` panicked; it now returns `zoo` (`nan` for
  `0/0`).
- `abs(3 + 4i)` folds to `5`.
- Generated `no_std` code called `libm::abs` (does not exist); now `fabs`.
  `symplex-build` emitted the `symplex_rt` runtime once per function.
- `expr_type()` reported `RootOf` as unevaluated; `piecewise_simplify`
  ignored assumption-decided conditions; `BoolEx::simplify` gained
  consensus.
- Parser: `binomial`, `beta`, `bessel{j,y,i,k}`, `cot/sec/csc/coth/sech/csch`,
  `min`/`max`, `polygamma`, `Sum`/`Product`, `Integral(f, x[, a, b])`, `n!`.
- `expr!(ctx, 2^10)` (purely numeric bodies) now compiles.

**Other**

- `∫₋₁¹ dx/x²` and other integrals across interior poles no longer return a
  finite value.
- `fourier_series` coefficients for `|x|`, `sign(x)` and piecewise inputs.
- Sign error in shifted alternating half-integer p-series.
- Gosper: dispersion via a bounded gcd scan instead of resultant
  interpolation (`Σ k⁸·2ᵏ` from 23 s to 26 ms); certificate degree cap.
- Gruntz limits: wrong answers for several `exp`/`ln` towers; work budget
  prevents hangs.
- Binomial series for large `|n|`; series at hidden valuations (`1/x` at
  order 1).
- `matrix_exp` for numeric complex eigenvalues (`sin(−1)` parity);
  Jordan chains for repeated eigenvalues; nilpotent blocks.
- Real-root parity in the polynomial root counter.
- `factor_zassenhaus` on non-square-free input.
- Log-to-real exactness guard; polar-form complex powers.
- Definite integrator rejects leaked limit-engine dummies; assumption-decided
  `Piecewise` branches.
- `eval_f64_with` reports `FreeSymbol` for unbound symbols.

### Infrastructure

- CI rewritten: fmt / clippy / test / UI compile-fail (pinned toolchain
  `1.95.0`, `TRYBUILD=overwrite` to refresh snapshots) / sub-crates
  (`symplex-macros`, `symplex-build`, `symplex-wasm` native + `wasm32`, fuzz
  build) / docs (`cargo doc -D warnings` + `mdbook build`) / MSRV `1.93.0` /
  every non-interactive example run.
- GitHub Pages deployment of the mdBook.
- `tests/v02_*` integration suites per area, one concept per test and
  each under a few seconds; SymPy 1.14 oracle (`tests/fixtures/*.json`,
  ~1,400 fixtures, one `#[test]` per subcategory, strict-xfail known-bug
  tables); `tests/README.md` documents the layout and how to regenerate
  fixtures.
- Crate, `symplex-macros`, `symplex-build` and `symplex-wasm` at 0.2.0.

## [0.1.0]

Initial public release: exact arithmetic on `Ratio<BigInt>`, hash-consed
expression arena, differentiation, indefinite integration (Risch,
Rothstein–Trager, Lazard–Rioboo–Trager, heuristics), Gruntz limits,
series, Laplace and Z-transforms, polynomial solving through quartic with
`RootOf`/`RootSum`, Gröbner bases, 13 ODE classes, symbolic matrices with
eigenvalues/Jordan form/matrix exponential, algebraic number fields ℚ(α),
Rust code generation with CSE, compile-time dimensional analysis, and the
`symplex-macros`, `symplex-build` and `symplex-wasm` companion crates.

[0.3.0]: https://github.com/cgorski/symplex/releases/tag/v0.3.0
[0.2.0]: https://github.com/cgorski/symplex/releases/tag/v0.2.0
[0.1.0]: https://github.com/cgorski/symplex/releases/tag/v0.1.0