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..cb51491659 --- /dev/null +++ b/research/p104-fixed-cover-cut-review/PROOF-REVIEW.md @@ -0,0 +1,417 @@ +# 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 (Nick Petalas, `4784b71d2e0833537c9ae1e8be05ad2a6b334d92`), + `research/p104-memory-relaxation-soundness/PROOF.md`. +- PR3427 (Jose Manuel, 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 + +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 + 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**, 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 (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 + 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) >= 23`** (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. 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, 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`. +- **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 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`. +- **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. 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 +`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.* Let P be the first path frame of dimension at +least 2. + +- 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, 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.* Let Q be the last path frame of dimension at most 7. + +- 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, + 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, 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]`; +- 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. ∎ + +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 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.** 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 + (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 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 +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 +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 (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 | + +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, +`(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 +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. 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) + +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 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 +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. + +## 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. +- 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. + +## 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 +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 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) >= 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. 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) | +|---|---|---:|---| +| 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, 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 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 | + +*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 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. + +*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` + (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 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 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 new file mode 100644 index 0000000000..11ee8c62fc --- /dev/null +++ b/research/p104-fixed-cover-cut-review/README.md @@ -0,0 +1,359 @@ +# 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 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 criterion, re-proved here in every + 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. + +**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 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 (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 +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. 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 + +| 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. 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)`. 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 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 | +|---|---|---:| +| Cross-layer nesting, as PR3259's proof drops it (a proof relaxation, not a contract change) | no | 2,681 | +| 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 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, +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 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 +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 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 +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 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). + +## Reproduce + +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 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>=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 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: + +- dropping the shared-helper-type requirement changes PR3427's masks; +- dropping containment `V <= W` over-grants on a fixed `F_2^4` instance: the + 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 +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 + +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 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 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. 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. +- 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 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; 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 + 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, 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 the rank bound apply only under those contracts. + +Open and not addressed here: + +- 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 or changed-path construction; +- a timed refinement of the sharp criterion. + +The selected cold replay is unchanged and was not rerun. + +## Open next questions + +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. 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, + with an explicit list of the changed channel obligations. + +## Predecessors and credit + +- Nick Petalas (petalas): + - PR2981 `3d24b92d8ba057b57cb2d480170ec407520e6882` (covers and flags); + - PR3252 `4784b71d2e0833537c9ae1e8be05ad2a6b334d92` (memory soundness); + - PR3259 `b572b0c25569898579041200e95731c5a43c9189` (pooled cut and + embedding argument); + - PR3013 `504dc9a15f7a874a47564cdf3ae6857bbbc8d000` (component pooling). +- dcharb78: PR3182 `ad848966cd62e13de5ad8d4b5169c221d74d2fcd` (the cut and its + 1,725/37 cones). +- commdata2338: PR3214 `faa6323371db1c5fbb43ab04c6e00715d2328bc6` (output + repair). +- Jose Manuel (jmbarrancoml): PR3427 `344774ba08a73fc3a85fdcb93fb319927bde3ea2` + (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 + 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. + +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..2810da4571 --- /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). 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. 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 (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. 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 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), 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." + }, + { + "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..d4e8db9388 --- /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": 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); 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": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{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 (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 new file mode 100644 index 0000000000..d4ae616f42 --- /dev/null +++ b/research/p104-fixed-cover-cut-review/test_verify.py @@ -0,0 +1,109 @@ +#!/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")) + + +_CACHE = [] + + +def result(): + if not _CACHE: + _CACHE.append(V["p104"]()) + return _CACHE[0] + + +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: " + why) + 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("input hash", 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("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 + # 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("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 + # admitted by some helper type, not necessarily the same one. + g = V["sharp_by_frames"].__globals__ + r = result() + 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_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. + 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)) + # 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 + # supported pair; a shrunk block fails the size-23 check. + g = V["rank_consequence"].__globals__ + r = result() + 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)) + + +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..20121e8a39 --- /dev/null +++ b/research/p104-fixed-cover-cut-review/verify.py @@ -0,0 +1,1427 @@ +#!/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; 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 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. +""" + +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) + + +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.""" + 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_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() + 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, 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} + 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) or not nested) + 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 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] + + +def p104(): + cert, word, fixture = load() + paths = frame_paths(word) + 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) + 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(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") + # 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)") + # 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} + + +# ------------------------------------------------ sensitivity rows (support) +def rows(r): + 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 = 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, 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 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): + inn[(t, j)] |= avail + changed = True + sup = [0] * 104 + for (t, j), m in inn.items(): + sup[t] |= m + 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") + 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, + "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( + 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), + "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), + "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 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]. + 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") + # 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): + """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.""" + + 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, 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 = () + + 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)] + 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)] + 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 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)) + 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, 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) 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 + + +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] + 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] + extra = (f[rng.below(len(f))], {("X", rng.below(len(xs))): Fraction(1)}) + + 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 += 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)) + 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]]) + 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)}) + 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 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, 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. + 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( + 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] + + 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]) + 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. + 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. 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([2]), 2: key([1, 2]), 3: key([1, 2, 4]), 4: full} + inst = (4, [[key([1]), full]], [[(), key([1, 2, 4])]], [t1, t2]) + 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 + + +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 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) + c = dict.fromkeys(("programs", "nonzero_coefficients", "helper_mediated", + "cross_type_relayed", "directed_multi_type", + "strict_gap", "strict_gap_pairs", + "exact_helper_pairs_realized", "unpooled_programs", + "unpooled_coefficients", "unpooled_multi_type", + "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) + 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) + 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 <= 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 + 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, 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 c, 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") + 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(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) + 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["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") + 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, g_rank = 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"], + "channel_first_Y71_X102": r["first_Y71_X102"], + "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, + "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], + "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, + "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>=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"])) + + +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_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)} + +if __name__ == "__main__": + main()