Merge current main into NAE-SAT reduction PR

Author: GiggleLiu

.claude/CLAUDE.md

@@ -142,7 +142,7 @@ Max<V>, Min<V>, Sum<W>, Or, And, Extremum<V>, ExtremumSense
 - Decision-equivalence rules map completed `Or` values identically. Decision-to-optimization rules own their feasibility/threshold map; reject target configurations that do not certify YES instead of returning an invalid source witness. Optimization rules decode optimal witnesses and evaluate the source; register a value map only when mathematically defined. Counting and universal rules map completed folds without witnesses. Follow [result mappings](../docs/src/design.md#result-mappings); no mandatory rule-category tags.
 - Decode only the reduction's defined mathematical mapping. Reject malformed structure with `ExtractionError`; never panic, truncate, clamp, invent defaults, or add recovery branches. Explicit mathematical alternatives and sentinels are allowed. Test successful decoding and every rejected representation.
 - CLI-facing dynamic formatting uses aggregate wrapper names directly (for example `Max(2)`, `Min(None)`, `Or(true)`, or `Sum(56)`)
-- Graph types: SimpleGraph, PlanarGraph, BipartiteGraph, UnitDiskGraph, KingsSubgraph, TriangularSubgraph
+- Graph types: SimpleGraph, PlanarGraph, BipartiteGraph, UnitDiskGraph, KingsSubgraph, TriangularSubgraph, SimpleDigraph, MultiDigraph, MultiMixedGraph
 - Weight types: `One` (unit weight marker), `i64`, `f64` — all implement `WeightElement` trait
 - `WeightElement` trait: `type Sum: NumericSize` + `fn to_sum(&self)` — converts weight to a summable numeric type
 - Weight management via inherent methods (`weights()`, `set_weights()`, `is_weighted()`), not traits
@@ -228,7 +228,7 @@ fields to issue templates. Changes to issue templates require user approval.
 ### Paper (docs/paper/reductions.typ)
 - `problem-def(name)[def][body]` — defines a problem with auto-generated schema, reductions list, and label `<def:ProblemName>`. Title comes from `display-name` dict.
 - `reduction-rule(source, target, example: bool, ...)[rule][proof]` — generates a theorem with label `<thm:Source-to-Target>` and registers in `covered-rules` state. Overhead auto-derived from JSON edge data.
-- Every directed reduction needs its own `reduction-rule` entry (except trivial Decision↔Optimization pairs which are auto-filtered)
+- Every directed reduction needs its own `reduction-rule` entry (except trivial Decision↔Optimization pairs and pure `One → i64 → f64` numeric casts, which are auto-filtered)
 - Completeness warnings auto-check that all JSON graph nodes/edges are covered in the paper; `Decision<P> ↔ P` edges are excluded since they are trivial solve-and-compare reductions
 - `display-name` dict maps `ProblemName` to display text
 
@@ -302,7 +302,7 @@ Also add to the `display-name` dictionary:
 ]
 ```
 
-Every directed reduction in the graph needs its own `reduction-rule` entry. The paper auto-checks completeness against the generated `reduction_graph.json` export.
+Every nontrivial directed reduction in the graph needs its own `reduction-rule` entry. Do not add paper explanations for pure `One → i64 → f64` numeric casts. Other same-model variant reductions, such as graph transformations and bounded-integer encodings, still require entries. The paper auto-checks completeness against the generated `reduction_graph.json` export.
 
 ## Complexity Verification Requirements
 

.claude/skills/how-to-code/SKILL.md

@@ -95,7 +95,7 @@ Traits and helpers: `src/rules/traits.rs`, `src/rules/test_helpers.rs`, `src/rul
    and parameter counts vs the transform (reuse existing inputs; the shared executable-rule check lives in `src/unit_tests/parameter_formula_validation.rs`), and one test per malformed representation the decoder
    rejects (zero/multiple one-hot bits, duplicate permutation entries, ...). Aggregate edges: test
    `extract_value` against `BruteForce::solve` on both sides.
-5. Paper `reduction-rule` entry — how-to-write-manual (adapt the how-to-verify proof, don't rewrite).
+5. Paper `reduction-rule` entry — how-to-write-manual (adapt the how-to-verify proof, don't rewrite). Pure `One -> i64 -> f64` numeric casts are exempt; other same-model variant reductions still need entries.
 
 ## Traps
 

.claude/skills/how-to-write-manual/SKILL.md

@@ -24,8 +24,8 @@ The paper `docs/paper/reductions.typ` is the mathematical manual: one `problem-d
 - `reduction-rule(source, target, example:, example-source-variant:, example-target-variant:,
   example-caption:, extra:)[statement][proof]` auto-derives overhead from the graph export and
   registers the edge for the completeness check; label `<thm:Source-to-Target>`.
-- Every directed reduction needs its own entry, including reverses. Only `Decision<P> <-> P` pairs are
-  exempt. The completeness warning block at the end of the paper lists missing edges; your change
+- Every directed reduction needs its own entry, including reverses. `Decision<P> <-> P` pairs and pure `One -> i64 -> f64` numeric casts are
+  exempt; do not explain numeric casts in the paper. Nontrivial same-model variant reductions still require entries. The completeness warning block at the end of the paper lists missing edges; your change
   must never increase it.
 
 ## Example data — never invent