diff --git a/research/p104-endpoint-span-audit/PROOF.md b/research/p104-endpoint-span-audit/PROOF.md new file mode 100644 index 0000000000..6d1d0cc025 --- /dev/null +++ b/research/p104-endpoint-span-audit/PROOF.md @@ -0,0 +1,281 @@ +# Endpoint-span constraints for P104 helper histories + +The necessary helper-history relaxations in Arham Tahir's +[PR2675](https://github.com/CrocSwap/integer-mult-bounds/pull/2675) and +[PR2682](https://github.com/CrocSwap/integer-mult-bounds/pull/2682) explicitly +leave compatible endpoint geometry unresolved. This note proves two further +necessary histogram constraints. A 400-lifetime profile satisfying the +reported cut, endpoint-count and lifetime-floor tests fails the new rows: +`329 (1,7,1) + 71 (1,1,1,1,1,1,1,1,1)` scores 826 against a requirement of +832. A 406-lifetime profile passes the new rows as well, so this is not a +rejection of the entire route or quoted investigation window. + +The rank-eight finite premises and monotone support arguments are credited to +Hiroki Kumazaki's [PR2353, exact head +`2704eadf6b5205d4b965e9c6fc6dce28b89783cf`](https://github.com/CrocSwap/integer-mult-bounds/blob/2704eadf6b5205d4b965e9c6fc6dce28b89783cf/research/p104-monotone-relay-floor-audit/README.md) +and ywz65's [PR2614, exact head +`a4a2a1c734283272691b1083c819e98e7d757f20`](https://github.com/CrocSwap/integer-mult-bounds/blob/a4a2a1c734283272691b1083c819e98e7d757f20/research/p104-relay-chronology-audit/PROOF.md). +The target relaxations are Arham Tahir's PR2675 head +`ad889658a5586099132c6d7f38374df9a9d20bca` and PR2682 head +`732ac496c06c080152483ed26af44749e9f26083`, retained at main +`ffbd90dd90dbe0055464f3a1411b25a3a4fdc6b8`; exact file bindings are in +[SOURCES.json](SOURCES.json). The new step is to retain the dimensions of +the entering subspaces and departing annihilators when summing those +arguments. Dimension subadditivity and annihilator duality are standard +linear algebra, not new general mathematical principles. + +The seven cut capacities used below belong to Nick Petalas's +[PR2640, exact head +`2a5b9d72371211eac1288b690bc2739a97132439`](https://github.com/CrocSwap/integer-mult-bounds/blob/2a5b9d72371211eac1288b690bc2739a97132439/research/p104-relay-crossing-capacity/PROOF.md). +Their discovery and the preceding endpoint-count floors are not claimed here. + +Sagar Thakrar's later [Discussion 2245 +finding](https://github.com/CrocSwap/integer-mult-bounds/discussions/2245#discussioncomment-18960667), +fork head `743640530229e1821ae11dc104798871272d6f00`, proves stronger lifetime +floors than 208 using top-level mixing. Its stated full/final-frame floors +are 219/234 with invertible mixing and 216/234 with singular mixing; an +unadopted sketch mentions 250/234. Those findings are credited and are not +reproved here. The new 400-lifetime witness exceeds all these numerical +floors. No independence from every structural fact in that proof is claimed; +the distinction is from its reported lifetime-count conditions. + +## 1. Model and finite premises + +Let `V=F2^9`. Keep the frozen PR1972 source and target frame paths retained by +PR1991. There are 104 distinct source lines `ell_s=` and 104 distinct +target endpoint hyperplanes `H_t`. Sources begin at their lines and end at +FULL; targets begin at ZERO and end at their respective hyperplanes. All +these paths increase by subspace inclusion. The required added logical +source-to-target matrix is `C=I-G/2`, with `G` the rational root Gram matrix +in the pinned port order. + +The added correction network is a finite linear program with fixed rational +coefficients. It reads immutable original sources, writes additively to +original targets, and uses new helpers. Every source read and target write +must occur at the original field's actual current frame. Helper operations +are linear combinations within equal frames; helper transports increase +frames by inclusion. Each helper lifetime begins at ZERO with +source-independent contents, follows a nested path, and ends at FULL with +its original logical dirt restored. Reusing storage starts another counted +lifetime. Projecting onto source inputs makes each lifetime's entrance row +zero, even if reused storage carries the same dirt as an earlier lifetime. + +The added network may not read targets or the original channel's helper or +private fields, write original sources, use source-dependent coefficients or +initialization, descend, or perform cross-frame operations. These are +substantive hypotheses, not omitted charges. The retained channel never +writes X or reads Y, so its simultaneous execution does not create an added +correction feedback path through those fields. All arguments below permit +arbitrary same-frame relay depth, cancellation and dirty values. + +The following are finite properties of the pinned paths and geometry, not +claims for arbitrary root systems. Define `T_s={t:C[t,s]!=0}` and +`supp_t={s:C[t,s]!=0}`. + +For target `t`, let + +``` +E_t = {s in supp_t : ell_s is contained in a proper earlier frame of Y_t}, +D_t = {s in supp_t : some frame on X_s's path equals H_t}, +N_t = supp_t minus (E_t union D_t). +``` + +The source-bound finite checks give `D_t` empty and +`span{q_s:s in N_t}=H_t`, of dimension eight, for every target. The sizes of +`N_t` range from 36 to 48. Including every earlier target contact and every +possible direct source read, regardless of chronology, favors the network. +The direct-read exclusion matters: a source read at `H_t` need not pass +through an added helper's proper-subspace entrance. + +For source `s`, let + +``` +R_s = {t in T_s : some source frame W has dim(W)>1 and W subset H_t}, +F_s = T_s minus R_s. +``` + +The checks give `intersection_{t in F_s} H_t = ell_s`. The same favorable +relaxation grants every later source frame without requiring its time to be +usable. The frozen target paths never visit a source line. In particular, +information read on `ell_s` must leave that line before reaching a target. +There are 336 later-readable source-target pairs; they are removed through +`R_s`, not silently assumed absent. + +These binary span statements concern frame labels. They are distinct from +the rank of a rational coefficient matrix. No ordinary binary dot-product +interpretation of the compressed root labels is assumed. Annihilators below +use the ordinary perfect pairing between the coordinate space `V` and its +dual `V*`. + +## 2. A dimension requirement at each target + +Project every helper value onto the independent original X inputs. At a +frame `W`, each source label appearing with nonzero coefficient lies in `W`. +This invariant follows by induction. A source read respects it because all +frames on `X_s` contain `ell_s`; equal-frame operations take unions of support +and cancellation only removes support; increasing transports preserve it. +Source-independent helper entrances have empty projected support. + +Fix a target `t`. List all helper lifetimes that enter `H_t`, and let `A_j` +be the proper frame immediately before that lifetime's first entry. Count an +entrance from ZERO with `dim(A_j)=0`. Counting source-independent entrances +as well only increases the bound's right-hand side. + +For each `s in N_t`, the required coefficient `C[t,s]` is nonzero. It cannot +be written to Y in a proper earlier target frame, by the support invariant +and the definition of `E_t`. It cannot come from a direct X read at `H_t`, +by the definition of `D_t`. Thus its dependence must reach `H_t` on a helper +entering from a proper subspace. At that entrance the source label belongs +to the corresponding `A_j`. Subsequent mixing among helpers already at +`H_t` cannot create an N_t dependence absent from every such entrance. +Equivalently, expand the linear program into its chronological dependence +graph: a nonzero final coefficient has a nonzero path, and that path must +use one of these entrances. Cancellation does not invalidate this necessary +existence statement. + +Consequently + +``` +{q_s:s in N_t} subset union_j A_j, +8 = dim(span{q_s:s in N_t}) <= dim(sum_j A_j) <= sum_j dim(A_j). (1) +``` + +This counts entrances, not final target writers. Several entrances may mix +into one writer. It also does not count the possibly enlarged support of a +helper after its entrance as if that support were available before it. + +## 3. A codimension requirement at each source + +Fix source `s`. Every path contributing its coefficient to a target in `F_s` +must begin with a read while X_s is still on `ell_s`. A read at a later source +frame `W` could reach `H_t` only if `W subset H_t`, which would place `t` in +`R_s`. All dependence paths increase their frames and cannot pass through +another original source or leave a target, since those operations are +forbidden. + +List all helper lifetimes that visit `ell_s` and subsequently leave it, and +let `B_j` be the first strictly larger frame of each. A path from a line read +to a target must traverse one such departure, because no target visits the +line. For every `t in F_s`, at least one contributing path therefore has a +departure with `B_j subset H_t`. + +Let `h_t` be the nonzero covector with kernel `H_t`. For that departure, +`h_t` belongs to the annihilator `B_j^ann`. Hence + +``` +{h_t:t in F_s} subset union_j B_j^ann. +``` + +The finite intersection premise and annihilator duality give + +``` +span{h_t:t in F_s} = ell_s^ann, +8 <= sum_j dim(B_j^ann) = sum_j (9-dim(B_j)). (2) +``` + +Source-independent departures may again be counted harmlessly. A jump +directly to FULL contributes zero, because no target hyperplane contains it. +Later reads and arbitrary relays remain allowed; the definition of `F_s` +is what makes the line-departure implication valid for those paths. + +## 4. From endpoints to complete dimension histories + +Write a lifetime's positive dimension increments as a composition `h` of +nine, from dimension zero to dimension nine. Equal-frame operations and +zero-rank repetitions do not affect this history. Define two integer weights: + +* `a(h)` is the dimension immediately before the history first visits + dimension eight; it is zero if the history never visits eight. +* `d(h)` is nine minus the dimension immediately after the history leaves + dimension one; it is zero if the history never visits one. + +A nested lifetime can visit at most one of the distinct source lines, and +at most one of the distinct target hyperplanes: subspaces of the same +dimension are comparable only when equal. Summing (1) over all targets +therefore counts each lifetime at most once, with at most its `a(h)` weight. +Summing (2) over all sources similarly uses at most its `d(h)` weight. +Histories whose dimension-one or dimension-eight frame is not a designated +endpoint are still charged their full weight in this relaxation, which can +only make the necessary inequalities easier to satisfy. + +If `x_h` is the number of lifetimes of history `h`, every permitted correction +network satisfies + +``` +sum_h a(h)*x_h >= 104*8 = 832, +sum_h d(h)*x_h >= 104*8 = 832. (3) +``` + +Actual counts are nonnegative integers. Adding (3) to a fractional history +relaxation is also valid: every realizable integer profile remains in that +enlarged necessary-constraint system. This does not assert that every +fractional point has a program interpretation. + +The two weights are distinct in general. The history `(1,1,6,1)` has +`(a,d)=(2,7)`, whereas `(1,6,1,1)` has `(a,d)=(7,2)`. Arrival and departure +are not interchangeable for an arbitrary profile. + +## 5. A 400-lifetime profile fails, but the relaxation stays nonempty + +For `h_c=(1,7,1)`, both weights are one. For +`h_f=(1,1,1,1,1,1,1,1,1)`, both are seven. Consider `329 h_c + 71 h_f`. +It has 400 lifetimes and rank mass `9*400=3600`. All 400 histories supply a +proper dimension-eight arrival and a dimension-one departure, so both +predecessor endpoint-count floors of 208 pass. At each of the seven cuts, +the credited PR2640 relaxed capacities are one for `h_c` and 64 for `h_f`: + +``` +329 + 64*71 = 4873 >= 4680, +``` + +where 4680 is the largest required cut count. The profile also satisfies +the optional lifetime cap of 482 and exceeds the credited numerical floors +listed above. It lies inside the quoted 387--482 investigation window; +387 is a predecessor's unproved estimate, not an adopted lower-bound theorem. +Nevertheless its two endpoint-span totals are + +``` +329*a(h_c) + 71*a(h_f) = 329 + 497 = 826 < 832, +329*d(h_c) + 71*d(h_f) = 826 < 832. +``` + +The deficit is six in each row. Thus no assignment of nested frames, allowed +reads, coefficients, relays and restoration operations can turn these exact +complete histories into the required correction network. This tests a +specific profile, not all profiles with 400 lifetimes. + +For comparison, `335 h_c + 71 h_f` has 406 lifetimes and passes both new rows +with equality: `335+7*71=832`. Its old cut capacities are +`335+64*71=4879`; its endpoint counts are 406; its rank mass is 3654. It +respects the same numerical floors and optional lifetime cap. This is only +a positive fixture for the necessary inequalities. No compatible subspaces, +chronological contacts, coefficients, physical owners or complete price are +provided for it by these tests. + +The published 208-lifetime relaxation witness is a useful historical +illustration of the same distinction: + +``` +137*a(h_c) + 71*a(h_f) = 137 + 497 = 634 < 832, +137*d(h_c) + 71*d(h_f) = 634 < 832. +``` + +Its deficit is 198 in each row. PR2675 and PR2682 explicitly call it a +relaxation witness, not a construction, so their claim remains correct. +Moreover, the later credited lifetime floors already exclude 208-lifetime +complete networks. Excluding this historical profile is not asserted as a +new lifetime-floor result. + +The result strengthens one declared relaxation and rejects a specific +400-lifetime profile beyond the credited numerical floors. It establishes no +new unrestricted lifetime floor and does not exclude the entire quoted +investigation window. Native realization, private disposal, +precision, movement, ownership, idle/residual work, recursive costs and the +complete supplier invoice remain separate obligations. No selected-frontier +change or new multiplication exponent follows. + +The derivation and prose were prepared with substantial OpenAI Codex +assistance, including a separate agent review. The written universal +implication and the finite premise checks have different roles; finite tests +alone do not enumerate or prove a claim about all possible relay programs. +No independent human or formal-kernel review is claimed. diff --git a/research/p104-endpoint-span-audit/README.md b/research/p104-endpoint-span-audit/README.md new file mode 100644 index 0000000000..c929c16312 --- /dev/null +++ b/research/p104-endpoint-span-audit/README.md @@ -0,0 +1,162 @@ +# Endpoint-span audit of P104 helper histories + +A favorable cost profile can still have insufficient endpoint geometry. Under +the frozen X-only monotone relay contract, this audit proves two necessary +constraints on complete helper histories: total arrival dimension at target +hyperplanes and total departure codimension from source lines must each be at +least **832**. The concrete 400-lifetime profile +`329 (1,7,1) + 71 (1,1,1,1,1,1,1,1,1)` passes the earlier seven cut constraints, +endpoint counts, reported lifetime-count floors and selected-budget cost +relaxation, but scores only **826** in each new row. It cannot realize the +required correction under this contract. + +This is a scoped proof and adversarial profile audit, not an error in +[PR2675](https://github.com/CrocSwap/integer-mult-bounds/pull/2675) or +[PR2682](https://github.com/CrocSwap/integer-mult-bounds/pull/2682): both expressly +leave geometry unresolved. It supplies one necessary coupling requested in +PR2682's open next question. It does not reject every 400-lifetime profile or +the P104 route, and does not change the selected frontier. + +## Result and evidence + +For a composition `h` of nine, let `a(h)` be the dimension immediately before +its visit to dimension eight, or zero if it never visits eight. Let `d(h)` be +nine minus the dimension immediately after its visit to dimension one, or zero +if it never visits one. For actual lifetime counts `x_h`, the result is + +```text +sum_h a(h) x_h >= 832 +sum_h d(h) x_h >= 832 +``` + +[PROOF.md](PROOF.md) gives the quantified support-path argument. Each target's +necessary source labels span its eight-dimensional hyperplane; every such +label must enter through a helper's proper predecessor frame. Dually, each +source's forced target normals span an eight-dimensional annihilator and must +be covered by its departure-frame annihilators. Arbitrary rational coefficients, +cancellation and singular same-frame helper mixing are permitted. Monotonicity +allows each lifetime to visit at most one designated endpoint on each side. + +For the two history types above, `a=d=1` and `a=d=7`, respectively: + +| Profile | Each old cut capacity (maximum required 4680) | Each endpoint row (required 832) | Certified cost upper bound | +| --- | ---: | ---: | ---: | +| 137 cheap + 71 unit-step; historical 208 | 4681 | 634: fails | 0.998430350408546 | +| **329 cheap + 71 unit-step; 400** | **4873** | **826: fails** | **0.999470826199440** | +| 335 cheap + 71 unit-step; 406 | 4879 | 832: passes | 0.999503341067906 | + +The costs are rationally certified outward decimal bounds for the *optimistic* +PR2675 channel-plus-helper-plus-ideal-idle moment at the pinned selected complex +saving `a=67018507072324140917/40000000000000000000000`. They reuse Douglas +Colkitt's exact ceiling engine with `m=73`, 832 families, nine stages and +centre 56. Baseline rank mass is 2368; helper mass is nine per lifetime; total +mass is 6712; maximum idle rank is 51. The 400 and 406 profiles leave 744 and +690 ideal idle mass. A moment below one is a surviving cost relaxation, not an +attainable complete invoice. No new cost optimum is computed. + +The 406 profile is only a positive control for these necessary rows. No +compatible frames, chronology, coefficients or completed network are supplied. +The historical 208 example was already excluded by the newer +[Sagar Thakrar mixer handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/2245#discussioncomment-18960667), +fork commit `743640530229e1821ae11dc104798871272d6f00`. Its reported lifetime +floors (219/234 with invertible mixing and 216/234 with singular mixing) are +credited, not reproved. The 400 witness exceeds them and the unadopted 250 +sketch. We claim separation from those reported count conditions, not from +all structural facts in that analysis. There is no new universal lifetime +floor here. + +## Reproduce + +Python 3.12 or later, standard library only, from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/p104-endpoint-span-audit --check-only +python3.12 -B scripts/research_package.py --package research/p104-endpoint-span-audit +``` + +The registered commands use `-I -O -B` and explicit exceptions, so optimization +does not disable checks. Expected markers: + +```text +PASS_P104_ENDPOINT_SPAN_AUDIT histories=256 rejected=400 control=406 +PASS_P104_ENDPOINT_SPAN_INDEPENDENT +``` + +`verify.py` authenticates declared input bytes and directly compiles the pinned +PR2675 geometry and ceiling source, bypassing source-adjacent bytecode. It +replays the finite premises, evaluates all 256 histories and reversal duality, +and certifies the three exact cost inequalities. `independent.py` imports no +primary or predecessor checker: it independently reconstructs the E8 roots, +port order, source/target paths and exclusions using binary row reduction, +then enumerates histories as positive compositions. Both find 104 rank-eight +arrival spans and 104 rank-eight departure spans; there are 4992 demands, +336 later-readable source-target pairs and no direct hyperplane bypass. + +Controls distinguish endpoint visits from positive span contribution, +zero-to-full jumps, equal endpoint counts with different span weights, and +asymmetric arrival/departure histories. Both independently reject the 400 +profile and retain the 406 control. The independent history-row digest is +`035513ddad4984a02aef5897e7f98bfb183e361eb3f0ad8b1441c2703400ac5a`. + +Local replay passed on CPython 3.12.13 and 3.14.4. The universal theorem is the +written proof, not a consequence of enumerating finite histories or tests. +No solver, formal kernel, selected cold replay, full physical supplier replay +or independent human review is claimed. + +## Scope, overlap and provenance + +The model retains the original X/Y paths, immutable X, unread Y, fixed rational +coefficients, no original helper/private reads, and source-independent new +helper lifetimes with nested ZERO-to-FULL paths and restored dirt. A different +initialization, source/target access contract, descent or cross-frame operation +requires a new argument. Native adapters, private disposal, physical owners, +precision, movement, idle/residual work and the complete caller remain open. + +The task refines the current adversarial-audit allocation to the pending P104 +supplier's cost-to-geometry implication. Because the original card says +*selected* supplier, [TASK.json](TASK.json) explicitly records this as a changed +scope. It follows priority revision 5's P104 endpoint/routing obligation and +stops after one necessary-constraint result; no construction campaign follows. +The card's historical owner audit and selected binding baseline were run only +as orientation controls. + +Started from canonical main `ffbd90dd90dbe0055464f3a1411b25a3a4fdc6b8`. +The final upstream checkpoint is recorded in TASK.json; the scientific inputs +remain pinned to that starting main in [SOURCES.json](SOURCES.json). Current +catalogue and selected-result hashes are historical provenance; declared +live inputs are authenticated at replay. The selected frontier is unchanged. +Overlap includes all open PRs, closed/merged PRs and Discussion comments/replies, +plus local package notes, with exact coverage and known omissions in TASK.json. +The canonical [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/2245#discussioncomment-18966662) +contains the scope and will link the public handoff. + +## Open next questions + +Can the 406 control be ruled out by compatible endpoint-frame assignments or +chronological contacts? First try to assign its 335 rank-one predecessors and +71 rank-seven predecessors to the 104 required residual spans, enforcing the +corresponding source-side constraints. This asks whether a surviving necessary +profile has any geometric realization; it does not justify a larger construction +search. The blocker is compatible geometry, followed by coefficients and the +complete cost ledger. Stronger local facts in the mixer handoff should be +checked before repeating that work. The structured question is in TASK.json. + +## Credit + +Prepared by Hiroki Kumazaki (kumagi), with substantial OpenAI Codex assistance +for derivation, implementation, separate-agent proof review and independent +checker development. Separate agents share task context; this is implementation +independence, not independent human discovery. New work is Apache-2.0. + +Credit Philippe Van Velzen and kumagi/PR2353 for the arrival/support argument; +ywz65/PR2614 for the later-source-read and departure audit; Nick Petalas/PR2640 +and PR2604 for crossing bounds and contact pricing; Arham Tahir/PR2675 and +PR2682 for the coupled cost and proper-arrival screens. Exact heads are in +PROOF.md and TASK.json. Credit Sagar Thakrar's newer mixer handoff for stronger +reported lifetime floors and structural facts. Standard dimension subadditivity, +annihilator duality, binary elimination and interval arithmetic are not new. + +The frozen geometry/native lineage includes Rohan Arun/PR1972, Chafik +Boukhalfa/PR1991, Adam Gall/PR1940, Josie Elliston/PR1071 and Ali Romman/PR1125. +Douglas Colkitt's ceiling engine retains its Claude (Anthropic) assistance +credit. No predecessor files are changed or vendored. diff --git a/research/p104-endpoint-span-audit/SOURCES.json b/research/p104-endpoint-span-audit/SOURCES.json new file mode 100644 index 0000000000..da5bf02196 --- /dev/null +++ b/research/p104-endpoint-span-audit/SOURCES.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "base_commit": "ffbd90dd90dbe0055464f3a1411b25a3a4fdc6b8", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "research/p104-coupled-profile-budget/README.md", + "usage": "input", + "git_blob": "7c4f6ed510cdb7538a03838c3a9e8ebf241c3995", + "sha256": "f137703f9dd308d8f9a32e8622e4404a6f61b783c6bd84bdc03daa1b824315c1" + }, + { + "path": "research/p104-crossing-profile-screen/README.md", + "usage": "input", + "git_blob": "21c2e9b34be085e81a6848a1f2e6f37fd5c0543e", + "sha256": "0115da2b96bd5bd79944bcc6f76f8eb4fba011afca67ad31ef900e715586c6ad" + }, + { + "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" + }, + { + "path": "research/p104-coupled-profile-budget/verify.py", + "usage": "input", + "git_blob": "97741578f4ccdb2d3ce304640a58e43708b16347", + "sha256": "6e5278c621bddbbea5271a1335de926d43d5cc89e3dd719d4ac82536e95fb4ee" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + }, + { + "path": "research/p104-monotone-relay-floor-audit/README.md", + "usage": "input", + "git_blob": "a8da976c83eda0c8c5ec7bc2f0f5068edb167c03", + "sha256": "1994370aa479f01b44a55c5f8afadec5e918dc60efac08cd29adbfc5098357e3" + }, + { + "path": "research/p104-relay-chronology-audit/PROOF.md", + "usage": "input", + "git_blob": "134144f5319cbb642d9e82595fb0f2af3138435f", + "sha256": "41064970c9d16328758b7eb26c3884cfe4753536dc420feb70a2d06d97510155" + }, + { + "path": "research/p104-relay-crossing-capacity/PROOF.md", + "usage": "input", + "git_blob": "b0201a475fbbda471f01cc6703817c4ebe1d8e1e", + "sha256": "a974303f9dd04db92b7efa339f73ab1921a191404ecdffce7f17f8a23503ca05" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + } + ] +} diff --git a/research/p104-endpoint-span-audit/TASK.json b/research/p104-endpoint-span-audit/TASK.json new file mode 100644 index 0000000000..8b8f960c38 --- /dev/null +++ b/research/p104-endpoint-span-audit/TASK.json @@ -0,0 +1,186 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 5, + "base_commit": "ffbd90dd90dbe0055464f3a1411b25a3a4fdc6b8", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one selected supplier obligation follow from its actual source-bound checks?", + "starting_points": [ + "certificates/selected-result.json", + "research/owner-boundary-audit/README.md" + ], + "methods": [ + "Trace one hypothesis through the source, checker and complete caller.", + "Construct one semantically invalid but superficially well-formed fixture and test rejection." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "research/owner-boundary-audit/verify.py" + ], + "expected": "PASS_PR626_NEXT_TOUCH_BOUNDARY_AUDIT", + "inspect": "Identify why the timing-only omission passes but the full production controller still rejects it.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one current supplier obligation and trace whether its acceptance depends on an independent check.", + "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.", + "allowed_variations": [ + "Audit one named current condition using a new semantic counterexample." + ], + "scope_change_triggers": [ + "Reporting the historical timing-only diagnostic as a new current acceptance bug." + ], + "overlap_terms": [ + "owner boundary", + "bridge omission", + "hosting" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove two endpoint-span constraints on complete P104 X-only monotone helper histories and reject one favorable 400-lifetime cost profile while retaining a 406-lifetime necessary-screen control.", + "scope_change_reason": "The original card names a selected supplier. This audit instead addresses the pending P104 supplier explicitly prioritized in revision 5: it tests the cost-relaxation-to-compatible-endpoint implication requested by PR2682. The selected supplier and historical owner audit are orientation controls, not alleged new bugs.", + "bottleneck_link": "P104 side correction remains a current endpoint/routing and completed-cost priority. These valid histogram rows reject a concrete apparently affordable profile before an invalid geometric construction is pursued; they neither admit a supplier nor change kappa.", + "budget_minutes": 60, + "stop_rule": "Stop after the universal endpoint implication, source-bound finite premises, one 400-lifetime counterexample to screen sufficiency and one 406-lifetime surviving control. No optimization campaign, construction search, new universal lifetime floor, merge or frontier change.", + "outcome": "completed", + "evidence": "PROOF.md proves sum a(h)x_h >=832 and sum d(h)x_h >=832. Both checkers reconstruct 104 rank-eight endpoint premises and all 256 histories. The 400 profile has 826 each versus 832 but passes old cut capacities 4873 and certified selected-budget cost upper 0.999470826199440. The 406 control scores 832 with upper 0.999503341067906. Two CPython versions and registered optimized replay are checked; finite evidence does not replace the written proof.", + "author": "kumagi", + "ai_assistance": "Substantial OpenAI Codex assistance for mathematical derivation, source inspection, implementation, separate-agent proof review, independent checker development and writing. Agents share context; code independence is not independent human discovery.", + "open_questions": [ + { + "question": "Can compatible endpoint-frame assignments or chronological contacts reject the 406-lifetime control that survives the endpoint-span rows?", + "why_it_matters": "A surviving necessary histogram is not a correction program. Eliminating it or identifying compatible geometry reduces the current P104 routing obligation.", + "first_step": "Check the newer mixer handoff for stronger relevant local facts, then try a bounded assignment of 335 rank-one and 71 rank-seven arrival predecessors to the 104 residual spans, with matching source-side constraints.", + "blocked_by": "Simultaneously compatible geometric paths and actual chronology; even a surviving assignment leaves coefficients, restoration, physical ownership and complete supplier costs." + } + ], + "assignment": { + "seed": "eae8d160f42d35df0cb5992dd426ba5b", + "track": "adversarial-audit", + "scope_key": "dcdb0fa8e49b08a958d0", + "method": "Construct one semantically invalid but superficially well-formed fixture and test rejection.", + "selection_reason": "Explicit user preference for another adversarial audit; one task chosen from current allocation after live overlap." + }, + "orientation": { + "baseline": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY; source binding and arithmetic only, no cold replay", + "first_card_command": [ + "python3", + "-B", + "research/owner-boundary-audit/verify.py" + ], + "first_card_result": "PASS_PR626_NEXT_TOUCH_BOUNDARY_AUDIT; historical timing-only omission positive control, not a new current bug" + }, + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2245#discussioncomment-18966662", + "thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2245", + "status": "Scoped proof/checker complete; publish artifact and release claim after PR creation." + }, + "predecessors": [ + { + "pr": 2353, + "author": "Hiroki Kumazaki (kumagi), crediting Philippe Van Velzen", + "head": "2704eadf6b5205d4b965e9c6fc6dce28b89783cf", + "role": "Target residual span and monotone support argument" + }, + { + "pr": 2614, + "author": "ywz65", + "head": "a4a2a1c734283272691b1083c819e98e7d757f20", + "role": "Later source reads and forced departure intersection" + }, + { + "pr": 2640, + "author": "Nick Petalas", + "head": "2a5b9d72371211eac1288b690bc2739a97132439", + "role": "Seven crossing cut capacities" + }, + { + "pr": 2675, + "author": "Arham Tahir (Arham-Tahir64)", + "head": "ad889658a5586099132c6d7f38374df9a9d20bca", + "role": "Coupled history cost relaxation; reused authenticated finite geometry and history enumeration" + }, + { + "pr": 2682, + "author": "Arham Tahir (Arham-Tahir64)", + "head": "732ac496c06c080152483ed26af44749e9f26083", + "role": "Proper arrival history screen; explicit open endpoint-geometry question" + }, + { + "author": "Sagar Thakrar (thakrarsagar)", + "head": "743640530229e1821ae11dc104798871272d6f00", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2245#discussioncomment-18960667", + "artifact": "https://github.com/thakrarsagar/integer-mult-bounds/tree/743640530229e1821ae11dc104798871272d6f00/research/p104-rank1-mixer-correction", + "role": "Newer reported 216/219/234 lifetime floors; 208 exclusion already known. Credited overlap; not replayed or newly adopted." + } + ], + "upstream_refresh": { + "checked_at": "2026-10-16T07:36:45Z", + "canonical_main": "38746ad3f6ffebcc0275e286b1dbb733d7c696dd", + "priority_revision": 5, + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "decision": "Continue. Canonical main advanced from ffbd90dd; diff shows no changes to AGENTS.md, autoresearch.md, catalogue, family gate, selected record or declared inputs. Rebase publication branch onto refreshed main, retaining scientific provenance at ffbd90dd." + }, + "overlap": { + "entry_coverage": { + "open_prs": 491, + "closed_prs": 2092, + "discussion_records": 1535, + "time_range_utc": "2026-10-16 07:22–07:23" + }, + "final_searched_at": "2026-10-16T07:39:22.632212+00:00", + "final_coverage": { + "open_prs": { + "fetched_at": "2026-10-16T07:36:45.347328+00:00", + "complete_pagination": true, + "records": 486 + }, + "discussions": { + "fetched_at": "2026-10-16T07:37:32.877629+00:00", + "complete_pagination": true, + "records": 1543 + }, + "closed_prs": { + "fetched_at": "2026-10-16T07:37:55.754296+00:00", + "complete_pagination": true, + "records": 2097 + } + }, + "terms": [ + "endpoint span", + "endpoint-span", + "arrival dimension", + "departure codimension", + "proper predecessor", + "400-lifetime" + ], + "findings": "Four focused matches: this package README/TASK, own public claim, and an unrelated five-subset endpoint-span note. Broader P104 and predecessor searches identified the named cost screens and newer mixer handoff. No conflicting claim for these two histogram rows was found; absence of matches does not establish novelty. The 400 witness, rather than already-excluded 208, is the discriminating example.", + "limits": "Remote PR scope includes open and closed/merged titles and bodies, with separate coverage and timestamps. State changes are deduplicated by latest PR update; snapshots are not atomic. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "cache_note": "Focused query reused the just-refreshed 07:36–07:37 complete corpus; no additional remote fetch for the 07:39 query. Remote snapshots are not atomic and omit code diffs/arbitrary nested files." + }, + "verification": { + "python": [ + "3.12.13", + "3.14.4" + ], + "registered_command": [ + "python3.12", + "-B", + "scripts/research_package.py", + "--package", + "research/p104-endpoint-span-audit" + ], + "optimization": "Both registered scripts use -I -O -B with explicit exception checks.", + "not_run": [ + "Full frozen native/channel reproduction", + "Selected frontier cold replay", + "Mixer fork full verification", + "LP optimization of the strengthened screen", + "Formal-kernel verification or independent human review" + ], + "limits": "The primary reuses authenticated predecessor geometry and exact ceiling code; independent.py reconstructs finite geometry and profiles without importing either. The cost enclosure is credited reuse, not a separately implemented transcendental checker." + } +} diff --git a/research/p104-endpoint-span-audit/VERIFY.json b/research/p104-endpoint-span-audit/VERIFY.json new file mode 100644 index 0000000000..15b0dd3c90 --- /dev/null +++ b/research/p104-endpoint-span-audit/VERIFY.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-coupled-profile-budget/README.md", + "research/p104-crossing-profile-screen/README.md", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "research/p104-native-channel/inputs/P104-FIXTURE.json", + "research/p104-coupled-profile-budget/verify.py", + "research/complex-local-word-ceiling/ceiling.py", + "research/p104-monotone-relay-floor-audit/README.md", + "research/p104-relay-chronology-audit/PROOF.md", + "research/p104-relay-crossing-capacity/PROOF.md", + "research/community-frontier1094-audit/ASSEMBLY.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate declared source bytes, replay credited finite geometry, check all 256 endpoint rows and reversal duality, reject cost-favorable 400-lifetime profile, retain 406-lifetime necessary-screen control." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Independent binary-elimination reconstruction of roots, chronology exclusions, both rank-eight premises and history/profile endpoint arithmetic; no predecessor or primary checker imports." + } + ] +} diff --git a/research/p104-endpoint-span-audit/independent.py b/research/p104-endpoint-span-audit/independent.py new file mode 100644 index 0000000000..6c39d6eef1 --- /dev/null +++ b/research/p104-endpoint-span-audit/independent.py @@ -0,0 +1,313 @@ +#!/usr/bin/env python3 +"""Independent endpoint-span checks; no optimizer or predecessor imports. + +Prepared by kumagi with substantial OpenAI Codex assistance. Apache-2.0. +The source fixture and old constraints are credited in README.md. This uses +binary row reduction, rather than the predecessor's enumeration of subspaces. +The network implication is a written theorem in PROOF.md, not proved by this run. +""" + +from collections import Counter +import hashlib +from itertools import combinations, product +import json +from pathlib import Path + + +ROOT = Path(__file__).resolve().parents[2] +PREFIX = "research/p104-native-channel/inputs/" +PINS = { + "LOWRANK-WITNESS.json": + "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e", + "P104-FIXTURE.json": + "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4", +} +EXPECTED_CUTS = [4656, 4656, 4672, 4680, 4672, 4656, 4656] +EXPECTED_BASE = {1: 1074, 2: 58, 3: 86, 4: 104, 5: 48, 6: 24, 7: 8, 8: 8} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def load(name): + raw = (ROOT / PREFIX / name).read_bytes() + require(hashlib.sha256(raw).hexdigest() == PINS[name], "source digest: " + name) + return json.loads(raw) + + +def reduce_vector(vector, basis): + for row in basis: + if vector & (1 << (row.bit_length() - 1)): + vector ^= row + return vector + + +def rref(vectors): + """Canonical rows with highest-set-bit pivots, over F_2^9.""" + rows = [] + for vector in vectors: + require(type(vector) is int and 0 <= vector < 512, "binary vector") + vector = reduce_vector(vector, rows) + if vector: + pivot = 1 << (vector.bit_length() - 1) + rows = [row ^ vector if row & pivot else row for row in rows] + rows.append(vector) + rows.sort(reverse=True) + return tuple(rows) + + +def frame(vectors): + basis = rref(vectors) + require(len(basis) == len(vectors), "independent supplied frame basis") + return basis + + +def contained(smaller, larger): + return all(reduce_vector(row, larger) == 0 for row in smaller) + + +def orthogonal(basis): + """Solve the homogeneous system using its free coordinates.""" + pivots = {row.bit_length() - 1 for row in basis} + result = [] + for free in set(range(9)) - pivots: + vector = 1 << free + for row in basis: + if (row & vector).bit_count() % 2: + vector ^= 1 << (row.bit_length() - 1) + result.append(vector) + return rref(result) + + +def source_geometry(): + witness, fixture = (load(name) for name in PINS) + roots = set() + for left, right in combinations(range(8), 2): + for sign in (-1, 1): + vector = [0] * 8 + vector[left], vector[right] = 2, sign * 2 + roots.add(tuple(vector)) + for tail in product((-1, 1), repeat=7): + if sum(value == -1 for value in tail) % 2 == 0: + roots.add((1, *tail)) + puncture = fixture["section4_explicit_P104"] + removed = {tuple(row) for row in puncture["F0"] + puncture["C"]} + require(len(roots) == 120 and len(removed) == 16 and removed <= roots, + "E8 roots and puncture") + ports = sorted(roots - removed) + require(len(ports) == 104, "104 ports") + + names = [f"{kind}{index}" for kind in "XY" for index in range(104)] + paths = {name: [frame(witness["initial_frames"][name])] for name in names} + paid = Counter() + require(len(witness["program"]) == 4058, "word length") + for event in witness["program"]: + require(event[0] in {"add", "copy", "zero", "erase", "transport"}, + "known frozen instruction kind") + if event[0] in {"add", "copy"}: + require(not event[1].startswith("X") and not event[2].startswith("Y"), + "immutable sources and unread targets") + elif event[0] in {"zero", "erase"}: + require(not event[1].startswith(("X", "Y")), + "no data-field initialization or erasure") + elif event[0] == "transport": + _, name, before, after, rank = event + paid[rank] += 1 + if name in paths: + before, after = frame(before), frame(after) + require(before == paths[name][-1] and contained(before, after) + and len(after) - len(before) == rank > 0, + "frozen monotone data path") + paths[name].append(after) + require(dict(paid) == EXPECTED_BASE, "frozen paid profile") + for name in names: + require(paths[name][-1] == frame(witness["final_frames"][name]), + "frozen final frame") + lines = [paths[f"X{s}"][0] for s in range(104)] + targets = [paths[f"Y{t}"][-1] for t in range(104)] + require(len(set(lines)) == len(set(targets)) == 104, "distinct endpoints") + require(all(len(line) == 1 for line in lines) + and all(len(target) == 8 for target in targets), "endpoint dimensions") + labels = [line[0] for line in lines] + require(all(len(paths[f"X{s}"][-1]) == 9 for s in range(104)) + and all(paths[f"Y{t}"][0] == () for t in range(104)), + "FULL source ends and ZERO target starts") + duals = [orthogonal(target) for target in targets] + require(all(len(dual) == 1 for dual in duals), "one-dimensional target duals") + normals = [dual[0] for dual in duals] + for target, normal in zip(targets, normals, strict=True): + require(orthogonal((normal,)) == target, "double annihilator") + require(all((reduce_vector(v, target) == 0) + == ((v & normal).bit_count() % 2 == 0) for v in range(512)), + "membership against independent parity equation") + odd_functionals = [] + for alphabet in (labels, normals): + possible = [v for v in range(1, 512) + if all((v & q).bit_count() % 2 == 1 for q in alphabet)] + require(possible, "affine odd functional used by old cut capacities") + odd_functionals.append(possible[0]) + + demands = set() + for t, left in enumerate(ports): + for s, right in enumerate(ports): + gram4 = sum(a * b for a, b in zip(left, right, strict=True)) + require(gram4 % 4 == 0, "integral Gram entry") + if 8 * (t == s) != gram4: + demands.add((t, s)) + require((reduce_vector(labels[s], targets[t]) == 0) + == (gram4 % 8 == 4), "root/label incidence binding") + require(len(demands) == 4992, "4992 correction demands") + require(all(sum((t, s) in demands for s in range(104)) == 48 + for t in range(104)), "48 demands per target") + + residual_sizes, forced_sizes = Counter(), Counter() + direct_bypasses = later_reads = 0 + for t, target in enumerate(targets): + residual = [] + for s, label in enumerate(labels): + if (t, s) not in demands: + continue + direct = target in paths[f"X{s}"] + direct_bypasses += direct + earlier = any(len(v) < 8 and reduce_vector(label, v) == 0 + for v in paths[f"Y{t}"]) + if not direct and not earlier: + residual.append(label) + require(rref(residual) == target, "rank-eight residual target span") + residual_sizes[len(residual)] += 1 + require(direct_bypasses == 0, "no direct source hyperplane bypass") + for s, line in enumerate(lines): + forced_normals = [] + for t, target in enumerate(targets): + require(line not in paths[f"Y{t}"], "no target source-line bypass") + if (t, s) in demands: + later = any(len(v) > 1 and contained(v, target) + for v in paths[f"X{s}"]) + later_reads += later + if not later: + forced_normals.append(normals[t]) + require(rref(forced_normals) == orthogonal(line), + "rank-eight forced target-normal span") + forced_sizes[len(forced_normals)] += 1 + require(later_reads == 336, "later-readable correction entries") + + cut_counts = [] + for cut in range(1, 8): + forced = 0 + for t, s in demands: + source_bypass = any(len(v) > cut and contained(v, targets[t]) + for v in paths[f"X{s}"]) + target_bypass = any(len(v) <= cut and reduce_vector(labels[s], v) == 0 + for v in paths[f"Y{t}"]) + forced += not source_bypass and not target_bypass + cut_counts.append(forced) + require(cut_counts == EXPECTED_CUTS, "seven old cut constraints") + return { + "demands": len(demands), "rank_eight_arrival_spans": len(targets), + "rank_eight_departure_spans": len(lines), "direct_bypasses": direct_bypasses, + "later_reads": later_reads, "arrival_sizes": dict(sorted(residual_sizes.items())), + "departure_sizes": dict(sorted(forced_sizes.items())), + "odd_functionals": odd_functionals, "cut_requirements": cut_counts, + "endpoint_span_requirement": 8 * len(targets), + } + + +def histories(): + # Positive compositions enumerate histories independently of stop-bit masks. + by_mass = [[()]] + for mass in range(1, 10): + by_mass.append([(first, *tail) for first in range(1, mass + 1) + for tail in by_mass[mass - first]]) + rows = {} + for jumps in by_mass[9]: + stops = [0] + for jump in jumps: + stops.append(stops[-1] + jump) + edges = list(zip(stops[:-1], stops[1:], strict=True)) + capacities = [] + for cut in range(1, 8): + crossing = [(a, b) for a, b in edges if a <= cut < b] + require(len(crossing) == 1, "unique crossing of every cut") + a, b = crossing[0] + capacities.append(0 if a == 0 or b == 9 else 1 << (7 - b + a)) + arrival = next((a for a, b in edges if b == 8), 0) + departure = next((9 - b for a, b in edges if a == 1), 0) + rows[jumps] = { + "cuts": capacities, "visits_one": int(1 in stops), + "visits_eight": int(8 in stops), "arrival": arrival, + "departure": departure, + } + require(0 <= arrival <= 7 * (8 in stops) + and 0 <= departure <= 7 * (1 in stops), "endpoint weights") + require(len(rows) == 256, "all 256 complete increasing histories") + expected_weights = {0: 129, **{weight: 2 ** (weight - 1) for weight in range(1, 8)}} + for key in ("arrival", "departure"): + require(dict(Counter(row[key] for row in rows.values())) == expected_weights, + "complete endpoint-weight distribution") + require(sum(row["visits_one"] for row in rows.values()) == 128 + and sum(row["visits_eight"] for row in rows.values()) == 128, + "old endpoint-visit distribution") + return rows + + +def profile(rows, cheap, full): + weights = [(cheap, rows[(1, 7, 1)]), (full, rows[(1,) * 9])] + cuts = [sum(n * row["cuts"][k] for n, row in weights) for k in range(7)] + totals = {key: sum(n * row[key] for n, row in weights) + for key in ("visits_one", "visits_eight", "arrival", "departure")} + old = (all(value >= required for value, required in zip(cuts, EXPECTED_CUTS, strict=True)) + and totals["visits_one"] >= 208 and totals["visits_eight"] >= 208 + and 9 * (cheap + full) <= 4344) + new = old and totals["arrival"] >= 832 and totals["departure"] >= 832 + return {"cheap": cheap, "full": full, "cuts": cuts, **totals, + "rank_mass": 9 * (cheap + full), "old_accepts": old, "new_accepts": new} + + +def calculate(): + finite = source_geometry() + rows = histories() + rejected = profile(rows, 329, 71) + require(rejected["old_accepts"] and not rejected["new_accepts"], + "400-lifetime profile separates the old and new necessary screens") + require(rejected["arrival"] == rejected["departure"] == 826 + and rejected["cuts"] == [4873] * 7, "400-lifetime profile exact totals") + # Only the reported numerical floors are compared here, not the mixer's + # entire structural argument; 250 is its explicitly unadopted sketch. + require(all(329 + 71 >= floor for floor in (216, 219, 234, 250)), + "400 lifetimes exceeds credited numerical floors") + surviving = profile(rows, 335, 71) + require(surviving["new_accepts"] and surviving["arrival"] == surviving["departure"] == 832 + and surviving["cuts"] == [4879] * 7, "406-lifetime equality profile survives rows") + historical = profile(rows, 137, 71) + require(historical["old_accepts"] and not historical["new_accepts"] + and historical["arrival"] == historical["departure"] == 634 + and historical["cuts"] == [4681] * 7, "historical published relaxation totals") + # Controls isolate mistakes that endpoint counts alone or uniform weights miss. + cheap = profile(rows, 208, 0) + require(not cheap["old_accepts"] and cheap["arrival"] == cheap["departure"] == 208, + "endpoint visitors alone do not supply cut or span capacity") + require(rows[(9,)]["arrival"] == rows[(9,)]["departure"] == 0, + "direct zero-to-full jump supplies no endpoint span") + require(rows[(8, 1)]["visits_eight"] == 1 and rows[(8, 1)]["arrival"] == 0 + and rows[(1, 8)]["visits_one"] == 1 and rows[(1, 8)]["departure"] == 0, + "endpoint visit is not a positive span contribution") + require(rows[(1, 7, 1)]["arrival"] != rows[(1,) * 9]["arrival"], + "equal endpoint counts do not justify equal span weights") + require((rows[(1, 1, 6, 1)]["arrival"], rows[(1, 1, 6, 1)]["departure"]) == (2, 7) + and (rows[(1, 6, 1, 1)]["arrival"], rows[(1, 6, 1, 1)]["departure"]) == (7, 2), + "arrival and departure rows differ on asymmetric histories") + serialized_rows = [{"jumps": jumps, **row} for jumps, row in sorted(rows.items())] + digest = hashlib.sha256(json.dumps(serialized_rows, sort_keys=True, + separators=(",", ":")).encode()).hexdigest() + return {"finite": finite, "histories": len(rows), "history_sha256": digest, + "rejected_400_profile": rejected, "span_deficit_each": 832 - 826, + "surviving_406_relaxation": surviving, + "historical_208_relaxation": historical, "negative_controls": 5} + + +if __name__ == "__main__": + result = calculate() + print("PASS_P104_ENDPOINT_SPAN_INDEPENDENT") + print(json.dumps(result, sort_keys=True)) diff --git a/research/p104-endpoint-span-audit/verify.py b/research/p104-endpoint-span-audit/verify.py new file mode 100644 index 0000000000..12cc2f0bba --- /dev/null +++ b/research/p104-endpoint-span-audit/verify.py @@ -0,0 +1,160 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Finite premises and exact profile screens for the endpoint-span proof. + +Hiroki Kumazaki (kumagi), with substantial OpenAI Codex assistance. +Credited geometry: Arham Tahir's PR2675 verifier. Credited cost engine: +Douglas Colkitt, with Claude assistance. See PROOF.md for the universal step; +this finite replay is not an enumeration of correction networks. +""" +from collections import Counter +from fractions import Fraction as Q +import hashlib +import json +from pathlib import Path +from types import ModuleType + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +SELECTED_A = Q(67018507072324140917, 40000000000000000000000) + + +def need(condition, reason): + if not condition: + raise ValueError(reason) + + +def authenticated_sources(): + manifest = json.loads((PACKAGE / 'SOURCES.json').read_text()) + sources = {} + for row in manifest['files']: + if row['usage'] != 'input': + continue + data = (ROOT / row['path']).read_bytes() + need(hashlib.sha256(data).hexdigest() == row['sha256'], + 'source hash: ' + row['path']) + sources[row['path']] = data + return sources + + +def source_module(sources, path, name): + # Execute the authenticated bytes themselves; never read a source-adjacent + # bytecode cache. These pinned modules import only the standard library. + module = ModuleType(name) + module.__file__ = str(ROOT / path) + exec(compile(sources[path], module.__file__, 'exec'), module.__dict__) + return module + + +def endpoint_weights(jumps): + need(bool(jumps) and all(type(x) is int and x > 0 for x in jumps) + and sum(jumps) == 9, 'complete positive dimension history') + previous = 0 + arrival = departure = 0 + for jump in jumps: + current = previous + jump + if current == 8: + arrival = previous + if previous == 1: + departure = 9 - current + previous = current + return arrival, departure + + +def screen(histogram, histories): + need(all(type(n) is int and n >= 0 for n in histogram.values()), + 'nonnegative integer lifetime counts') + cuts = [0] * 9 + endpoints = [0, 0] + local = Counter() + for index, number in histogram.items(): + jumps, column = histories[index] + for rank in jumps: + local[rank] += number + for i, value in enumerate(column): + cuts[i] += number * value + for i, value in enumerate(endpoint_weights(jumps)): + endpoints[i] += number * value + return cuts, endpoints, local + + +def upper_decimal(value): + scale = 10**15 + numerator = -((-value.numerator * scale) // value.denominator) + return f'{numerator // scale}.{numerator % scale:015d}' + + +def main(): + sources = authenticated_sources() + assembly = json.loads(sources['research/community-frontier1094-audit/ASSEMBLY.json']) + need(Q(assembly['complex_lower']) == SELECTED_A, 'selected saving binding') + predecessor = source_module(sources, 'research/p104-coupled-profile-budget/verify.py', + 'credited_geometry') + cost = source_module(sources, 'research/complex-local-word-ceiling/ceiling.py', + 'credited_cost') + witness = json.loads(sources['research/p104-native-channel/inputs/LOWRANK-WITNESS.json']) + fixture = json.loads(sources['research/p104-native-channel/inputs/P104-FIXTURE.json']) + for event in witness['program']: + need(event[0] in {'add', 'copy', 'zero', 'erase', 'transport'}, 'known instruction') + if event[0] in {'add', 'copy'}: + need(not event[1].startswith('X') and not event[2].startswith('Y'), + 'immutable sources and unread targets') + elif event[0] in {'zero', 'erase'}: + need(not event[1].startswith(('X', 'Y')), 'no data-field creation or erasure') + need(all(len(witness['final_frames'][f'X{s}']) == 9 for s in range(104)) + and all(witness['initial_frames'][f'Y{t}'] == [] for t in range(104)), + 'FULL source ends and ZERO target starts') + finite = predecessor.geometry(witness, fixture) + need(finite['departure_lines'] == finite['arrival_hyperplanes'] == 104, + '104 endpoints on each side') + histories = predecessor.histories() + need(len(histories) == 256 and len({tuple(h) for h, _ in histories}) == 256, + 'all positive compositions of nine') + for jumps, _ in histories: + a, d = endpoint_weights(jumps) + need(0 <= a <= 7 and 0 <= d <= 7, 'endpoint weight range') + need(endpoint_weights(jumps[::-1]) == (d, a), 'annihilator reversal') + controls = {(8, 1): (0, 0), (1, 8): (0, 0), (1, 1, 7): (0, 7), + (7, 1, 1): (7, 0), (1, 1, 6, 1): (2, 7), + (1, 6, 1, 1): (7, 2), (1, 7, 1): (1, 1), + (1,) * 9: (7, 7)} + for history, expected in controls.items(): + need(endpoint_weights(history) == expected, 'endpoint control ' + str(history)) + need(histories[129][0] == [1, 7, 1] and histories[255][0] == [1] * 9, + 'predecessor profile index binding') + results = [] + for label, cheap, full, expected, should_pass in [ + ('historical_208', 137, 71, 634, False), + ('adversarial_400', 329, 71, 826, False), + ('necessary_screen_control_406', 335, 71, 832, True), + ]: + counts, endpoints, extra = screen({129: cheap, 255: full}, histories) + lifetimes = cheap + full + need(counts[:7] == [cheap + 64 * full] * 7 and counts[7:] == [lifetimes] * 2, + 'old capacity totals') + need(all(c >= b for c, b in zip(counts, predecessor.RHS, strict=True)), + 'predecessor necessary rows') + need(endpoints == [expected, expected], 'endpoint totals') + need(all(x >= 832 for x in endpoints) == should_pass, 'new screen verdict') + if label != 'historical_208': + need(387 <= lifetimes <= 482 and lifetimes >= max(219, 234, 216, 250), + 'reported count floors and investigation window') + need(sum(r * n for r, n in extra.items()) == 9 * lifetimes <= 4344, + 'complete lifetime mass within ideal budget') + local = Counter(predecessor.BASE) + local.update(extra) + lo, hi = cost.relax(local, 73, 832, 9, 56, SELECTED_A) + need(0 < lo <= hi < 1, 'strict favorable selected-budget relaxation') + results.append({'profile': label, 'lifetimes': lifetimes, + 'cut_capacities': counts[:7], 'endpoint_counts': counts[7:], + 'arrival_dimension': endpoints[0], 'departure_codimension': endpoints[1], + 'endpoint_requirement': 832, 'new_rows_pass': should_pass, + 'ideal_idle_mass': 4344 - 9 * lifetimes, + 'relaxation_upper': upper_decimal(hi)}) + print(json.dumps({'finite_premises': finite, 'histories_checked': 256, + 'profiles': results}, indent=2)) + print('PASS_P104_ENDPOINT_SPAN_AUDIT histories=256 rejected=400 control=406') + + +if __name__ == '__main__': + main()