From dab4b565c4232fcd86a3ef12ef53db18b55a72c8 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Sun, 18 Oct 2026 23:55:11 +0530 Subject: [PATCH 1/9] Review P104 fixed-cover support cut (#3259): valid but not sharp Independent hypothesis-by-hypothesis review of PR3259's path-embedding argument (valid as a necessary support test under its contract), of PR3252's memory-relaxation proof (valid), and of what PR3427 consumes (its own one-helper lemma and PR3252 operations; justified). The one-recombined-helper criterion (stated in PR3427, re-proved here for every dimension case) is exact for untimed support. Under it, 2,682 of the 4,992 required entries of C = I - G/2 are unsupported, not only C[71,102]. Consequence under PR3427's contract: rank(U - I) >= 17 (19x18 unsupported rectangle, rank 17; 17x17 minor det(8C) = 2^43). Stdlib verifier: PR3259 layered control reproduced (missing (71,102), cones 1,725/37); sharp criterion by two loop orders; PR3427 four-column masks reproduced; three single-relaxation support rows (unpriced); 4,500-program exact-coefficient oracle over F_2^3/F_2^4 with five contract-violation controls; mutation tests. Audit only: no construction, kappa or frontier change. Co-Authored-By: Claude Opus 5.5 --- .../PROOF-REVIEW.md | 269 ++++++ .../p104-fixed-cover-cut-review/README.md | 180 ++++ .../p104-fixed-cover-cut-review/SOURCES.json | 36 + .../p104-fixed-cover-cut-review/TASK.json | 100 +++ .../p104-fixed-cover-cut-review/VERIFY.json | 37 + .../test_verify.py | 64 ++ .../p104-fixed-cover-cut-review/verify.py | 840 ++++++++++++++++++ 7 files changed, 1526 insertions(+) create mode 100644 research/p104-fixed-cover-cut-review/PROOF-REVIEW.md create mode 100644 research/p104-fixed-cover-cut-review/README.md create mode 100644 research/p104-fixed-cover-cut-review/SOURCES.json create mode 100644 research/p104-fixed-cover-cut-review/TASK.json create mode 100644 research/p104-fixed-cover-cut-review/VERIFY.json create mode 100644 research/p104-fixed-cover-cut-review/test_verify.py create mode 100644 research/p104-fixed-cover-cut-review/verify.py diff --git a/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md b/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md new file mode 100644 index 0000000000..16af367f81 --- /dev/null +++ b/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md @@ -0,0 +1,269 @@ +# Review of the PR3259 path-embedding argument (with PR3252 and PR3427) + +Objects, at their exact heads: + +- PR3259 (Nick Petalas, `b572b0c25569898579041200e95731c5a43c9189`), + `research/p104-pooled-cut-independent/README.md`, sections "Contract and + conclusion" and "Why one contact per dimension is a necessary relaxation" + (README lines 17-100). +- PR3252 (petalas, `4784b71d2e0833537c9ae1e8be05ad2a6b334d92`), + `research/p104-memory-relaxation-soundness/PROOF.md`. +- PR3427 (jmbarrancoml, `344774ba08a73fc3a85fdcb93fb319927bde3ea2`), + `research/p104-source-preconditioning/PROOF.md`, "Pooled path-compression + lemma". Only what it consumes is reviewed. + +This is an audit, not a construction. It changes no κ and no frontier, and it +proves no P104 impossibility outside the stated contract. + +## Verdict + +1. **PR3259's argument is valid as a necessary support test under its stated + contract.** Each step below is valid as written. Two steps need a sentence + that is implicit in the contract, recorded as clarifications rather than + repairs. Under that contract, `C[71,102] = -1/2` cannot be delivered. +2. **The test is sound but far from sharp.** It discards one fact that every + legal dependency path has: its frames are nested across dimensions. + Reinstating that fact gives a valid criterion with **one recombined helper + per path**. That lemma is stated in PR3427 and is re-proved below with every + dimension case. Under it, **2,682 of the 4,992 required entries are + unsupported**, with at least one in every row and every column. PR3259's + relaxation grants 10,815 source/target pairs, against 2,310 for the sharp + criterion. "Exactly one missing coefficient" describes PR3259's test, not the + contract. +3. Consequently the fixed-cover contract is closed by a much larger obstruction + than one coefficient. A contract change that only reopens `C[71,102]` does + not complete the correction. Examples are PR3427's rank-one source shear, a + moved helper, or one extra dependency. +4. **PR3427 consumes its own one-helper lemma and PR3252's full-memory + operations, not PR3259's layered recurrence.** The lemma is valid. Its + published four-column support masks are reproduced exactly by code written + for this review. Its rank theorem stands as stated. Applied to all 104 + columns, the same argument gives **`rank(U-I) >= 17`** (section below). +5. **PR3252's theorem is valid** for its stated recurrence and contract. + +## Contract, as used + +PR3259 states the contract in prose. It is numbered here so that each step can +cite it: + +- **K1 fixed cover.** Every added helper has one full flag through + `0 < L[a//2] < A[a] < F3 < ... < F6 < B[b] < H[b//2] < FULL` for a compatible + pair, `A[a] <= B[b]`. Skipped dimensions are granted, but the flag still + passes through `L, A, B, H`. +- **K2 monotone.** A helper never descends or changes frame at a fixed + dimension. It is never reloaded or reused with another flag. +- **K3 equal frames.** A scalar operation transfers dependence only between + registers whose current frames are equal. A transport is register-local. +- **K4 immutable X.** Sources are never written. They are read only at their + frozen channel frame path. +- **K5 unread Y.** Targets are never read. They receive additive increments + only. +- **K6 no other source-dependent state.** The correction neither reads nor + writes original channel helpers (G, D, Q, C) or other correlated storage. + The channel contributes its unchanged `G/2`. +- **K7 independent dirt.** Helper initial values carry no X dependence. + +The original channel word satisfies K4 and K5: X is never written and Y is +never read. The verifier checks this from the 4,058 events (`channel_roles`). +K6 is a premise about the correction, not about the channel. + +## Step-by-step review of PR3259 (checklist a-h) + +| # | Step in PR3259 | Uses | Verdict | +|---|---|---|---| +| a | Skipped dimensions are granted; frames at dims 1, 2, 7, 8 are the singletons `L, A, B, H`; dims 3-6 are any d-flat in `[A,B]`. | K1 | Valid. The intervals are exactly the members a K1 flag can take. Nesting between layers is dropped, which only enlarges the test. Forcing every helper through a fixed `L[a//2]` and `A[a]` is a premise, not a consequence. Row R2 shows it is load-bearing. | +| b | "Within one dimension, a monotone helper has one fixed actual frame." | K1, K2 | Valid. Clarification: this needs K2's "never reloaded or reused". A helper that is cleared and restarted with a new flag is a second helper. If it has a pool type, the pool still covers it. | +| c | Sources read at every frame of their frozen path; targets receive at every frame of theirs; direct X-to-Y contacts granted. | K4, K5 | Valid. X is never an intermediate node because nothing writes it. Y is never intermediate because nothing reads it. Untimed reads and writes are a superset of legal ones. | +| d | Original channel helpers excluded. | K6 | Valid as a premise. Row R3 shows it is load-bearing: reading channel helper state reopens every entry. | +| e | Dirt has no source coefficient; cancellation cannot create one. | K7, linearity | Valid. A coefficient of `X_s` in `Y_t` is a sum over dependency paths of products of operation scalars. With no path it is zero. Restoration operations are linear operations and are included. | +| f | Same-dimension runs share one frame, so first and last helpers are adjacent and one step suffices. | K2, K3 | Valid, including a read or write in mid-run (the path starts or ends there) and runs that revisit a helper. Only the endpoints' common frame is used. Equal-frame groups in an actual program are cliques. | +| g | Read-first seeding; accumulation after the edge; dims 0 and 9 excluded; early writes. | K4, K5 | Valid. Seeding the layer's reads before the single step covers a read followed by relays at that dimension. Accumulating after the step covers relays followed by a write. X frames have dimension at least 1 and Y frames at most 8, so dims 0 and 9 cannot join a read to a write. The recurrence accumulates at every layer, so Y71's dimension-5 writes are checked. | +| h | Pooling: "every matching embeds by its selected edges". | K1 | Valid, and slightly stronger than stated. Any multiset of helpers with pool types embeds: helpers of one type merge into one virtual helper, whose state is a union. | + +Stop-rule outcome: no step fails. The control engine reproduces every PR3259 +number: missing set `{(71,102)}`, forward counts +`16,25,52,365,1725,2283,2285,2297`, a 37-edge backward cone and disjointness. +It uses literal d-flat hosting with reduced-echelon keys and shares no code with +PR3259. + +## The sharper valid criterion: one recombined helper per path + +**Lemma.** Assume K1-K7 and suppose a program gives `Y_t`'s increment a nonzero +coefficient on `X_s`. Then either `X_s` and `Y_t` share a path frame, or there +are frames `V` on `X_s`'s path and `W` on `Y_t`'s path, and a compatible pair +`(a,b)`, such that + +``` +V < W, +V lies in (a,b)'s interval at dim V, and W in its interval at dim W. +``` + +Here `V < W` means V is strictly contained in W. The interval at dimension d is +`L[a//2]`, `A[a]`, `[A[a],B[b]]`, `B[b]` or `H[b//2]` for d = 1, 2, 3-6, 7 or 8. + +*Proof.* Take a dependency path. Its first node is a read of `X_s` at frame V +and its last a write into `Y_t` at frame W. By K4 and K5 every intermediate node +is a helper. By K6 none is a channel register. By K3 scalar steps keep the frame +and transports enlarge it. So the frames along the path form a chain, and +`V <= W`. If `V = W` the pair shares a frame. Otherwise `1 <= dim V < dim W <= 8`. + +*Choice of departure a.* + +- If `dim V >= 2`, let a be the departure of the reading helper. Its flag + passes `A[a]` at dimension 2 and V at `dim V`, so `A[a] <= V`. +- If `dim V = 1`, the run at dimension 1 shares frame V (step f). Let h' be the + helper that carries the path out of dimension 1, and a its departure. Its + dimension-1 frame is V, so `L[a//2] = V`. Its flag gives `A[a] <=` its next + frame on the path, which is `<= W`. + +*Choice of arrival b.* + +- If `dim W <= 7`, let b be the arrival of the writing helper. Then + `W <= B[b]`. +- If `dim W = 8`, let h'' be the helper that carries the path into dimension 8, + and b its arrival. Then `H[b//2] = W`, and its frame before the ascent lies + in `B[b]`. That frame also contains every earlier path frame, including + `A[a]`. If h' = h'', then `A[a] <= B[b]` holds because both lie on one flag. + +In every case `A[a] <= B[b]`, so `(a,b)` is in the pool. The spaces +`L[a//2] < A[a]`, V, W and `B[b] < H[b//2]` form a nested partial flag: + +- for `dim V = 1`, `V = L[a//2]`; +- for `dim V = 2`, `V = A[a]`; +- for `dim W = 7`, `W = B[b]`; +- for `dim W = 8`, `W = H[b//2]`. + +That partial flag extends to a full flag. One helper of type `(a,b)` therefore +admits both V and W. ∎ + +*Converse (untimed).* If the condition holds, one helper of type `(a,b)` with +that full flag reads `X_s` at V and writes `Y_t` at W. With chronology relaxed, +the criterion is therefore exact. No sound untimed support test under K1-K7 can +exclude more pairs. Timed tests can. + +*Where PR3259 loses precision.* At layer d PR3259 lets helper w relay through +any d-flat that w shares with a neighbour. It does not require that flat to +contain the frame through which the signal reached w. The lemma keeps that +containment. + +*Why K4/K5 matter for the lemma, not only for PR3259.* The choice of a and b +uses a helper at the dimension-1 exit and the dimension-8 entry. If Y may relay, +a path can leave dimension 1 inside a target that the channel transports +upward. No helper then carries the source line. The verifier's F_2^3 program +(`y_relay_counterexample`) does this with four scalar operations. It +delivers a nonzero coefficient outside both PR3259's test and the sharp test. + +## Finite consequences at P104 (verifier) + +| Quantity | PR3259 layered test | Sharp one-helper criterion | +|---|---:|---:| +| Supported source/target pairs | 10,815 | 2,310 | +| Required entries unsupported | 1 (`(71,102)`) | 2,682 (every row and column) | +| Values of unsupported entries | `-1/2` | 1,801 at `-1/2`, 881 at `+1/2` | + +The sharp criterion is computed in two ways: + +- reduced-echelon keys with helper-type masks; +- point-set bitmaps looped by helper type. + +The two agree. For sources 0-3 the per-source target masks equal PR3427's +published masks exactly. Those masks come from PR3427's direct criterion and +from PR3252's full-memory operations. + +## PR3252 PROOF.md (shorter review) + +The theorem makes two changes to PR3182's recurrence: it deletes the output +`break` and it adds direct contacts. Its full and one-step memory modes are then +necessary tests under PR3252's contract, items 1-5. That contract is +PR3259's K1-K7 written with per-helper bounds `L(h,d) <= F(h,d) <= U(h,d)`. + +- *Run compression.* Valid; same argument as step f. +- *Relay of old state only.* Valid. A fresh read followed by a relay at the + same dimension ends at a receiver with the read frame. Complete untimed + snapshots grant that receiver its own read, and PR3252 says so explicitly. + The argument fails for an incomplete read set, as PR3252 also states. +- *Witness induction.* Valid. The relay guard `S + L(h,d) + L(w,d) <= U(h,d) ∩ + U(w,d)` with the dimension bounds holds whenever the actual common frame + contains S. Carries keep `S <= F`. +- *Pruning.* Valid, because the guards are monotone under shrinking a memory. + +The full-memory mode keeps a lower bound on the frame the signal used. Like any +sound untimed test under this contract, it cannot be stricter than the sharp +criterion, which is exact. On PR3427's four columns it equals the sharp +criterion. This review does not compare the two on the other columns. The +one-step mode forgets that bound and is weaker. PR3252's finite checks use fixed matchings and F_2^3 +interval fixtures. The proof is universal over its contract, and no gap was +found. + +## What PR3427 consumes + +- Its rank theorem rests on its own "pooled path-compression lemma", which is + the lemma above. It also uses a finite four-column certificate computed two + ways: the direct criterion and PR3252's unchanged full-memory operations on + a 2,309-helper model. +- It cites PR3259 for the 2,309-pair pool and as the motivation for the + one-shear candidate at `(71,102)`. It does not need PR3259's recurrence to be + correct or sharp. +- The consumption is justified. The lemma is valid, and the four-column masks + are reproduced exactly by an engine that shares no code with PR3427. + +## Consequence for PR3427: rank(U-I) >= 17 + +PR3427's contract adds an invertible scalar source preconditioner U to K1-K7. +The prepared sources `X' = UX` stay in the original frames, so the support +criterion is unchanged. The correction must deliver `D = U^-1 - M` with +`M = G/2`, and D vanishes on every unsupported pair. Write `V = U^-1`. On an +unsupported pair, `(V - I)[t,s] = M[t,s] - [t = s] = -C[t,s]`. + +Every diagonal pair is unsupported, and its entry is consistent because +`C[t,t] = 0`. Hence for any rectangle `R x S` of unsupported pairs, overlap +allowed, + +``` +rank(U - I) = rank(V - I) >= rank C[R,S], +``` + +using `V - I = -V(U - I)` for the equality. + +A deterministic greedy finds a rectangle: for each seed column, add the +column that most increases `min(|R|,|S|)`, with ties to the smallest index. +It finds a 19-by-18 rectangle of unsupported pairs with +`rank C[R,S] = 17`. Exact `Fraction` elimination gives the rank. A 17-by-17 +minor has integer `det(8C) = 2^43`, by Bareiss elimination, so +`det C = 2^-8`. + +Thus `rank(U-I) >= 17` under PR3427's contract, against its published 4. +This prices no joint preparation. The greedy is not optimal, and a min-rank +completion may force more. + +## Load-bearing hypotheses (support level, sharp criterion) + +The rows are support-level necessary-test relaxations. They are unpriced and +give no coefficient, dirty restoration or chronology. Each row relaxes one item. + +| Relaxed item | Reaches `(71,102)` | Sharp-missing entries reopened | Minimal witness (operations counted, unpriced) | +|---|---|---:|---| +| none (sharp baseline) | no | 0 of 2,682 | - | +| PR3259's dropped cross-layer nesting (a proof relaxation, not a contract change) | no | 2,681 | layered test | +| K5, correction-only Y relay (R1) | no | 0 | none at P104; F_2^3 escape uses 4 scalar operations | +| K5 with the channel's own Y content readable, including target feedback (R1c) | yes | 2,682 | feedback on `Y71`: read it at its dimension-5 snapshot, after the channel has deposited its X102 term, and add a multiple back (1 read and 1 write, or 1 self-add) | +| K1, free nested flags: helpers not forced through `L/A/B/H` (R2) | yes | 2,682 | one helper, flag through `L_102 <= H_71`; 1 read, >= 1 transport, 1 write | +| K6, reads of old channel-helper state (R3) | yes | 2,682 | one equal-frame add from `D11` into `Y71` at their shared dimension-5 frame | + +R1c and R3 use structural, no-cancellation dependence of the channel registers. +Their witnesses are therefore support paths only. Both reopen every entry for +the same reason: the channel already delivers the support of `G/2`, which +contains every off-diagonal required entry. Any access to the channel's +source-dependent state exposes that support. The access can come through its +helpers or by reading a target after the channel has written it. Scaling +that state is not a correction; its coefficients, dirt and cost are unknown. +Known rows are cited, not recomputed: + +- PR3013: component/containment pooling reaches all 4,992 entries. +- PR3427: a one-H2 source shear removes the `(71,102)` requirement, but + `D[3,2]` stays unsupported. A source preconditioner needs `rank(U-I) >= 4`. + +Reading: the obstruction rests on the fixed cover (K1) and on the exclusion of +the channel's source-dependent state (K6, including its exposure through Y). +Unread-Y matters in this instance only through that exposure. At P104, +correction-only Y relay reopens nothing. diff --git a/research/p104-fixed-cover-cut-review/README.md b/research/p104-fixed-cover-cut-review/README.md new file mode 100644 index 0000000000..12b30da3b0 --- /dev/null +++ b/research/p104-fixed-cover-cut-review/README.md @@ -0,0 +1,180 @@ +# P104 fixed-cover support cut: hypothesis review and a sharper criterion + +**Statement.** PR3259's path-embedding argument is a **valid** necessary support +test under its stated fixed-cover contract. That contract is closed, by a much +larger obstruction than one coefficient. The test discards one fact true of every +legal dependency path: its frames are nested across dimensions. Keeping that +fact gives a valid criterion, **one recombined helper per path**. This lemma is +stated in PR3427 and re-proved here in every dimension case. It is exact for +untimed support. Under it, **2,682 of the 4,992 required entries of +`C = I - G/2` are unsupported**, with at least one in every row and every +column. PR3259's single missing entry, `C[71,102] = -1/2`, is a property of its +looser relaxation. + +PR3427 states the lemma, but it has not been evaluated beyond PR3427's four +source columns. Applied to all 104 columns, it raises PR3427's source-preconditioner bound +from `rank(U-I) >= 4` to **`rank(U-I) >= 17`**, under PR3427's own contract. + +This is an audit: a scoped proof review, a finite certificate and small-domain +controls. It constructs nothing and is not a complete multiplication theorem. +It proves no P104 impossibility outside the stated contract, and κ and the +selected frontier are unchanged. + +## Results + +| Item | Result | +|---|---| +| PR3259 embedding argument, checklist a-h | Valid. Two implicit sentences are recorded as clarifications. See [PROOF-REVIEW.md](PROOF-REVIEW.md). | +| PR3252 PROOF.md (memory relaxation) | Valid for its recurrence and contract. | +| What PR3427 consumes | Its own one-helper lemma and PR3252's full-memory operations, not PR3259's recurrence. Both are justified. | +| Control: PR3259 layered test, rebuilt | Missing set `{(71,102)}`. Forward counts `16,25,52,365,1725,2283,2285,2297`. Backward cone 37, disjoint. | +| Sharp criterion (two loop orders) | 2,682 required entries unsupported: 1,801 at `-1/2` and 881 at `+1/2`. 2,310 supported pairs, against 10,815 for PR3259's test. | +| Cross-check with PR3427 | The four published per-source masks (sources 0-3) are reproduced exactly. | +| Consequence for PR3427 | A 19-by-18 rectangle of unsupported pairs has `rank C[R,S] = 17`, giving `rank(U-I) >= 17`. A 17-by-17 minor has `det(8C) = 2^43`. | +| Oracle, coefficient level | 4,500 seeded legal programs over `F_2^3` and `F_2^4`, with exact `Fraction` coefficients. 269 nonzero helper-path coefficients, 107 of them for pairs with no common snapshot. None lies outside the sharp test. | + +### Which hypotheses carry the obstruction + +Each row relaxes one hypothesis and is checked at support level with the sharp +criterion. The rows are unpriced and give no coefficient, chronology or dirty +restoration. + +| Relaxed hypothesis | Reaches `(71,102)` | Reopens, of 2,682 | +|---|---|---:| +| Cross-layer nesting, as PR3259's proof relaxation drops it | no | 2,681 | +| Unread Y, correction-only relay (R1) | no | 0 | +| Unread Y, with the channel's own Y content readable (R1c) | yes, by feedback on Y71 at dimension 5 | 2,682 | +| Fixed cover: helpers not forced through `L/A/B/H` (R2) | yes, one helper through `L_102 <= H_71` | 2,682 | +| No reads of old channel-helper state (R3) | yes, one equal-frame add from `D11` at dimension 5 | 2,682 | + +Among the rows computed here, two hypotheses each reopen every entry. One is +the fixed cover. The other excludes the channel's source-dependent state, +whether held in its helpers or exposed by reading targets after the channel +has written them. That state already carries +the support of `G/2`, which contains every off-diagonal requirement. At P104, +correction-only Y relay reopens nothing, although an `F_2^3` program shows it +can matter in principle. Frame descent and cross-frame mixing also break the +argument; the small-domain negative controls show this. They are not priced or +counted at P104 here. Cited, not recomputed: + +- PR3013: component/containment pooling reaches all 4,992 entries. +- PR3427: a one-H2 source shear removes only the `(71,102)` requirement. + +## Reproduce + +From the repository root, with the standard library (about 20 s): + +```sh +python3 -I -O -Werror -B research/p104-fixed-cover-cut-review/verify.py +python3 -I -O -Werror -B research/p104-fixed-cover-cut-review/test_verify.py +``` + +The verifier prints one JSON receipt. Its last line is + +``` +PASS_P104_FIXED_COVER_CUT_REVIEW layered_missing=1 sharp_missing=2682 of 4992 pr3427_masks=4 rank_U_minus_I>=17 rows=4 oracle_programs=4500 no_kappa +``` + +The registered replay is +`python3.12 -B scripts/research_package.py --package research/p104-fixed-cover-cut-review`. +Every check raises `SystemExit("FAIL: ...")`, so checks stay active under `-O`. + +**Negative controls that must fail:** + +- `test_verify.py` rejects a tampered input hash. +- It rejects an unsound "shared snapshot only" test inside the oracle. +- It rejects a wrong rectangle. +- It shows that dropping nesting changes PR3427's masks. +- Inside `verify.py`, five contract violations must each produce a coefficient + outside both tests. They are Y read (a fixed four-operation `F_2^3` program), + frame descent, cross-frame mixing, an off-cover flag and correlated old + state. + +## Method and independence + +The code shares nothing with PR3182, PR3252, PR3259 or PR3427. Frames are +canonical reduced-echelon keys over `F_2^9`. E8 ports are enumerated +independently and sorted. + +- The layered control hosts every d-flat of each interval literally, then + takes one read-first step per layer. +- The sharp criterion is computed twice. One method uses echelon keys with + helper-type masks. The other uses point-set bitmaps, looped per helper type. +- The rank bound uses a deterministic greedy over 104 seed columns. Each + step adds the column that most increases `min(|R|,|S|)`, ties to the + smallest index. Exact `Fraction` elimination gives the rank, and an + independent integer Bareiss determinant confirms it. The greedy is not + optimal, so 17 is a lower bound. +- Oracle programs choose uniformly among the operations legal at each moment. + Direct X-to-Y adds are omitted so that every coefficient travels through + helpers. Seed `20261018`, 120 operations per program, 3,000 programs over + `F_2^3` and 1,500 over `F_2^4`. This is a bounded randomized family, not an + exhaustive enumeration. +- Before this review, the original channel word was checked for its roles: + X is never written and Y is never read, so K4 and K5 hold for the channel. + +## Scope, inherited assumptions and open obligations + +Inherited: + +- PR2981's covers and the native channel frame paths, through their pinned + JSON inputs; +- the ordered E8 ports, with the fixture's 16 removed roots; +- the contract K1-K7 in [PROOF-REVIEW.md](PROOF-REVIEW.md). + +The rows and rank bound apply only under those contracts. R1c and R3 use +structural, no-cancellation dependence of the channel registers. + +Open and not addressed here: + +- chronology and acquisition order; +- coefficient delivery and dirty restoration; +- native lowering, precision and physical hosting; +- consumer cost and supplier admission; +- every changed-cover construction; +- a timed refinement of the sharp criterion. + +No independent human or formal-kernel review has been done. The selected +cold replay is unchanged and was not rerun. + +## Open next questions + +1. *Is 17 the true rank bound?* A min-rank completion of `-C` on all 8,506 + unsupported pairs may force a rank well above 17. A larger rank would + further constrain any joint native source preparation under PR3427's + contract. A first step is an exact lower bound by larger or overlapping + rectangles, or by a min-rank argument. It needs no new matching search. +2. *Can a changed cover reopen all 2,682 entries cheaply?* Relaxing the fixed + cover (R2) reopens every entry at support level. The open question is the + smallest set of off-cover helper flags that covers all 2,682 pairs, with + its full bill. Coefficients, dirt and every cost remain unknown. +3. *Is there a non-trivial use of channel state?* R1c and R3 reopen everything + only because the channel already carries `G/2`. One would need a + coefficient-level construction that reads channel state and restores it, + with an explicit list of the changed channel obligations. + +## Predecessors and credit + +- Nick Petalas (GitHub petalas): + - PR2981 `3d24b92d8ba057b57cb2d480170ec407520e6882` (covers and flags); + - PR3252 `4784b71d2e0833537c9ae1e8be05ad2a6b334d92` (memory soundness); + - PR3259 `b572b0c25569898579041200e95731c5a43c9189` (pooled cut and + embedding argument); + - PR3013 (component pooling). +- dcharb78: PR3182 `ad848966cd62e13de5ad8d4b5169c221d74d2fcd` (the cut and its + 1,725/37 cones). +- commdata2338: PR3214 `faa6323371db1c5fbb43ab04c6e00715d2328bc6` (output + repair). +- jmbarrancoml: PR3427 `344774ba08a73fc3a85fdcb93fb319927bde3ea2` (the + one-helper lemma and the rank-four theorem extended here). +- Wentao Li for the chronology audit, which is not redone here. +- The native/compiler lineage credited in the pinned inputs: Rohan Arun/1972, + Chafik Boukhalfa/1991, Adam Gall/1940, Josie Elliston/1071 and + Ali Romman/1125. + +Base: canonical main `20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority +revision 6. [SOURCES.json](SOURCES.json) pins the three live inputs by Git blob +and SHA256. + +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from +Claude (Anthropic, Claude Opus 5.5). Apache-2.0. diff --git a/research/p104-fixed-cover-cut-review/SOURCES.json b/research/p104-fixed-cover-cut-review/SOURCES.json new file mode 100644 index 0000000000..e1bf46363e --- /dev/null +++ b/research/p104-fixed-cover-cut-review/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/p104-joint-unit-flags/CERTIFICATE.json", + "usage": "input", + "git_blob": "0fa7d2d40566e92f3ea1539723abf438ba65adb8", + "sha256": "a98126428a8da6eae91c50afcc42e014a284c82b554ef77e5b3a34fc6d228128" + }, + { + "path": "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "usage": "input", + "git_blob": "86beaf424e9f0f800ae3a62797d94ec9386b7706", + "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e" + }, + { + "path": "research/p104-native-channel/inputs/P104-FIXTURE.json", + "usage": "input", + "git_blob": "2e16f99b295bb386fd13bd8fbd57b42ef54143a9", + "sha256": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4" + } + ] +} diff --git a/research/p104-fixed-cover-cut-review/TASK.json b/research/p104-fixed-cover-cut-review/TASK.json new file mode 100644 index 0000000000..154c6239f7 --- /dev/null +++ b/research/p104-fixed-cover-cut-review/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "p104-side-correction", + "question": "Can the proposed P104 joint endpoint flags be realized by a chronological correction program with coefficients, dirty restoration and an affordable complete bill?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/p104-native-channel/README.md", + "research/p104-native-channel/PROOF.md", + "docs/research/community-efficient1000-review.md", + "research/p104-joint-unit-flags/README.md" + ], + "methods": [ + "Construct one side-correction word at an explicit chronological cut with the needed frames still available.", + "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the revision-6 family record and #2981 static joint flags, alongside the reviewed #1991 channel. #2981 is an author-checked source archive, not an independently validated executable correction or a refutation of program-level lifetime floors.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "After checking live handoffs, pin one named collection from #2981 and attach acquisition/delivery times, source dependencies and coefficient requirements. Test legal access and arbitrary dirty restoration; price any completion against the full channel/endpoint/hosting allowance. Stop with the exact missing implication or a scoped counterexample rather than expanding the static cover census.", + "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.", + "allowed_variations": [ + "One correction factorization, one chronological cut, or one explicit hosting obstruction.", + "A changed correction schedule with an updated full bill and native frame contract." + ], + "scope_change_triggers": [ + "Recompiling the already certified low-rank channel without closing a new obligation.", + "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier.", + "Repeating a correction or physical conversion already supplied by a pending follow-up without adding independent coverage or a different unresolved obligation.", + "Repeating the 208-flag static matching or calling a static nested cover a chronological correction program. Independent audit of that certificate is distinct and remains useful." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991", + "2586", + "endpoint transport", + "physical dual", + "relay composition", + "2981", + "joint unit flags", + "acquisition delivery", + "static nesting" + ], + "existing_checks": [ + { + "scope": "PR #2981 reports static joint endpoint flags and a matching of 208 departure and arrival flags; archival intake is not independent verification.", + "evidence": "research/p104-joint-unit-flags/README.md", + "remaining": "Independent flag check and a chronological coefficient program with dirty restoration and a complete cost.", + "status": "author-checked", + "source_commit": "3d24b92d8ba057b57cb2d480170ec407520e6882", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Independent hypothesis-by-hypothesis review of the PR3259 fixed-cover support-cut embedding argument (and PR3252's memory-relaxation proof, and what PR3427 consumes), with a sharper valid criterion (one recombined helper per path), its finite P104 consequences, three single-relaxation support rows and a small-domain coefficient oracle. Audit only.", + "scope_change_reason": "The card asks for a chronological correction program. The revision-6 decisions table (row 1) instead asks first for a review of the submitted #3259 support cut and its contract, which decides whether the fixed-cover route is closed and what any reopening must cover. No construction is attempted.", + "bottleneck_link": "Decides whether the fixed-cover, immutable-X, unread-Y, independent-dirt, monotone equal-frame P104 contract is closed and how large its obstruction is (2,682 unsupported required entries, not one), which bounds what a contract change or source preconditioner must reopen before any construction round.", + "budget_minutes": 150, + "stop_rule": "Stop at a proof-review verdict per step; on an engine disagreement, a proof gap or an oracle escape, stop and minimize. No matching search, no correction construction, no pricing beyond counting witness operations, at most three new relaxation rows, no Lean.", + "outcome": "completed", + "evidence": "PROOF-REVIEW.md (step table a-h, lemma proof, PR3252 review, PR3427 consumption); verify.py (layered control reproducing PR3259 numbers; sharp criterion by two loop orders; PR3427 four-column masks; rank(U-I)>=17 by Fraction elimination and Bareiss minor; rows R1/R1c/R2/R3; 4,500-program oracle and five negative controls); test_verify.py (four failing mutations and the Y-relay escape).", + "author": "Sagar Thakrar (thakrarsagar)", + "ai_assistance": "Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) for analysis, code and writing. No independent human or formal-kernel review is claimed.", + "open_questions": [ + { + "question": "What rank does the full unsupported pattern force on a P104 source preconditioner (U-I)?", + "why_it_matters": "A greedy rectangle already gives rank(U-I)>=17 versus PR3427's 4; a min-rank completion of -C on all 8,506 unsupported pairs may force much more and would further constrain joint native source preparation.", + "first_step": "Bound the min-rank completion exactly (larger or overlapping rectangles, or a min-rank argument) with the pinned sharp support; no matching search.", + "blocked_by": "Nothing beyond the sharp support certificate here; pricing a joint preparation remains separate." + }, + { + "question": "What is the smallest set of off-cover helper flags reopening all 2,682 sharp-missing entries, and its full bill?", + "why_it_matters": "Relaxing the fixed cover (R2) reopens every entry at support level, so it is the cheapest support reopening found here.", + "first_step": "Cover the 2,682 (V<=W) snapshot pairs by a minimum number of free full flags and list each added operation.", + "blocked_by": "Coefficients, dirty restoration, chronology, native/hosting/precision/consumer costs are unknown." + }, + { + "question": "Is there a coefficient-level correction that reads channel state (R1c/R3) and restores it?", + "why_it_matters": "Channel state already carries the support of G/2, so support tests reopen everything; only a coefficient-level construction can decide this route.", + "first_step": "Specify one target row, the channel registers read, the restoration of each, and the changed channel obligations.", + "blocked_by": "Changed original channel; restoration and pricing unknown." + } + ] +} diff --git a/research/p104-fixed-cover-cut-review/VERIFY.json b/research/p104-fixed-cover-cut-review/VERIFY.json new file mode 100644 index 0000000000..272525fadc --- /dev/null +++ b/research/p104-fixed-cover-cut-review/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-joint-unit-flags/CERTIFICATE.json", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "research/p104-native-channel/inputs/P104-FIXTURE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "PR3259 layered control, sharp criterion (two loop orders), PR3427 masks, rank(U-I)>=17, rows R1/R1c/R2/R3, 4,500-program oracle and five negative controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 300, + "checks": "Four deliberate defects must fail; Y-relay escape" + } + ] +} diff --git a/research/p104-fixed-cover-cut-review/test_verify.py b/research/p104-fixed-cover-cut-review/test_verify.py new file mode 100644 index 0000000000..c4fa2f26a2 --- /dev/null +++ b/research/p104-fixed-cover-cut-review/test_verify.py @@ -0,0 +1,64 @@ +#!/usr/bin/env python3 +"""Negative controls: each deliberate defect must make verify.py fail.""" + +import unittest +from pathlib import Path +from unittest import mock + +import runpy + +V = runpy.run_path(str(Path(__file__).resolve().parent / "verify.py")) + + +def fails(fn, *args): + try: + fn(*args) + except SystemExit as exc: + return str(exc).startswith("FAIL") + return False + + +class Controls(unittest.TestCase): + def test_tampered_input_hash(self): + bad = {k: "0" * 64 for k in V["INPUTS"]} + with mock.patch.dict(V["load"].__globals__["INPUTS"], bad): + self.assertTrue(fails(V["load"])) + + def test_oracle_rejects_an_unsound_test(self): + # A test that grants only shared snapshots misses helper paths. + g = V["oracle"].__globals__ + with mock.patch.dict(g, {"small_sharp": lambda inst: { + (t, s) for s, xc in enumerate(inst[1]) + for t, yc in enumerate(inst[2]) if set(xc) & set(yc)}}): + self.assertTrue(fails(V["oracle"], 7, ((3, 400),), 120)) + + def test_dropping_nesting_breaks_pr3427_masks(self): + g = V["sharp_by_frames"].__globals__ + r = V["p104"]() + loose = [0] * 104 + geo, paths = r["geo"], r["paths"] + masks = V["endpoint_masks"](geo) + frames = {f for k in "XY" for i in range(104) + for f in paths[k + str(i)]} + adm = {f: V["admit_mask"](geo, masks, f) for f in frames} + for t in range(104): + for s in range(104): + if any(adm[v] and adm[w] for v in paths["X%d" % s] + for w in paths["Y%d" % t]): + loose[t] |= 1 << s + got = [sum(1 << t for t in range(104) if loose[t] >> s & 1) + for s in range(4)] + self.assertNotEqual(tuple(got), g["PR3427_SOURCE_MASKS"]) + + def test_wrong_rectangle_is_rejected(self): + g = V["rank_consequence"].__globals__ + r = V["p104"]() + with mock.patch.dict(g, {"RANK_ROWS": g["RANK_ROWS"] + (71,)}): + self.assertTrue(fails(V["rank_consequence"], r)) + + def test_y_relay_counterexample_is_a_real_escape(self): + self.assertEqual(V["y_relay_counterexample"](), (1, True)) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/p104-fixed-cover-cut-review/verify.py b/research/p104-fixed-cover-cut-review/verify.py new file mode 100644 index 0000000000..c5cfd749b1 --- /dev/null +++ b/research/p104-fixed-cover-cut-review/verify.py @@ -0,0 +1,840 @@ +#!/usr/bin/env python3 +"""Review controls for the P104 fixed-cover support cut (PR3259) and its contract. + +Standard library only. Shares no code with PR3182, PR3252, PR3259 or PR3427. +Frames are GF(2) subspaces of F_2^n held as canonical reduced-echelon keys. + + P104 rebuilds frames, covers, the 2,309-edge pool and the 4,992 required + entries; replays PR3259's layered relaxation with a literal frame-hosting + index (control) and evaluates the path-nested one-helper criterion + (sharp untimed support) by two loop orders. + ORACLE exhaustive/bounded small programs with exact Fraction coefficients. + ROWS three single-relaxation witnesses (unpriced; operations counted). +""" + +import hashlib +import json +import sys +from fractions import Fraction +from itertools import combinations, product +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +INPUTS = { + "research/p104-joint-unit-flags/CERTIFICATE.json": + "a98126428a8da6eae91c50afcc42e014a284c82b554ef77e5b3a34fc6d228128", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json": + "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e", + "research/p104-native-channel/inputs/P104-FIXTURE.json": + "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4", +} + + +def need(ok, msg): + if not ok: + raise SystemExit("FAIL: " + msg) + + +# ---------------------------------------------------------------- GF(2) keys +def key(vectors): + """Canonical reduced row-echelon basis (descending pivots) of a span.""" + rows = [] + for v in vectors: + for r in rows: + v = min(v, v ^ r) + if v: + rows = [min(r, r ^ v) for r in rows] + [v] + return tuple(sorted(rows, reverse=True)) + + +def le(small, big): + """small <= big as subspaces (both canonical keys).""" + return len(key(big + small)) == len(big) + + +def span_add(k, v): + return key(k + (v,)) + + +def subspaces(dim_space, k): + """All k-dim subspaces of F_2^dim_space as tuples of basis vectors (RREF).""" + out = [] + for piv in combinations(range(dim_space), k): + free = [(i, j) for i, p in enumerate(piv) for j in range(p) + if j not in piv] + for code in range(1 << len(free)): + rows = [1 << p for p in piv] + for bit, (i, j) in enumerate(free): + if code >> bit & 1: + rows[i] |= 1 << j + out.append(tuple(rows)) + return out + + +# ---------------------------------------------------------------- P104 inputs +def load(): + data = {} + for rel, digest in INPUTS.items(): + raw = (ROOT / rel).read_bytes() + need(hashlib.sha256(raw).hexdigest() == digest, "input hash " + rel) + data[rel] = json.loads(raw) + return [data[r] for r in INPUTS] + + +def frame_paths(word): + paths = {n: [key(b)] for n, b in word["initial_frames"].items() + if n[0] in "XY"} + for ev in word["program"]: + if ev[0] == "transport" and ev[1][0] in "XY": + old, new = key(ev[2]), key(ev[3]) + need(paths[ev[1]][-1] == old and le(old, new) and + len(new) == len(old) + ev[4], "monotone transport " + ev[1]) + paths[ev[1]].append(new) + for n, b in word["final_frames"].items(): + need(n not in paths or paths[n][-1] == key(b), "final frame " + n) + need(len(paths) == 208, "104 X and 104 Y paths") + return paths + + +def channel_roles(word): + """X is never written and Y never read by the original channel.""" + writes, reads = set(), set() + for ev in word["program"]: + if ev[0] in ("add", "copy"): + writes.add(ev[1][0]) + reads.add(ev[2][0]) + elif ev[0] in ("zero", "erase"): + writes.add(ev[1][0]) + need("X" not in writes and "Y" not in reads, "immutable X / unread Y") + return sorted(writes), sorted(reads) + + +def hyperplane_of(cap, functional): + vals = [(v & functional).bit_count() & 1 for v in cap] + j = vals.index(1) + return key([v ^ (cap[j] if vals[i] else 0) + for i, v in enumerate(cap) if i != j]) + + +def covers(cert, paths): + L = [paths["X%d" % i][0] for i in range(104)] + H = [paths["Y%d" % i][-1] for i in range(104)] + need(all(len(x) == 1 for x in L) and all(len(h) == 8 for h in H), "ends") + A = [span_add(L[a // 2], v) for a, v in enumerate( + v for row in cert["forms"]["departure"] for v in row)] + B = [hyperplane_of(H[b // 2], f) for b, f in enumerate( + f for row in cert["forms"]["arrival"] for f in row)] + need(len(A) == len(B) == 208, "208 slots") + need(all(len(x) == 2 for x in A) and all(len(x) == 7 for x in B), "dims") + edges = [(a, b) for a in range(208) for b in range(208) if le(A[a], B[b])] + need(len(edges) == 2309, "2,309 compatible pairs") + return L, A, B, H, edges + + +def e8_ports(fixture): + """Positive E8 roots in doubled coordinates (first nonzero > 0).""" + roots = [] + for v in product((-2, 0, 2), repeat=8): + if sum(x * x for x in v) == 8: + roots.append(v) + for v in product((-1, 1), repeat=8): + if v.count(-1) % 2 == 0: + roots.append(v) + roots = [r for r in roots if next(x for x in r if x) > 0] + need(len(roots) == 120, "120 positive roots") + drop = {tuple(r) for k in ("F0", "C") + for r in fixture["section4_explicit_P104"][k]} + ports = sorted(set(roots) - drop) + need(len(ports) == 104, "104 ports") + return ports + + +def required(ports): + """C = I - G/8 (doubled roots): support and exact values.""" + n = len(ports) + C = [[Fraction(int(t == s)) - Fraction(sum( + x * y for x, y in zip(ports[t], ports[s])), 8) for s in range(n)] + for t in range(n)] + need(C[71][102] == Fraction(-1, 2), "C[71,102] = -1/2") + need(sum(c != 0 for row in C for c in row) == 4992, "4,992 required") + return C + + +# ------------------------------------------------- per-dimension intervals +def interval(L, A, B, H, edge, d): + a, b = edge + return {1: (L[a // 2], L[a // 2]), 2: (A[a], A[a]), + 7: (B[b], B[b]), 8: (H[b // 2], H[b // 2])}.get(d, (A[a], B[b])) + + +def admits(lo, hi, frame): + return len(frame) >= len(lo) and len(frame) <= len(hi) and \ + le(lo, frame) and le(frame, hi) + + +def flats_between(lo, hi, d): + """All d-dim keys F with lo <= F <= hi (literal enumeration).""" + if lo == hi: + return [lo] + comp, cur = [], lo + for v in hi: + nxt = span_add(cur, v) + if len(nxt) > len(cur): + comp.append(v) + cur = nxt + need(cur == hi, "complement") + out = [] + for sub in subspaces(len(comp), d - len(lo)): + vecs = [] + for row in sub: + w = 0 + for i in range(len(comp)): + if row >> i & 1: + w ^= comp[i] + vecs.append(w) + out.append(key(lo + tuple(vecs))) + return out + + +# --------------------------------------- PR3259 layered relaxation (control) +def layered(geo, paths): + L, A, B, H, edges = geo + n = len(edges) + direct = [sum(1 << s for s in range(104) + if set(paths["X%d" % s]) & set(paths["Y%d" % t])) + for t in range(104)] + out, state, hist, rel, wr = direct[:], [0] * n, [], [], [] + for d in range(1, 9): + ivs = [interval(L, A, B, H, e, d) for e in edges] + hosts, mine = {}, [] + for i, (lo, hi) in enumerate(ivs): + fl = flats_between(lo, hi, d) + mine.append(fl) + for f in fl: + hosts[f] = hosts.get(f, 0) | 1 << i + adj = [] + for fl in mine: + m = 0 + for f in fl: + m |= hosts[f] + adj.append(m) + reads = [0] * n + writes = [0] * n + for kind, acc in (("X", reads), ("Y", writes)): + for s in range(104): + for f in paths[kind + str(s)]: + if len(f) == d and f in hosts: + m = hosts[f] + while m: + low = m & -m + acc[low.bit_length() - 1] |= 1 << s + m ^= low + seeded = [st | r for st, r in zip(state, reads)] + state = seeded[:] + for i in range(n): + if seeded[i]: + m = adj[i] + while m: + low = m & -m + state[low.bit_length() - 1] |= seeded[i] + m ^= low + for i in range(n): + w = writes[i] + while w: + low = w & -w + out[low.bit_length() - 1] |= state[i] + w ^= low + hist.append(sum(1 << i for i in range(n) if state[i] >> 102 & 1)) + rel.append(adj) + wr.append(writes) + back = sum(1 << i for i in range(n) if wr[7][i] >> 71 & 1) + for d in (7, 6, 5): + grown = back + for i in range(n): + if back >> i & 1: + grown |= rel[d][i] + back = grown + return out, [bin(h).count("1") for h in hist], back, hist[4] + + +# ------------------------------------ path-nested one-helper criterion (sharp) +def endpoint_masks(geo): + L, A, B, H, edges = geo + dep, arr = [0] * 208, [0] * 208 + for i, (a, b) in enumerate(edges): + dep[a] |= 1 << i + arr[b] |= 1 << i + return dep, arr + + +def admit_mask(geo, masks, f): + """Helper types whose fixed-cover flag can pass through frame f.""" + L, A, B, H, edges = geo + dep, arr = masks + d = len(f) + if d in (1, 2): + low = L if d == 1 else A + return sum_or(dep[a] for a in range(208) + if (low[a // 2] if d == 1 else low[a]) == f) + if d in (7, 8): + return sum_or(arr[b] for b in range(208) + if (B[b] if d == 7 else H[b // 2]) == f) + if 3 <= d <= 6: + return sum_or(dep[a] for a in range(208) if le(A[a], f)) & \ + sum_or(arr[b] for b in range(208) if le(f, B[b])) + return 0 + + +def sum_or(masks): + m = 0 + for x in masks: + m |= x + return m + + +def sharp_by_frames(geo, paths): + """Method 1 (RREF keys): pair snapshots V <= W sharing a helper type.""" + masks = endpoint_masks(geo) + frames = {f for k in "XY" for i in range(104) for f in paths[k + str(i)]} + adm = {f: admit_mask(geo, masks, f) for f in frames} + out = [] + for t in range(104): + m = 0 + ys = paths["Y%d" % t] + for s in range(104): + xs = paths["X%d" % s] + if set(xs) & set(ys) or any( + adm[v] & adm[w] and le(v, w) for v in xs for w in ys): + m |= 1 << s + out.append(m) + return out + + +def points(k): + """Point-set bitmap of a span (512-bit integer).""" + pts = [0] + for v in k: + pts += [p ^ v for p in pts] + return sum(1 << p for p in pts) + + +def sharp_by_edges(geo, paths): + """Method 2 (point bitmaps): per helper type, admitted read/write pairs.""" + L, A, B, H, edges = geo + bm = {n: [points(f) for f in fs] for n, fs in paths.items()} + Lp, Ap = [points(x) for x in L], [points(x) for x in A] + Bp, Hp = [points(x) for x in B], [points(x) for x in H] + snaps = [(p, n) for n in bm if n[0] in "XY" for p in bm[n] + if 2 <= p.bit_count() <= 256] + out = [0] * 104 + for t in range(104): + for s in range(104): + if set(bm["X%d" % s]) & set(bm["Y%d" % t]): + out[t] |= 1 << s + for a, b in edges: + flag = {2: Lp[a // 2], 4: Ap[a], 128: Bp[b], 256: Hp[b // 2]} + ok = [] + for p, n in snaps: + c = p.bit_count() + if (flag.get(c) == p) if c in flag else ( + Ap[a] & p == Ap[a] and p & Bp[b] == p): + ok.append((p, n)) + for v, sn in ok: + if sn[0] != "X": + continue + for w, tn in ok: + if tn[0] == "Y" and v & w == v: + out[int(tn[1:])] |= 1 << int(sn[1:]) + return out + + +def missing(C, support): + return [(t, s) for t in range(104) for s in range(104) + if C[t][s] != 0 and not support[t] >> s & 1] + + +def p104(): + cert, word, fixture = load() + paths = frame_paths(word) + roles = channel_roles(word) + geo = covers(cert, paths) + C = required(e8_ports(fixture)) + lay, fwd, back, f5 = layered(geo, paths) + miss_l = missing(C, lay) + need(miss_l == [(71, 102)], "layered relaxation misses only (71,102)") + need(fwd == [16, 25, 52, 365, 1725, 2283, 2285, 2297], "forward cone") + need(bin(back).count("1") == 37 and back & f5 == 0, "backward 37, disjoint") + sharp = sharp_by_frames(geo, paths) + need(sharp == sharp_by_edges(geo, paths), "sharp criterion: two loop orders") + need(all(sharp[t] & ~lay[t] == 0 for t in range(104)), "sharp <= layered") + return {"roles": roles, "geo": geo, "paths": paths, "C": C, + "layered": lay, "sharp": sharp, "missing_layered": miss_l, + "missing_sharp": missing(C, sharp), "forward": fwd} + + +# ------------------------------------------------ sensitivity rows (support) +def channel_states(word): + """Structural X-dependence of every original-channel register per frame.""" + frame, dep, hist = {}, {}, {} + for n, b in word["initial_frames"].items(): + frame[n] = key(b) + dep[n] = 1 << int(n[1:]) if n[0] == "X" else 0 + hist[n] = {frame[n]: dep[n]} + for ev in word["program"]: + n = ev[1] + if ev[0] == "transport": + frame[n] = key(ev[3]) + elif ev[0] == "add": + dep[n] |= dep[ev[2]] + elif ev[0] == "copy": + frame[n], dep[n] = key(ev[3]), dep[ev[2]] + elif ev[0] == "zero": + frame[n], dep[n] = key(ev[2]), 0 + # erase: keep dependence (over-approximation; no cancellation used) + hist.setdefault(n, {}) + hist[n][frame[n]] = hist[n].get(frame[n], 0) | dep[n] + return hist + + +def rows(r, word): + geo, paths, ms = r["geo"], r["paths"], set(r["missing_sharp"]) + masks, adm = endpoint_masks(geo), {} + + def hop(v, w): + for f in (v, w): + if f not in adm: + adm[f] = admit_mask(geo, masks, f) + return v == w or (adm[v] & adm[w] and le(v, w)) + + def count(sup): + return sum(1 for t, s in ms if sup[t] >> s & 1), bool(sup[71] >> 102 & 1) + + hist = channel_states(word) + ys = [(t, j, w) for t in range(104) for j, w in enumerate(paths["Y%d" % t])] + xin = {(t, j): sum(1 << s for s in range(104) if any( + hop(v, w) for v in paths["X%d" % s])) for t, j, w in ys} + + def relay(seed): + inn = dict(seed) + changed = True + while changed: + changed = False + for u, k, wu in ys: + avail = 0 + for kk in range(k + 1): + avail |= inn[(u, kk)] + for t, j, wt in ys: + if t != u and avail & ~inn[(t, j)] and hop(wu, wt): + inn[(t, j)] |= avail + changed = True + sup = [0] * 104 + for (t, j), m in inn.items(): + sup[t] |= m + return sup + + r1 = relay(xin) + r1c = relay({(t, j): xin[(t, j)] | hist["Y%d" % t].get(w, 0) + for t, j, w in ys}) + free = [sum(1 << s for s in range(104) if any( + 1 <= len(v) <= len(w) <= 8 and le(v, w) + for v in paths["X%d" % s] for w in paths["Y%d" % t])) + for t in range(104)] + old = [(n, f, m) for n, h in hist.items() if n[0] not in "XY" + for f, m in h.items() if m] + r3 = [0] * 104 + for n, f, m in old: + for t in range(104): + if any(hop(f, w) for w in paths["Y%d" % t]): + r3[t] |= m + w2 = [(len(v), len(w)) for v in paths["X102"] for w in paths["Y71"] + if 1 <= len(v) <= len(w) <= 8 and le(v, w)] + w3 = sorted({(n, len(f)) for n, f, m in old if m >> 102 & 1 and + any(hop(f, w) for w in paths["Y71"])}) + # target feedback: first Y71 snapshot whose channel increments hold X102 + w1c = [len(f) for f in paths["Y71"] + if hist["Y71"].get(f, 0) >> 102 & 1][:1] + return {"R1_correction_only_Y_relay": count(r1), + "R1c_Y_relay_with_channel_content": count(r1c), + "R2_free_nested_flags": count(free), + "R3_old_channel_helper_reads": count(r3), + "R2_witness_dims": w2, "R3_witness_states": w3, + "R1c_witness_reads": w1c} + + +# ------------------------------------------- consequence for PR3427's rank +def frac_rank(rows): + a, rk = [list(r) for r in rows], 0 + for c in range(len(a[0]) if a else 0): + p = next((i for i in range(rk, len(a)) if a[i][c] != 0), None) + if p is None: + continue + a[rk], a[p] = a[p], a[rk] + for i in range(len(a)): + if i != rk and a[i][c] != 0: + f = a[i][c] / a[rk][c] + a[i] = [x - f * y for x, y in zip(a[i], a[rk])] + rk += 1 + return rk + + +def bareiss_det(m): + """Exact integer determinant by fraction-free elimination.""" + a, n, sign, prev = [r[:] for r in m], len(m), 1, 1 + for k in range(n - 1): + if a[k][k] == 0: + p = next((i for i in range(k + 1, n) if a[i][k]), None) + if p is None: + return 0 + a[k], a[p], sign = a[p], a[k], -sign + for i in range(k + 1, n): + for j in range(k + 1, n): + a[i][j] = (a[i][j] * a[k][k] - a[i][k] * a[k][j]) // prev + prev = a[k][k] + return sign * a[n - 1][n - 1] + + +def greedy_rectangle(sharp, C): + """Deterministic greedy: for each seed column grow S while the common + unsupported row set R keeps min(|R|,|S|) increasing; keep max rank.""" + n = len(C) + uns = [[not sharp[t] >> s & 1 for s in range(n)] for t in range(n)] + best = (0, (), ()) + for s0 in range(n): + S, R = [s0], [t for t in range(n) if uns[t][s0]] + while True: + cand = sorted(((min(len(r2), len(S) + 1), len(r2), -s, r2) + for s in range(n) if s not in S + for r2 in [[t for t in R if uns[t][s]]]), + reverse=True) + if not cand or cand[0][0] <= min(len(R), len(S)): + break + S.append(-cand[0][2]) + R = cand[0][3] + rk = frac_rank([[C[t][s] for s in S] for t in R]) + if rk > best[0]: + best = (rk, tuple(sorted(R)), tuple(sorted(S))) + return best + + +RANK_ROWS = (2, 4, 5, 13, 15, 25, 32, 36, 39, 48, 52, 73, 76, 82, 87, 89, + 94, 98, 102) +RANK_COLS = (2, 5, 11, 13, 15, 16, 20, 25, 28, 32, 40, 48, 61, 65, 76, 84, + 94, 102) +MINOR_ROWS = (2, 4, 5, 13, 15, 25, 32, 36, 39, 48, 52, 73, 76, 82, 87, 94, + 102) +MINOR_COLS = (2, 5, 11, 13, 15, 16, 20, 25, 28, 32, 40, 48, 61, 65, 76, 94, + 102) + + +def rank_consequence(r): + """Any D = U^-1 - G/2 vanishes on unsupported pairs, so on an unsupported + rectangle (U^-1 - I)[R,S] = -C[R,S] and rank(U - I) >= rank C[R,S].""" + sharp, C = r["sharp"], r["C"] + need(all(not sharp[t] >> s & 1 for t in RANK_ROWS for s in RANK_COLS), + "rectangle unsupported") + need(greedy_rectangle(sharp, C) == (17, RANK_ROWS, RANK_COLS), + "greedy rectangle") + rk = frac_rank([[C[t][s] for s in RANK_COLS] for t in RANK_ROWS]) + det = bareiss_det([[int(8 * C[t][s]) for s in MINOR_COLS] + for t in MINOR_ROWS]) + need(rk == 17 and det != 0, "rank 17 by elimination and a nonzero minor") + return rk, det + + +# ------------------------------------------------- small-domain oracle +class Rng: + """Deterministic LCG so the oracle needs no stdlib random state.""" + + def __init__(self, seed): + self.x = seed + + def below(self, n): + self.x = (self.x * 6364136223846793005 + 1442695040888963407) % 2**64 + return (self.x >> 33) % n + + def coef(self): + return Fraction(self.below(19) + 1, self.below(7) + 1) * ( + -1 if self.below(2) else 1) + + +def grow(rng, n, low, high, d): + """Random d-dim key between low and high (low <= high).""" + cur = low + while len(cur) < d: + v = rng.below(1 << n) + if le((v,), high): + cur = span_add(cur, v) + return cur + + +def instance(rng, n, nx=3, ny=3, nt=3, rigid=False): + full = key([1 << i for i in range(n)]) + zero = () + + def chain(start_dim, end_dim): + out = [grow(rng, n, zero, full, start_dim)] + while len(out[-1]) < end_dim: + step = 1 + rng.below(end_dim - len(out[-1])) + out.append(grow(rng, n, out[-1], full, len(out[-1]) + step)) + return out + xs = [chain(1, n) for _ in range(nx)] + ys = [chain(0, n - 1) for _ in range(ny)] + types = [] + pairs = [(a, b) for c in xs for a in c for e in ys for b in e + if 1 <= len(a) < len(b) and le(a, b)] + for _ in range(nt): + flag = [zero] + if pairs and rng.below(2): # thread the flag through a read/write pair + a, b = pairs[rng.below(len(pairs))] + while len(flag[-1]) < len(a): + flag.append(grow(rng, n, flag[-1], a, len(flag[-1]) + 1)) + while len(flag[-1]) < len(b): + flag.append(grow(rng, n, flag[-1], b, len(flag[-1]) + 1)) + for d in range(len(flag), n + 1): + flag.append(grow(rng, n, flag[-1], full, d)) + fixed = {0: zero, n: full} + for d in range(1, n): + if rigid or rng.below(2): + fixed[d] = flag[d] + types.append(fixed) + return n, xs, ys, types + + +def type_interval(fixed, d): + lo = max((k for k in fixed if k <= d)) + hi = min((k for k in fixed if k >= d)) + return fixed[lo], fixed[hi] + + +def small_admit(fixed, f): + lo, hi = type_interval(fixed, len(f)) + return le(lo, f) and le(f, hi) + + +def small_sharp(inst): + n, xs, ys, types = inst + sup = set() + for s, xc in enumerate(xs): + for t, yc in enumerate(ys): + if set(xc) & set(yc) or any( + le(v, w) and any(small_admit(ty, v) and small_admit(ty, w) + for ty in types) + for v in xc for w in yc if 1 <= len(v) <= len(w) <= n - 1): + sup.add((t, s)) + return sup + + +def small_layered(inst): + n, xs, ys, types = inst + sup = {(t, s) for s, xc in enumerate(xs) for t, yc in enumerate(ys) + if set(xc) & set(yc)} + state = [set() for _ in types] + for d in range(1, n): + fl = [set(flats_between(*type_interval(ty, d), d)) for ty in types] + reads = [{s for s, xc in enumerate(xs) if fl[i] & set(xc)} + for i in range(len(types))] + seeded = [state[i] | reads[i] for i in range(len(types))] + state = [set().union(*(seeded[j] for j in range(len(types)) + if fl[i] & fl[j])) for i in range(len(types))] + for i in range(len(types)): + for t, yc in enumerate(ys): + if fl[i] & set(yc): + sup |= {(t, s) for s in state[i]} + return sup + + +def helper_flag(rng, inst, ty): + """Random full flag through the type's fixed members, biased toward + X/Y snapshot frames so that contacts actually occur.""" + n, xs, ys, _ = inst + snaps = {f for c in xs + ys for f in c} + flag = [()] + for d in range(1, n + 1): + lo, hi = type_interval(ty, d) + base = key(flag[-1] + lo) + hits = sorted(f for f in snaps if len(f) == d and le(base, f) + and le(f, hi)) + if hits and rng.below(8): + flag.append(hits[rng.below(len(hits))]) + else: + flag.append(grow(rng, n, base, hi, d)) + return flag + + +def run_program(rng, inst, steps, violate=None, direct=True): + """Random straight-line program choosing uniformly among the operations + legal at each moment; returns its nonzero source->target pairs.""" + n, xs, ys, types = inst + full = key([1 << i for i in range(n)]) + nh = 4 + tys = [{0: (), n: full} if violate == "offcover" + else types[rng.below(len(types))] for _ in range(nh)] + flags = [helper_flag(rng, inst, ty) for ty in tys] + pos, xp, yp = [0] * nh, [0] * len(xs), [0] * len(ys) + hv = [{("D", h): Fraction(1)} for h in range(nh)] + yv = [{} for _ in ys] + extra = None + if violate == "oldstate": + f = [c for c in xs + ys for c in c if 1 <= len(c) < n] + extra = (f[rng.below(len(f))], {("X", rng.below(len(xs))): Fraction(1)}) + + def axpy(dst, c, src): + for k, v in src.items(): + dst[k] = dst.get(k, 0) + c * v + if dst[k] == 0: + del dst[k] + for _ in range(steps): + fr = [flags[h][pos[h]] for h in range(nh)] + xf = [xs[i][xp[i]] for i in range(len(xs))] + yf = [ys[j][yp[j]] for j in range(len(ys))] + acts = [("xadv", i) for i in range(len(xs)) if xp[i] + 1 < len(xs[i])] + acts += [("yadv", j) for j in range(len(ys)) if yp[j] + 1 < len(ys[j])] + for h in range(nh): + ups = range(pos[h] + 1, n + 1) + if violate == "descent": + ups = [p for p in range(n + 1) if p != pos[h]] + if ups: # one transport action per helper; target drawn later + acts.append(("tr", h, list(ups))) + acts += [("read", h, i) for i in range(len(xs)) if fr[h] == xf[i]] + acts += [("write", h, j) for j in range(len(ys)) if fr[h] == yf[j]] + acts += [("mix", h, g) for g in range(nh) if g != h and ( + fr[h] == fr[g] or violate == "crossframe")] + if violate == "yread": + acts += [("yread", h, j) for j in range(len(ys)) + if fr[h] == yf[j]] + if extra and fr[h] == extra[0]: + acts.append(("old", h)) + acts += [("direct", i, j) for i in range(len(xs)) + for j in range(len(ys)) if direct and xf[i] == yf[j]] + act = acts[rng.below(len(acts))] + c = rng.coef() + if act[0] == "xadv": + xp[act[1]] += 1 + elif act[0] == "yadv": + yp[act[1]] += 1 + elif act[0] == "tr": + pos[act[1]] = act[2][rng.below(len(act[2]))] + hv[act[1]] = {k: c * v for k, v in hv[act[1]].items()} + elif act[0] == "read": + axpy(hv[act[1]], c, {("X", act[2]): Fraction(1)}) + elif act[0] == "write": + axpy(yv[act[2]], c, hv[act[1]]) + elif act[0] == "mix": + axpy(hv[act[2]], c, hv[act[1]]) + elif act[0] == "yread": + axpy(hv[act[1]], c, yv[act[2]]) + elif act[0] == "old": + axpy(hv[act[1]], c, extra[1]) + else: + axpy(yv[act[2]], c, {("X", act[1]): Fraction(1)}) + return {(t, k[1]) for t in range(len(ys)) for k in yv[t] if k[0] == "X"} + + +def y_relay_counterexample(): + """Minimal F_2^3 program: reading a target relays X0 outside both tests. + + e1,e2,e3 = 1,2,4. X0: -> FULL. Y0: 0 -> -> . + Y1: 0 -> . Type T1 fixes < ; type T2 fixes + < . h1 (T1) reads X0 at and writes Y0 there; Y0 is + transported by the frozen channel; h2 (T2, dim-2 frame ) reads + Y0 and writes Y1. Four scalar operations; coefficient c1*c2*c3*c4. + """ + full = key([1, 2, 4]) + t1 = {0: (), 1: key([1]), 2: key([1, 4]), 3: full} + t2 = {0: (), 1: key([2]), 2: key([1, 2]), 3: full} + inst = (3, [[key([1]), full]], [[(), key([1]), key([1, 2])], + [(), key([1, 2])]], [t1, t2]) + c = [Fraction(2), Fraction(-3), Fraction(5, 7), Fraction(-1, 2)] + need(inst[1][0][0] == t1[1], "h1 reads X0 at its line") + h1 = c[0] # h1 += c0 * X0 at + y0 = c[1] * h1 # Y0 += c1 * h1 at + need(inst[2][0][2] == t2[2], "Y0 later frame equals h2 frame") + h2 = c[2] * y0 # h2 += c2 * Y0 at + y1 = c[3] * h2 # Y1 += c3 * h2 at + need(y1 != 0, "nonzero relayed coefficient") + sharp, lay = small_sharp(inst), small_layered(inst) + need((1, 0) not in sharp and (1, 0) not in lay, "Y relay escapes") + return (1, True) + + +def oracle(seed=20261018, trials=((3, 3000), (4, 1500)), steps=120): + rng = Rng(seed) + checked = {"programs": 0, "nonzero_coefficients": 0, "strict_gap": 0, + "helper_mediated": 0} + for n, count in trials: + for _ in range(count): + inst = instance(rng, n) + sharp, lay = small_sharp(inst), small_layered(inst) + need(sharp <= lay, "oracle: sharp support inside layered") + checked["strict_gap"] += sharp < lay + # Direct X->Y adds are seeded identically by both tests; omit + # them so every coefficient is carried by helper paths. + got = run_program(rng, inst, steps, direct=False) + need(got <= sharp, "oracle: legal coefficient outside sharp test") + checked["programs"] += 1 + checked["nonzero_coefficients"] += len(got) + checked["helper_mediated"] += sum( + not set(inst[1][s]) & set(inst[2][t]) for t, s in got) + escapes = {"yread": y_relay_counterexample()} + for bad in ("descent", "crossframe", "offcover", "oldstate"): + found = None + for attempt in range(1, 4001): + inst = instance(rng, 3 + attempt % 2, rigid=True) + got = run_program(rng, inst, steps, bad) + if not got <= small_sharp(inst): + found = (attempt, not got <= small_layered(inst)) + break + need(found is not None, "negative control has no teeth: " + bad) + escapes[bad] = found + return checked, escapes + + +PR3427_SOURCE_MASKS = ( # published per-source target masks, sources 0..3 + 0x15088a1021120142242d061684, 0x1504102110011204022d109084, + 0x1b0000480c4084800021001083, 0x2a889524212d01425a52a06020) + + +def main(): + r = p104() + sharp = r["sharp"] + for s, mask in enumerate(PR3427_SOURCE_MASKS): + need(sum(1 << t for t in range(104) if sharp[t] >> s & 1) == mask, + "PR3427 four-column support masks") + ms = r["missing_sharp"] + need(len(ms) == 2682 and (71, 102) in ms, "2,682 sharp-missing entries") + need(len({t for t, _ in ms}) == 104 and len({s for _, s in ms}) == 104, + "every row and column has a sharp-missing entry") + need(sum(bin(m).count("1") for m in sharp) == 2310 and + sum(bin(m).count("1") for m in r["layered"]) == 10815, "support sizes") + _, word, _ = load() + rw = rows(r, word) + need(rw["R1_correction_only_Y_relay"] == (0, False), "R1") + need(rw["R1c_Y_relay_with_channel_content"] == (2682, True), "R1c") + need(rw["R2_free_nested_flags"] == (2682, True), "R2") + need(rw["R3_old_channel_helper_reads"] == (2682, True), "R3") + need(rw["R2_witness_dims"] == [(1, 8)], "R2 witness") + need(rw["R3_witness_states"] == [("D11", 5)], "R3 witness") + need(rw["R1c_witness_reads"] == [5], "R1c feedback witness") + rk, det = rank_consequence(r) + checked, escapes = oracle() + need(checked == ORACLE_EXPECTED, "oracle receipt %r" % (checked,)) + need(escapes == ESCAPES_EXPECTED, "negative controls %r" % (escapes,)) + print(json.dumps({"channel_roles": r["roles"], "layered_missing": + r["missing_layered"], "forward_cone": r["forward"], + "rank_bound": rk, "minor_det_8C": det, + "sharp_missing": len(ms), "rows": rw, "oracle": checked, + "negative_controls": escapes}, sort_keys=True)) + print("PASS_P104_FIXED_COVER_CUT_REVIEW layered_missing=1 " + "sharp_missing=2682 of 4992 pr3427_masks=4 rank_U_minus_I>=17 " + "rows=4 oracle_programs=%d no_kappa" % checked["programs"]) + + +ORACLE_EXPECTED = {"programs": 4500, "nonzero_coefficients": 269, + "strict_gap": 3556, "helper_mediated": 107} +ESCAPES_EXPECTED = {"yread": (1, True), "descent": (1, True), + "crossframe": (7, True), "offcover": (184, True), + "oldstate": (144, True)} + +if __name__ == "__main__": + main() From b2b962aa2513cbab3376c623d2e4fe491eed56e0 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Sun, 18 Oct 2026 23:56:27 +0530 Subject: [PATCH 2/9] Clarify review README wording and credits Co-Authored-By: Claude Opus 5.5 --- research/p104-fixed-cover-cut-review/README.md | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/research/p104-fixed-cover-cut-review/README.md b/research/p104-fixed-cover-cut-review/README.md index 12b30da3b0..4246355296 100644 --- a/research/p104-fixed-cover-cut-review/README.md +++ b/research/p104-fixed-cover-cut-review/README.md @@ -12,8 +12,9 @@ column. PR3259's single missing entry, `C[71,102] = -1/2`, is a property of its looser relaxation. PR3427 states the lemma, but it has not been evaluated beyond PR3427's four -source columns. Applied to all 104 columns, it raises PR3427's source-preconditioner bound -from `rank(U-I) >= 4` to **`rank(U-I) >= 17`**, under PR3427's own contract. +source columns. Applied to all 104 columns, it raises PR3427's +source-preconditioner bound from `rank(U-I) >= 4` to **`rank(U-I) >= 17`**, +under PR3427's own contract. This is an audit: a scoped proof review, a finite certificate and small-domain controls. It constructs nothing and is not a complete multiplication theorem. @@ -41,7 +42,7 @@ restoration. | Relaxed hypothesis | Reaches `(71,102)` | Reopens, of 2,682 | |---|---|---:| -| Cross-layer nesting, as PR3259's proof relaxation drops it | no | 2,681 | +| Cross-layer nesting, as PR3259's proof drops it (a proof relaxation, not a contract change) | no | 2,681 | | Unread Y, correction-only relay (R1) | no | 0 | | Unread Y, with the channel's own Y content readable (R1c) | yes, by feedback on Y71 at dimension 5 | 2,682 | | Fixed cover: helpers not forced through `L/A/B/H` (R2) | yes, one helper through `L_102 <= H_71` | 2,682 | @@ -50,8 +51,8 @@ restoration. Among the rows computed here, two hypotheses each reopen every entry. One is the fixed cover. The other excludes the channel's source-dependent state, whether held in its helpers or exposed by reading targets after the channel -has written them. That state already carries -the support of `G/2`, which contains every off-diagonal requirement. At P104, +has written them. That state already carries the support of `G/2`, which +contains every off-diagonal requirement. At P104, correction-only Y relay reopens nothing, although an `F_2^3` program shows it can matter in principle. Frame descent and cross-frame mixing also break the argument; the small-domain negative controls show this. They are not priced or @@ -110,8 +111,8 @@ independently and sorted. helpers. Seed `20261018`, 120 operations per program, 3,000 programs over `F_2^3` and 1,500 over `F_2^4`. This is a bounded randomized family, not an exhaustive enumeration. -- Before this review, the original channel word was checked for its roles: - X is never written and Y is never read, so K4 and K5 hold for the channel. +- The verifier also checks the roles in the original channel word: X is + never written and Y is never read, so K4 and K5 hold for the channel. ## Scope, inherited assumptions and open obligations @@ -167,7 +168,8 @@ cold replay is unchanged and was not rerun. repair). - jmbarrancoml: PR3427 `344774ba08a73fc3a85fdcb93fb319927bde3ea2` (the one-helper lemma and the rank-four theorem extended here). -- Wentao Li for the chronology audit, which is not redone here. +- Wentao Li for the chronology audit (`p104-channel-touch-restoration-audit`), + which is not redone here. - The native/compiler lineage credited in the pinned inputs: Rohan Arun/1972, Chafik Boukhalfa/1991, Adam Gall/1940, Josie Elliston/1071 and Ali Romman/1125. From 050be3453293b6e291298e47dac5b0a92d8206e6 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Mon, 19 Oct 2026 00:03:29 +0530 Subject: [PATCH 3/9] Add PR3252 full-memory recurrence as third support method An independent multi-hop implementation of PR3252's full-memory recurrence over all 2,309 pool types and 104 sources equals the one-helper criterion on every pair (2,310 supported; the same 2,682 required entries unsupported). The count now rests on two separately proved sound tests computed by different algorithms. Co-Authored-By: Claude Opus 5.5 --- .../PROOF-REVIEW.md | 21 ++++-- .../p104-fixed-cover-cut-review/README.md | 19 +++-- .../p104-fixed-cover-cut-review/TASK.json | 2 +- .../p104-fixed-cover-cut-review/VERIFY.json | 2 +- .../test_verify.py | 13 +++- .../p104-fixed-cover-cut-review/verify.py | 74 ++++++++++++++++++- 6 files changed, 112 insertions(+), 19 deletions(-) diff --git a/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md b/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md index 16af367f81..a4feb0cd7b 100644 --- a/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md +++ b/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md @@ -161,14 +161,16 @@ delivers a nonzero coefficient outside both PR3259's test and the sharp test. | Required entries unsupported | 1 (`(71,102)`) | 2,682 (every row and column) | | Values of unsupported entries | `-1/2` | 1,801 at `-1/2`, 881 at `+1/2` | -The sharp criterion is computed in two ways: +The sharp criterion is computed in three ways: - reduced-echelon keys with helper-type masks; -- point-set bitmaps looped by helper type. +- point-set bitmaps looped by helper type; +- an independent multi-hop implementation of PR3252's full-memory recurrence + over the whole pool. -The two agree. For sources 0-3 the per-source target masks equal PR3427's -published masks exactly. Those masks come from PR3427's direct criterion and -from PR3252's full-memory operations. +All three agree on all 10,816 pairs. For sources 0-3 the per-source target +masks equal PR3427's published masks exactly. Those masks come from PR3427's +direct criterion and from PR3252's full-memory operations. ## PR3252 PROOF.md (shorter review) @@ -189,9 +191,12 @@ PR3259's K1-K7 written with per-helper bounds `L(h,d) <= F(h,d) <= U(h,d)`. The full-memory mode keeps a lower bound on the frame the signal used. Like any sound untimed test under this contract, it cannot be stricter than the sharp -criterion, which is exact. On PR3427's four columns it equals the sharp -criterion. This review does not compare the two on the other columns. The -one-step mode forgets that bound and is weaker. PR3252's finite checks use fixed matchings and F_2^3 +criterion, which is exact. A new implementation over the whole 2,309-type pool +and all 104 sources (`full_memory` in the verifier) **equals the sharp criterion +on every pair**: 2,310 supported pairs and the same 2,682 unsupported required +entries. The 2,682 count therefore rests on two separately proved sound tests, +computed by different algorithms. The one-step mode forgets the memory bound +and is weaker; it was not run. PR3252's finite checks use fixed matchings and F_2^3 interval fixtures. The proof is universal over its contract, and no gap was found. diff --git a/research/p104-fixed-cover-cut-review/README.md b/research/p104-fixed-cover-cut-review/README.md index 4246355296..a0b11ebf08 100644 --- a/research/p104-fixed-cover-cut-review/README.md +++ b/research/p104-fixed-cover-cut-review/README.md @@ -8,8 +8,10 @@ fact gives a valid criterion, **one recombined helper per path**. This lemma is stated in PR3427 and re-proved here in every dimension case. It is exact for untimed support. Under it, **2,682 of the 4,992 required entries of `C = I - G/2` are unsupported**, with at least one in every row and every -column. PR3259's single missing entry, `C[71,102] = -1/2`, is a property of its -looser relaxation. +column. PR3252's full-memory recurrence is a separate sound test, reviewed +valid here. A new implementation of it over the whole pool gives exactly the +same support, 2,310 pairs, on all 104 columns. PR3259's single missing entry, +`C[71,102] = -1/2`, is a property of its looser relaxation. PR3427 states the lemma, but it has not been evaluated beyond PR3427's four source columns. Applied to all 104 columns, it raises PR3427's @@ -29,7 +31,7 @@ selected frontier are unchanged. | PR3252 PROOF.md (memory relaxation) | Valid for its recurrence and contract. | | What PR3427 consumes | Its own one-helper lemma and PR3252's full-memory operations, not PR3259's recurrence. Both are justified. | | Control: PR3259 layered test, rebuilt | Missing set `{(71,102)}`. Forward counts `16,25,52,365,1725,2283,2285,2297`. Backward cone 37, disjoint. | -| Sharp criterion (two loop orders) | 2,682 required entries unsupported: 1,801 at `-1/2` and 881 at `+1/2`. 2,310 supported pairs, against 10,815 for PR3259's test. | +| Sharp criterion: two loop orders, plus PR3252's full-memory recurrence as a third method | 2,682 required entries unsupported: 1,801 at `-1/2` and 881 at `+1/2`. 2,310 supported pairs, against 10,815 for PR3259's test. All three methods agree on every pair. | | Cross-check with PR3427 | The four published per-source masks (sources 0-3) are reproduced exactly. | | Consequence for PR3427 | A 19-by-18 rectangle of unsupported pairs has `rank C[R,S] = 17`, giving `rank(U-I) >= 17`. A 17-by-17 minor has `det(8C) = 2^43`. | | Oracle, coefficient level | 4,500 seeded legal programs over `F_2^3` and `F_2^4`, with exact `Fraction` coefficients. 269 nonzero helper-path coefficients, 107 of them for pairs with no common snapshot. None lies outside the sharp test. | @@ -63,7 +65,7 @@ counted at P104 here. Cited, not recomputed: ## Reproduce -From the repository root, with the standard library (about 20 s): +From the repository root, with the standard library (about 2 minutes in all): ```sh python3 -I -O -Werror -B research/p104-fixed-cover-cut-review/verify.py @@ -99,8 +101,13 @@ independently and sorted. - The layered control hosts every d-flat of each interval literally, then takes one read-first step per layer. -- The sharp criterion is computed twice. One method uses echelon keys with - helper-type masks. The other uses point-set bitmaps, looped per helper type. +- The sharp criterion is computed in three ways: + - echelon keys with helper-type masks; + - point-set bitmaps, looped per helper type; + - PR3252's full-memory recurrence (carry, admitted reads, relay of old + memories `S + L(h,d) + L(w,d)`, minimal-memory pruning), rewritten over + all 2,309 types and 104 sources. It is a multi-hop recurrence and does + not assume the one-helper lemma. - The rank bound uses a deterministic greedy over 104 seed columns. Each step adds the column that most increases `min(|R|,|S|)`, ties to the smallest index. Exact `Fraction` elimination gives the rank, and an diff --git a/research/p104-fixed-cover-cut-review/TASK.json b/research/p104-fixed-cover-cut-review/TASK.json index 154c6239f7..455b56183a 100644 --- a/research/p104-fixed-cover-cut-review/TASK.json +++ b/research/p104-fixed-cover-cut-review/TASK.json @@ -74,7 +74,7 @@ "budget_minutes": 150, "stop_rule": "Stop at a proof-review verdict per step; on an engine disagreement, a proof gap or an oracle escape, stop and minimize. No matching search, no correction construction, no pricing beyond counting witness operations, at most three new relaxation rows, no Lean.", "outcome": "completed", - "evidence": "PROOF-REVIEW.md (step table a-h, lemma proof, PR3252 review, PR3427 consumption); verify.py (layered control reproducing PR3259 numbers; sharp criterion by two loop orders; PR3427 four-column masks; rank(U-I)>=17 by Fraction elimination and Bareiss minor; rows R1/R1c/R2/R3; 4,500-program oracle and five negative controls); test_verify.py (four failing mutations and the Y-relay escape).", + "evidence": "PROOF-REVIEW.md (step table a-h, lemma proof, PR3252 review, PR3427 consumption, rank consequence); verify.py (layered control reproducing PR3259 numbers; sharp criterion by two loop orders and by an independent PR3252 full-memory recurrence over all 104 columns, all equal; PR3427 four-column masks; rank(U-I)>=17 by Fraction elimination and a Bareiss minor; rows R1/R1c/R2/R3; 4,500-program oracle and five negative controls); test_verify.py (four failing mutations and the Y-relay escape).", "author": "Sagar Thakrar (thakrarsagar)", "ai_assistance": "Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) for analysis, code and writing. No independent human or formal-kernel review is claimed.", "open_questions": [ diff --git a/research/p104-fixed-cover-cut-review/VERIFY.json b/research/p104-fixed-cover-cut-review/VERIFY.json index 272525fadc..b0a87063ea 100644 --- a/research/p104-fixed-cover-cut-review/VERIFY.json +++ b/research/p104-fixed-cover-cut-review/VERIFY.json @@ -19,7 +19,7 @@ "{package}/verify.py" ], "timeout_seconds": 300, - "checks": "PR3259 layered control, sharp criterion (two loop orders), PR3427 masks, rank(U-I)>=17, rows R1/R1c/R2/R3, 4,500-program oracle and five negative controls" + "checks": "PR3259 layered control; sharp criterion by two loop orders and PR3252 full-memory recurrence (all equal); PR3427 masks; rank(U-I)>=17; rows R1/R1c/R2/R3; 4,500-program oracle; five negative controls" }, { "argv": [ diff --git a/research/p104-fixed-cover-cut-review/test_verify.py b/research/p104-fixed-cover-cut-review/test_verify.py index c4fa2f26a2..d3bce04c8e 100644 --- a/research/p104-fixed-cover-cut-review/test_verify.py +++ b/research/p104-fixed-cover-cut-review/test_verify.py @@ -10,6 +10,15 @@ V = runpy.run_path(str(Path(__file__).resolve().parent / "verify.py")) +_CACHE = [] + + +def result(): + if not _CACHE: + _CACHE.append(V["p104"]()) + return _CACHE[0] + + def fails(fn, *args): try: fn(*args) @@ -34,7 +43,7 @@ def test_oracle_rejects_an_unsound_test(self): def test_dropping_nesting_breaks_pr3427_masks(self): g = V["sharp_by_frames"].__globals__ - r = V["p104"]() + r = result() loose = [0] * 104 geo, paths = r["geo"], r["paths"] masks = V["endpoint_masks"](geo) @@ -52,7 +61,7 @@ def test_dropping_nesting_breaks_pr3427_masks(self): def test_wrong_rectangle_is_rejected(self): g = V["rank_consequence"].__globals__ - r = V["p104"]() + r = result() with mock.patch.dict(g, {"RANK_ROWS": g["RANK_ROWS"] + (71,)}): self.assertTrue(fails(V["rank_consequence"], r)) diff --git a/research/p104-fixed-cover-cut-review/verify.py b/research/p104-fixed-cover-cut-review/verify.py index c5cfd749b1..8ec7f1c271 100644 --- a/research/p104-fixed-cover-cut-review/verify.py +++ b/research/p104-fixed-cover-cut-review/verify.py @@ -7,7 +7,8 @@ P104 rebuilds frames, covers, the 2,309-edge pool and the 4,992 required entries; replays PR3259's layered relaxation with a literal frame-hosting index (control) and evaluates the path-nested one-helper criterion - (sharp untimed support) by two loop orders. + (sharp untimed support) by two loop orders and by an independent + full-memory recurrence in the manner of PR3252. ORACLE exhaustive/bounded small programs with exact Fraction coefficients. ROWS three single-relaxation witnesses (unpriced; operations counted). """ @@ -349,6 +350,76 @@ def sharp_by_edges(geo, paths): return out +def full_memory(geo, paths): + """Method 3: PR3252's full-memory recurrence, reimplemented over the whole + pool. Carry old memories; insert each admitted source snapshot; relay only + old memories S over contacts as S + L(h,d) + L(w,d) when it fits both + upper bounds; output a source at a target snapshot containing a memory. + Memories are grouped by subspace key with a source bitmask.""" + L, A, B, H, edges = geo + n = len(edges) + out = [sum(1 << s for s in range(104) + if set(paths["X%d" % s]) & set(paths["Y%d" % t])) + for t in range(104)] + snaps = {"X": {}, "Y": {}} + for k in "XY": + for i in range(104): + for f in paths[k + str(i)]: + snaps[k][f] = snaps[k].get(f, 0) | 1 << i + mem = [{} for _ in range(n)] + for d in range(1, 9): + ivs = [interval(L, A, B, H, e, d) for e in edges] + hosts, mine = {}, [] + for i, (lo, hi) in enumerate(ivs): + fl = flats_between(lo, hi, d) + mine.append(fl) + for f in fl: + hosts[f] = hosts.get(f, 0) | 1 << i + nxt = [dict(m) for m in mem] + for h in range(n): + nb = 0 + for f in mine[h] if mem[h] else (): + nb |= hosts[f] + nb &= ~(1 << h) + while nb: + w = (nb & -nb).bit_length() - 1 + nb &= nb - 1 + for S, sm in mem[h].items(): + T = key(S + ivs[h][0] + ivs[w][0]) + if len(T) <= d and le(T, ivs[h][1]) and le(T, ivs[w][1]): + nxt[w][T] = nxt[w].get(T, 0) | sm + for f, sm in snaps["X"].items(): + m = hosts.get(f, 0) if len(f) == d else 0 + while m: + i = (m & -m).bit_length() - 1 + m &= m - 1 + nxt[i][f] = nxt[i].get(f, 0) | sm + mem = [prune(m) for m in nxt] + for f, tm in snaps["Y"].items(): + m = hosts.get(f, 0) if len(f) == d else 0 + while m: + i = (m & -m).bit_length() - 1 + m &= m - 1 + src = sum_or(sm for S, sm in mem[i].items() if le(S, f)) + for t in range(104): + if tm >> t & 1: + out[t] |= src + return out + + +def prune(m): + """Keep, per source, only subset-minimal memories (outputs unchanged).""" + keep = {} + for S in sorted(m, key=len): + sm = m[S] + for S2, sm2 in keep.items(): + if len(S2) < len(S) and le(S2, S): + sm &= ~sm2 + if sm: + keep[S] = sm + return keep + + def missing(C, support): return [(t, s) for t in range(104) for s in range(104) if C[t][s] != 0 and not support[t] >> s & 1] @@ -367,6 +438,7 @@ def p104(): need(bin(back).count("1") == 37 and back & f5 == 0, "backward 37, disjoint") sharp = sharp_by_frames(geo, paths) need(sharp == sharp_by_edges(geo, paths), "sharp criterion: two loop orders") + need(sharp == full_memory(geo, paths), "PR3252 full-memory test = sharp") need(all(sharp[t] & ~lay[t] == 0 for t in range(104)), "sharp <= layered") return {"roles": roles, "geo": geo, "paths": paths, "C": C, "layered": lay, "sharp": sharp, "missing_layered": miss_l, From dd79433faa651deeabd5104c8672ee5bec95a4ce Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Mon, 19 Oct 2026 00:16:22 +0530 Subject: [PATCH 4/9] Strengthen oracle: pooled/unpooled families, path-directed relays The small-domain oracle now runs a checked interpreter (type flags, ascending transports, equal-frame reads/adds/writes, monotone frozen schedules) on 18,000 programs. Pooled (P104-like) instances: 1,043 nonzero helper-path coefficients, 633 relayed across helper types, none outside the one-helper test. Unpooled instances: 1,887 coefficients, none outside PR3259's layered test. A fixed F_2^4 two-type relay shows the one-helper lemma needs the pool to be closed under recombination, while PR3259's test does not. Co-Authored-By: Claude Opus 5.5 --- .../PROOF-REVIEW.md | 8 +- .../p104-fixed-cover-cut-review/README.md | 25 +- .../p104-fixed-cover-cut-review/TASK.json | 2 +- .../p104-fixed-cover-cut-review/VERIFY.json | 6 +- .../p104-fixed-cover-cut-review/verify.py | 249 ++++++++++++++++-- 5 files changed, 256 insertions(+), 34 deletions(-) diff --git a/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md b/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md index a4feb0cd7b..11ffec81f0 100644 --- a/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md +++ b/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md @@ -78,7 +78,7 @@ K6 is a premise about the correction, not about the channel. | e | Dirt has no source coefficient; cancellation cannot create one. | K7, linearity | Valid. A coefficient of `X_s` in `Y_t` is a sum over dependency paths of products of operation scalars. With no path it is zero. Restoration operations are linear operations and are included. | | f | Same-dimension runs share one frame, so first and last helpers are adjacent and one step suffices. | K2, K3 | Valid, including a read or write in mid-run (the path starts or ends there) and runs that revisit a helper. Only the endpoints' common frame is used. Equal-frame groups in an actual program are cliques. | | g | Read-first seeding; accumulation after the edge; dims 0 and 9 excluded; early writes. | K4, K5 | Valid. Seeding the layer's reads before the single step covers a read followed by relays at that dimension. Accumulating after the step covers relays followed by a write. X frames have dimension at least 1 and Y frames at most 8, so dims 0 and 9 cannot join a read to a write. The recurrence accumulates at every layer, so Y71's dimension-5 writes are checked. | -| h | Pooling: "every matching embeds by its selected edges". | K1 | Valid, and slightly stronger than stated. Any multiset of helpers with pool types embeds: helpers of one type merge into one virtual helper, whose state is a union. | +| h | Pooling: "every matching embeds by its selected edges". | K1 | Valid, and slightly stronger than stated. Any multiset of helpers with pool types embeds: helpers of one type merge into one virtual helper, whose state is a union. PR3259's layered test does not need the pool to be closed under recombination. The sharper lemma below does; see `unpooled_relay_example`. | Stop-rule outcome: no step fails. The control engine reproduces every PR3259 number: missing set `{(71,102)}`, forward counts @@ -136,6 +136,12 @@ In every case `A[a] <= B[b]`, so `(a,b)` is in the pool. The spaces That partial flag extends to a full flag. One helper of type `(a,b)` therefore admits both V and W. ∎ +The proof uses the fact that the pool contains *every* compatible pair, so +that the recombined type exists. For a type list without that closure the +conclusion can fail. The verifier's `F_2^4` example relays across two rigid +types at a shared plane. It lies in PR3259's test but outside the one-helper +test. + *Converse (untimed).* If the condition holds, one helper of type `(a,b)` with that full flag reads `X_s` at V and writes `Y_t` at W. With chronology relaxed, the criterion is therefore exact. No sound untimed support test under K1-K7 can diff --git a/research/p104-fixed-cover-cut-review/README.md b/research/p104-fixed-cover-cut-review/README.md index a0b11ebf08..1d177a16d4 100644 --- a/research/p104-fixed-cover-cut-review/README.md +++ b/research/p104-fixed-cover-cut-review/README.md @@ -34,7 +34,7 @@ selected frontier are unchanged. | Sharp criterion: two loop orders, plus PR3252's full-memory recurrence as a third method | 2,682 required entries unsupported: 1,801 at `-1/2` and 881 at `+1/2`. 2,310 supported pairs, against 10,815 for PR3259's test. All three methods agree on every pair. | | Cross-check with PR3427 | The four published per-source masks (sources 0-3) are reproduced exactly. | | Consequence for PR3427 | A 19-by-18 rectangle of unsupported pairs has `rank C[R,S] = 17`, giving `rank(U-I) >= 17`. A 17-by-17 minor has `det(8C) = 2^43`. | -| Oracle, coefficient level | 4,500 seeded legal programs over `F_2^3` and `F_2^4`, with exact `Fraction` coefficients. 269 nonzero helper-path coefficients, 107 of them for pairs with no common snapshot. None lies outside the sharp test. | +| Oracle, coefficient level | 18,000 seeded legal programs over `F_2^3` and `F_2^4`, with exact `Fraction` coefficients. On pooled (P104-like) instances there are 9,000 programs and 1,043 nonzero helper-path coefficients, 633 of them relayed across helper types; none lies outside the one-helper test. On unpooled instances there are 9,000 programs and 1,887 coefficients; none lies outside PR3259's test. | ### Which hypotheses carry the obstruction @@ -75,7 +75,7 @@ python3 -I -O -Werror -B research/p104-fixed-cover-cut-review/test_verify.py The verifier prints one JSON receipt. Its last line is ``` -PASS_P104_FIXED_COVER_CUT_REVIEW layered_missing=1 sharp_missing=2682 of 4992 pr3427_masks=4 rank_U_minus_I>=17 rows=4 oracle_programs=4500 no_kappa +PASS_P104_FIXED_COVER_CUT_REVIEW layered_missing=1 sharp_missing=2682 of 4992 pr3427_masks=4 rank_U_minus_I>=17 rows=4 oracle_programs=18000 no_kappa ``` The registered replay is @@ -92,6 +92,8 @@ Every check raises `SystemExit("FAIL: ...")`, so checks stay active under `-O`. outside both tests. They are Y read (a fixed four-operation `F_2^3` program), frame descent, cross-frame mixing, an off-cover flag and correlated old state. +- A sixth control, a fixed unpooled two-type relay over `F_2^4`, must lie + outside the one-helper test and inside PR3259's test. ## Method and independence @@ -113,11 +115,22 @@ independently and sorted. smallest index. Exact `Fraction` elimination gives the rank, and an independent integer Bareiss determinant confirms it. The greedy is not optimal, so 17 is a lower bound. -- Oracle programs choose uniformly among the operations legal at each moment. - Direct X-to-Y adds are omitted so that every coefficient travels through - helpers. Seed `20261018`, 120 operations per program, 3,000 programs over - `F_2^3` and 1,500 over `F_2^4`. This is a bounded randomized family, not an +- The oracle uses seed `20261018`, with 3,000 instances over `F_2^3` and 1,500 + over `F_2^4` in each family. It is a bounded randomized family, not an exhaustive enumeration. + - *Pooled* instances mirror P104. Departure chains fix the low dimensions, + arrival chains fix the high ones, and the types are every compatible pair. + - *Unpooled* instances use six random full flags as types. + - Each instance runs two programs. One chooses uniformly among the + operations legal at each moment, for 120 operations. The other follows a + random path through one to three relays. A checked interpreter executes + both: flags of the right type, ascending transports, and equal-frame + reads, adds and writes. + - Direct X-to-Y adds are omitted, so every coefficient travels through + helpers. + - Random unpooled programs found no escape from the one-helper test. A + fixed `F_2^4` two-type relay shows such an escape exists, so the lemma + needs pooling. PR3259's test does not. - The verifier also checks the roles in the original channel word: X is never written and Y is never read, so K4 and K5 hold for the channel. diff --git a/research/p104-fixed-cover-cut-review/TASK.json b/research/p104-fixed-cover-cut-review/TASK.json index 455b56183a..85d4366ee2 100644 --- a/research/p104-fixed-cover-cut-review/TASK.json +++ b/research/p104-fixed-cover-cut-review/TASK.json @@ -74,7 +74,7 @@ "budget_minutes": 150, "stop_rule": "Stop at a proof-review verdict per step; on an engine disagreement, a proof gap or an oracle escape, stop and minimize. No matching search, no correction construction, no pricing beyond counting witness operations, at most three new relaxation rows, no Lean.", "outcome": "completed", - "evidence": "PROOF-REVIEW.md (step table a-h, lemma proof, PR3252 review, PR3427 consumption, rank consequence); verify.py (layered control reproducing PR3259 numbers; sharp criterion by two loop orders and by an independent PR3252 full-memory recurrence over all 104 columns, all equal; PR3427 four-column masks; rank(U-I)>=17 by Fraction elimination and a Bareiss minor; rows R1/R1c/R2/R3; 4,500-program oracle and five negative controls); test_verify.py (four failing mutations and the Y-relay escape).", + "evidence": "PROOF-REVIEW.md (step table a-h, lemma proof, PR3252 review, PR3427 consumption, rank consequence); verify.py (layered control reproducing PR3259 numbers; sharp criterion by two loop orders and by an independent PR3252 full-memory recurrence over all 104 columns, all equal; PR3427 four-column masks; rank(U-I)>=17 by Fraction elimination and a Bareiss minor; rows R1/R1c/R2/R3; 18,000-program exact-coefficient oracle (pooled and unpooled families, uniform and path-directed programs, checked interpreter) and six negative controls); test_verify.py (four failing mutations and the Y-relay escape).", "author": "Sagar Thakrar (thakrarsagar)", "ai_assistance": "Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) for analysis, code and writing. No independent human or formal-kernel review is claimed.", "open_questions": [ diff --git a/research/p104-fixed-cover-cut-review/VERIFY.json b/research/p104-fixed-cover-cut-review/VERIFY.json index b0a87063ea..68391d978e 100644 --- a/research/p104-fixed-cover-cut-review/VERIFY.json +++ b/research/p104-fixed-cover-cut-review/VERIFY.json @@ -18,8 +18,8 @@ "-B", "{package}/verify.py" ], - "timeout_seconds": 300, - "checks": "PR3259 layered control; sharp criterion by two loop orders and PR3252 full-memory recurrence (all equal); PR3427 masks; rank(U-I)>=17; rows R1/R1c/R2/R3; 4,500-program oracle; five negative controls" + "timeout_seconds": 600, + "checks": "PR3259 layered control; sharp criterion by two loop orders and PR3252 full-memory recurrence (all equal); PR3427 masks; rank(U-I)>=17; rows R1/R1c/R2/R3; 18,000-program oracle; six negative controls" }, { "argv": [ @@ -30,7 +30,7 @@ "-B", "{package}/test_verify.py" ], - "timeout_seconds": 300, + "timeout_seconds": 600, "checks": "Four deliberate defects must fail; Y-relay escape" } ] diff --git a/research/p104-fixed-cover-cut-review/verify.py b/research/p104-fixed-cover-cut-review/verify.py index 8ec7f1c271..41df716261 100644 --- a/research/p104-fixed-cover-cut-review/verify.py +++ b/research/p104-fixed-cover-cut-review/verify.py @@ -640,7 +640,10 @@ def grow(rng, n, low, high, d): return cur -def instance(rng, n, nx=3, ny=3, nt=3, rigid=False): +def instance(rng, n, nx=3, ny=3, nt=3, rigid=False, pooled=False): + """Random small domain. pooled=True mirrors P104: departure chains fix + dims 1..p, arrival chains fix dims q..n-1, and the type list is every + compatible (departure, arrival) pair, so it is closed under recombination.""" full = key([1 << i for i in range(n)]) zero = () @@ -652,6 +655,8 @@ def chain(start_dim, end_dim): return out xs = [chain(1, n) for _ in range(nx)] ys = [chain(0, n - 1) for _ in range(ny)] + if pooled: + return n, xs, ys, pool_types(rng, n, xs, ys) types = [] pairs = [(a, b) for c in xs for a in c for e in ys for b in e if 1 <= len(a) < len(b) and le(a, b)] @@ -673,6 +678,40 @@ def chain(start_dim, end_dim): return n, xs, ys, types +def pool_types(rng, n, xs, ys): + full = key([1 << i for i in range(n)]) + p = 1 + rng.below(n - 2) + q = p + 1 + rng.below(n - 1 - p) + deps, arrs = [], [] + for _ in range(3): + line = xs[rng.below(len(xs))][0] if rng.below(3) else \ + grow(rng, n, (), full, 1) + dep = [line] + while len(dep) < p: + dep.append(grow(rng, n, dep[-1], full, len(dep) + 1)) + deps.append(dep) + for k in range(3): + if k == 0 or rng.below(2): # grow upward from a departure: compatible + arr = [grow(rng, n, deps[rng.below(3)][-1], full, q)] + while len(arr[-1]) < n - 1: + arr.append(grow(rng, n, arr[-1], full, len(arr[-1]) + 1)) + else: # descend from a target cap or a random hyperplane + arr = [ys[rng.below(len(ys))][-1] if rng.below(3) else + grow(rng, n, (), full, n - 1)] + while len(arr[0]) > q: + arr.insert(0, grow(rng, n, (), arr[0], len(arr[0]) - 1)) + arrs.append(arr) + types = [] + for dep in deps: + for arr in arrs: + if le(dep[-1], arr[0]): + fixed = {0: (), n: full} + fixed.update({len(f): f for f in dep + arr}) + types.append(fixed) + need(types, "pool has a compatible pair") + return types + + def type_interval(fixed, d): lo = max((k for k in fixed if k <= d)) hi = min((k for k in fixed if k >= d)) @@ -746,6 +785,8 @@ def run_program(rng, inst, steps, violate=None, direct=True): pos, xp, yp = [0] * nh, [0] * len(xs), [0] * len(ys) hv = [{("D", h): Fraction(1)} for h in range(nh)] yv = [{} for _ in ys] + relay = [set() for _ in range(nh)] # sources received across two types + via = [set() for _ in ys] extra = None if violate == "oldstate": f = [c for c in xs + ys for c in c if 1 <= len(c) < n] @@ -770,7 +811,7 @@ def axpy(dst, c, src): acts.append(("tr", h, list(ups))) acts += [("read", h, i) for i in range(len(xs)) if fr[h] == xf[i]] acts += [("write", h, j) for j in range(len(ys)) if fr[h] == yf[j]] - acts += [("mix", h, g) for g in range(nh) if g != h and ( + acts += 3 * [("mix", h, g) for g in range(nh) if g != h and ( fr[h] == fr[g] or violate == "crossframe")] if violate == "yread": acts += [("yread", h, j) for j in range(len(ys)) @@ -792,15 +833,21 @@ def axpy(dst, c, src): axpy(hv[act[1]], c, {("X", act[2]): Fraction(1)}) elif act[0] == "write": axpy(yv[act[2]], c, hv[act[1]]) + via[act[2]] |= relay[act[1]] elif act[0] == "mix": axpy(hv[act[2]], c, hv[act[1]]) + relay[act[2]] |= relay[act[1]] + if tys[act[1]] != tys[act[2]]: + relay[act[2]] |= {k[1] for k in hv[act[1]] if k[0] == "X"} elif act[0] == "yread": axpy(hv[act[1]], c, yv[act[2]]) elif act[0] == "old": axpy(hv[act[1]], c, extra[1]) else: axpy(yv[act[2]], c, {("X", act[1]): Fraction(1)}) - return {(t, k[1]) for t in range(len(ys)) for k in yv[t] if k[0] == "X"} + got = {(t, k[1]) for t in range(len(ys)) for k in yv[t] if k[0] == "X"} + run_program.cross_type = {(t, s) for t, s in got if s in via[t]} + return got def y_relay_counterexample(): @@ -830,36 +877,188 @@ def y_relay_counterexample(): return (1, True) +def meet(a, b): + """Intersection of two subspaces (small domains: enumerate a's points).""" + pts = [0] + for x in a: + pts += [p ^ x for p in pts] + return key([p for p in pts if p and le((p,), b)]) + + +def flag_through(rng, inst, ty, must): + """Random full flag of type ty passing through every frame in must + (a nested list), or None when the type cannot host them.""" + n = inst[0] + flag = [()] + for d in range(1, n + 1): + lo, hi = type_interval(ty, d) + base = key(flag[-1] + lo) + above = [f for f in must if len(f) >= d] + cap = meet(hi, above[0]) if above else hi + if len(base) > d or len(cap) < d or not le(base, cap): + return None + flag.append(grow(rng, n, base, cap, d)) + return flag + + +def execute(inst, helpers, ops): + """Run an explicit straight-line program, checking every contract rule: + flags of the helper's type, monotone transports, equal-frame reads, + mixes and writes, monotone frozen X/Y schedules. Exact Fractions.""" + n, xs, ys, _ = inst + for ty, fl in helpers: + need(all(small_admit(ty, f) for f in fl[1:n]) and all( + le(a, b) for a, b in zip(fl, fl[1:])), "helper flag of its type") + pos, xp, yp = [0] * len(helpers), [0] * len(xs), [0] * len(ys) + hv = [{("D", h): Fraction(1)} for h in range(len(helpers))] + yv = [{} for _ in ys] + + def axpy(dst, c, src): + for k, x in src.items(): + dst[k] = dst.get(k, 0) + c * x + if dst[k] == 0: + del dst[k] + for op, a, b, c in ops: + fr = [helpers[h][1][pos[h]] for h in range(len(helpers))] + if op == "x": + need(b >= xp[a], "X schedule monotone") + xp[a] = b + elif op == "y": + need(b >= yp[a], "Y schedule monotone") + yp[a] = b + elif op == "tr": + need(b >= pos[a], "transport ascends") + pos[a] = b + hv[a] = {k: c * x for k, x in hv[a].items()} + elif op == "read": + need(fr[a] == xs[b][xp[b]], "read at equal frame") + axpy(hv[a], c, {("X", b): Fraction(1)}) + elif op == "mix": + need(fr[a] == fr[b] and a != b, "mix at equal frame") + axpy(hv[b], c, hv[a]) + else: + need(fr[a] == ys[b][yp[b]], "write at equal frame") + axpy(yv[b], c, hv[a]) + return {(t, k[1]) for t in range(len(ys)) for k in yv[t] if k[0] == "X"} + + +def directed_program(rng, inst, hops): + """Legal program along a random path: read X_s at V, relay through + `hops` further helpers of random types at shared frames, write Y_t. + Returns (pairs, number of distinct helper types used).""" + n, xs, ys, types = inst + s = rng.below(len(xs)) + xi = rng.below(len(xs[s]) - 1) # never the full space + v = xs[s][xi] + targets = [(t, j) for t in range(len(ys)) for j in range(len(ys[t])) + if len(ys[t][j]) >= len(v) and le(v, ys[t][j])] + if not targets: + return set(), 0 + t, j = targets[rng.below(len(targets))] + w = ys[t][j] + helpers, ops, cur = [], [("x", s, xi, None)], v + for hop in range(hops + 1): + last = hop == hops + must = sorted({cur, w} if last else {cur}, key=len) + fl = None + for _ in range(8): + ty = types[rng.below(len(types))] + fl = flag_through(rng, inst, ty, must) + if fl: + break + if not fl: + return set(), 0 + h = len(helpers) + helpers.append((ty, fl)) + ops.append(("tr", h, fl.index(cur), rng.coef())) + if hop == 0: + ops.append(("read", h, s, rng.coef())) + else: + ops.append(("mix", h - 1, h, rng.coef())) + if last: + ops += [("y", t, j, None), ("tr", h, fl.index(w), rng.coef()), + ("write", h, t, rng.coef())] + else: + ups = [p for p in range(fl.index(cur), n) + if 1 <= len(fl[p]) and le(fl[p], w)] + p = ups[rng.below(len(ups))] + ops.append(("tr", h, p, rng.coef())) + cur = fl[p] + return execute(inst, helpers, ops), len({id(ty) for ty, _ in helpers}) + + +def unpooled_relay_example(): + """F_2^4, types not closed under recombination: a legal two-type relay + lies inside PR3259's layered test but outside the single-type criterion. + + T1 fixes < < ; T2 fixes < < + . h1 (T1) reads X0 at , rises to , adds into h2 + (T2) there; h2 rises to W = and writes Y0.""" + full = key([1, 2, 4, 8]) + t1 = {0: (), 1: key([1]), 2: key([1, 2]), 3: key([1, 2, 8]), 4: full} + t2 = {0: (), 1: key([4]), 2: key([1, 2]), 3: key([1, 2, 4]), 4: full} + inst = (4, [[key([1]), full]], [[(), key([1, 2, 4])]], [t1, t2]) + need(t1[2] == t2[2] and t2[3] == inst[2][0][1], "relay frames") + coef = Fraction(3) * Fraction(-2, 5) * Fraction(7) * Fraction(1, 3) + need(coef != 0, "nonzero relayed coefficient") + need((0, 0) not in small_sharp(inst) and (0, 0) in small_layered(inst), + "pooling is needed for the one-helper criterion") + return True + + def oracle(seed=20261018, trials=((3, 3000), (4, 1500)), steps=120): + """Pooled instances (P104-like): every legal coefficient lies in the + one-helper test, which lies in PR3259's layered test. Unpooled rigid + instances: every legal coefficient lies in the layered test (PR3259 needs + no pooling); escapes from the one-helper test are counted.""" rng = Rng(seed) - checked = {"programs": 0, "nonzero_coefficients": 0, "strict_gap": 0, - "helper_mediated": 0} + c = dict.fromkeys(("programs", "nonzero_coefficients", "helper_mediated", + "cross_type_relayed", "directed_multi_type", + "strict_gap", "unpooled_programs", + "unpooled_coefficients", "unpooled_multi_type", + "unpooled_single_type_escapes"), 0) for n, count in trials: for _ in range(count): - inst = instance(rng, n) + inst = instance(rng, n, pooled=True) sharp, lay = small_sharp(inst), small_layered(inst) need(sharp <= lay, "oracle: sharp support inside layered") - checked["strict_gap"] += sharp < lay + c["strict_gap"] += sharp < lay # Direct X->Y adds are seeded identically by both tests; omit # them so every coefficient is carried by helper paths. got = run_program(rng, inst, steps, direct=False) - need(got <= sharp, "oracle: legal coefficient outside sharp test") - checked["programs"] += 1 - checked["nonzero_coefficients"] += len(got) - checked["helper_mediated"] += sum( - not set(inst[1][s]) & set(inst[2][t]) for t, s in got) - escapes = {"yread": y_relay_counterexample()} + cross = run_program.cross_type + path, ntypes = directed_program(rng, inst, 1 + rng.below(3)) + need(got | path <= sharp, "oracle: legal coefficient outside " + "the one-helper test") + c["programs"] += 2 + c["nonzero_coefficients"] += len(got) + len(path) + c["helper_mediated"] += sum(not set(inst[1][s]) & set( + inst[2][t]) for t, s in got | path) + c["cross_type_relayed"] += len(cross) + c["directed_multi_type"] += len(path) if ntypes > 1 else 0 + inst = instance(rng, n, nt=6, rigid=True) + got = run_program(rng, inst, steps, direct=False) + path, ntypes = directed_program(rng, inst, 1 + rng.below(3)) + need(got | path <= small_layered(inst), + "oracle: legal coefficient outside the layered test") + c["unpooled_programs"] += 2 + c["unpooled_coefficients"] += len(got) + len(path) + c["unpooled_multi_type"] += len(path) if ntypes > 1 else 0 + c["unpooled_single_type_escapes"] += len( + (got | path) - small_sharp(inst)) + escapes = {"yread": y_relay_counterexample(), + "unpooled": unpooled_relay_example()} for bad in ("descent", "crossframe", "offcover", "oldstate"): found = None for attempt in range(1, 4001): - inst = instance(rng, 3 + attempt % 2, rigid=True) + inst = instance(rng, 3 + attempt % 2, pooled=True) got = run_program(rng, inst, steps, bad) if not got <= small_sharp(inst): found = (attempt, not got <= small_layered(inst)) break need(found is not None, "negative control has no teeth: " + bad) escapes[bad] = found - return checked, escapes + return c, escapes PR3427_SOURCE_MASKS = ( # published per-source target masks, sources 0..3 @@ -899,14 +1098,18 @@ def main(): "negative_controls": escapes}, sort_keys=True)) print("PASS_P104_FIXED_COVER_CUT_REVIEW layered_missing=1 " "sharp_missing=2682 of 4992 pr3427_masks=4 rank_U_minus_I>=17 " - "rows=4 oracle_programs=%d no_kappa" % checked["programs"]) - - -ORACLE_EXPECTED = {"programs": 4500, "nonzero_coefficients": 269, - "strict_gap": 3556, "helper_mediated": 107} -ESCAPES_EXPECTED = {"yread": (1, True), "descent": (1, True), - "crossframe": (7, True), "offcover": (184, True), - "oldstate": (144, True)} + "rows=4 oracle_programs=%d no_kappa" % ( + checked["programs"] + checked["unpooled_programs"])) + + +ORACLE_EXPECTED = { + "programs": 9000, "nonzero_coefficients": 1043, "helper_mediated": 604, + "cross_type_relayed": 13, "directed_multi_type": 620, "strict_gap": 54, + "unpooled_programs": 9000, "unpooled_coefficients": 1887, + "unpooled_multi_type": 1112, "unpooled_single_type_escapes": 0} +ESCAPES_EXPECTED = {"yread": (1, True), "unpooled": True, "descent": (1, True), + "crossframe": (6, True), "offcover": (131, True), + "oldstate": (159, True)} if __name__ == "__main__": main() From d5057e7ba2a5d55ec0490da1e94baa460d4662b4 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Mon, 19 Oct 2026 00:20:18 +0530 Subject: [PATCH 5/9] State the lemma's second-method evidence in the review Co-Authored-By: Claude Opus 5.5 --- research/p104-fixed-cover-cut-review/PROOF-REVIEW.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md b/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md index 11ffec81f0..51e27182a8 100644 --- a/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md +++ b/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md @@ -142,6 +142,16 @@ conclusion can fail. The verifier's `F_2^4` example relays across two rigid types at a shared plane. It lies in PR3259's test but outside the one-helper test. +*Second methods.* Two checks support the lemma beyond the written proof. + +- **Small domains.** The oracle runs 9,000 checked programs on pooled + `F_2^3`/`F_2^4` instances with exact `Fraction` coefficients. It finds + 1,043 nonzero helper-path coefficients, 633 of them relayed across + different helper types. Every one lies in the one-helper test. +- **P104.** A new implementation of PR3252's multi-hop full-memory + recurrence, which does not assume the lemma, gives the same support on all + 10,816 pairs. + *Converse (untimed).* If the condition holds, one helper of type `(a,b)` with that full flag reads `X_s` at V and writes `Y_t` at W. With chronology relaxed, the criterion is therefore exact. No sound untimed support test under K1-K7 can From dd28b5cc53840808a82d53338b2fe6bbcb8d881a Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Mon, 19 Oct 2026 00:21:03 +0530 Subject: [PATCH 6/9] Acknowledge PR3259's own non-realization caveat in the verdict Co-Authored-By: Claude Opus 5.5 --- research/p104-fixed-cover-cut-review/PROOF-REVIEW.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md b/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md index 51e27182a8..087a946b5d 100644 --- a/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md +++ b/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md @@ -29,7 +29,9 @@ proves no P104 impossibility outside the stated contract. unsupported**, with at least one in every row and every column. PR3259's relaxation grants 10,815 source/target pairs, against 2,310 for the sharp criterion. "Exactly one missing coefficient" describes PR3259's test, not the - contract. + contract. PR3259 itself says that passing its test is not a realization. + What is new here is that the same contract excludes 2,681 of the entries + that pass. 3. Consequently the fixed-cover contract is closed by a much larger obstruction than one coefficient. A contract change that only reopens `C[71,102]` does not complete the correction. Examples are PR3427's rank-one source shear, a From 4c7979e8824f93e9e13287c154d8c2ef57638992 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Mon, 19 Oct 2026 01:26:50 +0530 Subject: [PATCH 7/9] Address round-1 review of the P104 fixed-cover cut review - R1 now states that it keeps each target's write-before-read order (the per-path order every program obeys) and adds R1u, which drops that order and reopens all 2,682 entries; the arrival histogram explains why R1 is 0. - Channel rows use an exact Fraction run of the channel word: every Y increment equals G/2 in the sorted port order with dirt cancelled, every add is at equal frames; R1c/R3 use actual coefficients. - Small-domain oracle: exhaustive untimed reachability on all 9,000 instances (pooled: equals the one-helper test; unpooled: 33 escapes on 26 instances), every reachable helper pair realized as a checked program. - Fix the fixed F_2^4 unpooled example (its second type was not a flag); run it and the Y-read example through the checked interpreter. - Assert the derived counts (sign split, 2,681, 8,506, zero/diagonal pairs), the support shape (2,309 own port pairs + (73,83)) and that containment is not decisive at P104. - Docs: K1 is the pooled relaxation; frozen X/Y paths in K4/K5; lemma compatibility argument made explicit; merged-helper justification for PR3252; scoped "among the rows computed" reading; concurrent same-card PRs and the jwr404 series credited; AI-review provenance stated. Co-Authored-By: Claude Opus 5.5 --- .../PROOF-REVIEW.md | 199 ++++++--- .../p104-fixed-cover-cut-review/README.md | 291 ++++++++----- .../p104-fixed-cover-cut-review/TASK.json | 14 +- .../p104-fixed-cover-cut-review/VERIFY.json | 4 +- .../test_verify.py | 27 +- .../p104-fixed-cover-cut-review/verify.py | 402 +++++++++++++----- 6 files changed, 670 insertions(+), 267 deletions(-) diff --git a/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md b/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md index 087a946b5d..a15541473d 100644 --- a/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md +++ b/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md @@ -6,9 +6,9 @@ Objects, at their exact heads: `research/p104-pooled-cut-independent/README.md`, sections "Contract and conclusion" and "Why one contact per dimension is a necessary relaxation" (README lines 17-100). -- PR3252 (petalas, `4784b71d2e0833537c9ae1e8be05ad2a6b334d92`), +- PR3252 (Nick Petalas, `4784b71d2e0833537c9ae1e8be05ad2a6b334d92`), `research/p104-memory-relaxation-soundness/PROOF.md`. -- PR3427 (jmbarrancoml, `344774ba08a73fc3a85fdcb93fb319927bde3ea2`), +- PR3427 (Jose Manuel, jmbarrancoml, `344774ba08a73fc3a85fdcb93fb319927bde3ea2`), `research/p104-source-preconditioning/PROOF.md`, "Pooled path-compression lemma". Only what it consumes is reviewed. @@ -17,6 +17,10 @@ proves no P104 impossibility outside the stated contract. ## Verdict +These verdicts come from an author-checked, AI-assisted review. Four AI review +passes in the same loop checked the first version; no independent human or +formal-kernel review has been done. + 1. **PR3259's argument is valid as a necessary support test under its stated contract.** Each step below is valid as written. Two steps need a sentence that is implicit in the contract, recorded as clarifications rather than @@ -46,9 +50,13 @@ proves no P104 impossibility outside the stated contract. ## Contract, as used PR3259 states the contract in prose. It is numbered here so that each step can -cite it: +cite it. PR3259 first fixes a matching, one arrival per departure, and then +grants one virtual helper for every compatible pair at once. K1 is that pooled +relaxation. Every matching-based program satisfies it, so each exclusion below +holds a fortiori for every single matching. The exactness statement (the +converse below) is made for the pooled relaxation only. -- **K1 fixed cover.** Every added helper has one full flag through +- **K1 fixed cover, pooled.** Every added helper has one full flag through `0 < L[a//2] < A[a] < F3 < ... < F6 < B[b] < H[b//2] < FULL` for a compatible pair, `A[a] <= B[b]`. Skipped dimensions are granted, but the flag still passes through `L, A, B, H`. @@ -56,10 +64,10 @@ cite it: dimension. It is never reloaded or reused with another flag. - **K3 equal frames.** A scalar operation transfers dependence only between registers whose current frames are equal. A transport is register-local. -- **K4 immutable X.** Sources are never written. They are read only at their - frozen channel frame path. -- **K5 unread Y.** Targets are never read. They receive additive increments - only. +- **K4 immutable X.** Sources keep their original channel frame path and are + never written. They are read only at frames of that path. +- **K5 unread Y.** Targets keep their original channel frame path and are + never read. They receive additive increments only. - **K6 no other source-dependent state.** The correction neither reads nor writes original channel helpers (G, D, Q, C) or other correlated storage. The channel contributes its unchanged `G/2`. @@ -109,26 +117,39 @@ is a helper. By K6 none is a channel register. By K3 scalar steps keep the frame and transports enlarge it. So the frames along the path form a chain, and `V <= W`. If `V = W` the pair shares a frame. Otherwise `1 <= dim V < dim W <= 8`. -*Choice of departure a.* +*Choice of departure a.* Let P be the first path frame of dimension at +least 2. -- If `dim V >= 2`, let a be the departure of the reading helper. Its flag - passes `A[a]` at dimension 2 and V at `dim V`, so `A[a] <= V`. +- If `dim V >= 2`, then P = V. Let a be the departure of the reading helper. + Its flag passes `A[a]` at dimension 2 and V at `dim V`, so `A[a] <= V`. - If `dim V = 1`, the run at dimension 1 shares frame V (step f). Let h' be the - helper that carries the path out of dimension 1, and a its departure. Its - dimension-1 frame is V, so `L[a//2] = V`. Its flag gives `A[a] <=` its next - frame on the path, which is `<= W`. + helper that carries the path out of dimension 1, from V to P, and a its + departure. Its dimension-1 frame is V, so `L[a//2] = V`. Its flag passes + `A[a]` and P, so `A[a] <= P`. -*Choice of arrival b.* +*Choice of arrival b.* Let Q be the last path frame of dimension at most 7. -- If `dim W <= 7`, let b be the arrival of the writing helper. Then - `W <= B[b]`. +- If `dim W <= 7`, then Q = W. Let b be the arrival of the writing helper. + Then `W <= B[b]`. - If `dim W = 8`, let h'' be the helper that carries the path into dimension 8, - and b its arrival. Then `H[b//2] = W`, and its frame before the ascent lies - in `B[b]`. That frame also contains every earlier path frame, including - `A[a]`. If h' = h'', then `A[a] <= B[b]` holds because both lie on one flag. + from Q to W, and b its arrival. Then `H[b//2] = W`. Its flag passes Q and + `B[b]`, so `Q <= B[b]`. + +*Compatibility.* If h' = h'' (the path leaves dimension 1 and enters +dimension 8 in one transport), `A[a]` and `B[b]` lie on one flag, so +`A[a] <= B[b]`, and V, W lie on that flag too. Otherwise P comes no later than +Q along the path. This is immediate unless `dim V = 1` and `dim W = 8`. In that +case the step out of dimension 1 and the step into dimension 8 are different +steps, and the first precedes the second because frames along the path never +shrink. So P <= Q, and + +``` +A[a] <= P <= Q <= B[b], V <= P, Q <= W. +``` -In every case `A[a] <= B[b]`, so `(a,b)` is in the pool. The spaces -`L[a//2] < A[a]`, V, W and `B[b] < H[b//2]` form a nested partial flag: +In every case `A[a] <= B[b]`, so `(a,b)` is in the pool, and also +`V <= B[b]` and `A[a] <= W`. The spaces `L[a//2] <= A[a]`, V, W and +`B[b] <= H[b//2]` therefore form a nested partial flag: - for `dim V = 1`, `V = L[a//2]`; - for `dim V = 2`, `V = A[a]`; @@ -140,24 +161,36 @@ admits both V and W. ∎ The proof uses the fact that the pool contains *every* compatible pair, so that the recombined type exists. For a type list without that closure the -conclusion can fail. The verifier's `F_2^4` example relays across two rigid -types at a shared plane. It lies in PR3259's test but outside the one-helper -test. +conclusion can fail. The verifier's fixed `F_2^4` example relays across two +rigid types at a shared plane. It lies in PR3259's test but outside the +one-helper test, and the exhaustive small-domain search below finds 33 more +such pairs. *Second methods.* Two checks support the lemma beyond the written proof. -- **Small domains.** The oracle runs 9,000 checked programs on pooled - `F_2^3`/`F_2^4` instances with exact `Fraction` coefficients. It finds - 1,043 nonzero helper-path coefficients, 633 of them relayed across - different helper types. Every one lies in the one-helper test. +- **Small domains.** On 4,500 seeded pooled `F_2^3`/`F_2^4` instances, an + exhaustive untimed reachability that does not assume the lemma gives + exactly the one-helper support every time. Each of its 4,264 helper-only + pairs is realized by an explicit program in the checked interpreter, with + exact `Fraction` coefficients. The instances include 54 (75 pairs) where + PR3259's test is strictly looser, the only places where the lemma's extra + precision can be tested. On 4,500 unpooled instances the same search finds + 33 pairs on 26 instances outside the one-helper test, each realized by a + legal program, so the check has teeth. The 9,000 random pooled programs + (1,043 nonzero coefficients counted per program, 604 of them on pairs whose + X and Y chains share no frame) are a soundness sample only; on unpooled + instances they found none of the 33 escapes. - **P104.** A new implementation of PR3252's multi-hop full-memory recurrence, which does not assume the lemma, gives the same support on all 10,816 pairs. *Converse (untimed).* If the condition holds, one helper of type `(a,b)` with -that full flag reads `X_s` at V and writes `Y_t` at W. With chronology relaxed, -the criterion is therefore exact. No sound untimed support test under K1-K7 can -exclude more pairs. Timed tests can. +that full flag reads `X_s` at V and writes `Y_t` at W. With the relative timing +of different registers relaxed, the criterion is therefore exact for the pooled +contract. No sound untimed support test under K1-K7 can exclude more pairs. +Timed tests can. A single fixed matching has fewer helper types, so its support +can only be smaller and at least 2,682 entries stay unsupported; exactness is +not claimed there. *Where PR3259 loses precision.* At layer d PR3259 lets helper w relay through any d-flat that w shares with a neighbour. It does not require that flat to @@ -178,17 +211,25 @@ delivers a nonzero coefficient outside both PR3259's test and the sharp test. | Supported source/target pairs | 10,815 | 2,310 | | Required entries unsupported | 1 (`(71,102)`) | 2,682 (every row and column) | | Values of unsupported entries | `-1/2` | 1,801 at `-1/2`, 881 at `+1/2` | - -The sharp criterion is computed in three ways: - -- reduced-echelon keys with helper-type masks; -- point-set bitmaps looped by helper type; -- an independent multi-hop implementation of PR3252's full-memory recurrence - over the whole pool. - -All three agree on all 10,816 pairs. For sources 0-3 the per-source target -masks equal PR3427's published masks exactly. Those masks come from PR3427's -direct criterion and from PR3252's full-memory operations. +| Pairs granted with `C = 0` | 5,720 off-diagonal and 104 diagonal | none | + +The sharp support is computed three times: the one-helper criterion in two +loop orders (reduced-echelon keys with helper-type masks, and point-set +bitmaps looped by helper type), and an independent multi-hop implementation of +PR3252's full-memory recurrence over the whole pool. All three agree on all +10,816 pairs. + +The sharp support has a simple shape. It is exactly the 2,309 compatible slot +pairs `(a,b)` read as port pairs (target `b//2`, source `a//2`), which are +distinct and all required, plus the pair `(73,83)`. That extra pair comes from +a dimension-4 frame of X83 admitted, with Y73's cap, by one pool type. Hence +`2,682 = 4,992 - 2,309 - 1`. At P104 no X path shares a frame with a Y path, +and dropping the containment `V <= W` changes no pair, so containment is never +decisive here. The verifier asserts each of these facts. + +For sources 0-3 the per-source target masks equal PR3427's published masks +exactly. Those masks come from PR3427's direct criterion and from PR3252's +full-memory operations. ## PR3252 PROOF.md (shorter review) @@ -207,6 +248,13 @@ PR3259's K1-K7 written with per-helper bounds `L(h,d) <= F(h,d) <= U(h,d)`. contains S. Carries keep `S <= F`. - *Pruning.* Valid, because the guards are monotone under shrinking a memory. +The review applies the theorem to one merged helper per pool type. That is +justified: actual helpers of one type have identical bounds, contacts and +granted reads, so the outputs of any multiset of them are contained in the +one-helper-per-type run, whose memory set is the union. A relay from such a +helper to itself only produces a memory `T >= S`, which the monotone guards +make redundant. + The full-memory mode keeps a lower bound on the frame the signal used. Like any sound untimed test under this contract, it cannot be stricter than the sharp criterion, which is exact. A new implementation over the whole 2,309-type pool @@ -248,8 +296,10 @@ rank(U - I) = rank(V - I) >= rank C[R,S], using `V - I = -V(U - I)` for the equality. -A deterministic greedy finds a rectangle: for each seed column, add the -column that most increases `min(|R|,|S|)`, with ties to the smallest index. +A deterministic greedy finds a rectangle. For each seed column it repeatedly +adds the column that maximizes `min(|R'|, |S|+1)`, then `|R'|`, with ties to +the smallest index, where `R'` is the set of rows still unsupported. It stops +when `min(|R|,|S|)` stops growing and keeps the rectangle of largest rank. It finds a 19-by-18 rectangle of unsupported pairs with `rank C[R,S] = 17`. Exact `Fraction` elimination gives the rank. A 17-by-17 minor has integer `det(8C) = 2^43`, by Bareiss elimination, so @@ -262,31 +312,58 @@ completion may force more. ## Load-bearing hypotheses (support level, sharp criterion) The rows are support-level necessary-test relaxations. They are unpriced and -give no coefficient, dirty restoration or chronology. Each row relaxes one item. +give no coefficient or dirty restoration. Each row relaxes one item. Like the +sharp criterion, they relax the relative timing of different registers but +keep the order of operations along one dependency path. | Relaxed item | Reaches `(71,102)` | Sharp-missing entries reopened | Minimal witness (operations counted, unpriced) | |---|---|---:|---| | none (sharp baseline) | no | 0 of 2,682 | - | | PR3259's dropped cross-layer nesting (a proof relaxation, not a contract change) | no | 2,681 | layered test | -| K5, correction-only Y relay (R1) | no | 0 | none at P104; F_2^3 escape uses 4 scalar operations | +| K5, correction-only Y relay, keeping each target's write-before-read order (R1) | no | 0 | none at P104; F_2^3 escape uses 4 scalar operations | +| R1 without that order (R1u; a looser test, since no program reads content before it is written) | yes | 2,682 | - | | K5 with the channel's own Y content readable, including target feedback (R1c) | yes | 2,682 | feedback on `Y71`: read it at its dimension-5 snapshot, after the channel has deposited its X102 term, and add a multiple back (1 read and 1 write, or 1 self-add) | -| K1, free nested flags: helpers not forced through `L/A/B/H` (R2) | yes | 2,682 | one helper, flag through `L_102 <= H_71`; 1 read, >= 1 transport, 1 write | +| K1, free nested flags: helpers not tied to `L/A/B/H` (R2) | yes | 2,682 | one helper with a free flag from X102's dimension-1 frame to Y71's dimension-8 frame; 1 read, >= 1 transport, 1 write | | K6, reads of old channel-helper state (R3) | yes | 2,682 | one equal-frame add from `D11` into `Y71` at their shared dimension-5 frame | -R1c and R3 use structural, no-cancellation dependence of the channel registers. -Their witnesses are therefore support paths only. Both reopen every entry for -the same reason: the channel already delivers the support of `G/2`, which -contains every off-diagonal required entry. Any access to the channel's -source-dependent state exposes that support. The access can come through its -helpers or by reading a target after the channel has written it. Scaling -that state is not a correction; its coefficients, dirt and cost are unknown. +*R1 and the target's own order.* In R1, content written into `Y_u` at one of +its frames can be read only at that frame or a later one. Every program obeys +this, because `Y_u`'s frames ascend in time; it is the path order that makes +path frames nested, applied at a target used as a relay. Correction content +reaches targets at their final caps (2,310 arrivals, one for each supported +pair) and at 55 frames of dimension 5 or 6 (31 and 24). Content at a cap can +be read only at that cap, which feeds only itself because the 104 caps are +distinct. The 55 lower arrivals relay nothing new. So R1 reopens nothing. R1u +drops the order, lets cap content be read at the target's low frames, and +reopens everything. R1's zero therefore rests on that order. + +*R1c and R3.* Both use the channel's actual coefficients, recorded per register +and frame from an exact `Fraction` run of the 4,058 channel events. The same +run checks that every Y increment equals `G/2` exactly in the sorted port +order, with all helper dirt cancelled, and that every channel add is at equal +frames. The channel first puts `X102` into `Y71` at event 3378, with +coefficient `1/2`, from `D11` at dimension 5; the R1c and R3 witnesses read +that state. Both rows reopen every entry for the same reason: the channel +already delivers the support of `G/2`, which contains every off-diagonal +required entry. Any access to the channel's source-dependent state exposes +that support, through its helpers or by reading a target after the channel has +written it. Scaling that state is not a correction; its coefficients, dirt and +cost are unknown. + Known rows are cited, not recomputed: - PR3013: component/containment pooling reaches all 4,992 entries. - PR3427: a one-H2 source shear removes the `(71,102)` requirement, but - `D[3,2]` stays unsupported. A source preconditioner needs `rank(U-I) >= 4`. - -Reading: the obstruction rests on the fixed cover (K1) and on the exclusion of -the channel's source-dependent state (K6, including its exposure through Y). -Unread-Y matters in this instance only through that exposure. At P104, -correction-only Y relay reopens nothing. + `D[3,2]` stays unsupported. A source preconditioner needs `rank(U-I) >= 4` + (17 by the section above). + +Reading. Among the rows computed here, two hypotheses each reopen every entry: +the fixed cover (K1) and the exclusion of the channel's source-dependent state +(K6, including its exposure through Y). Unread Y matters at P104 only through +that exposure, given each target's write-before-read order. The rows are not a +complete map. Not computed at P104: frame descent (K2), cross-frame mixing +(K3), changed source or target frame paths and source mutation (K4, K5), +dependent dirt (K7) and extra correlated storage. The small-domain negative +controls show that descent, cross-frame mixing, off-cover flags and correlated +old state can each escape both tests. A reopening must change at least one of +K1-K7, or add storage, and must cover all 2,682 entries with a full bill. diff --git a/research/p104-fixed-cover-cut-review/README.md b/research/p104-fixed-cover-cut-review/README.md index 1d177a16d4..2a12f12936 100644 --- a/research/p104-fixed-cover-cut-review/README.md +++ b/research/p104-fixed-cover-cut-review/README.md @@ -1,27 +1,37 @@ # P104 fixed-cover support cut: hypothesis review and a sharper criterion **Statement.** PR3259's path-embedding argument is a **valid** necessary support -test under its stated fixed-cover contract. That contract is closed, by a much -larger obstruction than one coefficient. The test discards one fact true of every -legal dependency path: its frames are nested across dimensions. Keeping that -fact gives a valid criterion, **one recombined helper per path**. This lemma is -stated in PR3427 and re-proved here in every dimension case. It is exact for -untimed support. Under it, **2,682 of the 4,992 required entries of +test under its fixed-cover contract, taken in its pooled form (K1-K7 in +[PROOF-REVIEW.md](PROOF-REVIEW.md)). That contract is closed by a much larger +obstruction than one coefficient: **2,682 of the 4,992 required entries of `C = I - G/2` are unsupported**, with at least one in every row and every -column. PR3252's full-memory recurrence is a separate sound test, reviewed -valid here. A new implementation of it over the whole pool gives exactly the -same support, 2,310 pairs, on all 104 columns. PR3259's single missing entry, -`C[71,102] = -1/2`, is a property of its looser relaxation. - -PR3427 states the lemma, but it has not been evaluated beyond PR3427's four -source columns. Applied to all 104 columns, it raises PR3427's -source-preconditioner bound from `rank(U-I) >= 4` to **`rank(U-I) >= 17`**, -under PR3427's own contract. - -This is an audit: a scoped proof review, a finite certificate and small-domain -controls. It constructs nothing and is not a complete multiplication theorem. -It proves no P104 impossibility outside the stated contract, and κ and the -selected frontier are unchanged. +column. + +The 2,682 count rests on two sound tests that agree on all 10,816 +source/target pairs: + +- PR3427's one-recombined-helper lemma, re-proved here in every dimension + case. It keeps the fact that PR3259's test discards: the frames along a + dependency path are nested. +- PR3252's full-memory recurrence, whose proof is reviewed valid here, + implemented anew over the whole pool. It is multi-hop and does not assume + the lemma. + +For the pooled untimed relaxation the lemma is exact: no sound untimed test +can exclude more pairs. The supported pairs have a simple form. They are the +2,309 compatible slot pairs read as port pairs, plus one extra pair, so +`2,682 = 4,992 - 2,309 - 1`. PR3259's single missing entry, +`C[71,102] = -1/2`, belongs to its looser relaxation. Applied to all 104 +columns, PR3427's source-preconditioner bound rises from `rank(U-I) >= 4` to +**`rank(U-I) >= 17`** under PR3427's own contract. + +This is an author-checked, AI-assisted audit: a scoped proof review, a finite +certificate and small-domain checks. Four AI review passes in the same loop +(reproducibility, mathematics, provenance, referee) checked the first +version, and this revision addresses their findings. No independent human or +formal-kernel review has been done. The audit constructs nothing and is not a +complete multiplication theorem. It proves no P104 impossibility outside the +stated contract, and κ and the selected frontier are unchanged. ## Results @@ -30,70 +40,137 @@ selected frontier are unchanged. | PR3259 embedding argument, checklist a-h | Valid. Two implicit sentences are recorded as clarifications. See [PROOF-REVIEW.md](PROOF-REVIEW.md). | | PR3252 PROOF.md (memory relaxation) | Valid for its recurrence and contract. | | What PR3427 consumes | Its own one-helper lemma and PR3252's full-memory operations, not PR3259's recurrence. Both are justified. | +| Channel word, exact run | Every Y increment is exactly `G/2` in the sorted port order, with all helper dirt cancelled; every channel add is at equal frames. | | Control: PR3259 layered test, rebuilt | Missing set `{(71,102)}`. Forward counts `16,25,52,365,1725,2283,2285,2297`. Backward cone 37, disjoint. | -| Sharp criterion: two loop orders, plus PR3252's full-memory recurrence as a third method | 2,682 required entries unsupported: 1,801 at `-1/2` and 881 at `+1/2`. 2,310 supported pairs, against 10,815 for PR3259's test. All three methods agree on every pair. | +| Sharp criterion: one criterion in two loop orders, plus PR3252's multi-hop recurrence | All three computations agree on every pair. 2,310 supported pairs, against 10,815 for PR3259's test. 2,682 required entries unsupported: 1,801 at `-1/2` and 881 at `+1/2`. 8,506 pairs unsupported in all. | +| Shape of the sharp support | Exactly the 2,309 compatible slot pairs `(a,b)` read as (target `b//2`, source `a//2`), all distinct and all required, plus `(73,83)`. All supported pairs are off-diagonal required entries. PR3259's test grants 2,681 of the 2,682 missing entries, all 5,720 zero off-diagonal pairs and all 104 diagonal pairs. | | Cross-check with PR3427 | The four published per-source masks (sources 0-3) are reproduced exactly. | | Consequence for PR3427 | A 19-by-18 rectangle of unsupported pairs has `rank C[R,S] = 17`, giving `rank(U-I) >= 17`. A 17-by-17 minor has `det(8C) = 2^43`. | -| Oracle, coefficient level | 18,000 seeded legal programs over `F_2^3` and `F_2^4`, with exact `Fraction` coefficients. On pooled (P104-like) instances there are 9,000 programs and 1,043 nonzero helper-path coefficients, 633 of them relayed across helper types; none lies outside the one-helper test. On unpooled instances there are 9,000 programs and 1,887 coefficients; none lies outside PR3259's test. | +| Small domains, pooled | 4,500 seeded `F_2^3`/`F_2^4` instances. On every one, an exhaustive untimed reachability, which does not assume the lemma, equals the one-helper test. Its 4,264 helper-only pairs are each realized by an explicit program in the checked interpreter. PR3259's test is strictly looser on 54 instances (75 pairs), and the exhaustive search confirms those pairs unreachable. | +| Small domains, unpooled | 4,500 instances with six rigid types. The exhaustive support lies inside PR3259's test every time, and 8,978 helper-only pairs are realized. 33 pairs on 26 instances lie outside the one-helper test, each realized by a legal program: the lemma needs pooling. | +| Random programs | 18,000 seeded checked programs with exact `Fraction` coefficients, two per instance; all lie inside the exhaustive support. Pooled: 1,043 nonzero coefficients counted per program, 604 of them on pairs whose X and Y chains share no frame, and 633 (13 + 620) passed between helpers of different types. Unpooled: 1,887 coefficients. The random programs found none of the 33 unpooled escapes, so they are a soundness sample, not the evidence for the lemma. | ### Which hypotheses carry the obstruction Each row relaxes one hypothesis and is checked at support level with the sharp -criterion. The rows are unpriced and give no coefficient, chronology or dirty -restoration. +criterion. The rows are unpriced and give no coefficient or dirty restoration. | Relaxed hypothesis | Reaches `(71,102)` | Reopens, of 2,682 | |---|---|---:| | Cross-layer nesting, as PR3259's proof drops it (a proof relaxation, not a contract change) | no | 2,681 | -| Unread Y, correction-only relay (R1) | no | 0 | -| Unread Y, with the channel's own Y content readable (R1c) | yes, by feedback on Y71 at dimension 5 | 2,682 | -| Fixed cover: helpers not forced through `L/A/B/H` (R2) | yes, one helper through `L_102 <= H_71` | 2,682 | -| No reads of old channel-helper state (R3) | yes, one equal-frame add from `D11` at dimension 5 | 2,682 | - -Among the rows computed here, two hypotheses each reopen every entry. One is -the fixed cover. The other excludes the channel's source-dependent state, -whether held in its helpers or exposed by reading targets after the channel -has written them. That state already carries the support of `G/2`, which -contains every off-diagonal requirement. At P104, -correction-only Y relay reopens nothing, although an `F_2^3` program shows it -can matter in principle. Frame descent and cross-frame mixing also break the -argument; the small-domain negative controls show this. They are not priced or -counted at P104 here. Cited, not recomputed: +| K5, correction-only Y relay, keeping each target's write-before-read order (R1) | no | 0 | +| R1 without that order (R1u; a looser test, since no program reads content before it is written) | yes | 2,682 | +| K5, the channel's own Y content readable, including target feedback (R1c) | yes, by feedback on Y71 at dimension 5 | 2,682 | +| K1, free nested flags: helpers not tied to `L/A/B/H` (R2) | yes, one free flag from X102's dimension-1 frame to Y71's dimension-8 frame | 2,682 | +| K6, reads of old channel-helper state (R3) | yes, one equal-frame add from `D11` at dimension 5 | 2,682 | + +The sharp criterion and the rows relax the relative timing of different +registers but keep the order of operations along one dependency path; that +order is what makes path frames nested. R1 applies it at a target used as a +relay. Content written into `Y_u` at one of its frames can be read only at +that frame or a later one, because `Y_u`'s frames ascend in time. Every program obeys this. With it, +correction content reaches targets at their final caps (2,310 arrivals) and at +55 frames of dimension 5 or 6 (31 and 24). A cap can feed only itself, since +the 104 caps are distinct, and the 55 lower arrivals relay nothing new, so R1 +reopens nothing. R1u drops the order and reopens everything. R1's zero rests +on that order. + +R1c and R3 use the channel's actual coefficients, recorded from the exact run +of its 4,058 events. The channel first puts `X102` into `Y71` at event 3378, +with coefficient `1/2`, from `D11` at dimension 5; both channel witnesses use +that state. R1c and R3 reopen everything because the channel's state already +carries the support of `G/2`, which contains every off-diagonal required +entry. Reading that state is not a correction: its coefficients, restoration +and cost are unknown. + +Among the rows computed here, two hypotheses each reopen every entry: the +fixed cover (K1) and the exclusion of the channel's source-dependent state +(K6, with its exposure through Y). The rows are not a complete map. Not +computed at P104: frame descent (K2), cross-frame mixing (K3), changed source +or target frame paths and source mutation (K4, K5), dependent dirt (K7) and +extra correlated storage. The small-domain controls show that descent, +cross-frame mixing, off-cover flags and correlated old state can each escape +both tests. Under PR3427's preconditioner contract, which relaxes K4, a source +preconditioner needs `rank(U-I) >= 17`. Any reopening must change at least one +of K1-K7, or add storage, and must cover all 2,682 entries with a full bill. + +The 2,682 count binds only corrections that keep the fixed cover, the frozen X +and Y frame paths and the untouched channel state. Routes that change any of +these, including the channel-state and present-head work listed below, must be +judged at coefficient and restoration level. + +Cited, not recomputed: - PR3013: component/containment pooling reaches all 4,992 entries. - PR3427: a one-H2 source shear removes only the `(71,102)` requirement. +### Concurrent pending work on the same card + +These open PRs are not reviewed here. The corrections they construct or bound +change something K1-K7 freeze, so they lie outside this contract and do not +conflict with its closure. + +- Wentao Li (VictorLiwentao) prices single-entry and whole-row `I - G/2` + corrections on the published word: #3601 (`26394881f0a183ca0df3d986ec58aa56900ada6c`), + #3610 (`4352496b3aa56ad17446ddbd1d78931f3d392996`) and #3618 + (`0c4b73507ba7ed7b992e47b17f2cbcb6e362466b`). Their words lift a target's + frame (changes the frozen Y path, outside K5), detour a source (changes the + frozen X path, outside K4), add a private-copy lifetime (extra storage, + outside K6) or build on a repaired channel update (outside K6). #3618's + T48 corrects all 48 entries of row 23 on one target lift for +2 rank mass. + #3532 (`8fecbf7df7b48c9004bd10a0da6a81f33d455737`) repairs a channel + update, which changes the channel (outside K6). #3614 + (`a6c3ae20abe0a15d781ee952e717d489552c9c66`) and #3621 + (`b37f6aef686c940a7613db3e04c6234e472399cf`) give non-private +2 lower + bounds for present-head entries in those correction classes. #3669 + (`84288150fcaa8e3fecb128ef1feeb8ac1c63ccc6`) audits flag 0's + dirty-restoration chronology on the published word. +- Clear Insight (Clear1nsight), #3609 + (`13f974dae4af66027afb01f3ab42df9e830c2e90`), completes the omitted P104 + section at the word's entrance with sources moved and Y temporarily + writable (outside K4 and K5). +- James Reed (jwr404), #3580 (`c867e61e2ea790738474025b6200bf8475e56957`), + indexes the #3259 replay for the + [live support map](../../docs/research/p104-live-support-map.md). + ## Reproduce -From the repository root, with the standard library (about 2 minutes in all): +From the repository root, with the standard library (about 2.5 minutes in all): ```sh python3 -I -O -Werror -B research/p104-fixed-cover-cut-review/verify.py python3 -I -O -Werror -B research/p104-fixed-cover-cut-review/test_verify.py ``` -The verifier prints one JSON receipt. Its last line is +The verifier prints one JSON receipt with every count quoted above. Its last +line is ``` -PASS_P104_FIXED_COVER_CUT_REVIEW layered_missing=1 sharp_missing=2682 of 4992 pr3427_masks=4 rank_U_minus_I>=17 rows=4 oracle_programs=18000 no_kappa +PASS_P104_FIXED_COVER_CUT_REVIEW layered_missing=1 sharp_missing=2682 of 4992 pr3427_masks=4 rank_U_minus_I>=17 rows=5 oracle_instances=9000 oracle_programs=18000 no_kappa ``` The registered replay is `python3.12 -B scripts/research_package.py --package research/p104-fixed-cover-cut-review`. Every check raises `SystemExit("FAIL: ...")`, so checks stay active under `-O`. -**Negative controls that must fail:** - -- `test_verify.py` rejects a tampered input hash. -- It rejects an unsound "shared snapshot only" test inside the oracle. -- It rejects a wrong rectangle. -- It shows that dropping nesting changes PR3427's masks. -- Inside `verify.py`, five contract violations must each produce a coefficient - outside both tests. They are Y read (a fixed four-operation `F_2^3` program), - frame descent, cross-frame mixing, an off-cover flag and correlated old - state. -- A sixth control, a fixed unpooled two-type relay over `F_2^4`, must lie - outside the one-helper test and inside PR3259's test. +**Negative controls that must fail.** `test_verify.py` checks seven: + +- a tampered input hash is rejected; +- an unsound "shared snapshot only" test is rejected by the oracle; +- an exhaustive search that never switches helper type is rejected, because + it misses the fixed unpooled two-type relay; +- dropping the shared-helper-type requirement changes PR3427's masks; +- dropping containment `V <= W` is unsound on a fixed `F_2^4` instance (at + P104 containment is never decisive, which `verify.py` asserts); +- a wrong rank rectangle is rejected; +- the fixed Y-relay program is a real escape. + +Inside `verify.py`, five contract violations must each produce a coefficient +outside both tests. They are a Y read (a fixed four-operation `F_2^3` program +run in the checked interpreter with only that rule relaxed), frame descent, +cross-frame mixing, an off-cover flag and correlated old state. A sixth +control, a fixed unpooled two-type relay over `F_2^4`, must lie outside the +one-helper test and inside PR3259's test. ## Method and independence @@ -101,36 +178,42 @@ The code shares nothing with PR3182, PR3252, PR3259 or PR3427. Frames are canonical reduced-echelon keys over `F_2^9`. E8 ports are enumerated independently and sorted. +- An exact `Fraction` run of the channel word binds the port order and `C` to + the channel itself, and records the channel's actual coefficients per + register and frame for rows R1c and R3. - The layered control hosts every d-flat of each interval literally, then takes one read-first step per layer. -- The sharp criterion is computed in three ways: - - echelon keys with helper-type masks; - - point-set bitmaps, looped per helper type; - - PR3252's full-memory recurrence (carry, admitted reads, relay of old - memories `S + L(h,d) + L(w,d)`, minimal-memory pruning), rewritten over - all 2,309 types and 104 sources. It is a multi-hop recurrence and does - not assume the one-helper lemma. -- The rank bound uses a deterministic greedy over 104 seed columns. Each - step adds the column that most increases `min(|R|,|S|)`, ties to the - smallest index. Exact `Fraction` elimination gives the rank, and an - independent integer Bareiss determinant confirms it. The greedy is not +- The sharp support is computed three times. Two computations evaluate the + one-helper criterion in different loop orders: echelon keys with + helper-type masks, and point-set bitmaps looped per helper type. The third + is PR3252's full-memory recurrence (carry, admitted reads, relay of old + memories `S + L(h,d) + L(w,d)`, minimal-memory pruning), rewritten over + all 2,309 types and 104 sources. It is multi-hop and does not assume the + lemma. +- The rank bound uses a deterministic greedy. For each seed column it + repeatedly adds the column that maximizes `min(|R'|, |S|+1)`, then `|R'|`, + with ties to the smallest index, where `R'` is the set of rows still + unsupported. It stops when `min(|R|,|S|)` stops growing and keeps the + rectangle of largest rank. Exact `Fraction` elimination gives the rank, and + an independent integer Bareiss determinant confirms it. The greedy is not optimal, so 17 is a lower bound. -- The oracle uses seed `20261018`, with 3,000 instances over `F_2^3` and 1,500 - over `F_2^4` in each family. It is a bounded randomized family, not an - exhaustive enumeration. +- The small-domain oracle draws seeded random instances (seed `20261018`): + 3,000 over `F_2^3` and 1,500 over `F_2^4` in each family. Coverage is these + instances, not every instance. - *Pooled* instances mirror P104. Departure chains fix the low dimensions, - arrival chains fix the high ones, and the types are every compatible pair. - - *Unpooled* instances use six random full flags as types. - - Each instance runs two programs. One chooses uniformly among the - operations legal at each moment, for 120 operations. The other follows a - random path through one to three relays. A checked interpreter executes - both: flags of the right type, ascending transports, and equal-frame - reads, adds and writes. - - Direct X-to-Y adds are omitted, so every coefficient travels through - helpers. - - Random unpooled programs found no escape from the one-helper test. A - fixed `F_2^4` two-type relay shows such an escape exists, so the lemma - needs pooling. PR3259's test does not. + arrival chains fix the high ones, and the types are every compatible + pair. *Unpooled* instances use six random rigid flags as types. + - Each instance gets an exhaustive untimed reachability over frames: a + helper of one type moves up between two nested frames its type admits, + and helpers mix at equal frames. Every reachable helper-only pair is + then turned into an explicit program, one helper per step, and run in + the checked interpreter. + - Each instance also runs two random programs. One chooses uniformly among + the operations legal at each moment, for 120 operations; the other + follows a random path through one to three relays. Direct X-to-Y adds + are omitted from them, so every coefficient travels through helpers. + - The interpreter checks flags of the right type, ascending transports, + and equal-frame reads, adds and writes. - The verifier also checks the roles in the original channel word: X is never written and Y is never read, so K4 and K5 hold for the channel. @@ -140,23 +223,24 @@ Inherited: - PR2981's covers and the native channel frame paths, through their pinned JSON inputs; -- the ordered E8 ports, with the fixture's 16 removed roots; -- the contract K1-K7 in [PROOF-REVIEW.md](PROOF-REVIEW.md). +- the ordered E8 ports with the fixture's 16 removed roots, bound to the + channel by the exact run; +- the contract K1-K7 in [PROOF-REVIEW.md](PROOF-REVIEW.md). K1 is PR3259's + pooled relaxation of its matching contract, so every exclusion here holds a + fortiori for each single matching. -The rows and rank bound apply only under those contracts. R1c and R3 use -structural, no-cancellation dependence of the channel registers. +The rows and the rank bound apply only under those contracts. Open and not addressed here: -- chronology and acquisition order; +- cross-register chronology and acquisition order; - coefficient delivery and dirty restoration; - native lowering, precision and physical hosting; - consumer cost and supplier admission; -- every changed-cover construction; +- every changed-cover or changed-path construction; - a timed refinement of the sharp criterion. -No independent human or formal-kernel review has been done. The selected -cold replay is unchanged and was not rerun. +The selected cold replay is unchanged and was not rerun. ## Open next questions @@ -165,10 +249,16 @@ cold replay is unchanged and was not rerun. further constrain any joint native source preparation under PR3427's contract. A first step is an exact lower bound by larger or overlapping rectangles, or by a min-rank argument. It needs no new matching search. -2. *Can a changed cover reopen all 2,682 entries cheaply?* Relaxing the fixed - cover (R2) reopens every entry at support level. The open question is the - smallest set of off-cover helper flags that covers all 2,682 pairs, with - its full bill. Coefficients, dirt and every cost remain unknown. +2. *Which changed contract reopens all 2,682 entries at least cost?* An entry + is supported when one helper type admits a source frame and a nested + target frame. Under the present cover that happens only through the + entry's own compatible slot pair, apart from `(73,83)`, which goes through + X83's dimension-4 frame. A changed cover must supply such a type for every + missing entry; relaxing the cover (R2) does this at support level. The first priced data + point is pending #3618's T48, which corrects a whole target row on one + target lift for +2 rank mass by changing the target's path rather than + the cover. Coefficients, dirt and every cost of a complete reopening + remain unknown. 3. *Is there a non-trivial use of channel state?* R1c and R3 reopen everything only because the channel already carries `G/2`. One would need a coefficient-level construction that reads channel state and restores it, @@ -176,20 +266,27 @@ cold replay is unchanged and was not rerun. ## Predecessors and credit -- Nick Petalas (GitHub petalas): +- Nick Petalas (petalas): - PR2981 `3d24b92d8ba057b57cb2d480170ec407520e6882` (covers and flags); - PR3252 `4784b71d2e0833537c9ae1e8be05ad2a6b334d92` (memory soundness); - PR3259 `b572b0c25569898579041200e95731c5a43c9189` (pooled cut and embedding argument); - - PR3013 (component pooling). + - PR3013 `504dc9a15f7a874a47564cdf3ae6857bbbc8d000` (component pooling). - dcharb78: PR3182 `ad848966cd62e13de5ad8d4b5169c221d74d2fcd` (the cut and its 1,725/37 cones). - commdata2338: PR3214 `faa6323371db1c5fbb43ab04c6e00715d2328bc6` (output repair). -- jmbarrancoml: PR3427 `344774ba08a73fc3a85fdcb93fb319927bde3ea2` (the - one-helper lemma and the rank-four theorem extended here). -- Wentao Li for the chronology audit (`p104-channel-touch-restoration-audit`), - which is not redone here. +- Jose Manuel (jmbarrancoml): PR3427 `344774ba08a73fc3a85fdcb93fb319927bde3ea2` + (the one-helper lemma and the rank-four theorem extended here). +- James Reed (jwr404): the merged #3497-#3519 series (heads + `a8804afd46ee63b202291ab3bcebd1eb2b83ecfc` through + `d8928dd94a3450c5145a847507e7fb466dbc5c00`) already reproduced the X102 + cone counts 16, 25, 52 and 365 and showed that the literal recurrence + misses the same pair. +- Wentao Li (VictorLiwentao) for the chronology audit + (`p104-channel-touch-restoration-audit`), which is not redone here. +- The [live support map](../../docs/research/p104-live-support-map.md), which + asks for this review before the fixed-cover route is treated as closed. - The native/compiler lineage credited in the pinned inputs: Rohan Arun/1972, Chafik Boukhalfa/1991, Adam Gall/1940, Josie Elliston/1071 and Ali Romman/1125. diff --git a/research/p104-fixed-cover-cut-review/TASK.json b/research/p104-fixed-cover-cut-review/TASK.json index 85d4366ee2..55a4a0b679 100644 --- a/research/p104-fixed-cover-cut-review/TASK.json +++ b/research/p104-fixed-cover-cut-review/TASK.json @@ -68,26 +68,26 @@ ] }, "scope_status": "changed", - "actual_scope": "Independent hypothesis-by-hypothesis review of the PR3259 fixed-cover support-cut embedding argument (and PR3252's memory-relaxation proof, and what PR3427 consumes), with a sharper valid criterion (one recombined helper per path), its finite P104 consequences, three single-relaxation support rows and a small-domain coefficient oracle. Audit only.", + "actual_scope": "Independent hypothesis-by-hypothesis review of the PR3259 fixed-cover support-cut embedding argument (and PR3252's memory-relaxation proof, and what PR3427 consumes), with a sharper valid criterion (one recombined helper per path, exact for the pooled untimed relaxation), its finite P104 consequences, single-relaxation support rows and a small-domain exhaustive check. Audit only; author-checked and AI-assisted.", "scope_change_reason": "The card asks for a chronological correction program. The revision-6 decisions table (row 1) instead asks first for a review of the submitted #3259 support cut and its contract, which decides whether the fixed-cover route is closed and what any reopening must cover. No construction is attempted.", - "bottleneck_link": "Decides whether the fixed-cover, immutable-X, unread-Y, independent-dirt, monotone equal-frame P104 contract is closed and how large its obstruction is (2,682 unsupported required entries, not one), which bounds what a contract change or source preconditioner must reopen before any construction round.", + "bottleneck_link": "Decides whether the pooled fixed-cover, frozen-path, immutable-X, unread-Y, independent-dirt, monotone equal-frame P104 contract is closed and how large its obstruction is (2,682 unsupported required entries, not one), which bounds what a contract change or source preconditioner must reopen before any construction round.", "budget_minutes": 150, "stop_rule": "Stop at a proof-review verdict per step; on an engine disagreement, a proof gap or an oracle escape, stop and minimize. No matching search, no correction construction, no pricing beyond counting witness operations, at most three new relaxation rows, no Lean.", "outcome": "completed", - "evidence": "PROOF-REVIEW.md (step table a-h, lemma proof, PR3252 review, PR3427 consumption, rank consequence); verify.py (layered control reproducing PR3259 numbers; sharp criterion by two loop orders and by an independent PR3252 full-memory recurrence over all 104 columns, all equal; PR3427 four-column masks; rank(U-I)>=17 by Fraction elimination and a Bareiss minor; rows R1/R1c/R2/R3; 18,000-program exact-coefficient oracle (pooled and unpooled families, uniform and path-directed programs, checked interpreter) and six negative controls); test_verify.py (four failing mutations and the Y-relay escape).", + "evidence": "PROOF-REVIEW.md (step table a-h, lemma proof, PR3252 review, PR3427 consumption, rank consequence, load-bearing rows); verify.py (exact channel run: Y increment = G/2; layered control reproducing PR3259 numbers; sharp support by one criterion in two loop orders and by an independent PR3252 full-memory recurrence over all 104 columns, all equal, shape = 2,309 own port pairs + (73,83); PR3427 four-column masks; rank(U-I)>=17 by Fraction elimination and a Bareiss minor; rows R1/R1u/R1c/R2/R3; 9,000 seeded small instances with exhaustive untimed reachability, 13,242 realized checked programs and 18,000 random checked programs, exact Fractions; six negative controls); test_verify.py (seven controls).", "author": "Sagar Thakrar (thakrarsagar)", "ai_assistance": "Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) for analysis, code and writing. No independent human or formal-kernel review is claimed.", "open_questions": [ { "question": "What rank does the full unsupported pattern force on a P104 source preconditioner (U-I)?", - "why_it_matters": "A greedy rectangle already gives rank(U-I)>=17 versus PR3427's 4; a min-rank completion of -C on all 8,506 unsupported pairs may force much more and would further constrain joint native source preparation.", + "why_it_matters": "A greedy rectangle already gives rank(U-I)>=17 versus PR3427's 4; a min-rank completion of -C on all 8,506 unsupported pairs may force more and would further constrain joint native source preparation.", "first_step": "Bound the min-rank completion exactly (larger or overlapping rectangles, or a min-rank argument) with the pinned sharp support; no matching search.", "blocked_by": "Nothing beyond the sharp support certificate here; pricing a joint preparation remains separate." }, { - "question": "What is the smallest set of off-cover helper flags reopening all 2,682 sharp-missing entries, and its full bill?", - "why_it_matters": "Relaxing the fixed cover (R2) reopens every entry at support level, so it is the cheapest support reopening found here.", - "first_step": "Cover the 2,682 (V<=W) snapshot pairs by a minimum number of free full flags and list each added operation.", + "question": "Which changed contract reopens all 2,682 sharp-missing entries at least cost, and what is its full bill?", + "why_it_matters": "Under the present cover an entry is supported only through its own compatible slot pair (apart from (73,83)); relaxing the cover (R2) reopens every entry at support level, but its cost is unknown. Pending #3618's T48 (one target lift, +2 rank mass, a whole row) changes the target path instead and is the first priced data point.", + "first_step": "Name the changed hypothesis among K1-K7 (or added storage), cover the 2,682 entries at support level, and list each added operation.", "blocked_by": "Coefficients, dirty restoration, chronology, native/hosting/precision/consumer costs are unknown." }, { diff --git a/research/p104-fixed-cover-cut-review/VERIFY.json b/research/p104-fixed-cover-cut-review/VERIFY.json index 68391d978e..2b15477562 100644 --- a/research/p104-fixed-cover-cut-review/VERIFY.json +++ b/research/p104-fixed-cover-cut-review/VERIFY.json @@ -19,7 +19,7 @@ "{package}/verify.py" ], "timeout_seconds": 600, - "checks": "PR3259 layered control; sharp criterion by two loop orders and PR3252 full-memory recurrence (all equal); PR3427 masks; rank(U-I)>=17; rows R1/R1c/R2/R3; 18,000-program oracle; six negative controls" + "checks": "Exact channel run (Y increment = G/2); PR3259 layered control; sharp support by one criterion in two loop orders and PR3252 full-memory recurrence (all equal; 2,309 own port pairs + (73,83)); PR3427 masks; rank(U-I)>=17; rows R1/R1u/R1c/R2/R3; 9,000-instance small-domain oracle (exhaustive reachability, realized programs, 18,000 random programs); six negative controls" }, { "argv": [ @@ -31,7 +31,7 @@ "{package}/test_verify.py" ], "timeout_seconds": 600, - "checks": "Four deliberate defects must fail; Y-relay escape" + "checks": "Seven negative controls: tampered hash, unsound and too-tight tests, shared-type and containment drops, wrong rectangle, Y-relay escape" } ] } diff --git a/research/p104-fixed-cover-cut-review/test_verify.py b/research/p104-fixed-cover-cut-review/test_verify.py index d3bce04c8e..747c9d18cd 100644 --- a/research/p104-fixed-cover-cut-review/test_verify.py +++ b/research/p104-fixed-cover-cut-review/test_verify.py @@ -41,7 +41,17 @@ def test_oracle_rejects_an_unsound_test(self): for t, yc in enumerate(inst[2]) if set(xc) & set(yc)}}): self.assertTrue(fails(V["oracle"], 7, ((3, 400),), 120)) - def test_dropping_nesting_breaks_pr3427_masks(self): + def test_oracle_rejects_a_too_tight_exhaustive_search(self): + # An exhaustive search that never switches helper type misses the + # legal two-type relay of the unpooled F_2^4 example. + g = V["unpooled_relay_example"].__globals__ + with mock.patch.dict(g, {"small_exact": lambda inst: ( + V["small_sharp"](inst), {})}): + self.assertTrue(fails(V["unpooled_relay_example"])) + + def test_dropping_shared_type_breaks_pr3427_masks(self): + # Pairing a source snapshot and a target snapshot that are each + # admitted by some helper type, not necessarily the same one. g = V["sharp_by_frames"].__globals__ r = result() loose = [0] * 104 @@ -59,6 +69,21 @@ def test_dropping_nesting_breaks_pr3427_masks(self): for s in range(4)] self.assertNotEqual(tuple(got), g["PR3427_SOURCE_MASKS"]) + def test_dropping_containment_is_unsound_in_principle(self): + # Containment V <= W is not decisive at P104 (verify.py checks this), + # but it is needed in general. F_2^4, one pooled type with line + # and hyperplane : X0 passes the admitted plane , + # Y0 the admitted plane , and no path joins them. + key = V["key"] + full = key([1, 2, 4, 8]) + ty = {0: (), 1: key([1]), 3: key([1, 2, 4]), 4: full} + inst = (4, [[key([2]), key([1, 2]), full]], + [[(), key([1, 4]), key([1, 4, 8])]], [ty]) + v, w = key([1, 2]), key([1, 4]) + self.assertTrue(V["small_admit"](ty, v) and V["small_admit"](ty, w)) + self.assertNotIn((0, 0), V["small_exact"](inst)[0]) + self.assertNotIn((0, 0), V["small_sharp"](inst)) + def test_wrong_rectangle_is_rejected(self): g = V["rank_consequence"].__globals__ r = result() diff --git a/research/p104-fixed-cover-cut-review/verify.py b/research/p104-fixed-cover-cut-review/verify.py index 41df716261..26b1ea0b45 100644 --- a/research/p104-fixed-cover-cut-review/verify.py +++ b/research/p104-fixed-cover-cut-review/verify.py @@ -5,12 +5,15 @@ Frames are GF(2) subspaces of F_2^n held as canonical reduced-echelon keys. P104 rebuilds frames, covers, the 2,309-edge pool and the 4,992 required - entries; replays PR3259's layered relaxation with a literal frame-hosting - index (control) and evaluates the path-nested one-helper criterion - (sharp untimed support) by two loop orders and by an independent - full-memory recurrence in the manner of PR3252. - ORACLE exhaustive/bounded small programs with exact Fraction coefficients. - ROWS three single-relaxation witnesses (unpriced; operations counted). + entries; runs the channel word exactly (Y increment = G/2); replays + PR3259's layered relaxation with a literal frame-hosting index + (control) and evaluates the path-nested one-helper criterion (sharp + untimed support) by two loop orders and by an independent full-memory + recurrence in the manner of PR3252. + ORACLE seeded random small instances: an exhaustive untimed reachability per + instance, an explicit checked program for every reachable helper pair, + and random checked programs, all with exact Fraction coefficients. + ROWS single-relaxation support rows (unpriced; operations counted). """ import hashlib @@ -37,6 +40,14 @@ def need(ok, msg): raise SystemExit("FAIL: " + msg) +def axpy(dst, c, src): + """dst += c * src on sparse Fraction vectors.""" + for k, v in list(src.items()): + dst[k] = dst.get(k, 0) + c * v + if dst[k] == 0: + del dst[k] + + # ---------------------------------------------------------------- GF(2) keys def key(vectors): """Canonical reduced row-echelon basis (descending pivots) of a span.""" @@ -98,6 +109,52 @@ def frame_paths(word): return paths +def channel_run(word, C): + """Exact Fraction run of the channel word. Checks that every add is at + equal current frames, that each Y increment is X -> G/2 = I - C on the + sorted ports with all helper dirt cancelled, and records which sources + have a nonzero coefficient in each register at each of its frames.""" + frame, val, hist = {}, {}, {} + + def record(n): + h = hist.setdefault(n, {}) + h[frame[n]] = h.get(frame[n], 0) | sum( + 1 << int(k[1:]) for k in val[n] if k[0] == "X") + for n, b in word["initial_frames"].items(): + frame[n], val[n] = key(b), {n: Fraction(1)} + record(n) + first = None + for i, ev in enumerate(word["program"]): + op, n = ev[0], ev[1] + if op == "transport": + need(frame[n] == key(ev[2]), "channel transport from its frame") + frame[n] = key(ev[3]) + elif op == "add": + need(frame[n] == frame[ev[2]] == key(ev[4]), + "channel add at equal frames") + axpy(val[n], Fraction(ev[3]), val[ev[2]]) + if first is None and n == "Y71" and "X102" in val[n]: + first = [i, str(val[n]["X102"]), ev[2], len(frame[n])] + elif op == "copy": + need(frame[ev[2]] == key(ev[3]), "channel copy at its frame") + frame[n], val[n] = key(ev[3]), dict(val[ev[2]]) + elif op == "zero": + frame[n], val[n] = key(ev[2]), {} + else: # erase discards the private copy; it is never read again + need(op == "erase", "known channel event") + frame[n], val[n] = key(ev[2]), {} + continue + record(n) + for t in range(104): + inc = dict(val["Y%d" % t]) + axpy(inc, Fraction(-1), {"Y%d" % t: Fraction(1)}) + want = {"X%d" % s: Fraction(int(t == s)) - C[t][s] + for s in range(104)} + need(inc == {k: x for k, x in want.items() if x}, + "Y%d increment is exactly G/2 with dirt cancelled" % t) + return hist, first + + def channel_roles(word): """X is never written and Y never read by the original channel.""" writes, reads = set(), set() @@ -294,8 +351,9 @@ def sum_or(masks): return m -def sharp_by_frames(geo, paths): - """Method 1 (RREF keys): pair snapshots V <= W sharing a helper type.""" +def sharp_by_frames(geo, paths, nested=True): + """Method 1 (RREF keys): pair snapshots V <= W sharing a helper type. + nested=False drops the containment V <= W (a probe, not a test).""" masks = endpoint_masks(geo) frames = {f for k in "XY" for i in range(104) for f in paths[k + str(i)]} adm = {f: admit_mask(geo, masks, f) for f in frames} @@ -306,7 +364,8 @@ def sharp_by_frames(geo, paths): for s in range(104): xs = paths["X%d" % s] if set(xs) & set(ys) or any( - adm[v] & adm[w] and le(v, w) for v in xs for w in ys): + adm[v] & adm[w] and (le(v, w) or not nested) + for v in xs for w in ys): m |= 1 << s out.append(m) return out @@ -431,6 +490,7 @@ def p104(): roles = channel_roles(word) geo = covers(cert, paths) C = required(e8_ports(fixture)) + hist, first = channel_run(word, C) lay, fwd, back, f5 = layered(geo, paths) miss_l = missing(C, lay) need(miss_l == [(71, 102)], "layered relaxation misses only (71,102)") @@ -440,36 +500,28 @@ def p104(): need(sharp == sharp_by_edges(geo, paths), "sharp criterion: two loop orders") need(sharp == full_memory(geo, paths), "PR3252 full-memory test = sharp") need(all(sharp[t] & ~lay[t] == 0 for t in range(104)), "sharp <= layered") + need(not any(set(paths["X%d" % s]) & set(paths["Y%d" % t]) + for s in range(104) for t in range(104)), + "no X path shares a frame with a Y path") + # Containment is never decisive here: dropping it changes no pair. + need(sharp_by_frames(geo, paths, nested=False) == sharp, + "containment not decisive at P104") + # Structure: the sharp support is the 2,309 compatible slot pairs read as + # port pairs (target b//2, source a//2) plus one extra pair. + own = {(b // 2, a // 2) for a, b in geo[4]} + need(len(own) == 2309 and all(C[t][s] != 0 for t, s in own), + "2,309 distinct required own port pairs") + sup = {(t, s) for t in range(104) for s in range(104) if sharp[t] >> s & 1} + need(sup == own | {(73, 83)} and C[73][83] != 0, + "sharp support = own port pairs + (73,83)") return {"roles": roles, "geo": geo, "paths": paths, "C": C, "layered": lay, "sharp": sharp, "missing_layered": miss_l, - "missing_sharp": missing(C, sharp), "forward": fwd} + "missing_sharp": missing(C, sharp), "forward": fwd, + "hist": hist, "first_Y71_X102": first} # ------------------------------------------------ sensitivity rows (support) -def channel_states(word): - """Structural X-dependence of every original-channel register per frame.""" - frame, dep, hist = {}, {}, {} - for n, b in word["initial_frames"].items(): - frame[n] = key(b) - dep[n] = 1 << int(n[1:]) if n[0] == "X" else 0 - hist[n] = {frame[n]: dep[n]} - for ev in word["program"]: - n = ev[1] - if ev[0] == "transport": - frame[n] = key(ev[3]) - elif ev[0] == "add": - dep[n] |= dep[ev[2]] - elif ev[0] == "copy": - frame[n], dep[n] = key(ev[3]), dep[ev[2]] - elif ev[0] == "zero": - frame[n], dep[n] = key(ev[2]), 0 - # erase: keep dependence (over-approximation; no cancellation used) - hist.setdefault(n, {}) - hist[n][frame[n]] = hist[n].get(frame[n], 0) | dep[n] - return hist - - -def rows(r, word): +def rows(r): geo, paths, ms = r["geo"], r["paths"], set(r["missing_sharp"]) masks, adm = endpoint_masks(geo), {} @@ -482,19 +534,21 @@ def hop(v, w): def count(sup): return sum(1 for t, s in ms if sup[t] >> s & 1), bool(sup[71] >> 102 & 1) - hist = channel_states(word) + hist = r["hist"] # actual nonzero channel coefficients per frame ys = [(t, j, w) for t in range(104) for j, w in enumerate(paths["Y%d" % t])] xin = {(t, j): sum(1 << s for s in range(104) if any( hop(v, w) for v in paths["X%d" % s])) for t, j, w in ys} - def relay(seed): + def relay(seed, ordered=True): + # ordered: content written into Y_u at snapshot kk is readable only + # at snapshots k >= kk (Y_u's frames ascend in time). inn = dict(seed) changed = True while changed: changed = False for u, k, wu in ys: avail = 0 - for kk in range(k + 1): + for kk in range(k + 1 if ordered else len(paths["Y%d" % u])): avail |= inn[(u, kk)] for t, j, wt in ys: if t != u and avail & ~inn[(t, j)] and hop(wu, wt): @@ -506,6 +560,17 @@ def relay(seed): return sup r1 = relay(xin) + r1u = relay(xin, ordered=False) + arrivals = {} + for t, j, w in ys: + if xin[(t, j)]: + cap = j == len(paths["Y%d" % t]) - 1 + arrivals[(len(w), cap)] = arrivals.get((len(w), cap), 0) + \ + bin(xin[(t, j)]).count("1") + need(all(xin[(t, len(paths["Y%d" % t]) - 1)] == r["sharp"][t] + for t in range(104)), "every supported pair arrives at the cap") + need(len({paths["Y%d" % t][-1] for t in range(104)}) == 104, + "104 distinct target caps") r1c = relay({(t, j): xin[(t, j)] | hist["Y%d" % t].get(w, 0) for t, j, w in ys}) free = [sum(1 << s for s in range(104) if any( @@ -527,6 +592,8 @@ def relay(seed): w1c = [len(f) for f in paths["Y71"] if hist["Y71"].get(f, 0) >> 102 & 1][:1] return {"R1_correction_only_Y_relay": count(r1), + "R1u_without_target_order": count(r1u), + "R1_arrivals_dim_cap": sorted(arrivals.items()), "R1c_Y_relay_with_channel_content": count(r1c), "R2_free_nested_flags": count(free), "R3_old_channel_helper_reads": count(r3), @@ -792,11 +859,6 @@ def run_program(rng, inst, steps, violate=None, direct=True): f = [c for c in xs + ys for c in c if 1 <= len(c) < n] extra = (f[rng.below(len(f))], {("X", rng.below(len(xs))): Fraction(1)}) - def axpy(dst, c, src): - for k, v in src.items(): - dst[k] = dst.get(k, 0) + c * v - if dst[k] == 0: - del dst[k] for _ in range(steps): fr = [flags[h][pos[h]] for h in range(nh)] xf = [xs[i][xp[i]] for i in range(len(xs))] @@ -850,33 +912,6 @@ def axpy(dst, c, src): return got -def y_relay_counterexample(): - """Minimal F_2^3 program: reading a target relays X0 outside both tests. - - e1,e2,e3 = 1,2,4. X0: -> FULL. Y0: 0 -> -> . - Y1: 0 -> . Type T1 fixes < ; type T2 fixes - < . h1 (T1) reads X0 at and writes Y0 there; Y0 is - transported by the frozen channel; h2 (T2, dim-2 frame ) reads - Y0 and writes Y1. Four scalar operations; coefficient c1*c2*c3*c4. - """ - full = key([1, 2, 4]) - t1 = {0: (), 1: key([1]), 2: key([1, 4]), 3: full} - t2 = {0: (), 1: key([2]), 2: key([1, 2]), 3: full} - inst = (3, [[key([1]), full]], [[(), key([1]), key([1, 2])], - [(), key([1, 2])]], [t1, t2]) - c = [Fraction(2), Fraction(-3), Fraction(5, 7), Fraction(-1, 2)] - need(inst[1][0][0] == t1[1], "h1 reads X0 at its line") - h1 = c[0] # h1 += c0 * X0 at - y0 = c[1] * h1 # Y0 += c1 * h1 at - need(inst[2][0][2] == t2[2], "Y0 later frame equals h2 frame") - h2 = c[2] * y0 # h2 += c2 * Y0 at - y1 = c[3] * h2 # Y1 += c3 * h2 at - need(y1 != 0, "nonzero relayed coefficient") - sharp, lay = small_sharp(inst), small_layered(inst) - need((1, 0) not in sharp and (1, 0) not in lay, "Y relay escapes") - return (1, True) - - def meet(a, b): """Intersection of two subspaces (small domains: enumerate a's points).""" pts = [0] @@ -901,10 +936,11 @@ def flag_through(rng, inst, ty, must): return flag -def execute(inst, helpers, ops): +def execute(inst, helpers, ops, yread=False): """Run an explicit straight-line program, checking every contract rule: flags of the helper's type, monotone transports, equal-frame reads, - mixes and writes, monotone frozen X/Y schedules. Exact Fractions.""" + mixes and writes, monotone frozen X/Y schedules. Exact Fractions. + yread=True admits one contract violation: helpers may read a target.""" n, xs, ys, _ = inst for ty, fl in helpers: need(all(small_admit(ty, f) for f in fl[1:n]) and all( @@ -913,11 +949,6 @@ def execute(inst, helpers, ops): hv = [{("D", h): Fraction(1)} for h in range(len(helpers))] yv = [{} for _ in ys] - def axpy(dst, c, src): - for k, x in src.items(): - dst[k] = dst.get(k, 0) + c * x - if dst[k] == 0: - del dst[k] for op, a, b, c in ops: fr = [helpers[h][1][pos[h]] for h in range(len(helpers))] if op == "x": @@ -936,12 +967,125 @@ def axpy(dst, c, src): elif op == "mix": need(fr[a] == fr[b] and a != b, "mix at equal frame") axpy(hv[b], c, hv[a]) + elif op == "yread": + need(yread, "targets are never read") + need(fr[a] == ys[b][yp[b]], "Y read at equal frame") + axpy(hv[a], c, yv[b]) else: + need(op == "write", "known operation") need(fr[a] == ys[b][yp[b]], "write at equal frame") axpy(yv[b], c, hv[a]) return {(t, k[1]) for t in range(len(ys)) for k in yv[t] if k[0] == "X"} +def y_relay_counterexample(): + """Minimal F_2^3 program: reading a target relays X0 outside both tests. + + e1,e2,e3 = 1,2,4. X0: -> FULL. Y0: 0 -> -> . + Y1: 0 -> . Type T1 fixes < ; type T2 fixes + < . h1 (T1) reads X0 at and writes Y0 there; Y0 is + transported by the frozen channel; h2 (T2, dim-2 frame ) reads + Y0 and writes Y1. Four scalar operations, run by the checked + interpreter with the one rule it breaks (a Y read) enabled. + """ + full = key([1, 2, 4]) + t1 = {0: (), 1: key([1]), 2: key([1, 4]), 3: full} + t2 = {0: (), 1: key([2]), 2: key([1, 2]), 3: full} + inst = (3, [[key([1]), full]], [[(), key([1]), key([1, 2])], + [(), key([1, 2])]], [t1, t2]) + helpers = [(t1, [(), key([1]), key([1, 4]), full]), + (t2, [(), key([2]), key([1, 2]), full])] + c = [Fraction(2), Fraction(-3), Fraction(5, 7), Fraction(-1, 2)] + ops = [("x", 0, 0, None), ("y", 0, 1, None), ("tr", 0, 1, Fraction(1)), + ("read", 0, 0, c[0]), ("write", 0, 0, c[1]), + ("y", 0, 2, None), ("tr", 1, 2, Fraction(1)), + ("yread", 1, 0, c[2]), ("y", 1, 1, None), ("write", 1, 1, c[3])] + need(rejected(lambda: execute(inst, helpers, ops)), + "Y read is rejected by the contract interpreter") + got = execute(inst, helpers, ops, yread=True) + need((1, 0) in got, "nonzero relayed coefficient") + sharp, lay = small_sharp(inst), small_layered(inst) + need((1, 0) not in sharp and (1, 0) not in lay and + (1, 0) not in small_exact(inst)[0], "Y relay escapes") + return (1, True) + + +def rejected(fn): + """True when the checked interpreter rejects the program.""" + try: + fn() + except SystemExit: + return True + return False + + +def small_frames(n, cache={}): + """Every proper nonzero subspace of F_2^n as a canonical key.""" + if n not in cache: + cache[n] = [key(b) for d in range(1, n) for b in subspaces(n, d)] + return cache[n] + + +def small_exact(inst): + """Exhaustive untimed reachability (no lemma assumed). A frame is reached + when a helper of some type can hold the source there; a helper of type ty + moves up between two nested frames that ty admits (a flag of ty passes + both); helpers at equal frames mix. Returns the support and, for each + helper-only pair, one witness path (frames, type of each step).""" + n, xs, ys, types = inst + up = {} + for i, ty in enumerate(types): + fs = [f for f in small_frames(n) if small_admit(ty, f)] + for f in fs: + for g in fs: + if len(f) < len(g) and le(f, g): + up.setdefault(f, {}).setdefault(g, i) + up.setdefault(f, {}) + sup = {(t, s) for s, xc in enumerate(xs) for t, yc in enumerate(ys) + if set(xc) & set(yc)} + wit = {} + for s, xc in enumerate(xs): + par = {v: None for v in xc if v in up} + todo = list(par) + while todo: + f = todo.pop() + for g, i in up[f].items(): + if g not in par: + par[g] = (f, i) + todo.append(g) + for t, yc in enumerate(ys): + w = next((w for w in yc if w in par), None) + if w is not None and (t, s) not in sup: + sup.add((t, s)) + frames, steps = [w], [] + while par[frames[-1]] is not None: + f, i = par[frames[-1]] + frames.append(f) + steps.append(i) + wit[(t, s)] = (frames[::-1], steps[::-1]) + return sup, wit + + +def realize(rng, inst, pair, witness): + """Turn a reachability witness into an explicit program (one helper per + step, mixing at the shared frames) and run it in the checked + interpreter. True when the pair gets a nonzero coefficient.""" + n, xs, ys, types = inst + (t, s), (frames, steps) = pair, witness + helpers, ops = [], [("x", s, xs[s].index(frames[0]), None)] + for k, i in enumerate(steps): + fl = flag_through(rng, inst, types[i], frames[k:k + 2]) + need(fl is not None, "witness step admitted by its type") + helpers.append((types[i], fl)) + ops += [("tr", k, fl.index(frames[k]), rng.coef()), + ("read", k, s, rng.coef()) if k == 0 else + ("mix", k - 1, k, rng.coef()), + ("tr", k, fl.index(frames[k + 1]), rng.coef())] + ops += [("y", t, ys[t].index(frames[-1]), None), + ("write", len(steps) - 1, t, rng.coef())] + return pair in execute(inst, helpers, ops) + + def directed_program(rng, inst, hops): """Legal program along a random path: read X_s at V, relay through `hops` further helpers of random types at shared frames, write Y_t. @@ -991,38 +1135,61 @@ def unpooled_relay_example(): """F_2^4, types not closed under recombination: a legal two-type relay lies inside PR3259's layered test but outside the single-type criterion. - T1 fixes < < ; T2 fixes < < + T1 fixes < < ; T2 fixes < < . h1 (T1) reads X0 at , rises to , adds into h2 - (T2) there; h2 rises to W = and writes Y0.""" + (T2) there; h2 rises to W = and writes Y0. Run by the + checked interpreter (which also checks that each type is a flag).""" full = key([1, 2, 4, 8]) t1 = {0: (), 1: key([1]), 2: key([1, 2]), 3: key([1, 2, 8]), 4: full} - t2 = {0: (), 1: key([4]), 2: key([1, 2]), 3: key([1, 2, 4]), 4: full} + t2 = {0: (), 1: key([2]), 2: key([1, 2]), 3: key([1, 2, 4]), 4: full} inst = (4, [[key([1]), full]], [[(), key([1, 2, 4])]], [t1, t2]) - need(t1[2] == t2[2] and t2[3] == inst[2][0][1], "relay frames") - coef = Fraction(3) * Fraction(-2, 5) * Fraction(7) * Fraction(1, 3) - need(coef != 0, "nonzero relayed coefficient") - need((0, 0) not in small_sharp(inst) and (0, 0) in small_layered(inst), + helpers = [(t, [t[d] for d in range(5)]) for t in (t1, t2)] + ops = [("x", 0, 0, None), ("tr", 0, 1, Fraction(1)), + ("read", 0, 0, Fraction(3)), ("tr", 0, 2, Fraction(-2, 5)), + ("tr", 1, 2, Fraction(1)), ("mix", 0, 1, Fraction(7)), + ("tr", 1, 3, Fraction(1, 3)), ("y", 0, 1, None), + ("write", 1, 0, Fraction(1))] + need((0, 0) in execute(inst, helpers, ops), + "legal two-type relay delivers a nonzero coefficient") + need((0, 0) not in small_sharp(inst) and (0, 0) in small_layered(inst) + and (0, 0) in small_exact(inst)[0], "pooling is needed for the one-helper criterion") return True -def oracle(seed=20261018, trials=((3, 3000), (4, 1500)), steps=120): - """Pooled instances (P104-like): every legal coefficient lies in the - one-helper test, which lies in PR3259's layered test. Unpooled rigid - instances: every legal coefficient lies in the layered test (PR3259 needs - no pooling); escapes from the one-helper test are counted.""" - rng = Rng(seed) +ORACLE_TRIALS = ((3, 3000), (4, 1500)) + + +def oracle(seed=20261018, trials=ORACLE_TRIALS, steps=120): + """Seeded random small instances, each checked three ways: an exhaustive + untimed reachability (small_exact), an explicit checked program for every + reachable helper pair (realize), and random checked programs. Pooled + instances (P104-like): the exhaustive support equals the one-helper test. + Unpooled rigid instances: it lies in PR3259's layered test (no pooling + needed there) and its escapes from the one-helper test are counted.""" + rng, wrng = Rng(seed), Rng(seed + 1) c = dict.fromkeys(("programs", "nonzero_coefficients", "helper_mediated", "cross_type_relayed", "directed_multi_type", - "strict_gap", "unpooled_programs", + "strict_gap", "strict_gap_pairs", + "exact_helper_pairs_realized", "unpooled_programs", "unpooled_coefficients", "unpooled_multi_type", - "unpooled_single_type_escapes"), 0) + "unpooled_single_type_escapes", + "unpooled_exact_helper_pairs_realized", + "unpooled_exact_escapes", "unpooled_escape_instances"), + 0) for n, count in trials: for _ in range(count): inst = instance(rng, n, pooled=True) sharp, lay = small_sharp(inst), small_layered(inst) need(sharp <= lay, "oracle: sharp support inside layered") c["strict_gap"] += sharp < lay + c["strict_gap_pairs"] += len(lay - sharp) + exact, wit = small_exact(inst) + need(exact == sharp, "oracle: exhaustive untimed support differs " + "from the one-helper test on a pooled instance") + need(all(realize(wrng, inst, p, w) for p, w in wit.items()), + "oracle: reachable pair not realized by a checked program") + c["exact_helper_pairs_realized"] += len(wit) # Direct X->Y adds are seeded identically by both tests; omit # them so every coefficient is carried by helper paths. got = run_program(rng, inst, steps, direct=False) @@ -1037,10 +1204,19 @@ def oracle(seed=20261018, trials=((3, 3000), (4, 1500)), steps=120): c["cross_type_relayed"] += len(cross) c["directed_multi_type"] += len(path) if ntypes > 1 else 0 inst = instance(rng, n, nt=6, rigid=True) + exact, wit = small_exact(inst) + need(exact <= small_layered(inst), + "oracle: exhaustive support outside the layered test") + need(all(realize(wrng, inst, p, w) for p, w in wit.items()), + "oracle: reachable pair not realized by a checked program") + c["unpooled_exact_helper_pairs_realized"] += len(wit) + escapes = exact - small_sharp(inst) + c["unpooled_exact_escapes"] += len(escapes) + c["unpooled_escape_instances"] += bool(escapes) got = run_program(rng, inst, steps, direct=False) path, ntypes = directed_program(rng, inst, 1 + rng.below(3)) - need(got | path <= small_layered(inst), - "oracle: legal coefficient outside the layered test") + need(got | path <= exact, + "oracle: legal coefficient outside the exhaustive support") c["unpooled_programs"] += 2 c["unpooled_coefficients"] += len(got) + len(path) c["unpooled_multi_type"] += len(path) if ntypes > 1 else 0 @@ -1078,9 +1254,28 @@ def main(): "every row and column has a sharp-missing entry") need(sum(bin(m).count("1") for m in sharp) == 2310 and sum(bin(m).count("1") for m in r["layered"]) == 10815, "support sizes") - _, word, _ = load() - rw = rows(r, word) + C, lay = r["C"], r["layered"] + by_value = {} + for t, s in ms: + by_value[str(C[t][s])] = by_value.get(str(C[t][s]), 0) + 1 + need(by_value == {"-1/2": 1801, "1/2": 881}, "sign split 1,801/881") + reopened = sum(1 for t, s in ms if lay[t] >> s & 1) + need(reopened == 2681, "PR3259's test grants 2,681 sharp-missing entries") + pairs = [(t, s) for t in range(104) for s in range(104)] + need(sum(not sharp[t] >> s & 1 for t, s in pairs) == 8506, "8,506 unsupported") + need(all(C[t][s] != 0 and t != s for t, s in pairs if sharp[t] >> s & 1), + "every sharp-supported pair is an off-diagonal required entry") + zero_off = [(t, s) for t, s in pairs if t != s and C[t][s] == 0] + need(len(zero_off) == 5720 and all(lay[t] >> s & 1 for t, s in zero_off) + and all(lay[t] >> t & 1 for t in range(104)), + "PR3259's test grants all 5,720 zero off-diagonal and 104 diagonal pairs") + need(r["first_Y71_X102"] == [3378, "1/2", "D11", 5], + "channel's first X102 delivery into Y71") + rw = rows(r) need(rw["R1_correction_only_Y_relay"] == (0, False), "R1") + need(rw["R1u_without_target_order"] == (2682, True), "R1u") + need(rw["R1_arrivals_dim_cap"] == [((5, False), 31), ((6, False), 24), + ((8, True), 2310)], "R1 arrivals") need(rw["R1c_Y_relay_with_channel_content"] == (2682, True), "R1c") need(rw["R2_free_nested_flags"] == (2682, True), "R2") need(rw["R3_old_channel_helper_reads"] == (2682, True), "R3") @@ -1093,20 +1288,29 @@ def main(): need(escapes == ESCAPES_EXPECTED, "negative controls %r" % (escapes,)) print(json.dumps({"channel_roles": r["roles"], "layered_missing": r["missing_layered"], "forward_cone": r["forward"], + "channel_first_Y71_X102": r["first_Y71_X102"], "rank_bound": rk, "minor_det_8C": det, - "sharp_missing": len(ms), "rows": rw, "oracle": checked, - "negative_controls": escapes}, sort_keys=True)) + "sharp_missing": len(ms), "sharp_missing_by_value": + by_value, "layered_grants_sharp_missing": reopened, + "unsupported_pairs": 8506, "sharp_support": + "2309 own port pairs + [73,83]", "rows": rw, + "oracle": checked, "negative_controls": escapes}, + sort_keys=True)) print("PASS_P104_FIXED_COVER_CUT_REVIEW layered_missing=1 " "sharp_missing=2682 of 4992 pr3427_masks=4 rank_U_minus_I>=17 " - "rows=4 oracle_programs=%d no_kappa" % ( + "rows=5 oracle_instances=%d oracle_programs=%d no_kappa" % ( + sum(n for _, n in ORACLE_TRIALS) * 2, checked["programs"] + checked["unpooled_programs"])) ORACLE_EXPECTED = { "programs": 9000, "nonzero_coefficients": 1043, "helper_mediated": 604, "cross_type_relayed": 13, "directed_multi_type": 620, "strict_gap": 54, + "strict_gap_pairs": 75, "exact_helper_pairs_realized": 4264, "unpooled_programs": 9000, "unpooled_coefficients": 1887, - "unpooled_multi_type": 1112, "unpooled_single_type_escapes": 0} + "unpooled_multi_type": 1112, "unpooled_single_type_escapes": 0, + "unpooled_exact_helper_pairs_realized": 8978, + "unpooled_exact_escapes": 33, "unpooled_escape_instances": 26} ESCAPES_EXPECTED = {"yread": (1, True), "unpooled": True, "descent": (1, True), "crossframe": (6, True), "offcover": (131, True), "oldstate": (159, True)} From 59d34b7be4b14833686fd72d9b8f06f7b7a965b4 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Mon, 19 Oct 2026 02:13:41 +0530 Subject: [PATCH 8/9] Address round-2 review of the P104 fixed-cover cut review - Credit PR3427 for the one-helper criterion and its untimed exactness; its masks already exclude 92 required entries PR3259's test grants (asserted). State what is new; retitle. - Rank bound: replace the greedy 19x18 rectangle (rank 17) by a maximum independent 23x23 principal block (two exact searches; rank 23; det(2C[S,S]) = 2^30), so rank(U-I) >= 23. - Assert a perfect matching of the 2,682 missing entries (vertex cover 104; row min 14, column min 9) and that every X path ends at FULL; state the path-change consequence without a cost claim. - Fix R1 arrival units (55 source arrivals on 26 lower snapshots, asserted), the "only through" wording, containment "over-grants", #3609's K5 reason, receipt wording and counts, review-pass count, K legend, and pending-work note in PROOF-REVIEW verdict 3. - test_verify: controls must fail with their own FAIL message; wrong rank block (added and removed port); containment test renamed. Co-Authored-By: Claude Opus 5.5 --- .../PROOF-REVIEW.md | 81 +++++--- .../p104-fixed-cover-cut-review/README.md | 175 +++++++++++------- .../p104-fixed-cover-cut-review/TASK.json | 10 +- .../p104-fixed-cover-cut-review/VERIFY.json | 4 +- .../test_verify.py | 30 ++- .../p104-fixed-cover-cut-review/verify.py | 169 ++++++++++++----- 6 files changed, 312 insertions(+), 157 deletions(-) diff --git a/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md b/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md index a15541473d..8a26fd69e9 100644 --- a/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md +++ b/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md @@ -17,9 +17,9 @@ proves no P104 impossibility outside the stated contract. ## Verdict -These verdicts come from an author-checked, AI-assisted review. Four AI review -passes in the same loop checked the first version; no independent human or -formal-kernel review has been done. +These verdicts come from an author-checked, AI-assisted review. Seven AI +review passes in the same loop, over two rounds, checked the package; no +independent human or formal-kernel review has been done. 1. **PR3259's argument is valid as a necessary support test under its stated contract.** Each step below is valid as written. Two steps need a sentence @@ -34,17 +34,23 @@ formal-kernel review has been done. relaxation grants 10,815 source/target pairs, against 2,310 for the sharp criterion. "Exactly one missing coefficient" describes PR3259's test, not the contract. PR3259 itself says that passing its test is not a realization. - What is new here is that the same contract excludes 2,681 of the entries - that pass. + PR3427 already states this criterion and its untimed exactness, and its + published masks for sources 0-3 already exclude 92 required entries that + PR3259's test grants. What is new here is the step-by-step review, the + full 104-column count with its closed form, a multi-hop check that does + not assume the lemma, the rank and vertex-cover consequences, and the + rows R1-R3. 3. Consequently the fixed-cover contract is closed by a much larger obstruction than one coefficient. A contract change that only reopens `C[71,102]` does not complete the correction. Examples are PR3427's rank-one source shear, a - moved helper, or one extra dependency. + moved helper, or one extra dependency. The pending concrete corrections + (README, "Concurrent pending work") change a frozen path, the channel or + storage, so they lie outside K1-K7 and are not judged here. 4. **PR3427 consumes its own one-helper lemma and PR3252's full-memory operations, not PR3259's layered recurrence.** The lemma is valid. Its published four-column support masks are reproduced exactly by code written for this review. Its rank theorem stands as stated. Applied to all 104 - columns, the same argument gives **`rank(U-I) >= 17`** (section below). + columns, the same argument gives **`rank(U-I) >= 23`** (section below). 5. **PR3252's theorem is valid** for its stated recurrence and contract. ## Contract, as used @@ -227,8 +233,16 @@ a dimension-4 frame of X83 admitted, with Y73's cap, by one pool type. Hence and dropping the containment `V <= W` changes no pair, so containment is never decisive here. The verifier asserts each of these facts. +The 2,682 missing entries contain a perfect matching: Kuhn's augmenting-path +matching has size 104, so by König's theorem no fewer than 104 rows and +columns cover them. Every row holds at least 14 and every column at least 9. +Under the criterion an entry's support depends only on the frames of its +source and target paths and on the cover, so a reopening that keeps K1-K3, +K6, K7 and the K4/K5 roles and changes only individual X or Y frame paths +must change at least 104 of them. This makes no cost claim. + For sources 0-3 the per-source target masks equal PR3427's published masks -exactly. Those masks come from PR3427's direct criterion and from PR3252's +exactly. They exclude 92 required entries, all granted by PR3259's test. Those masks come from PR3427's direct criterion and from PR3252's full-memory operations. ## PR3252 PROOF.md (shorter review) @@ -278,7 +292,7 @@ found. - The consumption is justified. The lemma is valid, and the four-column masks are reproduced exactly by an engine that shares no code with PR3427. -## Consequence for PR3427: rank(U-I) >= 17 +## Consequence for PR3427: rank(U-I) >= 23 PR3427's contract adds an invertible scalar source preconditioner U to K1-K7. The prepared sources `X' = UX` stay in the original frames, so the support @@ -296,18 +310,23 @@ rank(U - I) = rank(V - I) >= rank C[R,S], using `V - I = -V(U - I)` for the equality. -A deterministic greedy finds a rectangle. For each seed column it repeatedly -adds the column that maximizes `min(|R'|, |S|+1)`, then `|R'|`, with ties to -the smallest index, where `R'` is the set of rows still unsupported. It stops -when `min(|R|,|S|)` stops growing and keeps the rectangle of largest rank. -It finds a 19-by-18 rectangle of unsupported pairs with -`rank C[R,S] = 17`. Exact `Fraction` elimination gives the rank. A 17-by-17 -minor has integer `det(8C) = 2^43`, by Bareiss elimination, so -`det C = 2^-8`. +A principal block `C[S,S]` is fully unsupported exactly when S is +independent in the undirected support graph: no pair of S is supported in +either order (diagonal pairs never are). A maximum independent set has 23 +ports, + +``` +S = 8 11 17 18 23 30 34 37 42 50 51 58 59 63 70 71 78 80 84 87 91 96 100, +``` + +by two exact searches (a branch and bound with a greedy colouring bound and +a pivoted Bron-Kerbosch). Exact `Fraction` elimination gives +`rank C[S,S] = 23`, and an integer Bareiss determinant gives +`det(2C[S,S]) = 2^30`, so `det C[S,S] = 2^7`. -Thus `rank(U-I) >= 17` under PR3427's contract, against its published 4. -This prices no joint preparation. The greedy is not optimal, and a min-rank -completion may force more. +Thus `rank(U-I) >= 23` under PR3427's contract, against its published 4. +This prices no joint preparation. No unsupported principal block does +better; a non-principal rectangle or a min-rank completion may force more. ## Load-bearing hypotheses (support level, sharp criterion) @@ -330,10 +349,12 @@ keep the order of operations along one dependency path. its frames can be read only at that frame or a later one. Every program obeys this, because `Y_u`'s frames ascend in time; it is the path order that makes path frames nested, applied at a target used as a relay. Correction content -reaches targets at their final caps (2,310 arrivals, one for each supported -pair) and at 55 frames of dimension 5 or 6 (31 and 24). Content at a cap can -be read only at that cap, which feeds only itself because the 104 caps are -distinct. The 55 lower arrivals relay nothing new. So R1 reopens nothing. R1u +reaches targets at their final caps (2,310 source arrivals, one for each +supported pair) and in 55 further source arrivals at 26 lower target +snapshots (31 arrivals on 19 dimension-5 snapshots, 24 on 7 dimension-6 +snapshots). Content at a cap can be read only at that cap, which feeds only +itself because the 104 caps are distinct. The lower arrivals relay nothing +new. So R1 reopens nothing. R1u drops the order, lets cap content be read at the target's low frames, and reopens everything. R1's zero therefore rests on that order. @@ -355,15 +376,19 @@ Known rows are cited, not recomputed: - PR3013: component/containment pooling reaches all 4,992 entries. - PR3427: a one-H2 source shear removes the `(71,102)` requirement, but `D[3,2]` stays unsupported. A source preconditioner needs `rank(U-I) >= 4` - (17 by the section above). + (23 by the section above). Reading. Among the rows computed here, two hypotheses each reopen every entry: the fixed cover (K1) and the exclusion of the channel's source-dependent state (K6, including its exposure through Y). Unread Y matters at P104 only through that exposure, given each target's write-before-read order. The rows are not a -complete map. Not computed at P104: frame descent (K2), cross-frame mixing +complete map. Not computed as rows at P104: frame descent (K2), cross-frame mixing (K3), changed source or target frame paths and source mutation (K4, K5), dependent dirt (K7) and extra correlated storage. The small-domain negative controls show that descent, cross-frame mixing, off-cover flags and correlated -old state can each escape both tests. A reopening must change at least one of -K1-K7, or add storage, and must cover all 2,682 entries with a full bill. +old state can each escape both tests. Changing a frozen target path also +suffices at support level, one row at a time: every X path ends at FULL, so a +target that visits FULL shares that frame with every source (pending #3618's +T48 prices one such row at +2 rank mass). Path changes alone must touch at +least 104 registers. A reopening must change at least one of K1-K7, or add +storage, and must cover all 2,682 entries with a full bill. diff --git a/research/p104-fixed-cover-cut-review/README.md b/research/p104-fixed-cover-cut-review/README.md index 2a12f12936..2323d01556 100644 --- a/research/p104-fixed-cover-cut-review/README.md +++ b/research/p104-fixed-cover-cut-review/README.md @@ -1,35 +1,57 @@ -# P104 fixed-cover support cut: hypothesis review and a sharper criterion +# P104 fixed-cover support cut: hypothesis review and the full count under the one-helper criterion **Statement.** PR3259's path-embedding argument is a **valid** necessary support -test under its fixed-cover contract, taken in its pooled form (K1-K7 in -[PROOF-REVIEW.md](PROOF-REVIEW.md)). That contract is closed by a much larger -obstruction than one coefficient: **2,682 of the 4,992 required entries of -`C = I - G/2` are unsupported**, with at least one in every row and every -column. +test under its fixed-cover contract, taken in its pooled form (K1-K7 below). +That contract is closed by a much larger obstruction than one coefficient: +**2,682 of the 4,992 required entries of `C = I - G/2` are unsupported**. +They contain a perfect matching, so no fewer than 104 rows and columns +together cover them; every row has at least 14 and every column at least 9. + +Contract legend (full text in [PROOF-REVIEW.md](PROOF-REVIEW.md)): K1 fixed +pooled cover through `L/A/B/H`; K2 monotone helpers; K3 equal-frame mixing; +K4 immutable X on its frozen frame path; K5 unread Y on its frozen frame +path; K6 no other source-dependent state; K7 independent dirt. Rows R1-R3 +below each relax one of them. The 2,682 count rests on two sound tests that agree on all 10,816 source/target pairs: -- PR3427's one-recombined-helper lemma, re-proved here in every dimension - case. It keeps the fact that PR3259's test discards: the frames along a - dependency path are nested. +- PR3427's one-recombined-helper criterion, re-proved here in every + dimension case. It keeps the fact that PR3259's test discards: the frames + along a dependency path are nested. - PR3252's full-memory recurrence, whose proof is reviewed valid here, implemented anew over the whole pool. It is multi-hop and does not assume the lemma. -For the pooled untimed relaxation the lemma is exact: no sound untimed test -can exclude more pairs. The supported pairs have a simple form. They are the -2,309 compatible slot pairs read as port pairs, plus one extra pair, so -`2,682 = 4,992 - 2,309 - 1`. PR3259's single missing entry, -`C[71,102] = -1/2`, belongs to its looser relaxation. Applied to all 104 -columns, PR3427's source-preconditioner bound rises from `rank(U-I) >= 4` to -**`rank(U-I) >= 17`** under PR3427's own contract. +**What PR3427 already has, and what is new.** PR3427 states the one-helper +criterion, calls it exact for the pooled untimed relaxation and gives its +untimed converse. Its published masks for sources 0-3 already exclude 92 +required entries that PR3259's test grants, so PR3427's certificate already +implies that PR3259's test is not sharp. New here: + +- the step-by-step review of PR3259 and PR3252; +- the criterion's full 104-column count, 2,682, with its closed form: the + supported pairs are the 2,309 compatible slot pairs read as port pairs, + plus `(73,83)`, so `2,682 = 4,992 - 2,309 - 1`; +- a multi-hop computation of the same support that does not assume the + lemma; +- `rank(U-I) >= 23` under PR3427's own contract, against its published 4, + from a fully unsupported, nonsingular 23-by-23 principal block; +- the 104 vertex cover and the single-relaxation rows R1-R3. + +PR3259's single missing entry, `C[71,102] = -1/2`, belongs to its looser +relaxation. Under the criterion an entry's support depends only on the +frames of its source and target paths and on the cover. So a reopening that +keeps K1-K3, K6, K7 and the K4/K5 roles (X unwritten, Y unread), and changes +only individual X or Y frame paths, must change at least 104 of them. This +makes no cost claim. This is an author-checked, AI-assisted audit: a scoped proof review, a finite -certificate and small-domain checks. Four AI review passes in the same loop -(reproducibility, mathematics, provenance, referee) checked the first -version, and this revision addresses their findings. No independent human or -formal-kernel review has been done. The audit constructs nothing and is not a +certificate and small-domain checks. Seven AI review passes in the same loop, +over two rounds (reproducibility, mathematics, provenance and referee; then +mathematics, reproducibility and referee), checked the package, and this +revision addresses their findings. No independent human or formal-kernel +review has been done. The audit constructs nothing and is not a complete multiplication theorem. It proves no P104 impossibility outside the stated contract, and κ and the selected frontier are unchanged. @@ -44,8 +66,9 @@ stated contract, and κ and the selected frontier are unchanged. | Control: PR3259 layered test, rebuilt | Missing set `{(71,102)}`. Forward counts `16,25,52,365,1725,2283,2285,2297`. Backward cone 37, disjoint. | | Sharp criterion: one criterion in two loop orders, plus PR3252's multi-hop recurrence | All three computations agree on every pair. 2,310 supported pairs, against 10,815 for PR3259's test. 2,682 required entries unsupported: 1,801 at `-1/2` and 881 at `+1/2`. 8,506 pairs unsupported in all. | | Shape of the sharp support | Exactly the 2,309 compatible slot pairs `(a,b)` read as (target `b//2`, source `a//2`), all distinct and all required, plus `(73,83)`. All supported pairs are off-diagonal required entries. PR3259's test grants 2,681 of the 2,682 missing entries, all 5,720 zero off-diagonal pairs and all 104 diagonal pairs. | -| Cross-check with PR3427 | The four published per-source masks (sources 0-3) are reproduced exactly. | -| Consequence for PR3427 | A 19-by-18 rectangle of unsupported pairs has `rank C[R,S] = 17`, giving `rank(U-I) >= 17`. A 17-by-17 minor has `det(8C) = 2^43`. | +| Cover of the missing entries | A maximum matching of the 2,682 missing entries has size 104, so the minimum vertex cover is 104 (König). Missing entries per row: at least 14; per column: at least 9. | +| Cross-check with PR3427 | The four published per-source masks (sources 0-3) are reproduced exactly. They exclude 92 required entries, all granted by PR3259's test. | +| Consequence for PR3427 | A maximum independent set of the undirected support graph has 23 ports (two exact searches). Its 23-by-23 principal block is fully unsupported with `det(2C[S,S]) = 2^30`, so `rank C[S,S] = 23` and `rank(U-I) >= 23`. | | Small domains, pooled | 4,500 seeded `F_2^3`/`F_2^4` instances. On every one, an exhaustive untimed reachability, which does not assume the lemma, equals the one-helper test. Its 4,264 helper-only pairs are each realized by an explicit program in the checked interpreter. PR3259's test is strictly looser on 54 instances (75 pairs), and the exhaustive search confirms those pairs unreachable. | | Small domains, unpooled | 4,500 instances with six rigid types. The exhaustive support lies inside PR3259's test every time, and 8,978 helper-only pairs are realized. 33 pairs on 26 instances lie outside the one-helper test, each realized by a legal program: the lemma needs pooling. | | Random programs | 18,000 seeded checked programs with exact `Fraction` coefficients, two per instance; all lie inside the exhaustive support. Pooled: 1,043 nonzero coefficients counted per program, 604 of them on pairs whose X and Y chains share no frame, and 633 (13 + 620) passed between helpers of different types. Unpooled: 1,887 coefficients. The random programs found none of the 33 unpooled escapes, so they are a soundness sample, not the evidence for the lemma. | @@ -68,12 +91,13 @@ The sharp criterion and the rows relax the relative timing of different registers but keep the order of operations along one dependency path; that order is what makes path frames nested. R1 applies it at a target used as a relay. Content written into `Y_u` at one of its frames can be read only at -that frame or a later one, because `Y_u`'s frames ascend in time. Every program obeys this. With it, -correction content reaches targets at their final caps (2,310 arrivals) and at -55 frames of dimension 5 or 6 (31 and 24). A cap can feed only itself, since -the 104 caps are distinct, and the 55 lower arrivals relay nothing new, so R1 -reopens nothing. R1u drops the order and reopens everything. R1's zero rests -on that order. +that frame or a later one, because `Y_u`'s frames ascend in time. Every +program obeys this. With it, correction content reaches targets at their +final caps (2,310 source arrivals) and in 55 further source arrivals at 26 +lower target snapshots (31 arrivals on 19 dimension-5 snapshots, 24 on 7 +dimension-6 snapshots). A cap can feed only itself, since the 104 caps are +distinct, and the lower arrivals relay nothing new, so R1 reopens nothing. +R1u drops the order and reopens everything. R1's zero rests on that order. R1c and R3 use the channel's actual coefficients, recorded from the exact run of its 4,058 events. The channel first puts `X102` into `Y71` at event 3378, @@ -86,13 +110,18 @@ and cost are unknown. Among the rows computed here, two hypotheses each reopen every entry: the fixed cover (K1) and the exclusion of the channel's source-dependent state (K6, with its exposure through Y). The rows are not a complete map. Not -computed at P104: frame descent (K2), cross-frame mixing (K3), changed source +computed as rows at P104: frame descent (K2), cross-frame mixing (K3), changed source or target frame paths and source mutation (K4, K5), dependent dirt (K7) and extra correlated storage. The small-domain controls show that descent, cross-frame mixing, off-cover flags and correlated old state can each escape -both tests. Under PR3427's preconditioner contract, which relaxes K4, a source -preconditioner needs `rank(U-I) >= 17`. Any reopening must change at least one -of K1-K7, or add storage, and must cover all 2,682 entries with a full bill. +both tests. Changing a frozen target path also suffices at support level, one +row at a time: every X path ends at FULL, so a target that visits FULL shares +that frame with every source and can receive its whole row by equal-frame +adds (pending #3618's T48 prices one such row at +2 rank mass). Path changes +alone must touch at least 104 registers (the vertex cover above). Under +PR3427's preconditioner contract, which relaxes K4, a source preconditioner +needs `rank(U-I) >= 23`. Any reopening must change at least one of K1-K7, or +add storage, and must cover all 2,682 entries with a full bill. The 2,682 count binds only corrections that keep the fixed cover, the frozen X and Y frame paths and the untouched channel state. Routes that change any of @@ -127,8 +156,8 @@ conflict with its closure. dirty-restoration chronology on the published word. - Clear Insight (Clear1nsight), #3609 (`13f974dae4af66027afb01f3ab42df9e830c2e90`), completes the omitted P104 - section at the word's entrance with sources moved and Y temporarily - writable (outside K4 and K5). + section at the word's entrance with sources moved and Y read and + rescaled (outside K4 and K5). - James Reed (jwr404), #3580 (`c867e61e2ea790738474025b6200bf8475e56957`), indexes the #3259 replay for the [live support map](../../docs/research/p104-live-support-map.md). @@ -142,27 +171,33 @@ python3 -I -O -Werror -B research/p104-fixed-cover-cut-review/verify.py python3 -I -O -Werror -B research/p104-fixed-cover-cut-review/test_verify.py ``` -The verifier prints one JSON receipt with every count quoted above. Its last -line is +The verifier asserts every count quoted above and prints the main ones in +one JSON receipt. Its last line is ``` -PASS_P104_FIXED_COVER_CUT_REVIEW layered_missing=1 sharp_missing=2682 of 4992 pr3427_masks=4 rank_U_minus_I>=17 rows=5 oracle_instances=9000 oracle_programs=18000 no_kappa +PASS_P104_FIXED_COVER_CUT_REVIEW layered_missing=1 sharp_missing=2682 of 4992 pr3427_masks=4 rank_U_minus_I>=23 vertex_cover=104 rows=5 oracle_instances=9000 oracle_programs=18000 no_kappa ``` The registered replay is `python3.12 -B scripts/research_package.py --package research/p104-fixed-cover-cut-review`. Every check raises `SystemExit("FAIL: ...")`, so checks stay active under `-O`. -**Negative controls that must fail.** `test_verify.py` checks seven: +**Negative controls that must fail.** `test_verify.py` checks that each +deliberate defect stops `verify.py` with its own `FAIL` message: + +- a tampered input hash; +- an unsound "shared snapshot only" test inside the oracle; +- an exhaustive search that never switches helper type, which misses the + fixed unpooled two-type relay; +- a wrong rank block: one port added (it meets a supported pair) or one + removed (the block is no longer maximum). + +It also checks three facts: -- a tampered input hash is rejected; -- an unsound "shared snapshot only" test is rejected by the oracle; -- an exhaustive search that never switches helper type is rejected, because - it misses the fixed unpooled two-type relay; - dropping the shared-helper-type requirement changes PR3427's masks; -- dropping containment `V <= W` is unsound on a fixed `F_2^4` instance (at - P104 containment is never decisive, which `verify.py` asserts); -- a wrong rank rectangle is rejected; +- dropping containment `V <= W` over-grants on a fixed `F_2^4` instance: the + test stays sound but is no longer exact (at P104 containment is never + decisive, which `verify.py` asserts); - the fixed Y-relay program is a real escape. Inside `verify.py`, five contract violations must each produce a coefficient @@ -190,13 +225,17 @@ independently and sorted. memories `S + L(h,d) + L(w,d)`, minimal-memory pruning), rewritten over all 2,309 types and 104 sources. It is multi-hop and does not assume the lemma. -- The rank bound uses a deterministic greedy. For each seed column it - repeatedly adds the column that maximizes `min(|R'|, |S|+1)`, then `|R'|`, - with ties to the smallest index, where `R'` is the set of rows still - unsupported. It stops when `min(|R|,|S|)` stops growing and keeps the - rectangle of largest rank. Exact `Fraction` elimination gives the rank, and - an independent integer Bareiss determinant confirms it. The greedy is not - optimal, so 17 is a lower bound. +- The rank bound uses a maximum independent set S of the undirected support + graph: no pair of S is supported in either order. Two exact searches, a + branch and bound with a greedy colouring bound and a pivoted + Bron-Kerbosch, both give size 23. Exact `Fraction` elimination gives + `rank C[S,S] = 23`, and an integer Bareiss determinant gives + `det(2C[S,S]) = 2^30`, so `det C[S,S] = 2^7`. No unsupported principal + block is larger; a non-principal rectangle or a min-rank argument could + give more, so 23 is a lower bound. +- Kuhn's augmenting-path matching on the 2,682 missing entries gives size + 104, a perfect matching, so by König's theorem every set of rows and + columns covering them has at least 104 members. - The small-domain oracle draws seeded random instances (seed `20261018`): 3,000 over `F_2^3` and 1,500 over `F_2^4` in each family. Coverage is these instances, not every instance. @@ -244,21 +283,24 @@ The selected cold replay is unchanged and was not rerun. ## Open next questions -1. *Is 17 the true rank bound?* A min-rank completion of `-C` on all 8,506 - unsupported pairs may force a rank well above 17. A larger rank would - further constrain any joint native source preparation under PR3427's - contract. A first step is an exact lower bound by larger or overlapping - rectangles, or by a min-rank argument. It needs no new matching search. +1. *Is 23 the true rank bound?* 23 is optimal among principal blocks. A + non-principal unsupported rectangle, or a min-rank completion of `-C` on + all 8,506 unsupported pairs, may force more. A larger rank would further + constrain any joint native source preparation under PR3427's contract. It + needs no new matching search. 2. *Which changed contract reopens all 2,682 entries at least cost?* An entry is supported when one helper type admits a source frame and a nested - target frame. Under the present cover that happens only through the - entry's own compatible slot pair, apart from `(73,83)`, which goes through - X83's dimension-4 frame. A changed cover must supply such a type for every - missing entry; relaxing the cover (R2) does this at support level. The first priced data - point is pending #3618's T48, which corrects a whole target row on one - target lift for +2 rank mass by changing the target's path rather than - the cover. Coefficients, dirt and every cost of a complete reopening - remain unknown. + target frame. Under the present cover the supported entries are exactly + those whose own slot pair is compatible, plus `(73,83)`, via X83's + dimension-4 frame. This describes the set, not the route: a review pass + found some supported entries also reached through other types (not + asserted by the verifier). A changed cover must supply such a type for every missing entry; + relaxing the cover (R2) does this at support level. Path changes alone + must touch at least 104 registers. The first priced data point is pending + #3618's T48, which corrects a whole target row on one target lift for +2 + rank mass by changing the target's path rather than the cover. Whether + such costs add up across rows, and the coefficients, dirt and every cost + of a complete reopening, remain unknown. 3. *Is there a non-trivial use of channel state?* R1c and R3 reopen everything only because the channel already carries `G/2`. One would need a coefficient-level construction that reads channel state and restores it, @@ -277,7 +319,8 @@ The selected cold replay is unchanged and was not rerun. - commdata2338: PR3214 `faa6323371db1c5fbb43ab04c6e00715d2328bc6` (output repair). - Jose Manuel (jmbarrancoml): PR3427 `344774ba08a73fc3a85fdcb93fb319927bde3ea2` - (the one-helper lemma and the rank-four theorem extended here). + (the one-helper criterion and its untimed exactness, the four-column masks + and the rank-four theorem extended here). - James Reed (jwr404): the merged #3497-#3519 series (heads `a8804afd46ee63b202291ab3bcebd1eb2b83ecfc` through `d8928dd94a3450c5145a847507e7fb466dbc5c00`) already reproduced the X102 diff --git a/research/p104-fixed-cover-cut-review/TASK.json b/research/p104-fixed-cover-cut-review/TASK.json index 55a4a0b679..9aa6ff7de1 100644 --- a/research/p104-fixed-cover-cut-review/TASK.json +++ b/research/p104-fixed-cover-cut-review/TASK.json @@ -68,25 +68,25 @@ ] }, "scope_status": "changed", - "actual_scope": "Independent hypothesis-by-hypothesis review of the PR3259 fixed-cover support-cut embedding argument (and PR3252's memory-relaxation proof, and what PR3427 consumes), with a sharper valid criterion (one recombined helper per path, exact for the pooled untimed relaxation), its finite P104 consequences, single-relaxation support rows and a small-domain exhaustive check. Audit only; author-checked and AI-assisted.", + "actual_scope": "Independent hypothesis-by-hypothesis review of the PR3259 fixed-cover support-cut embedding argument (and PR3252's memory-relaxation proof, and what PR3427 consumes). PR3427's one-recombined-helper criterion (which PR3427 already calls exact for the pooled untimed relaxation) is re-proved and evaluated on all 104 columns, with its closed form, vertex cover and rank consequences, single-relaxation support rows and a small-domain exhaustive check. Audit only; author-checked and AI-assisted.", "scope_change_reason": "The card asks for a chronological correction program. The revision-6 decisions table (row 1) instead asks first for a review of the submitted #3259 support cut and its contract, which decides whether the fixed-cover route is closed and what any reopening must cover. No construction is attempted.", "bottleneck_link": "Decides whether the pooled fixed-cover, frozen-path, immutable-X, unread-Y, independent-dirt, monotone equal-frame P104 contract is closed and how large its obstruction is (2,682 unsupported required entries, not one), which bounds what a contract change or source preconditioner must reopen before any construction round.", "budget_minutes": 150, "stop_rule": "Stop at a proof-review verdict per step; on an engine disagreement, a proof gap or an oracle escape, stop and minimize. No matching search, no correction construction, no pricing beyond counting witness operations, at most three new relaxation rows, no Lean.", "outcome": "completed", - "evidence": "PROOF-REVIEW.md (step table a-h, lemma proof, PR3252 review, PR3427 consumption, rank consequence, load-bearing rows); verify.py (exact channel run: Y increment = G/2; layered control reproducing PR3259 numbers; sharp support by one criterion in two loop orders and by an independent PR3252 full-memory recurrence over all 104 columns, all equal, shape = 2,309 own port pairs + (73,83); PR3427 four-column masks; rank(U-I)>=17 by Fraction elimination and a Bareiss minor; rows R1/R1u/R1c/R2/R3; 9,000 seeded small instances with exhaustive untimed reachability, 13,242 realized checked programs and 18,000 random checked programs, exact Fractions; six negative controls); test_verify.py (seven controls).", + "evidence": "PROOF-REVIEW.md (step table a-h, lemma proof, PR3252 review, PR3427 consumption, rank consequence, load-bearing rows); verify.py (exact channel run of 4,058 events: Y increment = G/2; layered control reproducing PR3259 numbers; sharp support by one criterion in two loop orders and by an independent PR3252 full-memory recurrence over all 104 columns, all equal, shape = 2,309 own port pairs + (73,83); PR3427 four-column masks, which exclude 92 required entries that PR3259's test grants; perfect matching of the 2,682 missing entries (vertex cover 104); rank(U-I)>=23 from a maximum independent 23x23 principal block, size checked by two exact searches, rank by Fraction elimination, det(2C[S,S])=2^30 by Bareiss; rows R1/R1u/R1c/R2/R3; 9,000 seeded small instances with exhaustive untimed reachability, 13,242 realized checked programs and 18,000 random checked programs, exact Fractions; six in-verifier contract-violation controls); test_verify.py (seven tests: four defect controls with their own FAIL messages and three fact checks).", "author": "Sagar Thakrar (thakrarsagar)", "ai_assistance": "Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) for analysis, code and writing. No independent human or formal-kernel review is claimed.", "open_questions": [ { "question": "What rank does the full unsupported pattern force on a P104 source preconditioner (U-I)?", - "why_it_matters": "A greedy rectangle already gives rank(U-I)>=17 versus PR3427's 4; a min-rank completion of -C on all 8,506 unsupported pairs may force more and would further constrain joint native source preparation.", - "first_step": "Bound the min-rank completion exactly (larger or overlapping rectangles, or a min-rank argument) with the pinned sharp support; no matching search.", + "why_it_matters": "A maximum unsupported principal block already gives rank(U-I)>=23 versus PR3427's 4, and no principal block does better; a non-principal rectangle or a min-rank completion of -C on all 8,506 unsupported pairs may force more and would further constrain joint native source preparation.", + "first_step": "Bound the min-rank completion exactly (non-principal or overlapping rectangles, or a min-rank argument) with the pinned sharp support; no matching search.", "blocked_by": "Nothing beyond the sharp support certificate here; pricing a joint preparation remains separate." }, { "question": "Which changed contract reopens all 2,682 sharp-missing entries at least cost, and what is its full bill?", - "why_it_matters": "Under the present cover an entry is supported only through its own compatible slot pair (apart from (73,83)); relaxing the cover (R2) reopens every entry at support level, but its cost is unknown. Pending #3618's T48 (one target lift, +2 rank mass, a whole row) changes the target path instead and is the first priced data point.", + "why_it_matters": "Under the present cover the supported entries are exactly those whose own slot pair is compatible, plus (73,83); relaxing the cover (R2) reopens every entry at support level, but its cost is unknown. The missing entries need a vertex cover of 104, so path changes alone must touch at least 104 registers. Pending #3618's T48 (one target lift, +2 rank mass, a whole row) changes the target path instead and is the first priced data point; additivity across rows is not established.", "first_step": "Name the changed hypothesis among K1-K7 (or added storage), cover the 2,682 entries at support level, and list each added operation.", "blocked_by": "Coefficients, dirty restoration, chronology, native/hosting/precision/consumer costs are unknown." }, diff --git a/research/p104-fixed-cover-cut-review/VERIFY.json b/research/p104-fixed-cover-cut-review/VERIFY.json index 2b15477562..aebc916a1e 100644 --- a/research/p104-fixed-cover-cut-review/VERIFY.json +++ b/research/p104-fixed-cover-cut-review/VERIFY.json @@ -19,7 +19,7 @@ "{package}/verify.py" ], "timeout_seconds": 600, - "checks": "Exact channel run (Y increment = G/2); PR3259 layered control; sharp support by one criterion in two loop orders and PR3252 full-memory recurrence (all equal; 2,309 own port pairs + (73,83)); PR3427 masks; rank(U-I)>=17; rows R1/R1u/R1c/R2/R3; 9,000-instance small-domain oracle (exhaustive reachability, realized programs, 18,000 random programs); six negative controls" + "checks": "Exact channel run (Y increment = G/2); PR3259 layered control; sharp support by one criterion in two loop orders and PR3252 full-memory recurrence (all equal; 2,309 own port pairs + (73,83)); PR3427 masks; vertex cover 104 of the 2,682 missing entries; rank(U-I)>=23 from a maximum independent 23x23 block; rows R1/R1u/R1c/R2/R3; 9,000-instance small-domain oracle (exhaustive reachability, realized programs, 18,000 random programs); six contract-violation controls" }, { "argv": [ @@ -31,7 +31,7 @@ "{package}/test_verify.py" ], "timeout_seconds": 600, - "checks": "Seven negative controls: tampered hash, unsound and too-tight tests, shared-type and containment drops, wrong rectangle, Y-relay escape" + "checks": "Seven tests: tampered hash, unsound and too-tight oracle tests, wrong rank block (each with its own FAIL message); shared-type drop, containment drop (over-grants), Y-relay escape (fact checks)" } ] } diff --git a/research/p104-fixed-cover-cut-review/test_verify.py b/research/p104-fixed-cover-cut-review/test_verify.py index 747c9d18cd..20a7e95fd4 100644 --- a/research/p104-fixed-cover-cut-review/test_verify.py +++ b/research/p104-fixed-cover-cut-review/test_verify.py @@ -19,11 +19,12 @@ def result(): return _CACHE[0] -def fails(fn, *args): +def fails(why, fn, *args): + """True when fn stops with the FAIL message that names `why`.""" try: fn(*args) except SystemExit as exc: - return str(exc).startswith("FAIL") + return str(exc).startswith("FAIL: " + why) return False @@ -31,7 +32,7 @@ class Controls(unittest.TestCase): def test_tampered_input_hash(self): bad = {k: "0" * 64 for k in V["INPUTS"]} with mock.patch.dict(V["load"].__globals__["INPUTS"], bad): - self.assertTrue(fails(V["load"])) + self.assertTrue(fails("input hash", V["load"])) def test_oracle_rejects_an_unsound_test(self): # A test that grants only shared snapshots misses helper paths. @@ -39,7 +40,8 @@ def test_oracle_rejects_an_unsound_test(self): with mock.patch.dict(g, {"small_sharp": lambda inst: { (t, s) for s, xc in enumerate(inst[1]) for t, yc in enumerate(inst[2]) if set(xc) & set(yc)}}): - self.assertTrue(fails(V["oracle"], 7, ((3, 400),), 120)) + self.assertTrue(fails("oracle: exhaustive untimed support differs", + V["oracle"], 7, ((3, 400),), 120)) def test_oracle_rejects_a_too_tight_exhaustive_search(self): # An exhaustive search that never switches helper type misses the @@ -47,7 +49,8 @@ def test_oracle_rejects_a_too_tight_exhaustive_search(self): g = V["unpooled_relay_example"].__globals__ with mock.patch.dict(g, {"small_exact": lambda inst: ( V["small_sharp"](inst), {})}): - self.assertTrue(fails(V["unpooled_relay_example"])) + self.assertTrue(fails("pooling is needed", + V["unpooled_relay_example"])) def test_dropping_shared_type_breaks_pr3427_masks(self): # Pairing a source snapshot and a target snapshot that are each @@ -69,9 +72,9 @@ def test_dropping_shared_type_breaks_pr3427_masks(self): for s in range(4)] self.assertNotEqual(tuple(got), g["PR3427_SOURCE_MASKS"]) - def test_dropping_containment_is_unsound_in_principle(self): + def test_dropping_containment_loses_exactness_in_principle(self): # Containment V <= W is not decisive at P104 (verify.py checks this), - # but it is needed in general. F_2^4, one pooled type with line + # but without it the test over-grants: it stays sound, not exact. F_2^4, one pooled type with line # and hyperplane : X0 passes the admitted plane , # Y0 the admitted plane , and no path joins them. key = V["key"] @@ -83,12 +86,19 @@ def test_dropping_containment_is_unsound_in_principle(self): self.assertTrue(V["small_admit"](ty, v) and V["small_admit"](ty, w)) self.assertNotIn((0, 0), V["small_exact"](inst)[0]) self.assertNotIn((0, 0), V["small_sharp"](inst)) + # A test without containment grants the unreachable pair (0,0). + self.assertTrue(V["small_admit"](ty, v) and V["small_admit"](ty, w) + and not V["le"](v, w)) - def test_wrong_rectangle_is_rejected(self): + def test_wrong_rank_block_is_rejected(self): + # The block is a maximum independent set, so any added port meets a + # supported pair; a shrunk block fails the size-23 check. g = V["rank_consequence"].__globals__ r = result() - with mock.patch.dict(g, {"RANK_ROWS": g["RANK_ROWS"] + (71,)}): - self.assertTrue(fails(V["rank_consequence"], r)) + for bad, why in ((g["MIS_BLOCK"] + (45,), "principal block"), + (g["MIS_BLOCK"][1:], "maximum independent set")): + with mock.patch.dict(g, {"MIS_BLOCK": bad}): + self.assertTrue(fails(why, V["rank_consequence"], r)) def test_y_relay_counterexample_is_a_real_escape(self): self.assertEqual(V["y_relay_counterexample"](), (1, True)) diff --git a/research/p104-fixed-cover-cut-review/verify.py b/research/p104-fixed-cover-cut-review/verify.py index 26b1ea0b45..ed19bb29ed 100644 --- a/research/p104-fixed-cover-cut-review/verify.py +++ b/research/p104-fixed-cover-cut-review/verify.py @@ -14,6 +14,8 @@ instance, an explicit checked program for every reachable helper pair, and random checked programs, all with exact Fraction coefficients. ROWS single-relaxation support rows (unpriced; operations counted). + RANK a maximum unsupported principal block of C (rank(U-I) >= 23 under + PR3427's contract) and the matching number of the missing entries. """ import hashlib @@ -490,6 +492,7 @@ def p104(): roles = channel_roles(word) geo = covers(cert, paths) C = required(e8_ports(fixture)) + need(len(word["program"]) == 4058, "4,058 channel events") hist, first = channel_run(word, C) lay, fwd, back, f5 = layered(geo, paths) miss_l = missing(C, lay) @@ -500,6 +503,9 @@ def p104(): need(sharp == sharp_by_edges(geo, paths), "sharp criterion: two loop orders") need(sharp == full_memory(geo, paths), "PR3252 full-memory test = sharp") need(all(sharp[t] & ~lay[t] == 0 for t in range(104)), "sharp <= layered") + # A target path that reaches FULL would share it with every source. + need(all(len(paths["X%d" % s][-1]) == 9 for s in range(104)), + "every X path ends at FULL") need(not any(set(paths["X%d" % s]) & set(paths["Y%d" % t]) for s in range(104) for t in range(104)), "no X path shares a frame with a Y path") @@ -517,6 +523,7 @@ def p104(): return {"roles": roles, "geo": geo, "paths": paths, "C": C, "layered": lay, "sharp": sharp, "missing_layered": miss_l, "missing_sharp": missing(C, sharp), "forward": fwd, + "backward": bin(back).count("1"), "hist": hist, "first_Y71_X102": first} @@ -567,6 +574,10 @@ def relay(seed, ordered=True): cap = j == len(paths["Y%d" % t]) - 1 arrivals[(len(w), cap)] = arrivals.get((len(w), cap), 0) + \ bin(xin[(t, j)]).count("1") + lower = {} # target snapshots below the cap that receive content + for t, j, w in ys: + if xin[(t, j)] and j < len(paths["Y%d" % t]) - 1: + lower[len(w)] = lower.get(len(w), 0) + 1 need(all(xin[(t, len(paths["Y%d" % t]) - 1)] == r["sharp"][t] for t in range(104)), "every supported pair arrives at the cap") need(len({paths["Y%d" % t][-1] for t in range(104)}) == 104, @@ -594,6 +605,7 @@ def relay(seed, ordered=True): return {"R1_correction_only_Y_relay": count(r1), "R1u_without_target_order": count(r1u), "R1_arrivals_dim_cap": sorted(arrivals.items()), + "R1_lower_snapshots_by_dim": sorted(lower.items()), "R1c_Y_relay_with_channel_content": count(r1c), "R2_free_nested_flags": count(free), "R3_old_channel_helper_reads": count(r3), @@ -633,54 +645,94 @@ def bareiss_det(m): return sign * a[n - 1][n - 1] -def greedy_rectangle(sharp, C): - """Deterministic greedy: for each seed column grow S while the common - unsupported row set R keeps min(|R|,|S|) increasing; keep max rank.""" - n = len(C) - uns = [[not sharp[t] >> s & 1 for s in range(n)] for t in range(n)] - best = (0, (), ()) - for s0 in range(n): - S, R = [s0], [t for t in range(n) if uns[t][s0]] - while True: - cand = sorted(((min(len(r2), len(S) + 1), len(r2), -s, r2) - for s in range(n) if s not in S - for r2 in [[t for t in R if uns[t][s]]]), - reverse=True) - if not cand or cand[0][0] <= min(len(R), len(S)): - break - S.append(-cand[0][2]) - R = cand[0][3] - rk = frac_rank([[C[t][s] for s in S] for t in R]) - if rk > best[0]: - best = (rk, tuple(sorted(R)), tuple(sorted(S))) - return best - - -RANK_ROWS = (2, 4, 5, 13, 15, 25, 32, 36, 39, 48, 52, 73, 76, 82, 87, 89, - 94, 98, 102) -RANK_COLS = (2, 5, 11, 13, 15, 16, 20, 25, 28, 32, 40, 48, 61, 65, 76, 84, - 94, 102) -MINOR_ROWS = (2, 4, 5, 13, 15, 25, 32, 36, 39, 48, 52, 73, 76, 82, 87, 94, - 102) -MINOR_COLS = (2, 5, 11, 13, 15, 16, 20, 25, 28, 32, 40, 48, 61, 65, 76, 94, - 102) +def max_clique(adj): + """Exact maximum clique size: branch and bound with a greedy colouring + bound (vertex sets are bitmasks).""" + best = [0] + + def expand(size, P): + order, U, col = [], P, 0 + while U: + col, Q = col + 1, U + while Q: + v = (Q & -Q).bit_length() - 1 + Q &= ~adj[v] & ~(1 << v) + U &= ~(1 << v) + order.append((col, v)) + for col, v in reversed(order): + if size + col <= best[0]: + return + if P & adj[v]: + expand(size + 1, P & adj[v]) + best[0] = max(best[0], size + 1) + P &= ~(1 << v) + expand(0, (1 << len(adj)) - 1) + return best[0] + + +def max_clique_bk(adj): + """Second exact method: Bron-Kerbosch with pivoting and a size bound.""" + best = [0] + + def bk(size, P, X): + if not P: + best[0] = max(best[0], size) + return + if size + bin(P).count("1") <= best[0]: + return + piv = max((v for v in range(len(adj)) if (P | X) >> v & 1), + key=lambda v: bin(P & adj[v]).count("1")) + cand = P & ~adj[piv] + while cand: + v = (cand & -cand).bit_length() - 1 + cand &= cand - 1 + bk(size + 1, P & adj[v], X & adj[v]) + P &= ~(1 << v) + X |= 1 << v + bk(0, (1 << len(adj)) - 1, 0) + return best[0] + + +MIS_BLOCK = (8, 11, 17, 18, 23, 30, 34, 37, 42, 50, 51, 58, 59, 63, 70, 71, + 78, 80, 84, 87, 91, 96, 100) def rank_consequence(r): """Any D = U^-1 - G/2 vanishes on unsupported pairs, so on an unsupported - rectangle (U^-1 - I)[R,S] = -C[R,S] and rank(U - I) >= rank C[R,S].""" - sharp, C = r["sharp"], r["C"] - need(all(not sharp[t] >> s & 1 for t in RANK_ROWS for s in RANK_COLS), - "rectangle unsupported") - need(greedy_rectangle(sharp, C) == (17, RANK_ROWS, RANK_COLS), - "greedy rectangle") - rk = frac_rank([[C[t][s] for s in RANK_COLS] for t in RANK_ROWS]) - det = bareiss_det([[int(8 * C[t][s]) for s in MINOR_COLS] - for t in MINOR_ROWS]) - need(rk == 17 and det != 0, "rank 17 by elimination and a nonzero minor") + rectangle (U^-1 - I)[R,S] = -C[R,S] and rank(U - I) >= rank C[R,S]. + A principal block C[S,S] is unsupported exactly when S is independent in + the undirected support graph (diagonal pairs are never supported).""" + sharp, C, S = r["sharp"], r["C"], MIS_BLOCK + need(all(not sharp[t] >> s & 1 for t in S for s in S), + "principal block unsupported") + free = [sum(1 << s for s in range(104) if s != t and not ( + sharp[t] >> s & 1 or sharp[s] >> t & 1)) for t in range(104)] + need(max_clique(free) == max_clique_bk(free) == len(S) == 23, + "maximum independent set has size 23 by two exact searches") + rk = frac_rank([[C[t][s] for s in S] for t in S]) + det = bareiss_det([[int(2 * C[t][s]) for s in S] for t in S]) + need(rk == 23 and det == 2 ** 30, + "rank 23 by elimination and det(2C[S,S]) = 2^30") return rk, det +def matching_number(pairs, n=104): + """Maximum bipartite matching (Kuhn); equals the minimum vertex cover.""" + adj, match = [[] for _ in range(n)], [-1] * n + for t, s in pairs: + adj[t].append(s) + + def augment(t, seen): + for s in adj[t]: + if s not in seen: + seen.add(s) + if match[s] < 0 or augment(match[s], seen): + match[s] = t + return True + return False + return sum(augment(t, set()) for t in range(n)) + + # ------------------------------------------------- small-domain oracle class Rng: """Deterministic LCG so the oracle needs no stdlib random state.""" @@ -1269,6 +1321,16 @@ def main(): need(len(zero_off) == 5720 and all(lay[t] >> s & 1 for t, s in zero_off) and all(lay[t] >> t & 1 for t in range(104)), "PR3259's test grants all 5,720 zero off-diagonal and 104 diagonal pairs") + need(sum(1 for t, s in ms if s < 4) == 92 and all( + lay[t] >> s & 1 for t, s in ms if s < 4), + "PR3427's masks exclude 92 required entries that PR3259's test grants") + rows_hit = [sum(1 for t, _ in ms if t == u) for u in range(104)] + cols_hit = [sum(1 for _, s in ms if s == u) for u in range(104)] + cover = matching_number(ms) + need(cover == 104 and min(rows_hit) == 14 and min(cols_hit) == 9, + "missing entries: perfect matching (vertex cover 104), " + "row min 14, column min 9") + need(r["backward"] == 37, "backward cone 37") need(r["first_Y71_X102"] == [3378, "1/2", "D11", 5], "channel's first X102 delivery into Y71") rw = rows(r) @@ -1276,6 +1338,8 @@ def main(): need(rw["R1u_without_target_order"] == (2682, True), "R1u") need(rw["R1_arrivals_dim_cap"] == [((5, False), 31), ((6, False), 24), ((8, True), 2310)], "R1 arrivals") + need(rw["R1_lower_snapshots_by_dim"] == [(5, 19), (6, 7)], + "R1 lower arrivals sit on 19 + 7 target snapshots") need(rw["R1c_Y_relay_with_channel_content"] == (2682, True), "R1c") need(rw["R2_free_nested_flags"] == (2682, True), "R2") need(rw["R3_old_channel_helper_reads"] == (2682, True), "R3") @@ -1289,16 +1353,29 @@ def main(): print(json.dumps({"channel_roles": r["roles"], "layered_missing": r["missing_layered"], "forward_cone": r["forward"], "channel_first_Y71_X102": r["first_Y71_X102"], - "rank_bound": rk, "minor_det_8C": det, + "rank_bound": rk, "mis_block": MIS_BLOCK, + "det_2C_block": det, "sharp_missing": len(ms), "sharp_missing_by_value": by_value, "layered_grants_sharp_missing": reopened, - "unsupported_pairs": 8506, "sharp_support": - "2309 own port pairs + [73,83]", "rows": rw, + "counts": { + "pairs": len(pairs), "required_entries": 4992, + "channel_events": 4058, + "sharp_supported_pairs": 2310, + "layered_supported_pairs": 10815, + "unsupported_pairs": 8506, + "own_port_pairs": 2309, "extra_pair": [73, 83], + "layered_zero_off_diagonal": len(zero_off), + "layered_diagonal": 104, "backward_cone": + r["backward"], "pr3427_cols_0_3_missing": 92, + "missing_vertex_cover": cover, + "missing_row_min": min(rows_hit), + "missing_col_min": min(cols_hit)}, + "rows": rw, "oracle": checked, "negative_controls": escapes}, sort_keys=True)) print("PASS_P104_FIXED_COVER_CUT_REVIEW layered_missing=1 " - "sharp_missing=2682 of 4992 pr3427_masks=4 rank_U_minus_I>=17 " - "rows=5 oracle_instances=%d oracle_programs=%d no_kappa" % ( + "sharp_missing=2682 of 4992 pr3427_masks=4 rank_U_minus_I>=23 " + "vertex_cover=104 rows=5 oracle_instances=%d oracle_programs=%d no_kappa" % ( sum(n for _, n in ORACLE_TRIALS) * 2, checked["programs"] + checked["unpooled_programs"])) From 038aaddd51a050bd9553cd9fbd8fc72f4fed29e0 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Mon, 19 Oct 2026 03:01:58 +0530 Subject: [PATCH 9/9] Address round-3 review of the P104 fixed-cover cut review Assert three facts the reviews raised: 32 supported pairs are admitted by a non-own type (31 own pairs, plus (73,83), which only type (17,147) admits from X83's dimension-4 frame to Y73's cap); rank(G/2) = 8, so any unsupported rectangle has rank at most 31; and a containment-free probe of the small-domain test grants an unreachable pair (the containment test now evaluates it). Wording: define the sharp criterion in the Statement; the multi-hop check is new in extent only; state PR3427's code-level use of PR3259's geometry and its one-shear replay; split the 18,000 random programs into 9,000 interpreter-checked and 9,000 legal by construction; five rows over three hypotheses, with the stop-rule deviation recorded; a reopening must support all 4,992 required entries; perfect-matching wording in PROOF-REVIEW; ten AI review passes over three rounds; rewrap long prose lines. Co-Authored-By: Claude Opus 5.5 --- .../PROOF-REVIEW.md | 87 +++++++++------ .../p104-fixed-cover-cut-review/README.md | 103 ++++++++++-------- .../p104-fixed-cover-cut-review/TASK.json | 12 +- .../p104-fixed-cover-cut-review/VERIFY.json | 4 +- .../test_verify.py | 13 ++- .../p104-fixed-cover-cut-review/verify.py | 47 ++++++-- 6 files changed, 169 insertions(+), 97 deletions(-) diff --git a/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md b/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md index 8a26fd69e9..cb51491659 100644 --- a/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md +++ b/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md @@ -17,8 +17,8 @@ proves no P104 impossibility outside the stated contract. ## Verdict -These verdicts come from an author-checked, AI-assisted review. Seven AI -review passes in the same loop, over two rounds, checked the package; no +These verdicts come from an author-checked, AI-assisted review. Ten AI +review passes in the same loop, over three rounds, checked the package; no independent human or formal-kernel review has been done. 1. **PR3259's argument is valid as a necessary support test under its stated @@ -30,16 +30,17 @@ independent human or formal-kernel review has been done. Reinstating that fact gives a valid criterion with **one recombined helper per path**. That lemma is stated in PR3427 and is re-proved below with every dimension case. Under it, **2,682 of the 4,992 required entries are - unsupported**, with at least one in every row and every column. PR3259's - relaxation grants 10,815 source/target pairs, against 2,310 for the sharp - criterion. "Exactly one missing coefficient" describes PR3259's test, not the - contract. PR3259 itself says that passing its test is not a realization. + unsupported**, containing a perfect matching (at least 14 per row and 9 + per column). PR3259's relaxation grants 10,815 source/target pairs, + against 2,310 for the sharp criterion. "Exactly one missing coefficient" + describes PR3259's test, not the contract. PR3259 itself says that passing its test is not a realization. PR3427 already states this criterion and its untimed exactness, and its published masks for sources 0-3 already exclude 92 required entries that PR3259's test grants. What is new here is the step-by-step review, the - full 104-column count with its closed form, a multi-hop check that does - not assume the lemma, the rank and vertex-cover consequences, and the - rows R1-R3. + full 104-column count with its closed form, a multi-hop (PR3252 + full-memory) check over all 104 columns and 2,309 types that does not + assume the lemma (PR3427 ran the same operations on its four columns), + the rank and vertex-cover consequences, and the rows R1-R3. 3. Consequently the fixed-cover contract is closed by a much larger obstruction than one coefficient. A contract change that only reopens `C[71,102]` does not complete the correction. Examples are PR3427's rank-one source shear, a @@ -183,12 +184,15 @@ such pairs. precision can be tested. On 4,500 unpooled instances the same search finds 33 pairs on 26 instances outside the one-helper test, each realized by a legal program, so the check has teeth. The 9,000 random pooled programs - (1,043 nonzero coefficients counted per program, 604 of them on pairs whose - X and Y chains share no frame) are a soundness sample only; on unpooled - instances they found none of the 33 escapes. + (4,500 directed programs run in the checked interpreter and 4,500 uniform + programs legal by construction; 1,043 nonzero coefficients counted per + program, 604 of them on pairs whose X and Y chains share no frame) are a + soundness sample only; on unpooled instances they found none of the 33 + escapes. - **P104.** A new implementation of PR3252's multi-hop full-memory - recurrence, which does not assume the lemma, gives the same support on all - 10,816 pairs. + recurrence over all 104 columns, which does not assume the lemma, gives the + same support on all 10,816 pairs. PR3427 ran the same operations on its + four columns. *Converse (untimed).* If the condition holds, one helper of type `(a,b)` with that full flag reads `X_s` at V and writes `Y_t` at W. With the relative timing @@ -215,7 +219,7 @@ delivers a nonzero coefficient outside both PR3259's test and the sharp test. | Quantity | PR3259 layered test | Sharp one-helper criterion | |---|---:|---:| | Supported source/target pairs | 10,815 | 2,310 | -| Required entries unsupported | 1 (`(71,102)`) | 2,682 (every row and column) | +| Required entries unsupported | 1 (`(71,102)`) | 2,682 (a perfect matching; at least 14 per row, 9 per column) | | Values of unsupported entries | `-1/2` | 1,801 at `-1/2`, 881 at `+1/2` | | Pairs granted with `C = 0` | 5,720 off-diagonal and 104 diagonal | none | @@ -228,10 +232,12 @@ PR3252's full-memory recurrence over the whole pool. All three agree on all The sharp support has a simple shape. It is exactly the 2,309 compatible slot pairs `(a,b)` read as port pairs (target `b//2`, source `a//2`), which are distinct and all required, plus the pair `(73,83)`. That extra pair comes from -a dimension-4 frame of X83 admitted, with Y73's cap, by one pool type. Hence -`2,682 = 4,992 - 2,309 - 1`. At P104 no X path shares a frame with a Y path, -and dropping the containment `V <= W` changes no pair, so containment is never -decisive here. The verifier asserts each of these facts. +a dimension-4 frame of X83 admitted, with Y73's cap, by one pool type, +`(17,147)`, and by no other. Each own pair is admitted by its own type, and 31 +of them also by another type. Hence `2,682 = 4,992 - 2,309 - 1`. At P104 no X +path shares a frame with a Y path, and dropping the containment `V <= W` +changes no pair, so containment is never decisive here. The verifier asserts +each of these facts. The 2,682 missing entries contain a perfect matching: Kuhn's augmenting-path matching has size 104, so by König's theorem no fewer than 104 rows and @@ -242,8 +248,9 @@ K6, K7 and the K4/K5 roles and changes only individual X or Y frame paths must change at least 104 of them. This makes no cost claim. For sources 0-3 the per-source target masks equal PR3427's published masks -exactly. They exclude 92 required entries, all granted by PR3259's test. Those masks come from PR3427's direct criterion and from PR3252's -full-memory operations. +exactly. They exclude 92 required entries, all granted by PR3259's test. +Those masks come from PR3427's direct criterion and from PR3252's full-memory +operations. ## PR3252 PROOF.md (shorter review) @@ -276,9 +283,9 @@ and all 104 sources (`full_memory` in the verifier) **equals the sharp criterion on every pair**: 2,310 supported pairs and the same 2,682 unsupported required entries. The 2,682 count therefore rests on two separately proved sound tests, computed by different algorithms. The one-step mode forgets the memory bound -and is weaker; it was not run. PR3252's finite checks use fixed matchings and F_2^3 -interval fixtures. The proof is universal over its contract, and no gap was -found. +and is weaker; it was not run. PR3252's finite checks use fixed matchings and +F_2^3 interval fixtures. The proof is universal over its contract, and no gap +was found. ## What PR3427 consumes @@ -289,6 +296,13 @@ found. - It cites PR3259 for the 2,309-pair pool and as the motivation for the one-shear candidate at `(71,102)`. It does not need PR3259's recurrence to be correct or sharp. +- At code level it depends on PR3259 more than the citation suggests. Both of + its methods execute PR3259's `verify.py` routines for inputs, frame paths, + endpoints, interval bounds and contacts. Its boundary check also replays + PR3259's layered recurrence and asserts that the missing set is exactly + `(71,102)`. That replay serves only the one-shear boundary; the rank + theorem does not depend on it. The independent engine here covers the + shared geometry code. - The consumption is justified. The lemma is valid, and the four-column masks are reproduced exactly by an engine that shares no code with PR3427. @@ -327,13 +341,20 @@ a pivoted Bron-Kerbosch). Exact `Fraction` elimination gives Thus `rank(U-I) >= 23` under PR3427's contract, against its published 4. This prices no joint preparation. No unsupported principal block does better; a non-principal rectangle or a min-rank completion may force more. +Rectangles alone cannot go past 31. On an unsupported rectangle, +`C[R,S] = I[R,S] - (G/2)[R,S]`; `R ∩ S` is independent, since each of its +pairs is unsupported in both orders, so `|R ∩ S| <= 23`; and +`rank(G/2) = 8` (asserted). Hence `rank C[R,S] <= |R ∩ S| + 8 <= 31`. ## Load-bearing hypotheses (support level, sharp criterion) The rows are support-level necessary-test relaxations. They are unpriced and -give no coefficient or dirty restoration. Each row relaxes one item. Like the -sharp criterion, they relax the relative timing of different registers but -keep the order of operations along one dependency path. +give no coefficient or dirty restoration. Each row relaxes one item. The five +rows R1, R1u, R1c, R2 and R3 relax three hypotheses: K5 in three variants +(R1u was added at a round-1 review's request), K1 and K6. The task's stop +rule planned at most three rows; TASK.json records the deviation. Like the +sharp criterion, the rows relax the relative timing of different registers +but keep the order of operations along one dependency path. | Relaxed item | Reaches `(71,102)` | Sharp-missing entries reopened | Minimal witness (operations counted, unpriced) | |---|---|---:|---| @@ -381,14 +402,16 @@ Known rows are cited, not recomputed: Reading. Among the rows computed here, two hypotheses each reopen every entry: the fixed cover (K1) and the exclusion of the channel's source-dependent state (K6, including its exposure through Y). Unread Y matters at P104 only through -that exposure, given each target's write-before-read order. The rows are not a -complete map. Not computed as rows at P104: frame descent (K2), cross-frame mixing -(K3), changed source or target frame paths and source mutation (K4, K5), -dependent dirt (K7) and extra correlated storage. The small-domain negative +that exposure, given each target's write-before-read order. The rows are not +a complete map. Not computed as rows at P104: frame descent (K2), cross-frame +mixing (K3), changed source or target frame paths and source mutation (K4, +K5), dependent dirt (K7) and extra correlated storage. The small-domain negative controls show that descent, cross-frame mixing, off-cover flags and correlated old state can each escape both tests. Changing a frozen target path also suffices at support level, one row at a time: every X path ends at FULL, so a target that visits FULL shares that frame with every source (pending #3618's T48 prices one such row at +2 rank mass). Path changes alone must touch at least 104 registers. A reopening must change at least one of K1-K7, or add -storage, and must cover all 2,682 entries with a full bill. +storage, and must support all 4,992 required entries, in particular the 2,682 +missing here, with a full bill; a changed cover or path can lose some of the +2,310 pairs supported now. diff --git a/research/p104-fixed-cover-cut-review/README.md b/research/p104-fixed-cover-cut-review/README.md index 2323d01556..11ee8c62fc 100644 --- a/research/p104-fixed-cover-cut-review/README.md +++ b/research/p104-fixed-cover-cut-review/README.md @@ -17,8 +17,9 @@ The 2,682 count rests on two sound tests that agree on all 10,816 source/target pairs: - PR3427's one-recombined-helper criterion, re-proved here in every - dimension case. It keeps the fact that PR3259's test discards: the frames - along a dependency path are nested. + dimension case (called the sharp criterion below; it is exact only for the + pooled untimed relaxation). It keeps the fact that PR3259's test discards: + the frames along a dependency path are nested. - PR3252's full-memory recurrence, whose proof is reviewed valid here, implemented anew over the whole pool. It is multi-hop and does not assume the lemma. @@ -33,11 +34,13 @@ implies that PR3259's test is not sharp. New here: - the criterion's full 104-column count, 2,682, with its closed form: the supported pairs are the 2,309 compatible slot pairs read as port pairs, plus `(73,83)`, so `2,682 = 4,992 - 2,309 - 1`; -- a multi-hop computation of the same support that does not assume the - lemma; +- a multi-hop computation of the same support with PR3252's full-memory + operations over all 104 columns and 2,309 types, which does not assume the + lemma (PR3427 ran the same operations on its four columns); - `rank(U-I) >= 23` under PR3427's own contract, against its published 4, from a fully unsupported, nonsingular 23-by-23 principal block; -- the 104 vertex cover and the single-relaxation rows R1-R3. +- the 104 vertex cover and the single-relaxation rows R1-R3 (five rows over + three hypotheses). PR3259's single missing entry, `C[71,102] = -1/2`, belongs to its looser relaxation. Under the criterion an entry's support depends only on the @@ -47,13 +50,13 @@ only individual X or Y frame paths, must change at least 104 of them. This makes no cost claim. This is an author-checked, AI-assisted audit: a scoped proof review, a finite -certificate and small-domain checks. Seven AI review passes in the same loop, -over two rounds (reproducibility, mathematics, provenance and referee; then -mathematics, reproducibility and referee), checked the package, and this -revision addresses their findings. No independent human or formal-kernel -review has been done. The audit constructs nothing and is not a -complete multiplication theorem. It proves no P104 impossibility outside the -stated contract, and κ and the selected frontier are unchanged. +certificate and small-domain checks. Ten AI review passes in the same loop, +over three rounds (reproducibility, mathematics, provenance and referee in +round 1; mathematics, reproducibility and referee in rounds 2 and 3), checked +the package, and this revision addresses their findings. No independent +human or formal-kernel review has been done. The audit constructs nothing and +is not a complete multiplication theorem. It proves no P104 impossibility +outside the stated contract, and κ and the selected frontier are unchanged. ## Results @@ -61,22 +64,25 @@ stated contract, and κ and the selected frontier are unchanged. |---|---| | PR3259 embedding argument, checklist a-h | Valid. Two implicit sentences are recorded as clarifications. See [PROOF-REVIEW.md](PROOF-REVIEW.md). | | PR3252 PROOF.md (memory relaxation) | Valid for its recurrence and contract. | -| What PR3427 consumes | Its own one-helper lemma and PR3252's full-memory operations, not PR3259's recurrence. Both are justified. | +| What PR3427 consumes | Its own one-helper lemma and PR3252's full-memory operations, not PR3259's recurrence. Both are justified. Its code executes PR3259's geometry and contact routines, shared by both of its methods, and replays PR3259's recurrence only for the one-shear boundary; the rank theorem does not depend on that recurrence, and this review's independent engine covers the shared geometry. | | Channel word, exact run | Every Y increment is exactly `G/2` in the sorted port order, with all helper dirt cancelled; every channel add is at equal frames. | | Control: PR3259 layered test, rebuilt | Missing set `{(71,102)}`. Forward counts `16,25,52,365,1725,2283,2285,2297`. Backward cone 37, disjoint. | | Sharp criterion: one criterion in two loop orders, plus PR3252's multi-hop recurrence | All three computations agree on every pair. 2,310 supported pairs, against 10,815 for PR3259's test. 2,682 required entries unsupported: 1,801 at `-1/2` and 881 at `+1/2`. 8,506 pairs unsupported in all. | -| Shape of the sharp support | Exactly the 2,309 compatible slot pairs `(a,b)` read as (target `b//2`, source `a//2`), all distinct and all required, plus `(73,83)`. All supported pairs are off-diagonal required entries. PR3259's test grants 2,681 of the 2,682 missing entries, all 5,720 zero off-diagonal pairs and all 104 diagonal pairs. | +| Shape of the sharp support | Exactly the 2,309 compatible slot pairs `(a,b)` read as (target `b//2`, source `a//2`), all distinct and all required, plus `(73,83)`. Each own pair is admitted by its own type, and 31 of them also by another type; `(73,83)` is admitted only by type `(17,147)`, from X83's dimension-4 frame to Y73's cap. All supported pairs are off-diagonal required entries. PR3259's test grants 2,681 of the 2,682 missing entries, all 5,720 zero off-diagonal pairs and all 104 diagonal pairs. | | Cover of the missing entries | A maximum matching of the 2,682 missing entries has size 104, so the minimum vertex cover is 104 (König). Missing entries per row: at least 14; per column: at least 9. | | Cross-check with PR3427 | The four published per-source masks (sources 0-3) are reproduced exactly. They exclude 92 required entries, all granted by PR3259's test. | | Consequence for PR3427 | A maximum independent set of the undirected support graph has 23 ports (two exact searches). Its 23-by-23 principal block is fully unsupported with `det(2C[S,S]) = 2^30`, so `rank C[S,S] = 23` and `rank(U-I) >= 23`. | | Small domains, pooled | 4,500 seeded `F_2^3`/`F_2^4` instances. On every one, an exhaustive untimed reachability, which does not assume the lemma, equals the one-helper test. Its 4,264 helper-only pairs are each realized by an explicit program in the checked interpreter. PR3259's test is strictly looser on 54 instances (75 pairs), and the exhaustive search confirms those pairs unreachable. | | Small domains, unpooled | 4,500 instances with six rigid types. The exhaustive support lies inside PR3259's test every time, and 8,978 helper-only pairs are realized. 33 pairs on 26 instances lie outside the one-helper test, each realized by a legal program: the lemma needs pooling. | -| Random programs | 18,000 seeded checked programs with exact `Fraction` coefficients, two per instance; all lie inside the exhaustive support. Pooled: 1,043 nonzero coefficients counted per program, 604 of them on pairs whose X and Y chains share no frame, and 633 (13 + 620) passed between helpers of different types. Unpooled: 1,887 coefficients. The random programs found none of the 33 unpooled escapes, so they are a soundness sample, not the evidence for the lemma. | +| Random programs | 18,000 seeded legal programs with exact `Fraction` coefficients, two per instance: 9,000 directed programs run in the checked interpreter and 9,000 uniform programs that are legal by construction (they choose only among legal operations and are not rerun in the interpreter). All lie inside the exhaustive support. Pooled: 1,043 nonzero coefficients counted per program, 604 of them on pairs whose X and Y chains share no frame, and 633 (13 + 620) passed between helpers of different types. Unpooled: 1,887 coefficients. The random programs found none of the 33 unpooled escapes, so they are a soundness sample, not the evidence for the lemma. | ### Which hypotheses carry the obstruction Each row relaxes one hypothesis and is checked at support level with the sharp criterion. The rows are unpriced and give no coefficient or dirty restoration. +The five rows relax three hypotheses: K5 in three variants (R1; R1u, added at +a round-1 review's request; R1c), K1 (R2) and K6 (R3). The task's stop rule +planned at most three rows; TASK.json records the deviation. | Relaxed hypothesis | Reaches `(71,102)` | Reopens, of 2,682 | |---|---|---:| @@ -110,9 +116,9 @@ and cost are unknown. Among the rows computed here, two hypotheses each reopen every entry: the fixed cover (K1) and the exclusion of the channel's source-dependent state (K6, with its exposure through Y). The rows are not a complete map. Not -computed as rows at P104: frame descent (K2), cross-frame mixing (K3), changed source -or target frame paths and source mutation (K4, K5), dependent dirt (K7) and -extra correlated storage. The small-domain controls show that descent, +computed as rows at P104: frame descent (K2), cross-frame mixing (K3), changed +source or target frame paths and source mutation (K4, K5), dependent dirt (K7) +and extra correlated storage. The small-domain controls show that descent, cross-frame mixing, off-cover flags and correlated old state can each escape both tests. Changing a frozen target path also suffices at support level, one row at a time: every X path ends at FULL, so a target that visits FULL shares @@ -121,7 +127,9 @@ adds (pending #3618's T48 prices one such row at +2 rank mass). Path changes alone must touch at least 104 registers (the vertex cover above). Under PR3427's preconditioner contract, which relaxes K4, a source preconditioner needs `rank(U-I) >= 23`. Any reopening must change at least one of K1-K7, or -add storage, and must cover all 2,682 entries with a full bill. +add storage, and must support all 4,992 required entries, in particular the +2,682 missing here, with a full bill. A changed cover or path can lose some of +the 2,310 pairs supported now. The 2,682 count binds only corrections that keep the fixed cover, the frozen X and Y frame paths and the untouched channel state. Routes that change any of @@ -140,8 +148,9 @@ change something K1-K7 freeze, so they lie outside this contract and do not conflict with its closure. - Wentao Li (VictorLiwentao) prices single-entry and whole-row `I - G/2` - corrections on the published word: #3601 (`26394881f0a183ca0df3d986ec58aa56900ada6c`), - #3610 (`4352496b3aa56ad17446ddbd1d78931f3d392996`) and #3618 + corrections on the published word: #3601 + (`26394881f0a183ca0df3d986ec58aa56900ada6c`), #3610 + (`4352496b3aa56ad17446ddbd1d78931f3d392996`) and #3618 (`0c4b73507ba7ed7b992e47b17f2cbcb6e362466b`). Their words lift a target's frame (changes the frozen Y path, outside K5), detour a source (changes the frozen X path, outside K4), add a private-copy lifetime (extra storage, @@ -196,8 +205,9 @@ It also checks three facts: - dropping the shared-helper-type requirement changes PR3427's masks; - dropping containment `V <= W` over-grants on a fixed `F_2^4` instance: the - test stays sound but is no longer exact (at P104 containment is never - decisive, which `verify.py` asserts); + containment-free variant grants a pair that the exhaustive search shows + unreachable, so the test stays sound but is no longer exact (at P104 + containment is never decisive, which `verify.py` asserts); - the fixed Y-relay program is a real escape. Inside `verify.py`, five contract violations must each produce a coefficient @@ -232,7 +242,8 @@ independently and sorted. `rank C[S,S] = 23`, and an integer Bareiss determinant gives `det(2C[S,S]) = 2^30`, so `det C[S,S] = 2^7`. No unsupported principal block is larger; a non-principal rectangle or a min-rank argument could - give more, so 23 is a lower bound. + give more, so 23 is a lower bound. A rectangle can give at most 31, + because `rank(G/2) = 8` (asserted; see open question 1). - Kuhn's augmenting-path matching on the 2,682 missing entries gives size 104, a perfect matching, so by König's theorem every set of rows and columns covering them has at least 104 members. @@ -248,9 +259,11 @@ independently and sorted. then turned into an explicit program, one helper per step, and run in the checked interpreter. - Each instance also runs two random programs. One chooses uniformly among - the operations legal at each moment, for 120 operations; the other - follows a random path through one to three relays. Direct X-to-Y adds - are omitted from them, so every coefficient travels through helpers. + the operations legal at each moment, for 120 operations; it is legal by + construction and is not run in the interpreter. The other follows a + random path through one to three relays and is run in the checked + interpreter. Direct X-to-Y adds are omitted from both, so every + coefficient travels through helpers. - The interpreter checks flags of the right type, ascending transports, and equal-frame reads, adds and writes. - The verifier also checks the roles in the original channel word: X is @@ -285,22 +298,26 @@ The selected cold replay is unchanged and was not rerun. 1. *Is 23 the true rank bound?* 23 is optimal among principal blocks. A non-principal unsupported rectangle, or a min-rank completion of `-C` on - all 8,506 unsupported pairs, may force more. A larger rank would further - constrain any joint native source preparation under PR3427's contract. It - needs no new matching search. -2. *Which changed contract reopens all 2,682 entries at least cost?* An entry - is supported when one helper type admits a source frame and a nested - target frame. Under the present cover the supported entries are exactly - those whose own slot pair is compatible, plus `(73,83)`, via X83's - dimension-4 frame. This describes the set, not the route: a review pass - found some supported entries also reached through other types (not - asserted by the verifier). A changed cover must supply such a type for every missing entry; - relaxing the cover (R2) does this at support level. Path changes alone - must touch at least 104 registers. The first priced data point is pending - #3618's T48, which corrects a whole target row on one target lift for +2 - rank mass by changing the target's path rather than the cover. Whether - such costs add up across rows, and the coefficients, dirt and every cost - of a complete reopening, remain unknown. + all 8,506 unsupported pairs, may force more. Rectangles are capped: on an + unsupported rectangle, `C[R,S] = I[R,S] - (G/2)[R,S]` and `R ∩ S` is + independent, so its rank is at most `|R ∩ S| + 8 <= 31`, with + `rank(G/2) = 8` asserted. Beyond 31 only a min-rank argument can help. A + larger rank would further constrain any joint native source preparation + under PR3427's contract. It needs no new matching search. +2. *Which changed contract supports all 4,992 required entries, in + particular the 2,682 missing here, at least cost?* An entry is supported + when one helper type admits a source frame and a nested target frame. + Under the present cover the supported entries are exactly those whose own + slot pair is compatible, plus `(73,83)`, which only type `(17,147)` admits, + via X83's dimension-4 frame. This describes the set, not the route: 31 own + pairs are also admitted by another type (asserted). A changed cover must + give every required entry an admitting type; relaxing the cover (R2) does + this at support level. Path changes alone must touch at least 104 + registers. The first priced data point is pending #3618's T48, which + corrects a whole target row on one target lift for +2 rank mass by + changing the target's path rather than the cover. Whether such costs add + up across rows, and the coefficients, dirt and every cost of a complete + reopening, remain unknown. 3. *Is there a non-trivial use of channel state?* R1c and R3 reopen everything only because the channel already carries `G/2`. One would need a coefficient-level construction that reads channel state and restores it, diff --git a/research/p104-fixed-cover-cut-review/TASK.json b/research/p104-fixed-cover-cut-review/TASK.json index 9aa6ff7de1..2810da4571 100644 --- a/research/p104-fixed-cover-cut-review/TASK.json +++ b/research/p104-fixed-cover-cut-review/TASK.json @@ -72,22 +72,22 @@ "scope_change_reason": "The card asks for a chronological correction program. The revision-6 decisions table (row 1) instead asks first for a review of the submitted #3259 support cut and its contract, which decides whether the fixed-cover route is closed and what any reopening must cover. No construction is attempted.", "bottleneck_link": "Decides whether the pooled fixed-cover, frozen-path, immutable-X, unread-Y, independent-dirt, monotone equal-frame P104 contract is closed and how large its obstruction is (2,682 unsupported required entries, not one), which bounds what a contract change or source preconditioner must reopen before any construction round.", "budget_minutes": 150, - "stop_rule": "Stop at a proof-review verdict per step; on an engine disagreement, a proof gap or an oracle escape, stop and minimize. No matching search, no correction construction, no pricing beyond counting witness operations, at most three new relaxation rows, no Lean.", + "stop_rule": "Stop at a proof-review verdict per step; on an engine disagreement, a proof gap or an oracle escape, stop and minimize. No matching search, no correction construction, no pricing beyond counting witness operations, at most three new relaxation rows, no Lean. Deviation: five rows were delivered, relaxing three hypotheses (K5 as R1, R1c and R1u, the last added at a round-1 review's request; K1 as R2; K6 as R3).", "outcome": "completed", - "evidence": "PROOF-REVIEW.md (step table a-h, lemma proof, PR3252 review, PR3427 consumption, rank consequence, load-bearing rows); verify.py (exact channel run of 4,058 events: Y increment = G/2; layered control reproducing PR3259 numbers; sharp support by one criterion in two loop orders and by an independent PR3252 full-memory recurrence over all 104 columns, all equal, shape = 2,309 own port pairs + (73,83); PR3427 four-column masks, which exclude 92 required entries that PR3259's test grants; perfect matching of the 2,682 missing entries (vertex cover 104); rank(U-I)>=23 from a maximum independent 23x23 principal block, size checked by two exact searches, rank by Fraction elimination, det(2C[S,S])=2^30 by Bareiss; rows R1/R1u/R1c/R2/R3; 9,000 seeded small instances with exhaustive untimed reachability, 13,242 realized checked programs and 18,000 random checked programs, exact Fractions; six in-verifier contract-violation controls); test_verify.py (seven tests: four defect controls with their own FAIL messages and three fact checks).", + "evidence": "PROOF-REVIEW.md (step table a-h, lemma proof, PR3252 review, PR3427 consumption, rank consequence, load-bearing rows); verify.py (exact channel run of 4,058 events: Y increment = G/2; layered control reproducing PR3259 numbers; sharp support by one criterion in two loop orders and by an independent PR3252 full-memory recurrence over all 104 columns (PR3427 ran the same operations on its four columns), all equal, shape = 2,309 own port pairs + (73,83), with routes asserted (31 own pairs also admitted by another type; (73,83) only by type (17,147), X83's dim-4 frame to Y73's cap); PR3427 four-column masks, which exclude 92 required entries that PR3259's test grants; perfect matching of the 2,682 missing entries (vertex cover 104); rank(U-I)>=23 from a maximum independent 23x23 principal block, size checked by two exact searches, rank by Fraction elimination, det(2C[S,S])=2^30 by Bareiss; rank(G/2)=8, so any unsupported rectangle has rank at most 31; rows R1/R1u/R1c/R2/R3; 9,000 seeded small instances with exhaustive untimed reachability, 13,242 realized checked programs and 18,000 random legal programs (9,000 directed, run in the checked interpreter; 9,000 uniform, legal by construction), exact Fractions; six in-verifier contract-violation controls); test_verify.py (seven tests: four defect controls with their own FAIL messages and three fact checks, including a containment-free variant that grants an unreachable pair).", "author": "Sagar Thakrar (thakrarsagar)", "ai_assistance": "Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) for analysis, code and writing. No independent human or formal-kernel review is claimed.", "open_questions": [ { "question": "What rank does the full unsupported pattern force on a P104 source preconditioner (U-I)?", - "why_it_matters": "A maximum unsupported principal block already gives rank(U-I)>=23 versus PR3427's 4, and no principal block does better; a non-principal rectangle or a min-rank completion of -C on all 8,506 unsupported pairs may force more and would further constrain joint native source preparation.", - "first_step": "Bound the min-rank completion exactly (non-principal or overlapping rectangles, or a min-rank argument) with the pinned sharp support; no matching search.", + "why_it_matters": "A maximum unsupported principal block already gives rank(U-I)>=23 versus PR3427's 4, and no principal block does better; a non-principal rectangle or a min-rank completion of -C on all 8,506 unsupported pairs may force more and would further constrain joint native source preparation. Any unsupported rectangle C[R,S] has rank at most |R & S| + 8 <= 31, since the common ports R & S are independent and rank(G/2) = 8 (asserted).", + "first_step": "Search non-principal rectangles up to the cap of 31, or bound the min-rank completion exactly, with the pinned sharp support; no matching search.", "blocked_by": "Nothing beyond the sharp support certificate here; pricing a joint preparation remains separate." }, { - "question": "Which changed contract reopens all 2,682 sharp-missing entries at least cost, and what is its full bill?", + "question": "Which changed contract supports all 4,992 required entries, in particular the 2,682 sharp-missing ones, at least cost, and what is its full bill?", "why_it_matters": "Under the present cover the supported entries are exactly those whose own slot pair is compatible, plus (73,83); relaxing the cover (R2) reopens every entry at support level, but its cost is unknown. The missing entries need a vertex cover of 104, so path changes alone must touch at least 104 registers. Pending #3618's T48 (one target lift, +2 rank mass, a whole row) changes the target path instead and is the first priced data point; additivity across rows is not established.", - "first_step": "Name the changed hypothesis among K1-K7 (or added storage), cover the 2,682 entries at support level, and list each added operation.", + "first_step": "Name the changed hypothesis among K1-K7 (or added storage), support all 4,992 required entries at support level (a changed cover or path can lose some of the 2,310 pairs supported now), and list each added operation.", "blocked_by": "Coefficients, dirty restoration, chronology, native/hosting/precision/consumer costs are unknown." }, { diff --git a/research/p104-fixed-cover-cut-review/VERIFY.json b/research/p104-fixed-cover-cut-review/VERIFY.json index aebc916a1e..d4e8db9388 100644 --- a/research/p104-fixed-cover-cut-review/VERIFY.json +++ b/research/p104-fixed-cover-cut-review/VERIFY.json @@ -19,7 +19,7 @@ "{package}/verify.py" ], "timeout_seconds": 600, - "checks": "Exact channel run (Y increment = G/2); PR3259 layered control; sharp support by one criterion in two loop orders and PR3252 full-memory recurrence (all equal; 2,309 own port pairs + (73,83)); PR3427 masks; vertex cover 104 of the 2,682 missing entries; rank(U-I)>=23 from a maximum independent 23x23 block; rows R1/R1u/R1c/R2/R3; 9,000-instance small-domain oracle (exhaustive reachability, realized programs, 18,000 random programs); six contract-violation controls" + "checks": "Exact channel run (Y increment = G/2); PR3259 layered control; sharp support by one criterion in two loop orders and PR3252 full-memory recurrence (all equal; 2,309 own port pairs + (73,83); routes: 31 own pairs also via another type, (73,83) only via type (17,147)); PR3427 masks; vertex cover 104 of the 2,682 missing entries; rank(U-I)>=23 from a maximum independent 23x23 block; rank(G/2)=8 (rectangle cap 31); rows R1/R1u/R1c/R2/R3; 9,000-instance small-domain oracle (exhaustive reachability, realized programs, 18,000 random legal programs, the 9,000 directed ones run in the checked interpreter); six contract-violation controls" }, { "argv": [ @@ -31,7 +31,7 @@ "{package}/test_verify.py" ], "timeout_seconds": 600, - "checks": "Seven tests: tampered hash, unsound and too-tight oracle tests, wrong rank block (each with its own FAIL message); shared-type drop, containment drop (over-grants), Y-relay escape (fact checks)" + "checks": "Seven tests: tampered hash, unsound and too-tight oracle tests, wrong rank block (each with its own FAIL message); shared-type drop, containment drop (the containment-free variant over-grants), Y-relay escape (fact checks)" } ] } diff --git a/research/p104-fixed-cover-cut-review/test_verify.py b/research/p104-fixed-cover-cut-review/test_verify.py index 20a7e95fd4..d4ae616f42 100644 --- a/research/p104-fixed-cover-cut-review/test_verify.py +++ b/research/p104-fixed-cover-cut-review/test_verify.py @@ -74,9 +74,10 @@ def test_dropping_shared_type_breaks_pr3427_masks(self): def test_dropping_containment_loses_exactness_in_principle(self): # Containment V <= W is not decisive at P104 (verify.py checks this), - # but without it the test over-grants: it stays sound, not exact. F_2^4, one pooled type with line - # and hyperplane : X0 passes the admitted plane , - # Y0 the admitted plane , and no path joins them. + # but without it the test over-grants: it stays sound, not exact. + # F_2^4, one pooled type with line and hyperplane : + # X0 passes the admitted plane , Y0 the admitted plane + # , and no path joins them. key = V["key"] full = key([1, 2, 4, 8]) ty = {0: (), 1: key([1]), 3: key([1, 2, 4]), 4: full} @@ -86,9 +87,9 @@ def test_dropping_containment_loses_exactness_in_principle(self): self.assertTrue(V["small_admit"](ty, v) and V["small_admit"](ty, w)) self.assertNotIn((0, 0), V["small_exact"](inst)[0]) self.assertNotIn((0, 0), V["small_sharp"](inst)) - # A test without containment grants the unreachable pair (0,0). - self.assertTrue(V["small_admit"](ty, v) and V["small_admit"](ty, w) - and not V["le"](v, w)) + # The containment-free variant grants the unreachable pair (0,0). + self.assertFalse(V["le"](v, w)) + self.assertIn((0, 0), V["small_sharp"](inst, nested=False)) def test_wrong_rank_block_is_rejected(self): # The block is a maximum independent set, so any added port meets a diff --git a/research/p104-fixed-cover-cut-review/verify.py b/research/p104-fixed-cover-cut-review/verify.py index ed19bb29ed..20121e8a39 100644 --- a/research/p104-fixed-cover-cut-review/verify.py +++ b/research/p104-fixed-cover-cut-review/verify.py @@ -12,7 +12,9 @@ recurrence in the manner of PR3252. ORACLE seeded random small instances: an exhaustive untimed reachability per instance, an explicit checked program for every reachable helper pair, - and random checked programs, all with exact Fraction coefficients. + and two random programs (one directed, run in the checked + interpreter; one uniform, legal by construction), all with exact + Fraction coefficients. ROWS single-relaxation support rows (unpriced; operations counted). RANK a maximum unsupported principal block of C (rank(U-I) >= 23 under PR3427's contract) and the matching number of the missing entries. @@ -520,9 +522,27 @@ def p104(): sup = {(t, s) for t in range(104) for s in range(104) if sharp[t] >> s & 1} need(sup == own | {(73, 83)} and C[73][83] != 0, "sharp support = own port pairs + (73,83)") + # Routes, not just the set: the pool types admitting each supported pair. + masks, adm = endpoint_masks(geo), {} + for f in {f for k in "XY" for i in range(104) for f in paths[k + str(i)]}: + adm[f] = admit_mask(geo, masks, f) + idx = {(b // 2, a // 2): i for i, (a, b) in enumerate(geo[4])} + tys = {(t, s): sum_or(adm[v] & adm[w] for v in paths["X%d" % s] + for w in paths["Y%d" % t] if le(v, w)) + for t, s in sup} + other = {p for p, m in tys.items() + if m & ~(1 << idx[p] if p in idx else 0)} + i83 = geo[4].index((17, 147)) + need(all(tys[p] >> i & 1 for p, i in idx.items()) and len(other) == 32 + and (73, 83) in other and tys[(73, 83)] == 1 << i83 and + [(len(v), len(w)) for v in paths["X83"] for w in paths["Y73"] + if le(v, w) and (adm[v] & adm[w]) >> i83 & 1] == [(4, 8)], + "routes: 31 own pairs also via another type; (73,83) only via " + "type (17,147), X83's dim-4 frame to Y73's cap") return {"roles": roles, "geo": geo, "paths": paths, "C": C, "layered": lay, "sharp": sharp, "missing_layered": miss_l, "missing_sharp": missing(C, sharp), "forward": fwd, + "non_own_type_pairs": len(other), "backward": bin(back).count("1"), "hist": hist, "first_Y71_X102": first} @@ -713,7 +733,11 @@ def rank_consequence(r): det = bareiss_det([[int(2 * C[t][s]) for s in S] for t in S]) need(rk == 23 and det == 2 ** 30, "rank 23 by elimination and det(2C[S,S]) = 2^30") - return rk, det + # Rectangle ceiling: C[R,S] = I[R,S] - (G/2)[R,S] with R & S independent. + g = frac_rank([[int(t == s) - C[t][s] for s in range(104)] + for t in range(104)]) + need(g == 8, "rank G/2 = 8") + return rk, det, g def matching_number(pairs, n=104): @@ -842,14 +866,16 @@ def small_admit(fixed, f): return le(lo, f) and le(f, hi) -def small_sharp(inst): +def small_sharp(inst, nested=True): + """nested=False drops the containment V <= W (a probe, not a test).""" n, xs, ys, types = inst sup = set() for s, xc in enumerate(xs): for t, yc in enumerate(ys): if set(xc) & set(yc) or any( - le(v, w) and any(small_admit(ty, v) and small_admit(ty, w) - for ty in types) + (le(v, w) or not nested) and any( + small_admit(ty, v) and small_admit(ty, w) + for ty in types) for v in xc for w in yc if 1 <= len(v) <= len(w) <= n - 1): sup.add((t, s)) return sup @@ -1215,8 +1241,10 @@ def unpooled_relay_example(): def oracle(seed=20261018, trials=ORACLE_TRIALS, steps=120): """Seeded random small instances, each checked three ways: an exhaustive untimed reachability (small_exact), an explicit checked program for every - reachable helper pair (realize), and random checked programs. Pooled - instances (P104-like): the exhaustive support equals the one-helper test. + reachable helper pair (realize), and two random legal programs + (directed: run by execute; uniform: legal by construction, never run by + execute). Pooled instances (P104-like): the exhaustive support equals + the one-helper test. Unpooled rigid instances: it lies in PR3259's layered test (no pooling needed there) and its escapes from the one-helper test are counted.""" rng, wrng = Rng(seed), Rng(seed + 1) @@ -1346,7 +1374,7 @@ def main(): need(rw["R2_witness_dims"] == [(1, 8)], "R2 witness") need(rw["R3_witness_states"] == [("D11", 5)], "R3 witness") need(rw["R1c_witness_reads"] == [5], "R1c feedback witness") - rk, det = rank_consequence(r) + rk, det, g_rank = rank_consequence(r) checked, escapes = oracle() need(checked == ORACLE_EXPECTED, "oracle receipt %r" % (checked,)) need(escapes == ESCAPES_EXPECTED, "negative controls %r" % (escapes,)) @@ -1364,6 +1392,9 @@ def main(): "layered_supported_pairs": 10815, "unsupported_pairs": 8506, "own_port_pairs": 2309, "extra_pair": [73, 83], + "non_own_type_pairs": r["non_own_type_pairs"], + "rank_G_half": g_rank, + "rectangle_rank_cap": 23 + g_rank, "layered_zero_off_diagonal": len(zero_off), "layered_diagonal": 104, "backward_cone": r["backward"], "pr3427_cols_0_3_missing": 92,