MathIdeasResearch in progressRepository ↗
← Research catalogOriginal Markdown ↓
On this page

Mean-payoff backend and strategy-region certificates

Edition 9 October 2026 v2. Keep a specialist research prototype; defer a broad strategy-synthesis product. A bounded implementation of the deterministic paper's recursion works on small controls, but elementary cases can exhaust its work budget. No competitive backend advantage, independent source-proof acceptance or buyer demand is established. Facility-planning assurance remains the first product experiment.

Research finding

Family 104 contains four algorithms with different contracts. Their quasipolynomial bounds use the complete explicit binary input length L, including graph and weight data. This does not imply a practical polynomial-time solver.

Variant Input and payoff Output Selected formal coverage
Ordinary deterministic Total directed multigraph, Max/Min vertices, signed integer edge rewards; liminf average against full-history opponents Complete nonnegative winning set; section 7 also reduces exact rational values and globally optimal positional strategies to threshold queries No separately selected deterministic theorem in the read scope
Ordinary randomized Same game; algorithm uses independent fair bits Whole winning set correct with probability at least 7/8, every-tape bit bound; section 8 adds checked potential/threshold strategies or failure, then expected-time repetition Comparator selects threshold set and every-tape bound, not the certifying/Las Vegas extension or value/strategy output
Turn-based stochastic Additional chance vertices; binary rational probabilities, including zero/unreduced fractions; behavioral full-history strategies Complete set with sup-inf E[pathwise liminf mean] >= 0, including equality Newer paper not selected by the read family scope
Mean-payoff parity Signed integer vertex rewards, binary nonnegative priorities; minimum recurring priority even AND liminf mean >= 0 Complete conjunction-winning set; no finite-memory controller output follows merely from this result Newer paper not selected by the read family scope

The 126-line randomized Comparator describes a three-tape finite-control machine, self-delimiting explicit input, exact vertex-bit output, all-tape halting and a cardinality inequality expressing success at least 7/8. Its 69-line solution entry invokes imported implementation/complexity results. Imported closure, kernel and source executable acceptance remain open. The challenge's intended theorem hole is not a solution failure. The separate Truffet counterexample has not received a new proof review in this edition.

Problem and buyer

A formal-methods team or verification consultancy needs winning states, an appropriate strategy when supported, and an explanation of the objective actually guaranteed. One possible job is reviewing an existing resource game and generated controller before integration. Budget for a separate plugin, rather than incumbent tools and internal review, is unknown.

What the finding could enable

The deterministic mass-and-width recursion is explicit enough for a bounded research backend. Its further threshold-query reductions offer a route to values and globally optimal strategies; those reductions are unimplemented here. Stochastic and parity variants would need separate model adapters and output evidence.

An independently checked threshold-region result can remain useful after a solver exhausts its budget: verify closure against opponent moves, restrict the claimed player's moves to a supplied positional strategy, then check cycle signs. This uses conventional exact graph reasoning. Possible value lies in interoperability and review, not novelty of that familiar checker.

Technical and commercial limits

The new Python reference implements deterministic Procedure 4.1 with exact integers/rational masses. Caps: 12 vertices, 96 explicit edges, 256-bit signed weights, depth 128 and 200,000 selected work charges by default (maximum two million). It charges call/pivot vertex visits and operator edge/vertex visits. Parsing, preprocessing, fraction bit arithmetic, allocation and wall time are outside this counter. Complete labels remain source-conditional; exhaustion returns unknown and no partial winning set.

A one-vertex 2^64 positive self-loop completes with 249 calls and 377 charges. A two-vertex +64/-64 zero cycle exhausts 200,000 charges. An all-negative two-vertex recursive control completes after 237,877 calls and 1,725,258 charges; the corresponding all-positive case exhausts two million. These measure this literal unoptimized implementation and fixtures, not lower bounds. Tiny exhaustive strategy enumeration is already much cheaper.

The randomized wrapper uses s=the least power of two >= 2^17*(g+1), then J=2*[s*(n+1)]^6+1. For the one-vertex 2^64 positive loop, J=2854495385411919762116571938898990272765493249 and the root crosses the Basic cutoff, so its first Ask would run J trials literally. For a zero loop the root selects Basic before any wrapper, despite a large declared J. This is schedule arithmetic, not a randomized execution or universal runtime lower bound.

