[isPANN]

Summary

Adds examples/complexity_consistency_audit.rs, which checks registered variant complexities against the reduction graph. For every path A → … → B of 1–3 witness hops (Turing and aggregate-only edges are skipped), it substitutes the path's composed parameter transform into B's registered complexity. The result is an upper bound on solving A, ignoring the polynomial cost of the reduction itself. The audit flags A when that derived bound is strictly smaller in Big-O than A's own registered complexity. In that case either A's entry is stale or a transform along the path is wrong.

cargo run --release --example complexity_consistency_audit

The audit found three wrong entries, fixed here along with the matching paper text:

Model	Before	After	Why
NonTautology	1.307^num_vars	2^num_vars	Disjunct width is unbounded, so by De Morgan duality the problem is CNF-SAT. 1.307 is the 3-SAT bound. No O*((2−ε)^n) algorithm is known (SETH). This one entry also flagged Satisfiability and KSatisfiability<KN>.
MinimumWeightDecoding	2^(0.0494 * num_cols)	2^(0.5 * num_cols)	0.0494 is an average-case exponent for information set decoding over random codes, not a worst-case bound. Meet-in-the-middle over the two column halves of H (store the lightest x_L per key H_L·x_L, look up s + H_R·x_R) is exact in O*(2^(m/2)). Combining it with coset enumeration 2^(m−rank H) does not improve the worst case. In terms of the coset rank k, 2^k is SETH-optimal (Stephens-Davidowitz & Vaikuntanathan, FOCS 2019, now cited in the paper); no exact worst-case bound below 2^(m/2) in block length is known.
MaxCut<SimpleGraph, One>	2^(0.7907 * num_vertices)	2^(2.372 * num_vertices / 3)	0.7907 rounded 2.372/3 = 0.79067 up, so the One variant was beaten by its own i64 variant. It now uses the same form.

Remaining findings (not fixed here; follow-ups)

• MaxCut<SimpleGraph, i64> = 2^(2.372n/3). Williams' algorithm runs in O*(M·2^(ωn/3)) for weights bounded by M, and the entry leaves out the weight factor. This flags SpinGlass, DecisionSpinGlass and GraphPartitioning.
• MaximumSetPacking (One and i64) = 2^num_sets. The reduction to MIS on the intersection graph gives 1.1996^num_sets. First we need to confirm that 1.1996^n also applies to weighted MIS (MaximumIndependentSet<SimpleGraph, i64>).
• ThreeDimensionalMatching = 2^num_triples. The 3DM → MWD reduction now bounds it by 2^(0.5 * num_triples).

Coverage limits

On the current main base the audit examines 2,358 paths: 533 consistent, 17 where the derived bound is better (the 6 variants above), 123 that compare bounds in different variables and can't be ranked, 9 that can't be composed, and 1,676 that hit forms the growth domain can't analyze. Most of the unknown ones are nonlinear exponents such as 2^(n*m); #1220 removes most of that bucket. The audit catches only entries that disagree with the graph; a wrong value that happens to be consistent still needs a literature review.

Verification

• make check: fmt, clippy and every test suite pass, with one exception. The doctest at problemreductions-macros/src/lib.rs:211 fails because it is an ignore-marked syntax example that --include-ignored forces to run. It fails on main too and is unrelated to this PR.
• make paper passes.

🤖 Generated with Claude Code

[isPANN]

Agentic Review Report

PR #1219 at 81b4f236. Generic review: one audit example and two complexity-entry fixes with paper text.

Structural

