On this page
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
- One Rational Matrix Hitting Point for Noncommutative Formulas
- Polynomial Hitting Lists for Noncommutative Rational Formulas
- Formal scope notes
Current alternative sources
Primary documentation reviewed on 8 October 2026. Product availability demonstrates alternatives, not demand or willingness to pay for this proposal.