The stochastic three-state fair split into +1/-1 absorbing rewards gives Q=4 from the two encoded denominators, H=122880, inverse discount N=483183820800 and 2,847 prescribed outer width updates. Those integers have short binary descriptions; the source does not require a loop of length N. Recursive labeling costs remain separate and unmeasured. Do not reject this backend solely from its discount denominator.

A fair split has expected limiting reward zero but probability only 1/2 of a nonnegative path. A parity conjunction can need unbounded memory: at a priority-1/reward-0 vertex, loop increasingly long between visits to a priority-0/reward-minus-1 vertex. The mean tends to zero and even priority recurs. Every deterministic finite-memory path is ultimately periodic: visiting the negative vertex in the period gives negative mean; avoiding it loses parity. Nonnegative long-run mean also does not guarantee a zero-credit finite-prefix energy condition.

Minimal architecture

Explicit edge-index import and objective declaration -> variant eligibility -> recorded bounded solver -> distinct result type (winning set, values, strategy or unknown) -> compatible independent certificate -> input/model/limit/evidence export. Preserve loops, parallel-edge identity, zero ties, chance probabilities and vertex-to-edge reward conversion. Refuse stochastic, parity and energy declarations in the ordinary adapter.

The current API offers source-conditional labels and a separate exact threshold-region certificate function. For Max, the closed strategy-restricted region must have no negative original cycle. For Min, negate transformed weights (n+1)*w+1 and exclude negative cycles; each original simple-cycle sum is then at most minus one. Distance potentials are retained. Closure and cycle decomposition give threshold guarantees against arbitrary histories. They do not certify value-optimality, universal source correctness, Python formal correctness or real-world model fidelity.

Existing alternatives and differentiation

PRISM-games already provides stochastic-game verification and strategy synthesis. Its property documentation, reviewed 9 October 2026, separates expected mean-payoff and almost-sure reward objectives, and states a controllable-multichain restriction for expected long-run/ratio objectives. The new stochastic statement suggests a broader-model research question, but exact expectation/limit semantics, numerical guarantees, translation and measured benefit remain unestablished.

PRISM-games was not installed or run. The comparator here is an independently written exhaustive positional-strategy oracle, not a competitive production baseline. A plugin needs measurable benefit on relevant published or permissioned models before claiming differentiation.

Monetization hypothesis

Retain AUD 5,000-20,000 as an unvalidated specialist integration/pilot hypothesis. An illustrative AUD 10,000 at 40 hours times AUD 180/hour leaves AUD 2,800 before other costs; 60 hours costs AUD 10,800 in labor alone. Model translation and support could consume the margin. No interviews, purchases or paid pilots exist; do not sum this hypothetical revenue with overlapping platform modules.

Validation experiment

1,097 controls cover all 324 complete two-vertex ownership/weight combinations over -1/0/1, thirty hash-derived three-vertex games, fourteen selected cases, invalid models, resource limits and certificate attacks. All completed source-reference labels agree with the exhaustive oracle. Independent threshold-region certificates pass for all 368 generated games, including unknown reference cases. This is finite evidence, not a universal proof.

Future comparisons must match objective, quantifiers, model and output. Measure translation effort and controller representation as well as runtime. A mature backend and published benchmarks remain required; tiny timings cannot establish buyer benefit.

Conditions to reject or defer

Defer a broad solver product until compatible workloads show repeatable practical advantage and a buyer needs its output. Reject controller claims based only on winning states, finite-memory promises for unrestricted parity conjunctions, and almost-sure claims derived from expectation thresholds. Defer the randomized literal wrapper; retain the stochastic statement for further research instead of judging it by parameter magnitude alone.

Next concrete action

Select a compatible published PRISM-games benchmark and inspect its objective/translation before implementing value-strategy reductions or a stochastic backend. Use the current reference and certificates as a research integration specification. No outreach or paid compute is authorized by this assessment. Continue facility-planning assurance as the first product hypothesis.

Source evidence and reading extent

Pinned revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. Eight exact source hashes accompany selected-section reading, not full manuscript acceptance.

The complete scope, randomized Comparator/configuration and randomized solution entry were read. No upstream Lean program or kernel was executed. The Python reference was independently written from the displayed procedure.