# Noncommutative formula identity testing library

Edition: 8 October 2026. Initial decision: **Conditional engineering**. The product interpretation and pricing are hypotheses; independent proof and buyer validation remain open.

## Research finding

The characteristic-zero paper constructs rational matrix inputs detecting every nonzero bounded-size division-free noncommutative formula. The paper bounds dimension by O(ns^2); that construction-cost bound is outside the selected universal-hitting formal statement. Separate rational-formula hitting-list statements have broader checked cost scope.

## Problem and buyer

A symbolic compiler or algebra software team needs reproducible ways to reject incorrect rewrites involving ordered multiplication. Random scalar substitution can miss the noncommutative semantics entirely.

## What the finding could enable

A matrix-evaluation backend can provide deterministic identity testing for a carefully specified algebraic formula class. It could serve rewrite validation and algebra tooling when formula size and field restrictions are explicit.

## Technical and commercial limits

An identity over freely noncommuting symbols is different from an identity valid only for fixed-dimensional matrices or a particular physical operator algebra. Floating-point matrices introduce additional error; arbitrary divisions require the separate rational-formula result.

## Minimal architecture

Formula parser and gate-count validator -> exact rational hitting construction -> exact matrix evaluator -> zero test -> traceable result. Preserve field characteristic and the declared formula class in the API.

## Existing alternatives and differentiation

Symbolic algebra systems already manipulate expressions. The potential differentiation is a bounded-class deterministic test with explicit ordered semantics and reproducible exact arithmetic.

## Monetization hypothesis

Hypothesis: an open-source core with paid integration or support for compiler and symbolic-software teams. AUD 3,000-10,000 proof-of-concept engagements could test demand without assuming a broad SaaS market.

## Validation experiment

Generate known identities and deliberately incorrect rewrites, compare with symbolic expansion for small cases, and benchmark exact coefficient growth as formula size increases.

## Conditions to reject or defer

Reject if target customers work in algebras outside the free-formula assumptions or rational-matrix arithmetic dominates the validation budget.

## Next concrete action

Extract the hitting construction and record paper versus selected formal cost coverage before implementing it.

## Source evidence

Repository sources are pinned to revision `fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb`. Selected scope notes and manuscript statements have been reviewed to the extent described above; these links do not represent successful kernel checks.

### Family 116

Subject: Uniform black-box noncommutative identity testing across characteristics.

- [Uniform Matrix Hitting Points in Every Positive Characteristic](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Uniform-Matrix-Hitting-Points-in-Every-Positive-Characteristic-October-4-2026/uniform-matrix-hitting-points-positive-characteristic.pdf)
- [One Rational Matrix Hitting Point for Noncommutative Formulas](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/One-Rational-Matrix-Hitting-Point-for-Noncommutative-Formulas-September-24-2026/One-Rational-Matrix-Hitting-Point-for-Noncommutative-Formulas-September-24-2026.pdf)
- [Polynomial Hitting Lists for Noncommutative Rational Formulas](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Polynomial-Hitting-Lists-for-Noncommutative-Rational-Formulas-September-24-2026/Polynomial-Hitting-Lists-for-Noncommutative-Rational-Formulas-September-24-2026.pdf)
- [Formal scope notes](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/116.md)

## Current alternative sources

Primary documentation reviewed on 8 October 2026. Product availability demonstrates alternatives, not demand or willingness to pay for this proposal.

- [SymPy polynomial operations](https://docs.sympy.org/latest/modules/polys/reference.html)