[Rule] SimultaneousIncongruences to bounded integer ILP #1197

Source

SimultaneousIncongruences (no variant parameters).

Given integer pairs (a_i,b_i) with 1 ≤ a_i ≤ b_i, find a nonnegative integer x satisfying x mod b_i ≠ a_i mod b_i for every pair. The existing constructor requires the least common multiple of all moduli to fit i64. Its actual Problem::Solution is i64 and its Problem::Value is Or.

Target

ILP<i64,i64,Bounded> — registered variant ILP/variable=i64/coefficient=i64/bounds=bounded.

All integer variables have explicit finite bounds. The objective is constant-zero minimization, so feasibility is the only relevant result. Target solutions have type Vec<i64> and values have type Extremum<i64>; use the library's explicit ilp_feasibility completed-value mapping. A feasible target witness is required before extraction.

Motivation

This gives the existing incongruence model a direct executable ILP formulation with three auxiliary variables and three rows per pair. It encodes numeric residues compactly, without enumerating a period of potentially enormous length.

The model discussion in #537 declined a direct ILP approach because the modular conditions were not directly linear. Explicit quotients, remainders and bounded binary disjunctions address that obstacle. No dedicated rule with these exact endpoints was found in the all-state issues/PR history captured on 2026-10-13. This is a statement about that project search, not global mathematical novelty.

Reference

The direct construction and proof are given below. Quotient/remainder representations and bounded disjunctions are established techniques; no claim is made that this is a new number-theoretic theorem.

Background inspected: Fred Glover, Improved Linear Integer Programming Formulations of Nonlinear Integer Problems, Management Science 22(4), 455–460 (1975), section 2, equations (1)–(3), on bounded conditional linearization. Author-hosted primary PDF. That article is background, not a source claiming this exact source/target rule.

Reduction Algorithm

Let m be the pair count, ρ_i = a_i mod b_i, and L = lcm(b_1,…,b_m), with L=1 for an empty input. Source construction guarantees 1 ≤ L ≤ 2^63−1. Every source witness may be reduced modulo L, preserving all incongruences.

1. Allocate coordinates in this order: x, all q_i, all r_i, all z_i.

2. Give them explicit integer bounds:

   • 0 ≤ x ≤ L−1;
   • 0 ≤ q_i ≤ L/b_i−1;
   • 0 ≤ r_i ≤ b_i−1;
   • 0 ≤ z_i ≤ 1.

3. For each pair add these three rows:

   x − b_i q_i − r_i = 0
   r_i − b_i z_i ≤ ρ_i − 1
   r_i − b_i z_i ≥ (ρ_i − b_i) + 1
   

4. Minimize zero. Validate target feasibility once and extract coordinate zero, x.

Correctness, forward. Start with a source witness and replace it by x mod L. Choose q_i=floor(x/b_i) and r_i=x mod b_i. Their bounds follow from b_i | L and x<L. Since r_i≠ρ_i, choose z_i=0 for r_i<ρ_i and z_i=1 for r_i>ρ_i. The division equation holds. For z_i=0, the upper inequality gives the required strict lower interval, while the lower inequality follows from r_i≥0 and ρ_i<b_i. For z_i=1, the lower inequality is r_i≥ρ_i+1; the upper inequality follows from r_i≤b_i−1. Hence the target is feasible.

Correctness, backward. The division equation together with 0≤r_i<b_i makes r_i the unique Euclidean remainder of x modulo b_i. If z_i=0, the upper inequality implies r_i<ρ_i. If z_i=1, the lower inequality implies r_i>ρ_i. Thus x avoids every forbidden residue and is a source witness. For b_i=1, both residues are zero and neither selector value can satisfy both inequalities, correctly giving infeasibility.

Complexity and arithmetic. LCM computation and row construction are polynomial in the encoded input length. There is no expansion into L individual choices. Products and partial sums remain representable for every in-domain target vector, including infeasible ones: b_i q_i ≤ L−b_i and b_i q_i+r_i ≤ L−1, so the normalized division row cannot overflow i64; also −b_i ≤ r_i−b_i z_i ≤ b_i−1. Compute the lower right-hand side as (ρ_i−b_i)+1. Allocation/index counts are checked. Empty input has a single variable fixed to zero and no rows.

Size Overhead

