diff --git a/research/restoration-coalescing/CERTIFICATE.json b/research/restoration-coalescing/CERTIFICATE.json new file mode 100644 index 0000000000..0876a1c366 --- /dev/null +++ b/research/restoration-coalescing/CERTIFICATE.json @@ -0,0 +1,94 @@ +{ + "base": "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08", + "cases": { + "hetero_negative": { + "children": 3, + "composed_form": "dense", + "composed_inverse_dense": true, + "composed_inverse_nnz": 64, + "deferred_dense_mults": 64, + "deferred_factorized_mults": 16, + "deferred_factorized_passes": 3, + "eager_structured_mults": 16, + "factorized_matches_dense": true, + "mult_elimination": false, + "observables_equal": true + }, + "perm": { + "children": 3, + "composed_form": "perm", + "deferred_moves": 8, + "deferred_restoration_passes": 1, + "eager_moves": 24, + "eager_restoration_passes": 3, + "observables_equal": true + }, + "phase": { + "children": 3, + "composed_form": "diag", + "deferred_mults": 8, + "deferred_restoration_passes": 1, + "eager_mults": 24, + "eager_restoration_passes": 3, + "mult_ratio": "3", + "observables_equal": true + }, + "reader_cancellation": { + "children": 5, + "deferred_restoration_passes": 1, + "eager_restoration_passes": 5, + "observables_equal": true, + "reader_coefficients": [ + "1", + "1", + "1", + "-1", + "1" + ], + "readers_nonzero": true, + "summed_defect_zero": true + }, + "reader_negative": { + "discrepancy": [ + [ + "0", + "0" + ], + [ + "3", + "-1" + ], + [ + "4", + "0" + ], + [ + "6", + "0" + ], + [ + "3", + "-1" + ], + [ + "6", + "4" + ], + [ + "6", + "0" + ], + [ + "3", + "5" + ] + ], + "discrepancy_nonzero": true, + "observables_equal": false, + "summed_defect_nonzero": true + } + }, + "dimension_N": 8, + "e": 3, + "summary": "phase=PASS perm=PASS hetero_dense=CONFIRMED reader_diverges=CONFIRMED reader_cancels=CONFIRMED factorized_matches_dense=CONFIRMED" +} \ No newline at end of file diff --git a/research/restoration-coalescing/CLAIM.json b/research/restoration-coalescing/CLAIM.json new file mode 100644 index 0000000000..7ca62654f2 --- /dev/null +++ b/research/restoration-coalescing/CLAIM.json @@ -0,0 +1,47 @@ +{ + "track": "recursive-interfaces", + "track_range": "50-59", + "assignment_seed": 53, + "seed_source": "operating-system randomness (Cryptographic RandomNumberGenerator), 0-99", + "contributor": "Navinor", + "ai_assistance": "with help from opencode", + "base_commit": "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08", + "branch": "research/agent-13-recursive-seed53", + "object_investigated": "Elimination of per-child dirty-workspace restoration across one recursion batch by deferring it to a single composed restoration at the node exit.", + "proposed_method": "Exact Gaussian-rational operator algebra at N=8: eager (restore after every child) vs deferred (restore once at exit). Two questions decided exactly: the summed-defect criterion sum_i B_i (G_{i-1}...G_1 - I) = 0 for exact observables (read-free batches are SUFFICIENT, not necessary) and composable restoration family / retained factorization (cost).", + "parameter_range": "N=8 coefficient positions (e=3); r=3 children per node; restoration families: diagonal unit phases (a in {1,2,3} via i^(a*popcount)), cyclic permutations (shifts {1,2,4}), and a heterogeneous mix (phase+Walsh+permutation).", + "candidates_considered": [ + "Coalesce per-child dirty-workspace restoration across a batch (chosen)", + "Defer compact-control exceptional-address repair charged at every node to the root", + "Eliminate the Walsh entrance/exit boundary between same-subset children" + ], + "overlap_check": { + "CrocSwap/integer-mult-bounds#1012": "concurrent, same track 50-59 (seed 57, thakrarsagar): prices restoration DEFERRAL of U8 helper rank/frame climbs at the ASSEMBLY level (hosted T37 recurrence, coverage identity, kappa ceilings), finds it mass-neutral. Distinct layer and cost unit from this note's OPERATOR-level coalescing of phase/routing restoration passes. Complementary; not duplicated; numbers not reproduced here.", + "CrocSwap/integer-mult-bounds#974": "concurrent, same track (avirazza): prices the same boundary classes with zero parent cost at the assembly level. Distinct method; not duplicated.", + "research/seed51-clean-residual-dilation": "seed 51, recursive-interface track; prices a spectral-split residual ENCODER and its per-stream dirty restoration. Different object (encoded hosting vs restoration coalescing), different boundary. No duplication.", + "kernel-frame-coalescing": "changes frame ranks (rank-1 to rank-2 climbs), not restoration passes. Different cost axis.", + "universal-connector-boundary": "query-path / dirty-connector census; supplies the restoration invariant this note prices, not the coalescing mechanism." + }, + "expected_deliverable": "A research note with a complete restoration cost recurrence, a sharp correctness boundary (read-free), a sharp cost boundary (composable family), and an exact stdlib verifier with two positive cases and two negative controls. No new kappa.", + "pinned_coordination_issue": "none reachable; claim recorded locally", + "expected_finish": "same session; verification reserved for the final quarter", + "status": "completed", + "result": "Scoped research note: a complete restoration cost recurrence plus (corrected) the exact terminal-observation criterion sum_i B_i (G_{i-1}...G_1 - I) = 0 for the observables, with read-free batches as a sufficient, not necessary, condition, and a cost boundary (pass reduction r->1 when the restorations collapse under composition to one cheap pass, with composition charged r*c_desc under the succinct descriptor hypothesis (c_desc = O(1)) and Theta(r*N) for full-length descriptor tables; deferral costs more only when no cheap factorization is retained and the dense product is applied directly). Two positive cases (phase 3->1 passes / 24->8 mults; permutation 3->1 passes), one example where a single reader breaks deferral, one exact nonzero-reader cancellation case (5 reader children, coefficients [1,1,1,-1,1], summed defect exactly zero, restorations 5->1), and the heterogeneous example: composed product dense (64/64 nonzero) yet its retained factorization costs the eager sum 16 mults at N=8 (verified against the dense product on every basis column), against 64 mults for DIRECT dense application. No new kappa; selected frontier and upstream/ unchanged.", + "post_review_correction": { + "trigger": "Batch review follow-up on https://github.com/CrocSwap/integer-mult-bounds/pull/1155#issuecomment-6161612247 (record: https://github.com/CrocSwap/integer-mult-bounds/blob/main/docs/research/community-efficient300-review.md)", + "corrected_claims": [ + "Correctness: read-free is SUFFICIENT, not necessary. The exact terminal-observation criterion is vanishing summed defect sum_i B_i (G_{i-1}...G_1 - I) = 0; nonzero-reader counterexamples: https://github.com/CrocSwap/integer-mult-bounds/pull/1199, https://github.com/CrocSwap/integer-mult-bounds/pull/1203, https://github.com/CrocSwap/integer-mult-bounds/pull/1205. Prefix/adaptive observation requires each prefix defect B_i (P_{i-1} - I) to vanish (https://github.com/CrocSwap/integer-mult-bounds/pull/1205).", + "Cost: matrix density of the composed product is not an application-cost statement. A dense phase/Walsh/permutation product retains its cheap factorization; sequential factor application costs the eager sum (verified 16 = 16 mults at N=8). Deferral costs more only when no cheap factorization is retained and the dense product must be applied directly; the 64 vs 16 numbers at N=8 are kept as a statement about DIRECT dense application only." + ], + "unchanged": "The original reader counterexample (one reader can break deferral) and the original heterogeneous direct-dense counts (64 vs 16 at N=8) still run unchanged; only their scope is corrected." + }, + "post_review_correction_2": { + "trigger": "Second review follow-up on https://github.com/CrocSwap/integer-mult-bounds/pull/1155#issuecomment-6197859152 (record: https://github.com/CrocSwap/integer-mult-bounds/blob/main/docs/research/community-efficient1100-review.md)", + "corrected_claims": [ + "Cost recurrence: the O(r) descriptor-composition and one-pass terms are charged under an explicit succinct descriptor hypothesis (fixed-size parameter tuples: phase G = diag(omega^(a*chi(x))) with one exponent a and per-node character chi (checker shape chi(x)=popcount(x), q=4); permutation x -> +-x + s (mod N) with one shift s). Composition is r*c_desc with c_desc = O(1) under the hypothesis; the general full-length-descriptor case is recorded at Theta(r*N) to form the composed table, not O(r).", + "Evidence scope: the N=8 checker (r=3 phase/rotation/heterogeneous, r=2 reader, r=5 cancellation, all composed as exact dense products) establishes exact observables and costs on those instances only; the general r,N recurrence is a priced hypothesis, not a tested identity." + ], + "unchanged": "All algebraic content and every cost number of the first correction and of the original cases stand unchanged; only the pricing scope of the composition/bookkeeping term changed." + }, + "pr_url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1155" +} diff --git a/research/restoration-coalescing/README.md b/research/restoration-coalescing/README.md new file mode 100644 index 0000000000..9773fc6661 --- /dev/null +++ b/research/restoration-coalescing/README.md @@ -0,0 +1,429 @@ +# Restoration coalescing across a recursion batch + +Research note: one explicit way to eliminate restoration work, with a complete +cost recurrence, a sufficient correctness condition (and the exact defect +criterion behind it), and a sharp cost boundary. Navinor, with help from +opencode. Apache-2.0. **No new multiplication exponent.** + +## Summary + +Every recursive child that borrows a dirty workspace stream must return it, and +the inherited contract restores it **after every child** so that the next child +sees the node-entry state. When a node issues `r` children this pays `r` +restoration passes. This note prices a single operator-level change: let the +workspace drift across the batch and replace the `r` restorations by the **one** +composed restoration `(G_r...G_1)^{-1}` at the node exit. The question is not +what a particular assembly does with that slack (that is assembly pricing), but +when this rewrite is even a *valid and pass-reducing identity on the restored +operator*. Two independent questions decide it, both decidable exactly: the +summed-defect criterion (exactness) and closure under cheap composition (pass +reduction). + +* **Correctness (vanishing defect; read-free is sufficient, not necessary).** + The deferred single restoration returns the identical observables (final data + and final workspace) exactly when the summed defect vanishes, + `sum_i B_i (G_{i-1}...G_1 - I) = 0` (diagonal readers here; `P_0 = I`). A + batch in which no child reads the workspace's intermediate value into an + observable makes every term vanish separately, so read-free is a clean + **sufficient** condition — but it is **not necessary**: nonzero readers can + cancel. The note's own reader example only shows one reader child *can* break + deferral. Exact nonzero-reader counterexamples where deferral is valid are in + [#1199](https://github.com/CrocSwap/integer-mult-bounds/pull/1199) (five + children reading and negating the workspace with coefficients `[1,1,1,-1,1]`, + restoration `5 -> 1`), + [#1203](https://github.com/CrocSwap/integer-mult-bounds/pull/1203) (distinct + outputs: per-reader condition `H_i(P_{i-1} - I) = 0`; one shared output at + batch exit: only the summed defect must vanish), and + [#1205](https://github.com/CrocSwap/integer-mult-bounds/pull/1205) (the + terminal summed-defect theorem and the prefix theorem `B_i(P_{i-1} - I) = 0` + per child, which still does not require `B_i = 0`). + +* **Cost (composable family; density is not application cost).** Deferral + removes restoration passes when the individual restoration operators are + closed under a composition that stays cheap to apply: unit phases -> one phase + pass, permutations -> one routing pass (`r -> 1`). The pass statement is + priced under an explicit descriptor hypothesis in the recurrence below: + composing `r` descriptors is charged `r * c_desc` (`c_desc = O(1)` for the + succinct parameter-tuple descriptors, `c_desc = Theta(N)` for full length-`N` + descriptor tables). Matrix density of the + composed product is **not** an application-cost statement: the composed + restoration retains its factorization into its cheap factors, and applying + those factors sequentially costs exactly the eager sum. For the heterogeneous + mix (a phase, a Walsh transform, a permutation) the composed restoration is + dense, yet its retained factorization is verified to cost the same `16` + multiplications as the three structured eager restorations at `N = 8`; + deferral costs *more* only when no cheap factorization is retained and the + dense product must be applied directly (`64` vs `16` multiplications at + `N = 8` — a statement about direct dense application). Structure, not the + number of restorations alone, decides. + +Both facts are checked by one exact stdlib program over Gaussian rationals. +Nothing here changes the selected frontier, `upstream/`, or the assembly. + +## Reproduce + +From the repository root, Python 3.10+, standard library only: + +```sh +python3 -I -O -B research/restoration-coalescing/verify.py +``` + +Expected first line: + +``` +PASS_RESTORATION_COALESCING phase=3->1(x3) perm=3->1 hetero_dense=True reader_diverges=True reader_cancels_5to1=True hetero_mults=eager16|factorized16|dense64 +``` + +The command recomputes the certificate and compares every field with +[CERTIFICATE.json](CERTIFICATE.json), failing on any drift. `--json` prints the +full certificate; `--write PATH` writes the same deterministic result elsewhere. +There is no floating point, no random tolerance, and no imported supplier +verifier. Coefficients are exact Gaussian rationals (`Fraction` real and +imaginary parts); the checker builds every operator explicitly at `N = 8`. + +## Starting point and scope selection + +Base commit `ce7ad1b6ab09452c3478723a2e96ed5ff212dc08` (current `origin/main`). +At this base the selected conditional result is the +`CrocSwap/integer-mult-bounds#1094`-on-`CrocSwap/integer-mult-bounds#1087` +assembly, +`kappa = 836330098538459/500000000000000000 = 0.001672660197076918`; see the +[selected record](../../certificates/selected-result.json) and +[current status](../../docs/research/current-status.md). This note does not +adopt any larger number from a pending pull request. + +The OS-generated assignment seed was **53**, assigning the recursive-interface +track (one explicit way to eliminate boundary or restoration work, with a +complete cost recurrence). The three candidates I weighed were: coalescing +per-child dirty-workspace restoration (chosen); deferring the compact-control +"exceptional-address repair charged at every node"; and eliminating the Walsh +entrance/exit boundary between same-subset children. The seed selected +restoration coalescing because it is the one whose correctness and cost +conditions can both be decided exactly and independently, without re-opening a +closed supplier search. + +There was no pinned sprint coordination issue reachable here. The local +[claim](CLAIM.json) records the three candidates, the overlap check against +`research/seed51-clean-residual-dilation` (seed 51, recursive-interface track: +a spectral-split residual encoder, a different object), and the scope. +Exact source and dependency heads are in [SOURCE-PINS.json](SOURCE-PINS.json). + +## The model + +State is a data stream `D` and a borrowed dirty workspace stream `W`, each of +`N` Gaussian-rational positions, plus a read-only source vector `s`. A node +issues `r` children. Child `i` applies an invertible workspace operator `G_i` +(as scratch) and contributes a data increment: + +``` +scratch-only child i : D' = D + B_i s , W' = G_i W +reader child i : D' = D + B_i W , W' = G_i W (reads W) +``` + +The inherited **eager** rule restores `W` to its node-entry value `w0` after +every child, i.e. it applies `G_i^{-1}` immediately. The **deferred** rule lets +`W` drift and applies the single composed restoration +`(G_r ... G_1)^{-1} = G_1^{-1} ... G_r^{-1}` at the node exit. Observables are +the final `D` and final `W`. The child data work `sum_i B_i(·)` is identical in +both schemes and cancels from the comparison; only restoration is priced. + +This is the same restoration invariant the repository already charges: dirty +connectors and private child scratch are restored +(`CrocSwap/integer-mult-bounds#905`, `CrocSwap/integer-mult-bounds#929`, +`CrocSwap/integer-mult-bounds#951`; +[universal-connector-boundary](../universal-connector-boundary/README.md)), and +the compact-control construction "restores arbitrary values ... and charges +exceptional-address repair at every node" ([current status](../../docs/research/current-status.md)). + +## Complete cost recurrence + +Write `Restore(N)` for one restoration pass over `N` coefficient positions. In +the repository's additive accounting a coefficient pass is a `Scan(N,p)`; a +diagonal unit-phase restoration is exactly one such pass, and a permutation +restoration is one routing pass. Let `r` be the children per node. The node's +restoration term is + +``` +eager : r * Restore(N) +deferred: 1 * Restore_composed(N) +``` + +**Composable family (phases, or permutations).** The composition stays in the +family: the composed restoration is again one phase descriptor (one `Scan(N, p)`) +or one permutation descriptor (one routing pass), so the applied restoration is +one pass once the composed descriptor exists. Forming that descriptor is the +composition step, and its cost depends on how a descriptor is represented; the +recurrence below states the representation it prices. + +**Descriptor hypothesis (the representation behind the `O(r)` term).** A +restoration descriptor is a fixed-size parameter tuple, not an arbitrary +`N`-entry table: + +* phase: `G = diag(omega^(a * chi(x)))` for a per-node character + `chi : {0..N-1} -> Z/q` fixed once (the checker's shape is + `chi(x) = popcount(x)`, `q = 4`), with one stored exponent `a`; +* permutation: a rotation `x -> x + s (mod N)` (the checker's shape), or any + dihedral map `x -> +-x + s (mod N)` with a constant-size tuple. + +Composing `r` descriptors in either family then combines `r` tuples +(`a <- sum_i a_i`; `s <- sum_i s_i` mod `N`): `O(r)` tuple operations, +`c_desc = O(1)` per descriptor, and the product stays in the family. Applying +the composed descriptor is exactly one pass, `Scan(N, p)` (`N` phase +multiplications) or one routing pass (`N` moves, `0` multiplications), each pass +priced as `Restore(N)`. The node pays + +``` +eager : r * Restore(N) + 0 +deferred: 1 * Restore(N) + r * c_desc +``` + +and saves + +``` +(r - 1) * Restore(N) - r * c_desc = (r - 1) * Scan(N, p) - r * c_desc +``` + +so composition is charged, not absorbed. Over a recursion with `r` children per +node and `d` levels, the restoration *pass* overhead falls by the same factor `r` +(`sum_nodes r*Scan -> sum_nodes 1*Scan`) plus the added composition charge +`sum_nodes r * c_desc`, while every child term `(k/m)^sigma / W` is untouched. +The full node recurrence, restoring only the changed term and charging +composition, is + +``` +R(N, {k_i}) = sum_i (k_i/m)^sigma / W + Restore(N) + r * c_desc + unchanged + ^ was r * Restore(N) in the inherited rule +``` + +with `c_desc = O(1)` under the descriptor hypothesis. + +**Outside the hypothesis (general descriptors).** For arbitrary per-position +unit phases or arbitrary permutations stored as full length-`N` tables there is +no succinct composition: forming the composed descriptor must read `r` tables of +`N` entries, so the composition bill is `Theta(r * N)` (and `N` storage), not +`O(r)`; the applied restoration is still one pass. The recurrence holds there +with `r * c_desc` replaced by `Theta(r * N)`. The `O(r)` term is claimed only +under the descriptor hypothesis; the general descriptor case is recorded at its +`Theta(r * N)` charge, not as `O(r)`. + +**Heterogeneous family.** The composed restoration `G_1^{-1}...G_r^{-1}` is a +dense matrix here (64 of 64 entries nonzero at `N = 8`), but density of the +matrix is not a statement about application cost. The composed operator +*retains its factorization* into the three cheap structured inverses; applying +them sequentially costs exactly the eager sum — `16` multiplications at +`N = 8`, verified against the exact dense product on every basis column — so +with the factorization retained deferral is multiplication-neutral (`16` vs +`16`) and pass-neutral (three factor applications, nothing collapses to one +pass). Deferral costs *more* only when no cheap factorization is retained and +the dense product must be applied directly: `64` vs `16` multiplications at +`N = 8`, `4x`. In this example deferral is therefore rejected as a pass +reduction (nothing to save), not because dense entries imply quadratic +application cost; the `64` vs `16` pair is a statement about **direct dense +application** only. + +This is a complete invoice for the restoration term only. It is not a transfer +into the tight fixed-tape overhead allowance, and it makes no claim that the +restoration term is binding in the selected assembly. If restoration is a +lower-order term beside the child recursion, the induced change to `kappa` is +zero. **No stronger bound is claimed.** + +## Exact evidence and limits + +`verify.py` builds every operator explicitly at `N = 8` over Gaussian rationals +and checks, on the actual vectors: + +1. **Phase batch (3 children, read-free).** Deferred equals eager on both + observables; the composed restoration is verified to be diagonal and applied + as one pass. Restoration passes `3 -> 1`; multiplications `24 -> 8`. +2. **Permutation batch (3 children, read-free).** Deferred equals eager; the + composed restoration is verified to be a permutation and applied as one + routing pass. Restoration passes `3 -> 1`; moves `24 -> 8`; multiplications + `0 -> 0`. +3. **Reader example (sufficiency, not necessity).** A single reader child is + inserted. The final workspace is still restored to `w0`, but the data output + of the deferred scheme differs from eager by an explicit nonzero + Gaussian-rational vector, and the exact summed defect is nonzero. This is a + concrete counterexample to *unrestricted* deferral — one reader child **can** + break it, so read-free is sufficient. It is **not** evidence that read-free is + necessary. +4. **Nonzero-reader cancellation (necessity fails).** Five reader children, each + reading and negating the workspace with coefficients `[1,1,1,-1,1]` (the + counterexample shape of + [#1199](https://github.com/CrocSwap/integer-mult-bounds/pull/1199)). Every + child reads `W`, four of them after nonidentity drift, yet the exact summed + defect `sum_i B_i (G_{i-1}...G_1 - I)` is verified to be the zero matrix and + deferred equals eager on both observables for the tested `w0`. The + restoration bill falls from five negations to one (`5 -> 1`). The + checker computes the defect matrix as exact Gaussian rationals and asserts + it vanishes, so the cancellation is an algebraic identity on all workspace + coordinates, not a coincidence on one vector. +5. **Heterogeneous composition (cost; density is not application cost).** A + phase, a Walsh transform and a permutation compose to a dense operator (64 of + 64 entries nonzero). The structured-form detector self-checks each cheap + application against the exact dense product on the standard basis before + using it, so the low cost figures are certified against the exact operator + rather than assumed. Direct dense application of the composed product is `64` + multiplications against the eager structured sum `16`: the `64` vs `16` pair + is a statement about **direct dense application**. Applying the same exact + composed restoration through its **retained factorization** (the three + structured inverses in sequence, self-checked against the dense product on + every basis column) costs exactly `16` — the eager sum — so deferral with the + factorization retained is multiplication-neutral here, and costs more only + when no cheap factorization is retained. + +For each batch the composed restoration is *derived* from the exact dense +product `G_1^{-1} ... G_r^{-1}` and then checked to agree with it, so a +composition-order bug cannot silently flatter the result. What this establishes +is instance-level: exact observables and exact costs at `N = 8` for `r = 3` +(phase batch, rotation batch, heterogeneous mix), `r = 2` (single reader) and +`r = 5` (cancellation batch), with every composition performed as an exact +dense product. It does not establish the recurrence for arbitrary `r` and `N`: +the `O(r)` descriptor composition and the one-pass composed application are the +charges of the descriptor hypothesis above (an implementation hypothesis about +a succinct descriptor representation, not a tested identity), and outside that +hypothesis the recorded charge is `Theta(r * N)`. Controls that must +fail do fail: no "no candidate" claim, no impossibility theorem, no optimality +claim for the eager rule. + +The scope is a restoration-elimination mechanism, its recurrence, and its exact +applicability boundary. It is **not** an all-size physical compiler, a numerical +precision contract, a common tape, an analytic transfer, a full owner schedule, +or the integer-multiplication theorem. The finite checks are exact algebraic +identities and exact cost counts; they do not certify a whole E8 word or the +selected `kappa`. Neither the selected frontier nor `upstream/` changes. Inherited +all-size/compiler, hosting, precision/tape and analytic assumptions remain with +their existing constructions. + +## Relation to concurrent and prior work + +Two concurrent, same-track contributions already price *restoration deferral* at +the assembly level, and this note is deliberately narrower and complementary, +not a replacement or a re-derivation of either. + +* **[CrocSwap/integer-mult-bounds#1012](https://github.com/CrocSwap/integer-mult-bounds/pull/1012)** + (thakrarsagar, seed 57) prices restoration deferral of the U8 helper + rank/frame *climbs* inside the hosted T37 recurrence, using the hosting lemma + and the `8k+1+hosted+idle=73` coverage identity, and reports exact kappa + ceilings. Its conclusion is that deferral is *mass-neutral* there and its value + is consolidation inside shared hosting windows. That is a statement about rank + mass and window capacity in one frozen assembly. + +* **[CrocSwap/integer-mult-bounds#974](https://github.com/CrocSwap/integer-mult-bounds/pull/974)** + (avirazza, same track) prices the same boundary classes with zero parent cost; + thakrarsagar's note independently reproduces its T37 one-unit value. + +This note asks a different question at a different layer: **as an operator +identity, when does replacing `r` restorations by one composed restoration +preserve the observables and actually remove passes?** Its two answers — the +summed-defect criterion (correctness; read-free is one sufficient case) and the +composable-family condition (cost) — are exact algebraic facts about the +restored operator, independent of any assembly, kappa ceiling, hosting lemma, or +T37 payload. The cost unit here is a +coefficient/routing pass (a diagonal unit phase is one `Scan`, a permutation is +one `Route`, per the retained recurrence vocabulary), not the rank mass those +assembly notes count. So there is no contradiction with the "mass-neutral" +finding there: helper climbs are rank-advancing frame work whose mass is +coverage-productive, whereas the restoration passes coalesced here are +phase/routing passes whose operators compose. This note gives the +operator-level preconditions and a standalone sub-second exact verifier (no T37 +archives, no pinned engines); those notes give the assembly-level ceiling +effect. Both are needed before deferral can be placed in a real supplier call. +Where thakrarsagar's note shows the T37 slack is consolidation in shared +windows, this note shows exactly which restoration families admit a genuine +`r -> 1` pass reduction at all, and which (heterogeneous) leave nothing to +collapse — costing more only under direct dense application of the product. + +This is a second, independent treatment of the restoration question using a +meaningfully different method (exact Gaussian-rational operator algebra and +structure detection, versus assembly-level pricing on frozen payloads), as the +sprint invites. It does not claim priority on "restoration deferral" and does not +reproduce either note's numbers. + +## Correction after review (read-free is sufficient, not necessary) + +The original version of this note claimed the read-free condition was +*necessary and sufficient*, and treated density of the composed heterogeneous +product as proof that deferred application costs more. Both claims were wrong; +the corrected statements are the ones above. The evidence: + +* **[CrocSwap/integer-mult-bounds#1199](https://github.com/CrocSwap/integer-mult-bounds/pull/1199)** + (thakrarsagar) gives an exact nonzero-reader counterexample in the shape the + checker now replays: five children that each read and negate the workspace + with reader coefficients `[1,1,1,-1,1]` share one final restoration + (five negations -> one) with identical observables. Its exact interval + criterion `E_ab = sum_{i=a}^{b-1} b_i (p_i - 1)` (and the general linear form + `sum B_i (P_i - I) = 0`) replaces the iff, and its checkpoint planner shows + intermediate observation points can force the restoration bill back up. +* **[CrocSwap/integer-mult-bounds#1203](https://github.com/CrocSwap/integer-mult-bounds/pull/1203)** + (mightyOil) separates the two observation contracts: with distinct outputs + the exact all-input condition is `H_i (P_{i-1} - I) = 0` per reader; with one + shared output observed only at batch exit only the summed defect must vanish. + Its example `G_1 = swap(0,1)`, `G_2 = G_3 = I`, readers `0, e_0, e_1` has + nonzero readers whose defects cancel exactly. +* **[CrocSwap/integer-mult-bounds#1205](https://github.com/CrocSwap/integer-mult-bounds/pull/1205)** + (adamgall) states the terminal theorem for the additive model exactly — + agreement for every dirty input iff `sum_i B_i (P_{i-1} - I) = 0`, with + `P_j = G_j ... G_1`, `P_0 = I` — and the prefix theorem + `B_i (P_{i-1} - I) = 0` per child, which still does not require `B_i = 0`. + Its census of 46,656 three-child tuples finds 7,712 terminal-safe tuples + containing a nonzero reader. + +The correction was requested in the batch review comment on this pull request +([comment](https://github.com/CrocSwap/integer-mult-bounds/pull/1155#issuecomment-6161612247), +[batch review record](https://github.com/CrocSwap/integer-mult-bounds/blob/main/docs/research/community-efficient300-review.md)). +The original evidence is untouched and still runs: the reader example shows +only that one reader *can* break deferral, and the `64` vs `16` pair counts +**direct dense application**. The checker now additionally verifies the exact +summed-defect criterion on both reader examples and the retained-factorization +cost of the heterogeneous composition (`16` factorized = eager `16` against +`64` direct dense at `N = 8`). Remaining open: the checkpoint/partition +optimum over intermediate observation points (priced by +[CrocSwap/integer-mult-bounds#1199](https://github.com/CrocSwap/integer-mult-bounds/pull/1199) +for its own model, not derived here), and the question of when a dense +composition whose factors are *discarded* must be paid as `N^2` — this note +answers only that direct dense application is the expensive case. + +## Correction after review (composition and routing are charged) + +A second review pass +([comment](https://github.com/CrocSwap/integer-mult-bounds/pull/1155#issuecomment-6197859152), +[batch review record](https://github.com/CrocSwap/integer-mult-bounds/blob/main/docs/research/community-efficient1100-review.md)) +found the cost recurrence pricing `r`-descriptor composition at `O(r)` and the +composed restoration at one `Scan`/routing pass with no descriptor +representation behind those terms, and the explicit `N = 8` matrix tests as the +only evidence. The recurrence now states the descriptor hypothesis (fixed-size +parameter tuples; `O(r)` tuple composition; one-pass application once the +composed descriptor is formed) and charges composition explicitly as +`r * c_desc`; the general full-length-descriptor case is recorded at its +`Theta(r * N)` composition bill instead of `O(r)`; and the evidence section +separates what the `N = 8` checker establishes from the priced general +recurrence. No verified algebraic content or cost number from the first +correction or from the original cases changed. + +## Attribution + +The eager per-child restoration contract and the dirty-connector model are +repository-wide: `CrocSwap/integer-mult-bounds#905`/ +`CrocSwap/integer-mult-bounds#929`/ `CrocSwap/integer-mult-bounds#951` (Chafik +Boukhalfa), `CrocSwap/integer-mult-bounds#877`/ +`CrocSwap/integer-mult-bounds#896` (Gareth Davidson), +`CrocSwap/integer-mult-bounds#934`/ `CrocSwap/integer-mult-bounds#943`/ +`CrocSwap/integer-mult-bounds#944`/ `CrocSwap/integer-mult-bounds#953` (Ross +Richardson), and +[universal-connector-boundary](../universal-connector-boundary/README.md). The +compact-control per-node restoration/repair charge is credited to Douglas +Colkitt's retained construction ([current status](../../docs/research/current-status.md)). +The unequal-width child recurrence `(k/m)^sigma / W` is from the retained +[complex batching note](../../notes/batched-complex-rows.tex). + +The sibling recursive-interface note +[research/clean-residual-dilation](../clean-residual-dilation/README.md) (seed 51, +Douglas R. Colkitt with Codex) prices a *spectral-split residual encoder* and its +own per-stream dirty restoration. This note is a different object (restoration +coalescing across a batch, not encoded hosting), reaches a different and +independent boundary (vanishing summed defect + composable family), and does not +rely on its +conclusions. Where both charge a "restoration" pass, the accounting vocabulary is +shared but the mechanisms are distinct. This encoder-free coalescing result, +exact checker and scoped recurrence were developed by Navinor with help from +opencode, under the repository's Apache-2.0 license. diff --git a/research/restoration-coalescing/SOURCE-PINS.json b/research/restoration-coalescing/SOURCE-PINS.json new file mode 100644 index 0000000000..c8ae95808e --- /dev/null +++ b/research/restoration-coalescing/SOURCE-PINS.json @@ -0,0 +1,47 @@ +{ + "base_commit": "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08", + "base_remote": "https://github.com/CrocSwap/integer-mult-bounds (origin/main)", + "note": "All in-repository references below resolve at the base commit. SHA-256 is over the exact committed bytes.", + "in_repo_sources_sha256": { + "notes/batched-complex-rows.tex": "64c70926a8705874f1c9b42a2f703e42cad4e90f927f544458cfdf729540236c", + "certificates/selected-result.json": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "docs/research/current-status.md": "1f59d648763c77d574d18dc59ea8bf62d2ee74aaed3c202c9c8cfa4f901badbd", + "docs/research/pr-ledger.md": "4c8ea39063531bb218506e613c5b48d5fd8ea309071dd7bace4f47481021a0a7", + "research/universal-connector-boundary/README.md": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476", + "CONTRIBUTING.md": "1cae543effcabab91dab7f78423ee9283e60fb504f10848483d153331cd72bc4" + }, + "external_ref_pins": { + "research/clean-residual-dilation (sibling seed51 note)": { + "git_ref": "refs/remotes/origin/research/seed51-clean-residual-dilation", + "commit": "d0e4f1eb295e5cce508dc76c6937290a9175e42b", + "relationship": "cited as distinct predecessor; not depended on for any identity or number" + }, + "PR1199 (thakrarsagar, reader-restoration-cuts-seed53)": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1199", + "commit": "85ac2880ea5bda44f28632b71ffa2b4e35ec6b7d", + "relationship": "source of the nonzero-reader counterexample shape (coefficients [1,1,1,-1,1], restorations 5->1) replayed in case reader_cancellation, and of the interval defect criterion; cited for the correction that read-free is sufficient, not necessary" + }, + "PR1203 (mightyOil, invariant-reader-restoration)": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1203", + "commit": "38459854fd5bb93099871a84324413bd0e338d8e", + "relationship": "cited for the distinct-output criterion H_i(P_{i-1}-I)=0 versus the shared-output summed-defect criterion; not depended on for any number" + }, + "PR1205 (adamgall, observer-safe-restoration)": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1205", + "commit": "e2008d7ffcad464da7ec21c69e8d8a8c91de4930", + "relationship": "cited for the terminal theorem sum_i B_i(P_{i-1}-I)=0 and the prefix theorem B_i(P_{i-1}-I)=0 in the additive model; not depended on for any number" + } + }, + "selected_result_at_base": { + "kappa": "836330098538459/500000000000000000", + "decimal": "0.001672660197076918", + "source_pr_top": 1094, + "reproduce": "make frontier1094-verify", + "note": "Not changed by this contribution." + }, + "stdlib_only": true, + "python_interpreters_verified": [ + "CPython 3.13 (Python313/python.exe)", + "CPython 3.12 (python3.12.exe)" + ] +} diff --git a/research/restoration-coalescing/verify.py b/research/restoration-coalescing/verify.py new file mode 100644 index 0000000000..d6740cbe06 --- /dev/null +++ b/research/restoration-coalescing/verify.py @@ -0,0 +1,753 @@ +#!/usr/bin/env python3 +"""Exact checker for the restoration-coalescing research note. + +Independently builds a recursion batch that borrows a dirty workspace stream, +then compares the inherited eager per-child restoration against a deferred +single-pass restoration. All arithmetic is exact Gaussian rationals +(Fraction real and imaginary parts); no floating point, no random tolerance, +no imported supplier verifier. Pure standard library. + +Run: + python3 -I -O -B research/restoration-coalescing/verify.py + +Expected first line: + PASS_RESTORATION_COALESCING phase=... perm=... hetero_dense=... reader_diverges=... reader_cancels_5to1=... hetero_mults=... + +`--write PATH` emits the deterministic certificate JSON to PATH. +`--json` prints the full certificate to stdout. +""" +from __future__ import annotations + +import argparse +import json +from fractions import Fraction +from hashlib import sha256 +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +BASE = "ce7ad1b6ab09452c3478723a2e96ed5ff212dc08" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +# -------------------------------------------------------------------------- +# Exact Gaussian rationals: a + b i, a,b in Fraction. +# -------------------------------------------------------------------------- +class G: + __slots__ = ("re", "im") + + def __init__(self, re=0, im=0): + self.re = Fraction(re) + self.im = Fraction(im) + + def __add__(self, other): + other = _g(other) + return G(self.re + other.re, self.im + other.im) + + __radd__ = __add__ + + def __neg__(self): + return G(-self.re, -self.im) + + def __sub__(self, other): + return self + (-_g(other)) + + def __mul__(self, other): + other = _g(other) + return G(self.re * other.re - self.im * other.im, + self.re * other.im + self.im * other.re) + + __rmul__ = __mul__ + + def conj(self): + return G(self.re, -self.im) + + def scale(self, s): + return G(self.re * Fraction(s), self.im * Fraction(s)) + + def __eq__(self, other): + other = _g(other) + return self.re == other.re and self.im == other.im + + def is_zero(self): + return self.re == 0 and self.im == 0 + + def key(self): + return (str(self.re), str(self.im)) + + def __repr__(self): + return f"({self.re}+{self.im}i)" + + +def _g(x): + return x if isinstance(x, G) else G(x) + + +def gi_pow(j): + """i^j for integer j, exact.""" + j %= 4 + return (G(1), G(0, 1), G(-1), G(0, -1))[j] + + +def popcount(x): + return bin(x).count("1") + + +# -------------------------------------------------------------------------- +# Structured appliers. Each returns (result_vector, opcount_dict). +# -------------------------------------------------------------------------- +def apply_diag(v, phases): + """Diagonal unit-phase restoration. Cost: one coefficient pass = N mults.""" + need(len(v) == len(phases), "diag dimension") + out = [p * x for p, x in zip(phases, v)] + return out, {"passes": 1, "mults": len(v), "adds": 0} + + +def apply_perm(v, perm): + """Permutation restoration. Cost: one routing pass = N moves, 0 mults.""" + need(sorted(perm) == list(range(len(v))), "perm not a permutation") + out = [v[perm[x]] for x in range(len(v))] + return out, {"passes": 1, "mults": 0, "adds": 0, "moves": len(v)} + + +def _walsh_dense(e): + n = 1 << e + H = [[G((-1) ** (popcount(x & y))) for y in range(n)] for x in range(n)] + return H + + +def apply_walsh_fast(v): + """Fast Walsh-Hadamard on e bits, then scale by 1/N = H^{-1}. + Cost: N*log2(N) adds and N mults (the 1/N scaling). Exact.""" + n = len(v) + need(n & (n - 1) == 0, "walsh length") + e = n.bit_length() - 1 + a = list(v) + adds = 0 + step = 1 + while step < n: + for i in range(0, n, 2 * step): + for j in range(i, i + step): + u, w = a[j], a[j + step] + a[j] = u + w + a[j + step] = u - w + adds += 2 + step *= 2 + scale = Fraction(1, n) + out = [x.scale(scale) for x in a] + return out, {"passes": 1, "mults": n, "adds": adds} + + +def apply_dense(M, v): + """Dense matrix-vector product. Cost: N^2 mults + N(N-1) adds.""" + n = len(v) + out = [] + mults = 0 + adds = 0 + for x in range(n): + acc = G(0) + for y in range(n): + acc = acc + M[x][y] * v[y] + mults += 1 + adds += 1 + out.append(acc) + adds -= 1 # N-1 additions per row + return out, {"passes": 1, "mults": mults, "adds": max(adds, 0), "dense": True} + + +# -------------------------------------------------------------------------- +# Linear algebra on exact matrices (used to build and verify compositions). +# -------------------------------------------------------------------------- +def mat_identity(n): + return [[G(1) if x == y else G(0) for y in range(n)] for x in range(n)] + + +def mat_diag(phases): + n = len(phases) + return [[phases[x] if x == y else G(0) for y in range(n)] for x in range(n)] + + +def mat_perm(perm): + n = len(perm) + return [[G(1) if perm[x] == y else G(0) for y in range(n)] for x in range(n)] + + +def mat_mul(A, B): + n = len(A) + out = [[G(0)] * n for _ in range(n)] + for x in range(n): + for k in range(n): + if A[x][k].is_zero(): + continue + a = A[x][k] + for y in range(n): + if B[k][y].is_zero(): + continue + out[x][y] = out[x][y] + a * B[k][y] + return out + + +def mat_vec(M, v): + n = len(v) + return [sum((M[x][y] * v[y] for y in range(n)), G(0)) for x in range(n)] + + +def mat_eq(A, B): + return all(A[x][y] == B[x][y] for x in range(len(A)) for y in range(len(A))) + + +def mat_nnz(M): + return sum(1 for row in M for c in row if not c.is_zero()) + + +# -------------------------------------------------------------------------- +# The recursion batch. +# +# State: D (data stream) and W (borrowed dirty workspace), both length N. +# A fixed source vector s (read-only) supplies each child's data increment. +# +# scratch-only child i : D' = D + B_i s , W' = G_i W +# reader child i : D' = D + B_i W , W' = G_i W (reads W) +# +# The inherited invariant restores W to its node-entry value w0 after EVERY +# child (eager). The deferred scheme lets W drift and restores it ONCE at the +# node exit via (G_r ... G_1)^{-1}. Observables are the final D and final W. +# -------------------------------------------------------------------------- +class Batch: + def __init__(self, n, e): + self.n = n + self.e = e + self.Walsh = _walsh_dense(e) + + def run_eager(self, w0, children): + """Restore W to w0 after each child. Returns (D, W, cost).""" + n = self.n + D = [G(0)] * n + W = list(w0) + cost = {"passes": 0, "mults": 0, "adds": 0, "moves": 0, "restoration_passes": 0} + for child in children: + kind = child["kind"] + Bvec = child["B"] + s = child["s"] + Gmat = child["G"] + inverse = child["Ginv"] # restoration operator G_i^{-1} + apply = child["apply_inverse"] # callable(v) -> (vec, cost) + if kind == "reader": + incr = _scalevec(Bvec, W) + else: + incr = _scalevec(Bvec, s) + D = _vecadd(D, incr) + W = mat_vec(Gmat, W) # child dirties the workspace + # eager restoration to w0 (equivalently apply G_i^{-1} to the + # just-dirtied W; both return exactly w0 when the invariant held). + W, rcost = apply(W) + _acc(cost, rcost) + cost["restoration_passes"] += 1 + return D, W, cost + + def run_deferred(self, w0, children, deferred_apply): + """No intermediate restoration; one composed restoration at exit. + + deferred_apply applies (G_r ... G_1)^{-1} to the drifted workspace using + whatever structure the composed operator RETAINS: a diagonal phase, a + permutation, or a dense matrix. This is where the cost result lives.""" + n = self.n + D = [G(0)] * n + W = list(w0) + cost = {"passes": 0, "mults": 0, "adds": 0, "moves": 0, "restoration_passes": 0} + for child in children: + kind = child["kind"] + Bvec = child["B"] + s = child["s"] + Gmat = child["G"] + if kind == "reader": + incr = _scalevec(Bvec, W) + else: + incr = _scalevec(Bvec, s) + D = _vecadd(D, incr) + W = mat_vec(Gmat, W) # no restoration here + # one composed restoration: (G_r ... G_1)^{-1} applied to drifted W + W, rcost = deferred_apply(W) + _acc(cost, rcost) + cost["restoration_passes"] += 1 + return D, W, cost + + +def _vecadd(a, b): + return [x + y for x, y in zip(a, b)] + + +def _scalevec(Bvec, v): + return [b * x for b, x in zip(Bvec, v)] + + +def _acc(total, delta): + for k in ("mults", "adds", "moves", "passes"): + total[k] = total.get(k, 0) + delta.get(k, 0) + + +# -------------------------------------------------------------------------- +# Operator construction helpers returning full child records. +# -------------------------------------------------------------------------- +def make_child(B, s, Gmat, Ginv_mat, apply_inverse, kind, inv_struct): + return { + "B": B, "s": s, "G": Gmat, + "Ginv": Ginv_mat, + "apply_inverse": apply_inverse, + "kind": kind, + "inv_struct": inv_struct, # ("diag",phases)|("perm",perm)|("walsh",e) + "composed_inverse_dense": None, + } + + +def build_phase_children(n, e, a_list): + """Scratch-only children whose restorations are diagonal unit phases.""" + children = [] + for a in a_list: + phases = [gi_pow(a * popcount(x)) for x in range(n)] + inv_phases = [p.conj() for p in phases] # unit phase inverse + Gmat = mat_diag(phases) + Ginv = mat_diag(inv_phases) + B = [G(1) for _ in range(n)] + s = [G(popcount(x) + 1) for x in range(n)] + apply_inv = lambda v, ph=inv_phases: apply_diag(v, ph) + children.append(make_child(B, s, Gmat, Ginv, apply_inv, "scratch", + ("diag", inv_phases))) + return children + + +def build_perm_children(n, e, shifts): + """Scratch-only children whose restorations are permutations (rotations).""" + children = [] + for sh in shifts: + perm = [((x + sh) % n) for x in range(n)] + inv_perm = [((x - sh) % n) for x in range(n)] + Gmat = mat_perm(perm) + Ginv = mat_perm(inv_perm) + B = [G(1) for _ in range(n)] + s = [G(x + 1) for x in range(n)] + apply_inv = lambda v, ip=inv_perm: apply_perm(v, ip) + children.append(make_child(B, s, Gmat, Ginv, apply_inv, "scratch", + ("perm", inv_perm))) + return children + + +def build_hetero_children(n, e): + """Scratch-only children with MIXED restoration families: a diagonal + phase, then a Walsh transform, then a permutation. Their composition is + dense and destroys the cheap structure.""" + phase = [gi_pow(popcount(x)) for x in range(n)] + inv_phase = [p.conj() for p in phase] + c0 = make_child([G(1)] * n, [G(popcount(x) + 1) for x in range(n)], + mat_diag(phase), mat_diag(inv_phase), + (lambda v, ph=inv_phase: apply_diag(v, ph)), "scratch", + ("diag", inv_phase)) + H = _walsh_dense(e) + # H^{-1} = (1/N) H + Hinv = [[c.scale(Fraction(1, n)) for c in row] for row in H] + c1 = make_child([G(1)] * n, [G(x + 1) for x in range(n)], + H, Hinv, + (lambda v: apply_walsh_fast(v)), "scratch", + ("walsh", e)) + sh = 1 + perm = [((x + sh) % n) for x in range(n)] + inv_perm = [((x - sh) % n) for x in range(n)] + c2 = make_child([G(1)] * n, [G(2) for _ in range(n)], + mat_perm(perm), mat_perm(inv_perm), + (lambda v, ip=inv_perm: apply_perm(v, ip)), "scratch", + ("perm", inv_perm)) + return [c0, c1, c2] + + +def build_reader_children(n, e): + """One scratch-only child then one READER child (reads W into D). + + This is a counterexample to *unrestricted* deferral: one reader child CAN + break the rewrite. It is not a proof that read-free is necessary; see + build_reader_cancellation_children for an exact nonzero-reader batch on + which deferral is valid (as in PR1199/PR1203/PR1205).""" + a_list = [1, 1] + children = build_phase_children(n, e, a_list) + children[1]["kind"] = "reader" + return children + + +def build_reader_cancellation_children(n, e): + """Five READER children that each read and negate the workspace. + + Exact nonzero-reader counterexample in the shape of PR1199: reader + coefficients [1,1,1,-1,1], scratch G_i = -I for every child. Read-free + fails outright (every child reads W, four of them after nonidentity drift), + yet the summed defect vanishes and deferral is exact: both schemes add + 3*w0 to the data and restore W, while the restoration bill falls from + five negations to one.""" + coeffs = [G(1), G(1), G(1), G(-1), G(1)] + children = [] + for c in coeffs: + neg = [G(-1) for _ in range(n)] + Gmat = mat_diag(neg) # negation is its own inverse + B = [c for _ in range(n)] + apply_inv = lambda v, ph=neg: apply_diag(v, ph) + children.append(make_child(B, [G(0)] * n, Gmat, Gmat, apply_inv, + "reader", ("diag", neg))) + return children + + +# -------------------------------------------------------------------------- +# Compose the individual structured inverses; return a deferred_apply that uses +# the RETAINED structure, plus a description of what structure survived. +# -------------------------------------------------------------------------- +def _is_diag(M): + n = len(M) + for x in range(n): + for y in range(n): + if x != y and not M[x][y].is_zero(): + return False + return True + + +def _is_perm(M): + n = len(M) + for x in range(n): + row = [y for y in range(n) if not M[x][y].is_zero()] + if len(row) != 1 or M[x][row[0]] != G(1): + return False + cols = set() + for x in range(n): + col = [y for y in range(n) if not M[y][x].is_zero()] + if len(col) != 1: + return False + cols.add(col[0]) + return len(cols) == n + + +def compose_structured(children): + """Return (deferred_apply, description). + + The mathematically exact composed restoration is + (G_r ... G_1)^{-1} = G_1^{-1} ... G_r^{-1}, built as a dense product by + direct_composed_inverse. We then detect whether that exact product RETAINS + cheap structure: + + * diagonal -> a single unit-phase pass (N mults) + * permutation -> a single routing pass (moves, 0 mults) + * otherwise -> dense (N^2 mults) + + The structured form is derived from the exact dense product and then checked + to agree with it on the standard basis, so the cheap application is certified + against the exact operator rather than assumed.""" + n = len(children[0]["B"]) + dense = direct_composed_inverse(children) # exact G_1^{-1}...G_r^{-1} + if _is_diag(dense): + ph = [dense[x][x] for x in range(n)] + # self-check: diagonal application equals dense application + for x in range(n): + basis = [G(1) if y == x else G(0) for y in range(n)] + a, _ = apply_diag(basis, ph) + b = mat_vec(dense, basis) + need(_veceq(a, b), "diag structured != dense") + return (lambda v, p=ph: apply_diag(v, p)), {"form": "diag", "nnz": mat_nnz(dense)} + if _is_perm(dense): + perm = [0] * n + for x in range(n): + for y in range(n): + if not dense[x][y].is_zero(): + perm[x] = y + for x in range(n): + basis = [G(1) if y == x else G(0) for y in range(n)] + a, _ = apply_perm(basis, perm) + b = mat_vec(dense, basis) + need(_veceq(a, b), "perm structured != dense") + return (lambda v, p=perm: apply_perm(v, p)), {"form": "perm", "nnz": mat_nnz(dense)} + return (lambda v, M=dense: apply_dense(M, v)), {"form": "dense", + "nnz": mat_nnz(dense)} + + +def direct_composed_inverse(children): + """Return (G_r ... G_1)^{-1}. + + The workspace drifts as W_r = (G_r ... G_1) w0. Since + (G_r ... G_1)^{-1} = G_1^{-1} G_2^{-1} ... G_r^{-1}, we build the product in + forward child order: acc = G_1^{-1} G_2^{-1} ... G_r^{-1}. + Applying acc to W_r returns w0 exactly.""" + n = len(children[0]["B"]) + inv = mat_identity(n) + for child in children: # forward order + inv = mat_mul(inv, child["Ginv"]) # acc = acc * G_i^{-1} + return inv + + +def summed_defect(children): + """Exact terminal-observation criterion for this note's additive model. + + Under eager restoration every reader reads the node-entry workspace w0. + Under deferral reader i reads the drifted P_{i-1} w0, with + P_{i-1} = G_{i-1} ... G_1 and P_0 = I. The final data therefore differ by + + M w0, M = sum_{reader i} Diag(B_i) (P_{i-1} - I). + + The deferred scheme returns the same observables for every w0 exactly when + M is the zero matrix (the final workspace is restored by the single + composed restoration in both schemes). This is the summed-defect criterion + of PR1199/PR1203/PR1205. Read-free batches make every term vanish + separately and are therefore SUFFICIENT; nonzero-reader batches can cancel + and are not excluded, so read-free is NOT necessary.""" + n = len(children[0]["B"]) + P = mat_identity(n) # P_0 = I (drift before child 1) + M = [[G(0) for _ in range(n)] for _ in range(n)] + for child in children: + if child["kind"] == "reader": + B = child["B"] + for x in range(n): + for y in range(n): + cell = P[x][y] - (G(1) if x == y else G(0)) + M[x][y] = M[x][y] + B[x] * cell + P = mat_mul(child["G"], P) # P_i = G_i P_{i-1} + return M + + +def apply_factorized(v, children): + """Apply the exact composed restoration G_1^{-1} ... G_r^{-1} through its + RETAINED factorization: the cheap structured inverses applied one after + another (G_r^{-1} first, ..., G_1^{-1} last). The cost is the sum of the + factor costs, not N^2: a dense composed product retains its factors, and + density of the matrix is not a statement about application cost.""" + total = {"passes": 0, "mults": 0, "adds": 0, "moves": 0} + out = list(v) + for child in reversed(children): + out, c = child["apply_inverse"](out) + _acc(total, c) + return out, total + + +# -------------------------------------------------------------------------- +# Main verification. +# -------------------------------------------------------------------------- +def verify(): + cert = {"base": BASE, "cases": {}} + n = 8 + e = 3 + batch = Batch(n, e) + w0 = [G(popcount(x) + 1, x % 3) for x in range(n)] + + # ---- Case 1: homogeneous phase restorations, read-free batch. ---- + phase_children = build_phase_children(n, e, [1, 2, 3]) + r = len(phase_children) + comp_inv = direct_composed_inverse(phase_children) + phase_defer, phase_desc = compose_structured(phase_children) + need(phase_desc["form"] == "diag", "phase composition should stay diagonal") + + D_e, W_e, cost_e = batch.run_eager(w0, phase_children) + D_d, W_d, cost_d = batch.run_deferred(w0, phase_children, phase_defer) + need(_veceq(D_e, D_d), "phase: data mismatch under deferral") + need(_veceq(W_d, w0), "phase: workspace not restored by deferral") + need(_veceq(W_e, w0), "phase: workspace not restored eagerly") + need(cost_e["restoration_passes"] == r, "phase: eager restoration count") + need(cost_d["restoration_passes"] == 1, "phase: deferred restoration count") + need(cost_d["mults"] < cost_e["mults"], "phase: deferral should cut mults") + cert["cases"]["phase"] = { + "children": r, + "composed_form": phase_desc["form"], + "eager_restoration_passes": cost_e["restoration_passes"], + "deferred_restoration_passes": cost_d["restoration_passes"], + "eager_mults": cost_e["mults"], + "deferred_mults": cost_d["mults"], + "mult_ratio": str(Fraction(cost_e["mults"], max(cost_d["mults"], 1))), + "observables_equal": True, + } + + # ---- Case 2: homogeneous permutation restorations, read-free batch. ---- + perm_children = build_perm_children(n, e, [1, 2, 4]) + r2 = len(perm_children) + perm_defer, perm_desc = compose_structured(perm_children) + need(perm_desc["form"] == "perm", "perm composition should stay a permutation") + D_e2, W_e2, cost_e2 = batch.run_eager(w0, perm_children) + D_d2, W_d2, cost_d2 = batch.run_deferred(w0, perm_children, perm_defer) + need(_veceq(D_e2, D_d2), "perm: data mismatch under deferral") + need(_veceq(W_d2, w0), "perm: workspace not restored by deferral") + need(cost_e2["restoration_passes"] == r2, "perm: eager restoration count") + need(cost_d2["restoration_passes"] == 1, "perm: deferred restoration count") + need(cost_d2["mults"] <= cost_e2["mults"], "perm: deferral should not raise mults") + cert["cases"]["perm"] = { + "children": r2, + "composed_form": perm_desc["form"], + "eager_restoration_passes": cost_e2["restoration_passes"], + "deferred_restoration_passes": cost_d2["restoration_passes"], + "eager_moves": cost_e2.get("moves", 0), + "deferred_moves": cost_d2.get("moves", 0), + "observables_equal": True, + } + + # ---- Case 3 (correctness): one reader child CAN break deferral. ---- + # This is a counterexample to unrestricted deferral, hence a proof that + # read-free is SUFFICIENT. It is not evidence that read-free is necessary: + # Case 5 gives an exact nonzero-reader batch on which deferral is valid + # (the counterexamples of PR1199/PR1203/PR1205). + reader_children = build_reader_children(n, e) + reader_defer, _ = compose_structured(reader_children) + D_e3, W_e3, _ = batch.run_eager(w0, reader_children) + D_d3, W_d3, _ = batch.run_deferred(w0, reader_children, reader_defer) + need(_veceq(W_d3, w0), "reader: final workspace should still be restored") + need(not _veceq(D_e3, D_d3), "reader: this example should CHANGE the data output") + diff = _vecsub(D_e3, D_d3) + need(any(not c.is_zero() for c in diff), "reader: expected nonzero discrepancy") + M3 = summed_defect(reader_children) + need(mat_nnz(M3) > 0, "reader: summed defect should be nonzero in this example") + cert["cases"]["reader_negative"] = { + "observables_equal": False, + "discrepancy_nonzero": True, + "summed_defect_nonzero": True, + "discrepancy": [c.key() for c in diff], + } + + # ---- Case 5 (correctness): nonzero readers that cancel exactly. ---- + # PR1199's counterexample shape: five reader children, each reading and + # negating the workspace, coefficients [1,1,1,-1,1]. Read-free fails + # outright, yet the summed defect is exactly the zero matrix and deferral + # is valid: both schemes add 3*w0 to the data and restore W. The + # restoration bill falls from five negations to one. This falsifies the + # "read-free is necessary" direction of the note's original iff. + cancel_children = build_reader_cancellation_children(n, e) + cancel_defer, cancel_desc = compose_structured(cancel_children) + Mc = summed_defect(cancel_children) + need(mat_nnz(Mc) == 0, "cancellation: summed defect should vanish exactly") + D_e5, W_e5, cost_e5 = batch.run_eager(w0, cancel_children) + D_d5, W_d5, cost_d5 = batch.run_deferred(w0, cancel_children, cancel_defer) + need(_veceq(D_e5, D_d5), "cancellation: data mismatch under deferral") + need(_veceq(W_d5, w0), "cancellation: workspace not restored by deferral") + need(cost_e5["restoration_passes"] == 5, "cancellation: eager restoration count") + need(cost_d5["restoration_passes"] == 1, "cancellation: deferred restoration count") + cert["cases"]["reader_cancellation"] = { + "children": 5, + "reader_coefficients": ["1", "1", "1", "-1", "1"], + "readers_nonzero": True, + "summed_defect_zero": True, + "observables_equal": True, + "eager_restoration_passes": cost_e5["restoration_passes"], + "deferred_restoration_passes": cost_d5["restoration_passes"], + } + + # ---- Case 4 (cost): heterogeneous composition is dense, and density of + # the composed matrix is NOT an application-cost statement. ---- + # The composed inverse of a phase/Walsh/permutation mix is dense (all N^2 + # entries nonzero). Applying that dense product DIRECTLY costs N^2 = 64 + # multiplications against 16 for the three structured eager restorations, + # so direct dense deferral loses 64 vs 16 at N = 8. But the composed + # operator retains its factorization into the three cheap structured + # inverses; applied sequentially it costs exactly the eager sum (16) and + # matches the dense product on every basis column. Deferral therefore + # costs more only when no cheap factorization is retained and the dense + # product must be applied directly. + hetero = build_hetero_children(n, e) + comp_inv4 = direct_composed_inverse(hetero) + hetero_defer, hetero_desc = compose_structured(hetero) + need(hetero_desc["form"] == "dense", + "hetero: composed inverse should be dense (structure destroyed)") + # eager restoration cost = sum of structured inverse applications + eager_struct_cost = {"mults": 0, "adds": 0, "moves": 0, "passes": 0} + for c in hetero: + _, rc = c["apply_inverse"](list(w0)) + _acc(eager_struct_cost, rc) + # deferred restoration cost, DIRECT dense application of the composed product + _, dcost = hetero_defer(list(w0)) + # deferred restoration cost, RETAINED factorization: sequential application + # of G_3^{-1}, G_2^{-1}, G_1^{-1}, self-checked against the dense product + # on the standard basis before its cost is trusted. + fac_w, fac_cost = apply_factorized(w0, hetero) + need(_veceq(fac_w, mat_vec(comp_inv4, w0)), + "hetero: factorized application != dense product on w0") + for x in range(n): + basis = [G(1) if y == x else G(0) for y in range(n)] + a, _ = apply_factorized(basis, hetero) + b = mat_vec(comp_inv4, basis) + need(_veceq(a, b), "hetero: factorized application != dense product on basis") + need(fac_cost["mults"] == eager_struct_cost["mults"], + "hetero: retained factorization should cost exactly the eager sum") + need(dcost["mults"] > fac_cost["mults"], + "hetero: direct dense application should exceed factorized application") + nnz = mat_nnz(comp_inv4) + is_dense = nnz == n * n + D_e4, W_e4, cost_e4 = batch.run_eager(w0, hetero) + D_d4, W_d4, cost_d4 = batch.run_deferred(w0, hetero, hetero_defer) + need(_veceq(D_e4, D_d4), "hetero: data mismatch under deferral") + need(_veceq(W_d4, w0), "hetero: workspace not restored by deferral") + need(is_dense, "hetero: composed inverse should be dense") + need(dcost["mults"] >= eager_struct_cost["mults"], + "hetero: direct dense application eliminates no multiplications") + cert["cases"]["hetero_negative"] = { + "children": len(hetero), + "composed_form": hetero_desc["form"], + "composed_inverse_nnz": nnz, + "composed_inverse_dense": is_dense, + "eager_structured_mults": eager_struct_cost["mults"], + "deferred_dense_mults": dcost["mults"], + "deferred_factorized_mults": fac_cost["mults"], + "deferred_factorized_passes": fac_cost["passes"], + "factorized_matches_dense": True, + "observables_equal": True, + "mult_elimination": False, + } + + cert["dimension_N"] = n + cert["e"] = e + cert["summary"] = ( + "phase=PASS perm=PASS hetero_dense=CONFIRMED " + "reader_diverges=CONFIRMED reader_cancels=CONFIRMED " + "factorized_matches_dense=CONFIRMED" + ) + return cert + + +def _veceq(a, b): + return len(a) == len(b) and all(x == y for x, y in zip(a, b)) + + +def _vecsub(a, b): + return [x - y for x, y in zip(a, b)] + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--write", type=Path) + ap.add_argument("--json", action="store_true") + args = ap.parse_args() + + cert = verify() + phase = cert["cases"]["phase"] + perm = cert["cases"]["perm"] + reader = cert["cases"]["reader_negative"] + cancel = cert["cases"]["reader_cancellation"] + hetero = cert["cases"]["hetero_negative"] + + line = ( + "PASS_RESTORATION_COALESCING " + f"phase={phase['eager_restoration_passes']}->{phase['deferred_restoration_passes']}" + f"(x{phase['mult_ratio']}) " + f"perm={perm['eager_restoration_passes']}->{perm['deferred_restoration_passes']} " + f"hetero_dense={hetero['composed_inverse_dense']} " + f"reader_diverges={reader['observables_equal'] == False} " + f"reader_cancels_5to1=" + f"{cancel['observables_equal'] and cancel['deferred_restoration_passes'] == 1} " + f"hetero_mults=eager{hetero['eager_structured_mults']}" + f"|factorized{hetero['deferred_factorized_mults']}" + f"|dense{hetero['deferred_dense_mults']}" + ) + committed = ROOT / "CERTIFICATE.json" + if args.write is None and committed.exists(): + recorded = json.loads(committed.read_text()) + if json.dumps(recorded, sort_keys=True) != json.dumps(cert, sort_keys=True): + raise ValueError("recomputed certificate differs from committed CERTIFICATE.json") + print(line) + if args.json: + print(json.dumps(cert, indent=2, sort_keys=True)) + if args.write: + args.write.write_text(json.dumps(cert, indent=2, sort_keys=True)) + print(f"WROTE {args.write}") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())