polyfrac

Exact polynomial and rational-function arithmetic over ℚ, with Sturm-sequence real-root counting. No floating point anywhere.

Why this exists

Testing a parameter at chosen values cannot establish that a property holds everywhere in a range — a crossing may sit between two samples, and no sampling density fixes that. Interval arithmetic gives you a conservative bound; a numerical root-finder gives you an approximate answer with an error term. Neither gives you an integer.

Sturm's theorem does: the exact count of distinct real roots in an interval, computed by counting sign changes over rational arithmetic. Zero roots plus a known sign at one endpoint settles the sign for the whole continuum. That is the difference between "we tested 10,000 points" and "there is no crossing", and it is what you need if the answer goes into a specification.

Zero dependencies. Pure standard library (fractions). ~390 lines you can read in one sitting.

Install

# from GitHub (PyPI release pending)
pip install "polyfrac @ git+https://github.com/nickharris808/polyfrac.git"

pip install polyfrac does not work yet — the package is not on PyPI. Install from GitHub as shown above. The distribution builds and is twine check-clean, with no unpublished dependencies, so it is ready to upload whenever that happens.

30-second quickstart

from fractions import Fraction
from polyfrac import Poly, count_roots, positive_on

p = Poly.from_roots([1, 2, 3])         # (x-1)(x-2)(x-3)

count_roots(p, 0, 4)                   # 3   — exactly three real roots in (0, 4]
count_roots(p, 0, Fraction(3, 2))      # 1   — exactly one, namely x = 1
count_roots(p, 4, 10)                  # 0   — none out here

positive_on(Poly([-1, 1]), 2, 5)       # certificate that x - 1 > 0 on (2, 5]
# {'endpoint_a': '2', 'endpoint_b': '5', 'P_a': '1', 'P_b': '4',
#  'n_roots_in_interval': 0, 'positive_on_interval': True}

Intervals are half-open, (a, b] — left-exclusive, right-inclusive — which is the convention Sturm's theorem states most cleanly. Repeated roots count once: count_roots counts distinct roots.

Worked example — certifying a bound over a whole interval

Suppose a guarded procedure has failure probability p/500 and an unguarded baseline has 3p/5, where p ∈ (0, 1] is an environment parameter you do not control. Does the guarded procedure meet a target of 1/20 for every p, or only for the ones you happened to test?

from fractions import Fraction
from polyfrac import Poly, count_roots, positive_on

target   = Fraction(1, 20)
guarded  = Poly([0, Fraction(1, 500)])     # p/500
baseline = Poly([0, Fraction(3, 5)])       # 3p/5

# Does target - guarded(p) stay positive on the whole interval?
positive_on(Poly([target]) - guarded, 0, 1)["positive_on_interval"]
# True  -> the guarded procedure meets the target for EVERY p in (0, 1]

# The baseline does not. Where exactly does it cross?
count_roots(Poly([target]) - baseline, 0, 1)      # 1  -> exactly one crossing
(Poly([target]) - baseline).eval(Fraction(1, 12)) # 0  -> the crossing is exactly p = 1/12

That last line is the point: the crossing is reported as the exact rational 1/12, not as 0.0833333.... You can put it in a specification.

Rational functions and linear systems

PolyFrac is a ratio of two Poly, kept in lowest terms, and gauss_solve solves linear systems whose entries are rational functions of the parameter. This is what you need to solve a parameterised Markov chain symbolically — the hitting probability comes out as an exact N(p)/D(p) rather than as a number for one chosen p.

from polyfrac import Poly, PolyFrac, gauss_solve

one = PolyFrac(Poly([1]), Poly([1]))
P   = PolyFrac(Poly([0, 1]), Poly([1]))    # the parameter p
(h,) = gauss_solve([[one]], [P])           # solve 1*h = p
# h is exactly p, as a rational function

API

Name	What it does
Poly(coeffs)	Dense univariate polynomial, Fraction coefficients, ascending order
Poly.from_roots(rs)	The monic polynomial with exactly those roots
Poly.const, Poly.x	Constant and identity constructors
+ - * neg scale divmod gcd derivative eval degree is_zero	Exact polynomial arithmetic
PolyFrac(num, den)	Rational function, auto-reduced
gauss_solve(A, b)	Gaussian elimination over the field of rational functions
sturm_chain(P)	The squarefree Sturm chain
count_roots(P, a, b)	Exact integer count of distinct real roots in (a, b]
positive_on(P, a, b)	Certificate dict: endpoints, values, root count, verdict