Every row support has respectively 3, 2 and 2 distinct nonzero terms, including modulus one. These formulas use the registered source parameter num_pairs only. The magnitude bound covers coefficients, right-hand sides and explicit variable endpoints over the complete accepted source range.

Validation Method

The general correctness argument is above; finite checks search for counterexamples and audit the implementations.

• Constructor audit: 12,931 instance executions, 502,071 assertions, seed 2026101301, including all ordered lists of up to five pairs with moduli at most three, sampled larger moduli, every feasible local target completion, raw small Cartesian target domains, and signed-i64 boundaries. All seven required audit sections passed.
• Fresh-context adversary, given only the Typst proof: 5,440 instance executions, 481,855 assertions, seeds 2026101301 and 2026101302, two Hypothesis strategies with 300 examples each, database=None, deadline=None; zero failures. It independently implemented construction, target checking and extraction.
• Constructor/adversary cross-comparison: 105 identical target constructions, 3,150 target-feasibility comparisons and 67 cross-extractions; zero disagreements.
• Rust focused tests: 6 passed, 0 failed, total 0.03 seconds. These include ILPSolver/source-BruteForce closed loops, exhaustive small bounded target domains, infeasible and empty inputs, malformed witness rejection, magnitude boundaries and the canonical example. Formatting passed.
• A local implementation is prepared at commit a0e8a7d671a5873f74d18136f3375353243fc4a0, branch contrib/simultaneous-incongruences-ilp. Full integration, clippy, complete suite, paper and coverage gates remain part of PR preparation; they are not claimed complete here.

Counts above are assertions and instance executions, not numbers of distinct statistically independent samples. Proof, scripts, seeds and machine-readable cross-comparison evidence are prepared for the verification certificate. The local evidence paths are research/coauthorship-2026-10-13/verification/algebra_incongruences*, adversary/adv_incongruences*, and verification/cross_algebra_round1*; these are not yet public links.

Example

YES source. Pairs [(2,2),(1,3),(2,3)] give L=6 and forbidden residues (0,1,2). The unique witness in one period is x=3.

Construction and target. Bounds are x∈[0,5], quotients (q_1,q_2,q_3)∈[0,2]×[0,1]×[0,1], remainders (r_1,r_2,r_3)∈[0,1]×[0,2]×[0,2], and three binary selectors. The nine rows are:

x − 2q_1 − r_1 = 0       −1 ≤ r_1 − 2z_1 ≤ −1
x − 3q_2 − r_2 = 0       −1 ≤ r_2 − 3z_2 ≤  0
x − 3q_3 − r_3 = 0        0 ≤ r_3 − 3z_3 ≤  1

Each displayed two-sided inequality is stored as two separate rows. The complete witness is (3,1,1,1,1,0,0,1,0,0). Division rows evaluate to 3−2−1=0, 3−3−0=0, 3−3−0=0; exclusion expressions are (-1,0,0) and lie in the specified intervals. This target has 10 variables, 9 rows and 21 nonzeros. Extraction returns 3.

NO source and target. Replace the source by [(2,2),(1,2),(1,3)], still with L=6. The first pair excludes even values and the second excludes odd values. The target would simultaneously require remainder 1 and remainder 0 modulo 2 for the same x; its division equations make that impossible.

BibTeX

@article{Glover1975ImprovedILP,
  author = {Glover, Fred},
  title = {Improved Linear Integer Programming Formulations of Nonlinear Integer Problems},
  journal = {Management Science},
  volume = {22},
  number = {4},
  pages = {455--460},
  year = {1975},
  url = {https://leeds-faculty.colorado.edu/glover/fred%20pubs/69%20-%20Improved%20Linear%20Integer%20Programming%20Formulations%20of%20Nonlinear%20Integer%20Problems%20_%20%20Fred%20Glover.pdf}
}

Attribution and submission status

Responsible human contributor: Thiago Costa (@ThiagoCAltoe). Discovery, drafting, implementation and automated adversarial checking were assisted by Codex AI agents. Human scientific review is pending. No claim of maintainer acceptance, reserved credit or earned coauthorship is made. Maintainers determine whether the contribution meets the project's nontriviality and authorship criteria.

This proposal is submitted for maintainer review; acceptance and authorship credit remain unconfirmed.