[isPANN]

The previous catalog used an average-case decoding exponent as a worst-case guarantee and a fixed-width SAT bound for unrestricted DNF non-tautology. This corrects NonTautology to 2^num_vars, MinimumWeightDecoding to meet-in-the-middle 2^(0.5 * num_cols), and the unit-weight MaxCut expression to the same 2^(2.372 * num_vertices / 3) form as its integer-weight variant.

The manual gives the decoding algorithm's floor/ceil split, time and space requirements, and distinguishes block length from the code dimension used by the cited SETH lower bound. It also corrects NonTautology's complexity class to NP-complete.

The new complexity_consistency_audit example enumerates paths of one to three witness reductions and compares composed growth bounds. Findings are candidates requiring manual checks of monotonicity, tightness, and reduction cost. A known growth form is not a monotonicity certificate. Turing and aggregate-only paths are excluded; unsupported and missing metadata are reported separately. Failure diagnostics now pair the reason with the side that actually failed.

Validation at 22b3c0b9e:

• Independent semantic and policy review passed. The meet-in-the-middle algorithm agreed with exhaustive search on 1,800 deterministic cases; the SETH citation was checked against the primary paper.
• make check: 7,194 tests passed, none failed, ignored, or filtered; formatting and all-target/all-feature Clippy passed. make paper passed.
• Real CLI creation, inspection and brute-force solving passed for NonTautology, MinimumWeightDecoding, and MaxCut. The changed MaxCut/SimpleGraph/One variant reports the corrected bound and its canonical example solves to Max(6).
• The audit ran successfully: 2,358 paths, 533 consistent, 17 candidate improvements across six variants, 123 incomparable, 1,676 unsupported growth forms, nine uncomposable paths, and no missing complexity entries.
• All nine GitHub checks passed on this commit; Codecov reports 97.18% project coverage and all modified coverable lines covered.

The six remaining audit candidates concern SpinGlass/DecisionSpinGlass/GraphPartitioning through weighted MaxCut, MaximumSetPacking variants through IndependentSet, and ThreeDimensionalMatching through decoding. They are reported for manual follow-up rather than silently changing unrelated catalog entries.

[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 (22b3c0b).

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.

[GiggleLiu]

Agentic Review Report

Re-review of final commit 22b3c0b9eae0add3ca242cc37a93519365e57327: PASS. This supersedes my earlier request for changes; the decoding-bound blocker is resolved.

Structural and semantic review

The meet-in-the-middle decoding bound is valid: store the minimum-weight left word for each syndrome, then enumerate right words and look up the complementary syndrome. The manual now states the floor/ceil split, time and space, and distinguishes block length from the code dimension in the SETH citation. An independent implementation agreed with exhaustive search on 1,800 deterministic cases, including odd splits, deficient rank, and infeasible systems. NonTautology's NP-completeness and bound are consistent with CNF-SAT duality; the unweighted MaxCut exponent removes the rounding discrepancy.

Quality and feature validation

The audit uses existing graph/transform APIs and reports candidates requiring manual checks of monotonicity, tightness, and reduction cost. Its failure diagnostics now label the correct side. No unintended trait, model behavior, dependency or generated-file changes were found. Independent quality and policy review passed.

• make check: 7,194 tests passed, zero failed/ignored/filtered; formatting and all-feature Clippy passed.
• make paper passed.
• Real CLI creation, inspection and brute-force solving passed for the affected models; the changed unweighted MaxCut variant returned Max(6) and displayed the corrected bound.
• The audit completed over 2,358 paths: 533 consistent, 17 candidate improvements, 123 incomparable, 1,676 unsupported-growth, nine uncomposable, and zero missing-complexity paths.
• All nine GitHub checks passed on this exact commit. Codecov reports 97.18% project coverage and all modified coverable lines covered.
• Rechecked discussion comments, reviews, inline comments, CI and Codecov; no outstanding findings remain in this PR.

The six remaining catalog candidates reported by the audit require separate mathematical follow-up; this PR does not claim they are proved improvements.