feat(num): real-algebraic number kernel — replace the quadratic Ext tower #19

Merged

toph merged 9 commits from feat/real-algebraic-kernel into main

2026-06-30 12:58:29 +00:00

toph commented

2026-06-30 12:55:34 +00:00

Owner

Slice 1 of axiom 7 (Justin ⑦, the Beloch fold): replaces Num's quadratic Ext tower with an exact real-algebraic kernel, so creases of degree ≤ 3 — including the casus-irreducibilis cubics axiom 7 needs — become representable. No .bel surface change; axioms 1–6 are unchanged in behaviour.

New lib/poly.ml: ℚ-polynomials — arithmetic, Sylvester resultant, Euclidean gcd/squarefree, Sturm sequences, real-root isolation. [bpr2006]
lib/num.ml rewritten: Rat of Q.t | Alg { poly; lo; hi } — the unique real root of a squarefree ℚ-polynomial in an isolating rational interval. Arithmetic builds the result's defining polynomial by resultant-via-interpolation (Alg±Rat/Alg×Rat fast paths); sqrt via poly(y²); exact sign/compare/equal by interval refinement; new real_roots. The Rat fast-path keeps axioms 1–4 in ℚ.
Public Num interface frozen (+ real_roots), so geom/isometry/fold_state/fold_emit/eval compile unchanged.
ADR 0012 supersedes 0010; bpr2006 (Basu–Pollack–Roy) added to the bibliography.

The casus irreducibilis is why a Cbrt generator won't do — three real roots that aren't real radicals — so the kernel stays on the real line via defining-polynomial + isolating interval, no complex arithmetic. Cost: √-heavy axioms 5/6 lose the closed-form a+b√d speed; correctness over speed, as ADR 0010 already bargained.

108/108 tests pass. Next slice: the axiom 7 statement surface (map .p onto --d and .q onto --e) on top of this kernel.

Design: docs/superpowers/specs/2026-06-30-real-algebraic-kernel-design.md

Slice 1 of axiom 7 (Justin ⑦, the Beloch fold): replaces `Num`'s quadratic `Ext` tower with an exact real-algebraic kernel, so creases of degree ≤ 3 — including the casus-irreducibilis cubics axiom 7 needs — become representable. No `.bel` surface change; axioms 1–6 are unchanged in behaviour. - New `lib/poly.ml`: ℚ-polynomials — arithmetic, Sylvester resultant, Euclidean gcd/squarefree, Sturm sequences, real-root isolation. `[bpr2006]` - `lib/num.ml` rewritten: `Rat of Q.t | Alg { poly; lo; hi }` — the unique real root of a squarefree ℚ-polynomial in an isolating rational interval. Arithmetic builds the result's defining polynomial by resultant-via-interpolation (`Alg±Rat`/`Alg×Rat` fast paths); `sqrt` via `poly(y²)`; exact `sign`/`compare`/`equal` by interval refinement; new `real_roots`. The `Rat` fast-path keeps axioms 1–4 in ℚ. - Public `Num` interface frozen (+ `real_roots`), so `geom`/`isometry`/`fold_state`/`fold_emit`/`eval` compile unchanged. - ADR 0012 supersedes 0010; `bpr2006` (Basu–Pollack–Roy) added to the bibliography. The casus irreducibilis is why a `Cbrt` generator won't do — three real roots that aren't real radicals — so the kernel stays on the real line via defining-polynomial + isolating interval, no complex arithmetic. Cost: √-heavy axioms 5/6 lose the closed-form `a+b√d` speed; correctness over speed, as ADR 0010 already bargained. 108/108 tests pass. Next slice: the axiom 7 statement surface (`map .p onto --d and .q onto --e`) on top of this kernel. Design: `docs/superpowers/specs/2026-06-30-real-algebraic-kernel-design.md`

toph added 9 commits

2026-06-30 12:55:35 +00:00

docs(spec): real-algebraic number kernel — replace the quadratic Ext tower 4f55ed2bd5

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

docs(plan): real-algebraic kernel — implementation plan (slice 1) fa3e63ccfc

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

feat(poly): univariate ℚ-polynomials — core arithmetic + compose e34b89f594

feat(poly): divmod, Sylvester resultant, gcd, squarefree part e37c93255e

feat(poly): Sturm sequences, real-root counting and isolation e52825617e

feat(num): real-algebraic kernel — poly+interval, retire the Ext tower 9ac8573e2f

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

fix(num): tighten squaring-shortcut guard to provably-same value 3ef94d54ee

docs(num): ADR 0012 real-algebraic kernel, bpr2006, spec + journal 1040982d95

refactor(num): DRY product enclosure, document sqrt floor + squaring shortcut fe7b011ca0

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

toph merged commit 35ec244ed9 into main

2026-06-30 12:58:29 +00:00

toph referenced this pull request from a commit

2026-06-30 12:58:30 +00:00

feat(num): real-algebraic number kernel — replace the quadratic Ext tower (#19)

No reviewers

No labels

No milestone

No project

No assignees

1 participant

Notifications

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference

toph/beloch!19

No description provided.

Rows
Columns