Why not SymPy?

SymPy will do all of this and much more. polyfrac exists for the case where you want the root count and nothing else, with no dependency, no import cost, and a source file short enough to audit before you trust it in a certification path.

Honest scope

Exactness is enforced at the boundary, not merely intended. Passing a float raises InexactInput rather than being converted, because 0.1 is not one tenth — it is 3602879701896397/36028797018963968, and exact arithmetic on it produces an exact answer to a question you did not ask. Use Fraction(1, 10), the string "0.1", or the explicit Poly.from_floats() when a float really is the value you mean.

>>> Poly([0.1])
InexactInput: refusing the float 0.1: it is a binary approximation ...
>>> Poly(["0.1"]).c[0]
Fraction(1, 10)

What it proves. An exact count of distinct real roots in the half-open interval (a, b], and an exact sign certificate over an interval. No sampling, no tolerance, no numerical root finding — the count comes from sign changes in a Sturm chain over exact rationals.

What it does not prove.

• Univariate only, over ℚ. For multivariate sign conditions you want cylindrical algebraic decomposition, which this package does not implement.
• Multiplicities are not reported. Poly.from_roots([2, 2, 2]) has one distinct root.
• Irrational and complex roots are outside the interval arithmetic entirely; only real roots at rational-bounded intervals are counted.
• The interval convention is half-open (a, b] — the left endpoint is excluded and the right is included. Off-by-one here is silent, so it is asserted in the test suite.
• gauss_solve requires a non-singular system; a singular one raises rather than returning a value.
• The zero polynomial raises. It is zero at every point, so no finite root count exists, and returning 0 would be a confident wrong answer.

Troubleshooting

InexactInput: refusing the float 0.1. Deliberate. 0.1 is not one tenth in binary, so exact arithmetic on it answers a question you did not ask. Use Fraction(1, 10), the string "0.1", or Poly.from_floats([...]) if the binary value really is what you mean. This applies to interval bounds too — a float a or b silently shifts what is being certified.

ValueError: need a < b. The interval is empty or reversed. Bounds are not sorted for you, because swapping them would answer a different question than the one asked.

ValueError: the zero polynomial is zero at every point. It has infinitely many roots in any interval, so there is no finite count to return. 0 would be a confident wrong answer.

count_roots returned fewer roots than I expected. It counts distinct roots. Poly.from_roots([2, 2, 2]) has one. Multiplicities are not reported.

A root exactly at an endpoint is or is not counted. The interval is half-open (a, b] — left excluded, right included. count_roots(Poly.from_roots([2]), 2, 5) is 0; count_roots(Poly.from_roots([2]), 0, 2) is 1.

positive_on says False but the polynomial looks positive. It certifies over the whole interval. One root inside is enough to refuse, even if both endpoints are positive. Check n_roots_in_interval in the returned dict.

gauss_solve raised instead of returning. The system is singular over the field of rational functions, so there is no unique solution to return.

FAQ

"Why not SymPy?" SymPy will do all of this and much more, and if you already depend on it, use it. polyfrac exists for the case where you want the root count and nothing else, with no dependency, no import cost, and a source file short enough to audit before you trust it in a certification path.

"Refusing floats is annoying. Why not just convert them?" Because 0.1 is not one tenth — it is 3602879701896397/36028797018963968 — and exact arithmetic on it produces an exact answer to a question you did not ask. Silently converting would make that failure invisible, which is worse than a wrong answer you can see. Fraction(1, 10), the string "0.1", and Poly.from_floats() are all one keystroke away, and each says which value you meant.

"Is Sturm's theorem really exact, or is this just high precision?" Exact. Every coefficient is a Fraction, every operation is rational arithmetic, and the answer is an integer obtained by counting sign changes. There is no tolerance parameter anywhere in the package, because there is nothing for one to control.

