Noncommutative formula testing and rewrite witnesses

Edition 9 October 2026 v2. Retain a specialist exact-witness SDK experiment at low commercial confidence. The characteristic-zero matrix construction is explicit enough to prototype. Existing exact matrix probes already detect the generated mistakes more cheaply; no competitive software advantage or buyer demand is established. The larger positive-characteristic and inverse-formula constructions are deferred.

Research finding

Family 116 contains three distinct statements. The characteristic-zero division-free paper constructs a single rational tuple T, depending only on variable count n and formula tree-size bound s, which the source claims detects every nonzero formula of that size over every characteristic-zero field. All leaves and binary addition/ordered multiplication gates count toward s. Its dimension is d=2ns^2 except n=s=1, where T1=[1]. The selected Comparator asserts universal nonvanishing, not a separately stated construction-time or dimension bound. The paper asserts polynomial bit construction; evaluating arbitrary field coefficients is a separate oracle cost.

The positive-characteristic companion replaces integration with a multiplicative shift, then represents a truncated coefficient ring as prime-field matrices. It promises a prime p in binary and n,s in unary, arbitrary extension-field coefficients and dense output, including p=2. Reducing the rational characteristic-zero tuple modulo p is not a valid substitute. This newer paper has no linked Comparator in the selected family scope; no broad formal-coverage claim is made.

The rational-formula companion permits inverse gates over Q. It supplies a list with one defined, invertible evaluation for every admissible nonzero formula. Admissibility means some defined rational matrix evaluation exists, and every original inverse gate must remain defined even in branches that later cancel. Its generator complexity excludes evaluation of unbounded-height unknown coefficients. The selected RationalHitting statement includes a finite-state machine, complete output encoding, common dimension and polynomial bounds. That statement's wider coverage does not establish practical parameters or successful kernel execution.

Problem and buyer

Possible buyers are compiler, computer-algebra and symbolic-modeling teams checking transformations involving ordered multiplication. Treating variables as commuting scalars can erase errors: xy-yx evaluates to zero at every scalar substitution but is a nonzero free polynomial. A reproducible exact matrix witness can explain why a proposed universal rewrite fails.

The actual need depends on the target algebra. A free-polynomial identity must hold at all matrix sizes; a relation for fixed matrices or operators is a different question. For example, x^2-1 is nonzero as a free polynomial but vanishes at the two-by-two Pauli X matrix. This tool must not reject a valid domain-specific rewrite merely because it fails in the free algebra. No interviews, authorized customer formula corpus or purchase commitments exist.

What the finding could enable

If independently accepted, the first paper offers a deterministic evaluation tuple chosen before seeing formula coefficients. That could support opaque formula-oracle regression testing or version-to-version equivalence checks under a truthful size and algebra promise. This universal size-only choice is the proposed research contribution; deterministic tests with access to formula structure already exist, as the paper's introduction records.

The implemented bounded reference instead accepts a visible JSON formula tree over exact rationals. It computes the first column f(T)e0 through structured matrix actions and returns a concrete nonzero entry when found. A nonzero exact matrix evaluation disproves a free identity without requiring the source's universal hitting theorem. A zero result remains unknown or source-conditional; the prototype never presents it as an independently proved identity.

The concrete product experiment is a small SDK and CI adapter for ordered-algebra rewrite tests, with explicit algebra declarations and replayable witnesses. Its visible-tree prototype is not an opaque black-box implementation. Packaging a general CAS, a quantum compiler or a broad symbolic-proof service would require additional semantics and evidence.

Technical and commercial limits

For q<r, the paper's matrix entry is (-1)^(r-q-1)/(ri^(r-q)), with other entries zero. Multiplication is ordered and the rightmost operator acts first. For a coefficient vector v, divide its series by z+i using c_t=(v_t-c_(t-1))/i, with c_(-1)=0, then integrate: output_r=c_(r-1)/r and output_0=0. This gives O(d) selected rational operations per variable action. Composing the visible tree costs O(sd) such operations, excluding growth in rational bit lengths. It is an implementation derivation from the explicit entries, not a new asymptotic theorem or a dense black-box timing bound.

The reference accepts 1-8 variables, at most 127 tree gates and depth 32, canonical rational input scalars with 256-bit numerator/denominator, a requested coefficient dimension at most 16,384, at most one million selected arithmetic charges and intermediate numerator/denominator size at most 8,192 bits. Parsing, unary negation, rational bit operations, allocation and wall time are not covered by the arithmetic counter. Exhaustion returns unknown with no completed witness. These caps do not provide production capacity or latency promises.

Optional shorter truncation can expose a nonzero witness, but zero at that truncation proves nothing universal. Even a full-dimension zero first column depends on the paper's first-column detection argument and correct implementation; the Comparator's bare matrix-nonvanishing statement alone is not a first-column acceptance argument. The exceptional n=s=1 generator is handled separately.

Shared arithmetic circuits are not accepted using their DAG node count: unfolding can enlarge tree size. Inverse gates, positive characteristic, approximate floating arithmetic, noncentral constants, rectangular shape systems and imposed commutation/operator relations need separate adapters or results. The utility rejects unsupported gate/field declarations.

