symplex 0.8.0

Exact symbolic mathematics for Rust: calculus, summation, solving, linear algebra, transforms, compile-time dimensional analysis, and Rust/C code generation
Documentation
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
# 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.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