"Zero roots in the interval — does that mean the polynomial is positive there?" Only with a sign at one endpoint, which is why positive_on returns both: n_roots_in_interval and P_a/P_b. Zero roots plus a known sign settles the sign for the whole continuum. Zero roots alone settles nothing about which side.

"It counted fewer roots than the polynomial has." It counts distinct roots. Poly.from_roots([2, 2, 2]) has one. Multiplicities are not reported, and the squarefree Sturm chain is why.

"Can I use this for two parameters?" No. It is univariate over ℚ. Multivariate sign conditions need cylindrical algebraic decomposition, which this does not implement and will not — that is a genuinely different and much larger piece of software.

"Is it production-ready?" Yes. Small, exact, no dependencies, and it refuses inexact input rather than silently approximating. Of everything in this portfolio it is the piece with the least to qualify.

"Something here gave me a confident answer that was wrong." Worth an issue rather than a workaround, and please include the polynomial and the interval. An exact method returning a wrong integer is the most serious failure this package can have.

Performance

Measured on an M-series laptop, CPython 3.11, on Poly.from_roots(range(1, d+1)) over (0, d+1] — d distinct roots, the worst case for the chain:

degree	count_roots
10	~0.6 ms
20	~2.1 ms
40	~8.7 ms

Cost is dominated by the Sturm chain, which is quadratic in the degree, and by Fraction growth in the coefficients — so a polynomial with large rational coefficients costs more than its degree suggests. Nothing here has needed optimising; if you hit a case that is slow, it is worth reporting rather than working around.

Tests

pip install -e ".[test]" && pytest

$ pytest -q
....................................................................     [100%]
68 passed in 0.36s

68 tests, including the worked example above and explicit checks that the arithmetic is exact ((1/3) * 3 == 1, not 0.9999999999999999). One asserts this README's own test count against pytest --collect-only, so the badge cannot drift.

numpy is a test-only extra and does not touch the zero-dependency runtime. It is required rather than optional on purpose: the differential test against an independent root finder used to skip silently when numpy was absent, which it was on every CI platform — leaving the most valuable check in this suite running nowhere.

Where this came from

polyfrac was extracted from a formal-methods system that certifies reliability orderings over a continuum of environment parameters — the worked example above is a stripped-down version of what it does for real. The arithmetic is here under MIT. The certification pipeline built on it, and the models it runs against, are the commercial offering.

The portfolio

minicheck	The engine: an explicit-state model checker with a CLI. Shortest counterexamples, no required dependencies.
protocol-bench	Published IEEE 802.11 / 3GPP procedures with ground-truth verdicts. A claimed detection must replay.
specforge	A benchmark that cannot be memorised — ground truth is computed by the checker, not written down.
minicheck-mcp	The checker as an MCP server, so an agent can verify a state machine instead of guessing.
minicheck-action	Model-check every spec in a repo, in CI. Diagrams in the PR, SARIF in the Security tab.
protocol-bench-action	Score a submission in CI and fail the build if a claimed detection cannot be proved by replay.
failclosed	Default-deny ASGI middleware: a gated endpoint succeeds only on an affirmative verdict.
polyfrac ← you are here	Exact polynomial and rational-function arithmetic over ℚ with Sturm real-root counting. Zero deps.
the docs site	The front door: why a verdict you cannot check is not a verdict, and how these compose.

One idea runs through all of them: a verdict you cannot check is not a verdict — and its corollary, which governs every surface here: undetermined is not a pass.

Try it in the browser · model-check a state machine · the specforge leaderboard

Ground-truth data · protocol-bench · specforge

The commercial offering

These are the engine. What is not open source is what makes it useful at scale: the maintained hazard-property corpora, composition analysis that finds hazards existing only when two components are combined, the trust-model sensitivity sweep, and the evidence trail that makes a verdict auditable after the fact. The tools above are MIT and stay that way.

Documentation

Full documentation, including the concepts guide and an honest comparison against TLA+, SPIN, Alloy and CBMC, is at https://nickharris808.github.io/verification-docs/.

Contributing

Bug reports and pull requests are welcome — see CONTRIBUTING.md. A counterexample that this tool gets wrong is the single most useful thing you can send.

Citing

Citation metadata is in CITATION.cff; GitHub renders a Cite this repository button from it.

Licence

MIT. See LICENSE.