fix(search): close proof-audit counterexamples and certify pruning arithmetic

.github/workflows/ci.yml

@@ -33,9 +33,21 @@ jobs:
       - uses: actions/checkout@v4
       - uses: dtolnay/rust-toolchain@stable
       - uses: Swatinem/rust-cache@v2
-      # benchmark_proof brute-force cases skip gracefully without masterdata.
+      # External masterdata proofs are explicitly ignored, not counted as passes.
       - run: cargo test --all-features
 
+  exactness:
+    name: exhaustive search matrices
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@stable
+      - uses: Swatinem/rust-cache@v2
+      - run: cargo test --locked --release --all-features --lib long_exact_all_scene_property_matrix -- --ignored --nocapture --test-threads=1
+      - run: cargo test --locked --release --all-features --lib validation_oracle_extended -- --ignored --nocapture --test-threads=1
+        env:
+          ALLIUM_VALIDATION_ORACLE_SEEDS: 16
+
   msrv:
     name: msrv (1.89)
     runs-on: ubuntu-latest

docs/exactness-proof.md

@@ -98,11 +98,14 @@ Top-K set, and the best canonical representative is retained. The public
 `compare_deck_results` wrapper exposes this same order for aggregation paths;
 callers must not replace it with a score-only comparator.
 
-Numeric branch-and-bound thresholds deliberately ignore later tie-break fields.
-For maximizing searches, a branch is discarded only when its admissible upper
-bound is strictly below the current K-th score. Equality is retained, including
-the SIMD mask. For minimization, the dual rule discards only when the
-admissible lower bound is strictly above the K-th value.
+A numeric-only branch-and-bound test deliberately ignores later tie-break
+fields: maximizing searches discard a branch only when its admissible upper
+bound is strictly below the K-th score; minimization uses a lower bound
+strictly above it. Equality survives these tests, including the SIMD mask.
+The Power/Skill specializations may additionally reject equality when a proved
+lower bound on the public-set key is strictly worse than the K-th set
+(pruning-proof Sections 20.5 and 21.2). Their smallest-ID frontiers carry an
+explicit occupied length: public ID 65535 is a value, never an empty slot.
 
 This strict relation is required even when K incumbents already exist: an
 equal-objective branch may contain a distinct public set or a canonically better
@@ -207,8 +210,10 @@ every completion-relevant condition represented by the mode:
 - attribute and unit-membership semantics needed by the remaining deck are
   identical;
 - fixed public identities are never removed;
-- for World Bloom, worst-case support-deck displacement is bounded and any
-  deficit is paid for by guaranteed base event-bonus surplus;
+- for World Bloom, sorted support order statistics must not decrease, or the
+  guaranteed base surplus must exceed the outward-bounded support loss by
+  more than the proved two-deck floating-point error; equality over the reals
+  alone never authorizes compensation (pruning-proof Theorems 3a–3b);
 - for Final member-only dominance, leader-only numeric benefits are excluded
   from the comparison and the appropriate leader support profile is used.
 
