On this page
Unique-solution promise solver limitation audit
Family 242: Single-fold Diophantine representations and undecidability under an at-most-one-solution promise. First application triage, 9 October 2026 Australia/Brisbane.
Problem and potential new use
Constraint-solver researchers can flag the inference that at-most-one Diophantine solution makes a general nonnegative-integer solver decidable.
Applicability and commercial boundary
The representation and undecidability statements do not rule out restricted decidable polynomial families or validated witnesses. Exactly-one auxiliary solutions differ from efficient witness search.
Initial business decision
Research reference or conditional symbolic/verification engineering. No practical implementation, recurring buyer need or profitability has been demonstrated; a weak business bridge is explicitly deferred.
Next verification action
Record domain, promise and unknown outcomes in a rational/integer solver contract framework.
Evidence scope
The catalog statement was individually reviewed. Main-paper proof, construction effectiveness and selected formal scope comparison remain queued. No independent Lean verification was run. Source revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. See source metadata.