The companion schedules are much larger. For n=2,s=3, the positive-characteristic formula gives N=31, E=526 and dense dimension 16,306: 531,771,272 entries across the two matrices. The literal inverse-formula list already has dimension 32,768 and traverses 92,950,340,097,909,002,166,337,537 grid triples at n=s=1. This is the number of explicit candidate triples visited, not the number of retained tuples. No companion matrices or list were allocated. Sparse/block representations, shortcuts and smaller special-case algorithms need their own cost and correspondence analysis.

Minimal architecture

1. Strict expression/model adapter preserving multiplication order, scalar field, all tree occurrences and source version.
2. Cheap existing exact scalar/matrix probes for nonzero witnesses, with zero kept unknown.
3. Optional structured source-tuple evaluation with explicit coefficient, arithmetic and rational-bit limits.
4. Witness replay using exact entries and the original expression; report the target algebra and matrix dimension.
5. Separate identity-acceptance path using a trusted appropriate symbolic method or accepted source proof/implementation bridge. Never silently turn an inconclusive zero into pass.

The current interface is a local CLI and Python function. No hosted upload API, production compiler integration, arbitrary black-box adapter or Lean execution is deployed.

Existing alternatives and differentiation

SymPy's core documentation supports noncommuting symbols and symbolic operations; its matrix-expression API preserves ordered matrix products. Primary documentation was reviewed 9 October 2026. The existing local SymPy 1.13.1 environment was reused unchanged, while the current online docs identify 1.14.0.

All 548 generated tiny formula trees agreed with independent exact word expansion and SymPy. On the generated product of sixteen copies of (x+y), full symbolic expansion emitted 65,536 terms and took about 14.8 seconds; a completed 32-coefficient witness took about 3.5 ms. Those outputs differ. The fairer nonzero-witness baseline evaluates the same expression at tiny exact matrices: both recorded two-by-two presets find a witness in about 0.16 ms, and a scalar substitution already suffices. Thus the expansion comparison establishes no competitive advantage. Full source-dimension attempts on the eight- and sixteen-factor cases stopped at the rational-bit cap.

A deliberately chosen polynomial x^2y-yx^2 vanishes at the first nilpotent preset, while a second preset and the source-derived prefix detect it. This demonstrates that one fixed small probe can miss; it does not establish universal superiority of this prototype. No optimized white-box PIT implementation, representative compiler workload or source-black-box evaluation cost has been benchmarked.

Monetization hypothesis

Retain the earlier AUD 3,000-10,000 integration/support experiment only for a specific recurring engineering workflow. An illustrative AUD 6,000 engagement taking 20 hours at an assumed AUD 180/hour leaves AUD 2,400 before overhead and other costs; 35 hours cost AUD 6,300 in labor alone. These are planning assumptions, not market prices or earnings. A standalone subscription has no validated basis. The facility-planning workbench remains the first product recommendation.

Validation experiment

686 controls cover all 548 formula trees of size 1,3,5 over leaves {-1,0,x,y}, exact word and SymPy agreement, 108 matrix-basis action comparisons, source commutator coefficient -1/24, short-prefix unknowns, exhaustion, malformed models and nine generated comparisons. 32 additional controls compare scalar and two exact matrix presets across ten cases. Eight boundary controls distinguish the Pauli relation from a free identity and exercise input/resource refusals.

These 726 controls establish finite implementation evidence only. They do not prove the universal source theorem, formal correctness of Python, caller promises or customer value. Inputs, comparison and source schedules.

Conditions to reject or defer

Defer the literal inverse-formula and dense positive-characteristic backends because their concrete sizes are already prohibitive for small inputs. Keep the rational division-free prototype only if a real workflow requires deterministic size-bound coverage or useful exact witnesses beyond cheaper existing methods. Reject commercial differentiation based on comparing a witness with full expansion, or on testing a free algebra when customers require fixed operator relations. Full zero acceptance remains blocked on accepted proof/correctness bridges; positive witnesses remain independently useful finite calculations.

Next concrete action

Find a permissioned rewrite workload and identify whether its oracle is opaque, whether it accepts arbitrary-dimensional exact matrices, and what algebraic relations must be preserved. Compare complete integration and adjudication effort with the current method, including existing white-box algorithms and small probes. No outreach has been performed. The facility-planning product retains priority while this specialist SDK remains exploratory.

Source and verification record

Pinned revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. Characteristic-zero PDF pages 1-12 were read, including the explicit construction and body proof; page 13 references were not separately reviewed. Positive-characteristic pages 1-4 and 10-13 and rational-formula pages 1-4 and 16-21 were read. Five construction pages were visually inspected: characteristic-zero 10/11, positive 12, rational 16/17.

The family scope, both linked Comparators/configurations, 100-line Hitting entry and 49-line RationalHitting Main were read. Imported proof closure and Lean/kernel/source-program execution remain unverified. The implemented rational entries and structured action are independent Python code. The positive-characteristic and rational-formula generators were only numerically planned. Ten exact source pointers/hashes and preserved runtime identity.