@@ -226,9 +231,14 @@ card by its surviving dominance root to obtain D'. By substitutability,
 
     objective(D') >= objective(D),
 
-and when objectives tie, D' is not canonically worse. If D belongs to the true
-Top-K, D' is therefore at or above the K-th threshold in the compacted pool.
-Production search discovers the root set. Post-search substitution expansion
+and when objectives tie, D' is not canonically worse. If K distinct compacted
+public sets preceded the best compacted representative of D', their full-pool
+representatives would also precede D, contradicting its true Top-K rank. Thus
+the root set is retained. This is a full-order counting argument, not merely a
+comparison with a numeric threshold. Production search discovers the root set.
+Before inverse-score pruning, reconstruction enumerates every original
+cultivation realization of a retained public set; the best realization can
+change after another card is substituted. Post-search substitution expansion
 walks the inverse dominance chains, re-evaluates every substituted deck exactly,
 and merges legal distinct public sets through the canonical tracker. Multi-slot
 substitutions are recursive, so chains involving more than one dominated card
@@ -335,8 +345,12 @@ bonus: the logarithm of the event-point ceiling of every deck that can reach
 the threshold is at most an affine function of its aggregate features
 (pruning-proof Section 18.8). Each group is weighted by its best card under
 that function, and a node is pruned when the sum of the weights it can still
-reach is below the logarithm of the threshold's event point. Like the other
-tests it only discards subtrees without a deck at or above the threshold.
+reach is below the logarithm of the threshold's event point. All model preparation, logarithms, weights,
+sums and threshold subtraction have outward interval bounds. Logarithms use
+an atanh series with an explicit remainder, not a platform `ln` error
+assumption. An uncertifiable near-degenerate chord falls back to the independent
+bound. Like the other tests it only discards subtrees without a deck at or
+above the threshold.
 
 ### 5.3 Support-deck upper bound
 
@@ -543,7 +557,10 @@ same resolved skill tables / semantics used by evaluation. A bound may relax
 correlations upward, but it may not silently change numeric precision in a way
 that can underestimate a legal completion.
 
-The floating-point side of these invariants is proved in
+Cross-deck support compensation and the log-linear optimization have separate
+floating-point proofs in pruning-proof Sections 5 and 18.8; neither follows
+merely from a real-valued inequality. The aggregate floating-point invariants
+are proved in
 [pruning-proof.md, Section 29](pruning-proof.md#29-numeric-admissibility): every
 integer or fixed-point ceiling dominates the `f64` leaf evaluator after its
 truncations, because the ceilings' integer grids are coarser than the
@@ -584,6 +601,10 @@ state.
 
 ## 15. Verification evidence and what each class proves
 
+The [2026-09-26 audit and repairs](proof-audit-20260926.md) records concrete
+wrong-result counterexamples, their regression tests, and the distinction
+between repaired proof obligations and empirical release evidence.
+
 The runnable matrix and evidence boundaries are documented in
 [search-validation.md](search-validation.md). Final Top-K reconstruction must
 keep a forced leader in the concrete first slot: event bonuses and support

docs/proof-audit-20260926.md

@@ -0,0 +1,141 @@
+# Proof audit: 2026-09-26
+
+Base audited: `165ff63525be2c13d4ae9b6417924e0b789e5ff6`.
+
+This review compares the implementation with `exactness-proof.md` and
+`pruning-proof.md`. It does not change the leaf evaluator to make search
+counterexamples disappear. The two reproduced wrong-result cases are distinct
+from arithmetic hazards and incomplete arguments found during the repair.
+
+## Reproduced wrong results
+
+### Floating-point support compensation
+
+Six cards give two possible public sets. Cards 100 and 200 have the same
+character, attribute, unit mask, power (90,000 in every context) and skill (100).
+Their base bonuses are 64.1% and 62.5%; four other characters have no bonus.
+The support profile, count 4, is:
+
+```text
+(100, 7.05), (200, 5.45), (300, 2.05), (301, 0.8), (302, 0.5)
+```
+
+Over the reals both choices total 72.9%. The unchanged evaluator produces
+72.89999999999999147 and 72.90000000000000568, and MYSEKAI values 1728 and
+1729. In Final Chapter with character 2 fixed as leader, the old dominance
+predicate deleted card 200 and returned `Complete` with 1728. The exhaustive
+ordered oracle and dominance-disabled search returned 1729.
+
+Repair: support order-statistic monotonicity handles the no-loss case; a
+positive loss requires a strict outward-certified surplus exceeding the
+proved two-deck floating error. Malformed profiles cannot certify deletion.
+See pruning-proof Theorems 3a and 3b. The inverse substitution theorem now
+inherits preservation of the implemented objective, not just a real formula.
+
+Permanent tests: `proof_audit::support_compensation_preserves_actual_floating_point_top_one`,
+`strict_support_surplus_still_allows_certified_dominance`, and malformed-profile
+regressions. The first also exercises K > 1, ordinary WL and other targets.
+
+### Public ID 65535 is not an empty slot
+
+The eight `(public ID, power)` rows are:
+
+```text
+(101,107), (106,107), (104,105), (102,109),
+(107,108), (105,101), (103,110), (65535,105)
+```
+
+They have distinct characters and identical composition contexts. Power K=20
+previously returned `Complete`, with rank 20 equal to
+`534 / [101,103,104,106,65535]` instead of the canonical
+`534 / [101,102,104,107,65535]`.
+
+Repair: both Power and generic numeric ID frontiers use `SmallestIds` with an
+explicit occupied length. Every `u16` remains representable. No new candidate
+filter or reduced public-ID range is introduced.
+
+Permanent tests include the exact failing box, deterministic tied boxes,
+Power/Skill/MYSEKAI, constrained Power, minimization, and the builder's acceptance
+of public ID 65535. See pruning-proof Sections 3.3, 20.5 and 21.2.
+
+## Additional repair obligations
+
+| Area | Defect or missing argument | Repair |
+| --- | --- | --- |
+| Log-linear bound | A fixed epsilon and a few-ulp claim do not certify a ratio of nearly equal logarithms | Outward interval preparation, an explicit atanh-series logarithm remainder, certified endpoint widening, and fallback for an uncertifiable chord |
+| Log-bound consumers | Ordinary sums and last-group subtraction also need an error argument | Products/sums upward; threshold logarithm and threshold-minus-fixed terms downward at every consumer |
+| Event cutoff inversion | Probe values can exceed legal-leaf maxima; narrowing event stages could wrap | Shared `i128` stages and a final monotone clip above every supported leaf output |
+| Optional joint bound | Large coefficient/rational intermediates are not covered merely by bounded final scores | Checked coefficient/product/denominator operations; decline or return an infinite ceiling on overflow |
+| Support-only identity | A card excluded from the main pool could still have its support ID clamped before deduplication | Checked conversion before constructing support seeds, including the standalone support operation |
+| Raw character identity | A malformed character could be skipped before the later representation check | Validate before the unit-mask preparation filter |
+| Root recovery proof | Numeric threshold alone does not establish membership in canonical Top-K | Full-order counting argument and explicit cultivation enumeration before inverse-score pruning |
+| Floating operation count | Reference shares are not generally quarter-integral; Multi Average adds another dependency chain | Count the whole dependency path conservatively and distinguish loose bounds from legal-leaf maxima |
+| Evidence reporting | Missing external data returned from tests as if successful | Explicit ignored tests; an explicit invocation without prerequisites fails |
+
+The log-linear analytic derivation remains in Section 18.8. Its machine
+arithmetic now follows that derivation using interval enclosures. No platform
+`ln` accuracy assumption or heuristic epsilon authorizes pruning. No claim of a
+third end-to-end wrong-result counterexample is made for the old log bound.
+
+## Verification
+
+The core patch was checked on native x86-64, Rust 1.98.1, one pinned logical
+CPU with an 80% quota and a 1536 MiB memory limit, without swap:
+
+```sh
+cargo fmt --all --check
+cargo clippy --locked --all-features --all-targets -- -D warnings
+cargo test --locked --release --all-features
+cargo test --locked --release --all-features --lib \
+  long_exact_all_scene_property_matrix -- --ignored --nocapture --test-threads=1
+ALLIUM_VALIDATION_ORACLE_SEEDS=16 cargo test --locked --release --all-features \
+  --lib validation_oracle_extended -- --ignored --nocapture --test-threads=1
+```
+
+The native unit suite passes 308 tests with 8 explicitly ignored. The default
+integration suite runs its corpus-classification test and explicitly ignores
+three external-masterdata proofs; one doctest passes. The all-scene matrix
+passes 256 cases / 3840 comparisons. The 16-seed extended matrix passes 4608
+contexts, 18,432 complete searches, 13,765,632 ordered assignments and 287,232
+compared rows (oracle digest `6c7ca192360864cb`).
+
+Additional checks on the same implementation:
+
+- the separate Server workspace passes 13 unit tests and 13 HTTP/engine parity
+  tests locally; hosted CI also passes its release tests and default/jemalloc/
+  mimalloc lint configurations;
+- hosted CI passes `cargo check --all-features --locked` on Rust 1.89;
+- a real `wasm32-unknown-unknown` release module builds with Rust 1.94.0 and
+  version-matched wasm-bindgen 0.2.126 bindings;
+- Node 22.17.0 executes nine synthetic cases, each three times, matching 288
+  result rows against the native CLI. Cases cover Power, Power minimization,
+  Skill, Solo Average Score, Auto Score, Multi event Score, Cheerful Score,
+  MYSEKAI and Bonus. The comparison retains integer objective keys as decimal
+  strings, and compares order, power, skill and cultivation fields as well as
+  completion. Inputs include a legal public ID 65535;
+- the native build of `wasm/` contains zero tests and is **not** counted as
+  execution of the WebAssembly module.
+
+The runtime fixture is derived solely from `server/fixtures/synthetic.rs`:
+its full masterdata is retained while the account is restricted to eight
+characters, with one public card identity changed consistently to 65535.
+These are nine inputs, not 27 independent inputs. This smoke check does not
+replace Final/WL coverage or a real-browser release gate. The PR records
+hosted check status separately from these local results.
+
+The ordinary PR/push CI now executes both exhaustive synthetic matrices.
+`ExactOracle` independently enumerates placements and canonical public sets,
+but shares the leaf evaluator. It proves search equivalence only on the tested
+finite boxes, not independent correctness of the game's scoring rules.
+
+## Scope
+
+The low-level search theorem assumes a pool and context preserving the handler's
+numeric, representation, support-order and alignment invariants. It is not a
+promise for arbitrary invalid mutations of `SearchContext`.
+
+This review repairs the counterexamples and the identified proof obligations;
+it is not a machine-checked whole-program proof or a claim that no other bug
+exists. No real-account corpus, production-tail latency, or real-browser
+release acceptance is inferred from synthetic/native tests. In particular,
+this correctness change does not certify a 20 ms performance target.