• No generated exports (reduction_graph.json, problem_schemas.json, examples.json) in the diff. No unrelated edits, and no trait or macro changes.
• declare_variants! strings parse, and the MWD metadata test was updated. cargo test --lib -- minimum_weight_decoding non_tautology passes 29/29.
• NonTautology 2^num_vars: correct. Satisfiability -> NonTautology exists, so an unbounded-width DNF is CNF-SAT by De Morgan, and no O*((2-eps)^n) CNF-SAT algorithm is known. The old 1.307 came from 3-SAT and was wrong.
• MinimumWeightDecoding 2^num_cols: a valid upper bound, but not the best known. The new paper sentence is false; see finding 1.
• Audit soundness. Substituting upper-bound fields is sound in practice, but only because of the Growth trust contract (nonnegative, weakly monotone, subtraction widened to addition), not because "complexities are monotone". Non-monotone registered complexities such as (num_orientation_samples / num_links)^num_links land in Unknown and are skipped. ParameterTransform::compose already marks unsafe intermediate upper-bound substitutions unavailable. Today no unsound finding is emitted. The guard is implicit, though; see finding 3.

Quality

• The is_polynomial string heuristic is crude (finding 2). The polynomial bucket is empty today, so this is dormant.
• The audit is a report-only example with no regression test. That is acceptable for an example.

Feature test

• cargo run --release --example complexity_consistency_audit reproduces the PR body: 1935 paths, 420 consistent, 15 violating paths over 5 variants (SpinGlass, DecisionSpinGlass, GraphPartitioning via MaxCut/i64; MaximumSetPacking One/i64 via MIS), 100 incomparable, 1386 unknown, 14 uncomposable, and 0 polynomial findings.
• pred show NonTautology gives O(2^num_vars) and pred show MinimumWeightDecoding gives O(2^num_cols). pred create --example followed by pred solve reports optimal for both.

Findings

Important

1. docs/paper/reductions.typ:10968 and src/models/algebraic/minimum_weight_decoding.rs:182-184: the claim "In the worst case no algorithm is known beyond enumerating the solution coset" is false, and a trivial argument beats 2^m. Let r = rank(H). A consistent system has a solution of weight ≤ r: write s in a basis of r independent columns. So take the cheaper of two procedures:

   • enumerate the coset x0 + ker H, costing 2^(m-r);
   • enumerate all x with |x| ≤ r, costing sum_{w≤r} C(m,w) ≤ 2^(m·H(r/m)).

   The worst case is at 1 - ρ = H(ρ), ρ ≈ 0.2271, which gives O*(2^(0.7730 m)) for every instance.

   Fix: either register 2^(0.773 * num_cols) and state this derivation in the paper, or keep 2^num_cols and reword to something like "ISD exponents are average-case over random codes; we register the simple exhaustive bound O*(2^m), and better worst-case bounds follow from combining coset enumeration with low-weight enumeration." Also update the code comment ("no worst-case bound below exhaustive search over x is known") to match.

Minor
2. examples/complexity_consistency_audit.rs:78-85 (is_polynomial): this is a string heuristic over Expr::to_string().

• It classifies exp(n) and factorial(n) as polynomial, because neither contains a ^.
• It classifies n^(1/2) and n^(k) as exponential, because the exponent starts with (.
• The module doc (lines 10-11) says "both bounds polynomial", but only the registered side is checked.

Fix: decide from the growth domain instead. For example, add Growth::is_polynomial() (true iff no term has an exponential factor) in src/growth.rs and call it on registered_growth. Alternatively, drop the partition: it is empty today, and polynomial-vs-polynomial comparisons are already caveated.
3. examples/complexity_consistency_audit.rs:71-75: the comment "complexities are monotone" is not true for every registered string. Soundness actually rests on Growth::from_expr widening and its monotone trust contract.

Fix: make the guard explicit. Skip (count as unknown) when Growth::from_expr(&Expr::parse(target)) is Unknown before substituting, and reword the comment to cite the growth-domain contract.
4. examples/complexity_consistency_audit.rs:113-119: a variant with no registered complexity is counted as uncomposable, the same bucket as a transform-composition failure. Fix: use a separate counter (for example, missing complexity) so the coverage numbers in the PR body mean what they say.
5. examples/complexity_consistency_audit.rs:48: only Turing edges are filtered. An aggregate-only edge (witness == false) would yield a value bound, not a solution bound. None exist today (0 in reduction_graph.json). Fix: also continue when !edge.capabilities.witness, since the registered complexities describe witness-returning solves.
6. docs/paper/reductions.typ:5705: "the best known algorithm is O*(2^n) exhaustive search" overstates the case. For CNF-SAT with m = poly(n) clauses, 2^(n(1 - 1/O(log(m/n)))) algorithms exist (Calabro–Impagliazzo–Paturi). Fix: say "no O*((2-ε)^n) algorithm is known (SETH), so we register O*(2^n)."

Verdict: the NonTautology fix and the audit tool are sound. Finding 1 should be addressed before merge: the new MWD paper statement is mathematically false.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 97.18%. Comparing base (a10ee83) to head (c89e6ea).

Additional details and impacted files

@@           Coverage Diff           @@
##             main    #1219   +/-   ##
=======================================
  Coverage   97.18%   97.18%           
=======================================
  Files        1146     1146           
  Lines      151076   151076           
=======================================
  Hits       146819   146819           
  Misses       4257     4257           

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

[isPANN]

Addressed the Agentic Review Report in ea882aa:

1. Important, MinimumWeightDecoding bound: fixed. It now registers 2^(0.773 * num_cols), and the paper has the derivation. A consistent system has a solution of weight at most r = rank(H), so we can take the cheaper of coset enumeration, 2^(m−r), and weight-≤r enumeration, 2^(m·h(r/m)). The two balance at r/m ≈ 0.22709, giving an exponent of 0.77291, which 0.773 rounds up safely.
2. is_polynomial: removed, along with the polynomial/exponential split. The header now says a finding with a polynomial registered bound is only suggestive.
3. Monotonicity: paths whose target complexity the growth domain can't analyze are now skipped before substitution, and the comment now relies on the growth domain's monotone class.
4. Missing complexity: now has its own no complexity counter.
5. Aggregate-only edges: skipped (!capabilities.witness).
6. NonTautology wording: now "no O*((2−ε)^n) algorithm is known (SETH); we register O*(2^n)".

New audit result: 6 flagged variants. Fixing MinimumWeightDecoding exposed another stale entry, ThreeDimensionalMatching = 2^num_triples, which the 3DM → MWD reduction now bounds by 2^(0.773·num_triples). I've left that out of this PR, along with the MaxCut-weight and weighted-MIS items, as follow-ups.

Gates: make check passes except the pre-existing problemreductions-macros doctest (line 211, an ignore block forced by --include-ignored). make paper passes.

[isPANN]

Please kindly check the following items (PR #1219):

• Paper (PDF): check the NonTautology and MinimumWeightDecoding complexity discussion (the 2^(0.773 m) derivation in particular)
• Implementation (Optional): spot-check examples/complexity_consistency_audit.rs and the two declare_variants! changes

Join the discussion on Zulip — feel free to ask questions or leave feedback there.

[isPANN]

Retargeted onto feat/binary-ilp-to-sat (#1218) and merged that branch in (no rebase); the diff is again only this PR's five files. On the combined tree: cargo test --workspace, fmt, clippy, and make paper pass. The audit's totals now count the extra rules on #1218 (2155 paths: 431 consistent, 16 derived-better paths, 103 incomparable, 1594 unknown growth, 11 uncomposable); the flagged variants are the same six listed above (SpinGlass ×2 and GraphPartitioning via MaxCut weights, MaximumSetPacking ×2, ThreeDimensionalMatching). #1220 removes most of the unknown-growth bucket.

[GiggleLiu]

Agentic Review Report

PR #1219. Reviewed head 77fb850f21d01330111c081965c715fabfff59b2 against own base 0daa9a8265aefe40983beeba0464f8feea8c3316 (feat/binary-ilp-to-sat). Read-only review; no tracked edits, pushes, PR comments or merges.

Verdict

HOLD for the new MinimumWeightDecoding complexity entry. The NonTautology exponential-base correction is justified; the decoding bound is valid but already beaten by elementary exact meet-in-the-middle.

Structural

Reviewed the five-file own-base diff, full audit example, model definitions and complexity registrations, relevant manual text and metadata test. The audit skips aggregate-only and Turing edges, accounts for unavailable transforms, and enumerates simple paths of at most three witness hops. It is a heuristic consistency report, not a proof that an algorithm is optimal or that every apparent violation is sound.

Quality

The new MWD test pins the literal 0.773, so it cannot detect that the chosen algorithm is not best known. The proposed entropy/coset derivation gives a valid upper bound, but checking only that derivation misses a much simpler smaller bound. The printed audit conclusions also need caution when a growth is only a widened upper bound; a future exactness API alone does not establish monotonicity of arbitrary complexity expressions.

Feature test

A separate Python meet-in-the-middle solver was checked against exhaustive minimum-weight search on 1,320 deterministic arbitrary binary matrix/syndrome cases, with 0–10 columns, 0–5 rows, empty/rank-deficient/infeasible cases included. All agreed. The construction and running-time derivation below are independent of average-case decoding assumptions. No full exact-head audit rerun or CLI install was performed in this review. git diff --check BASE...HEAD passed.

Findings

1. Important: 2^(0.773*num_cols) is not a best-known worst-case bound. src/models/algebraic/minimum_weight_decoding.rs:182-185, with corresponding paper discussion at docs/paper/reductions.typ:10995. Split the m columns as H=[H_L H_R]. Enumerate every left half-word and keep the minimum Hamming weight witness for each syndrome H_L x_L. Enumerate right half-words and look up s xor H_R x_R, minimizing the sum of the two stored weights. Every full word has a unique left/right split, and retaining the lightest half-word per syndrome cannot discard a better completion. Sorting or hashing gives O*(2^ceil(m/2)) worst-case time with O*(2^floor(m/2)) space; deterministic sorting adds only polynomial factors. Thus the new entry is already worse than a straightforward exact O*(2^(m/2)) algorithm. Register at least that sound bound after checking for stronger known worst-case algorithms, and state the space requirement. No assumption that the code is random is involved.
2. Minor: qualify the entropy-count sentence. The bound sum_{w≤r} C(m,w)≤2^(m h(r/m)) applies for r≤m/2. For r>m/2 use coset enumeration directly. The final 0.773 upper bound remains valid, but the paper's intermediate enumeration statement is too broad.
3. Minor: update PR description. Its table still says the MWD change ends at 2^num_cols; the head registers 2^(0.773*num_cols).

Primary-source verification

The CNF-SAT/SETH distinction is supported by Cygan et al., On Problems as Hard as CNFSAT: sub-2^n improvements do not imply a constant exponential base below 2. De Morgan duality directly transfers the unbounded-width DNF non-tautology search to CNF-SAT. The MWD counterexample to best-known status above is a complete direct algorithmic derivation, checked independently on small instances; it is not an inference from an average-case ISD exponent. Attempts to open the IACR decoding-estimator paper returned HTTP 403, so this report does not claim a complete literature survey or a final optimal exponent.

GitHub PR policy audit

GATE: PASS. This is the harm-signals gate only; it does not override the correctness verdict above.

• harm.secrets (security.no-secrets): OK. No obvious credential/private-key/token addition detected in the own-base diff.
• harm.dangerous-files (git.harm-signals): OK. No conflict markers, unexplained archives or local scratch/config artifacts detected.
• harm.generated-artifacts (code.generated-artifacts): OK. No blacklisted generated graph/schema/example exports or build targets added. Test oracle fixtures are intentional test inputs; small browser contracts/fonts are intentional source assets.
• harm.cache (code.generated-cache): OK. No cache directories added.
• harm.debug-leftovers (code.debug-leftovers): OK. No debugger, breakpoint or temporary debug print addition detected. Browser performance marks are deliberate verification instrumentation.
• pr.description-quality (github.pr-description-quality): ISSUE. Stale scope/final-bound details identified above; update before approval.
• pr.traceable (github.prs-traceable): OK. The PR states its purpose and own stack context.

Policy evidence: own-base name/status, numstat and patch inspection; added-line secret/conflict/debug scan; git diff --check; gh-axi pr view 1219 --full --comments --reviews. No claim of exhaustive secret scanning. The parent reviewer owns the final head/base recheck before any merge.