diff --git a/research/p104-target-order-delivery/README.md b/research/p104-target-order-delivery/README.md new file mode 100644 index 0000000000..582e4c7989 --- /dev/null +++ b/research/p104-target-order-delivery/README.md @@ -0,0 +1,283 @@ +# A chronological P104 schedule attains the known 32-chain bound + +**New constructive attainment and a scoped tail invoice, not a new lower +bound, restored supplier, or kappa.** + +Ali Romman's [PR1125](https://github.com/CrocSwap/integer-mult-bounds/pull/1125) +already proves that monotone P104 fixed-term delivery needs at least +**32 paths**, including the eight seeds. Its proof explicitly does not +construct a schedule attaining that bound (PROOF lines 204–206). +This package supplies that missing **globally executable 32-chain +attainment for the exact fixture from Josie Elliston's +[PR1071](https://github.com/CrocSwap/integer-mult-bounds/pull/1071)**. + +Allowing independent target read orders reduces that fixture's witnessed +delivery bank from PR1071's **55 under a global order** to **32**, or +**24 additional arrays instead of 47**. `SCHEDULE.json` executes all +**416 reads on 104 targets**, and its conditional supplied-copy tail +profile improves componentwise. The existing 32-path antichain bound is +rechecked as a credited special case, not claimed anew. The supplied-copy +boundary does **not** form or restore copies: those costs remain unknown, +not free work. + +## Exact object and retained restrictions + +The fixture is `section4_explicit_P104` of the hash-pinned +`research/biframe-decoder-ladder/RESULTS.json`. The eight pairs `(a_k,b_k)` +are doubled-coordinate E8 roots. On the 104 live root lines, + +``` +D[t,k] = , T[s,k] = 2 / , +D T^transpose = 2 G. +``` + +Each centre gathers in an eight-dimensional binary label hyperplane and has +a rank-seven drop to its one-dimensional survivor `span(u_a_k)`. Its 52 +readers are orthogonal to that survivor. All eight survivor labels are +independent over F2. These are predecessor facts, independently rechecked +here for this fixture, including all 10,816 decoder entries and all eight +pairing ranks. The copied-information charge **56 is not a new result**. + +Let `K_t` be the nonzero positions in row `D[t]`. A target chooses any +permutation of `K_t`; immediately after its j-th read its frame is **exactly** +the span of those j survivor labels. There are no additional spectator +frame directions. A delivery array carries one fixed centre value throughout +its lifetime, follows nested read frames, and has no subsequent drop, reload, +or mixing with another centre. Equal-frame reads may share the same array. + +Compared with PR1071 this changes the global-order restriction. Compared +with PR1125 it adds an explicit chronological attaining witness and tail +invoice, not a stronger obstruction. PR1125's lower bound covers all 7168 +mixed decoders and permits additional frame directions and paid downward +moves; our witness concerns one pinned decoder with exact prefix frames. +It does not optimize other decoders, dynamic centre mixing, additional +drops, or an admitted physical P104 compiler. Its target frames stay inside +their final hyperplanes because each read survivor is orthogonal to that +target's label. + +## Proof of the sharp minimum + +### Credited lower bound: 32 incomparable final reads + +The following is the minimal-prefix special case of PR1125's terminal-read +theorem (PROOF sections 1 and 4). The independent replay rederives its finite +premises on this fixture; the bound and antichain idea belong to PR1125. +The exact target support distribution is + +| Number of centres read | 2 | 3 | 4 | 5 | 6 | +|---|---:|---:|---:|---:|---:| +| Targets | 12 | 24 | **32** | 24 | 12 | + +The 104 support masks are distinct. In particular, each of the 32 four-read +targets has a final read at its four-dimensional support span. Because all +eight survivor labels are independent, those 32 subspaces are distinct. +Distinct subspaces of equal dimension are incomparable. Any monotone +fixed-centre delivery chain can visit at most one of them, regardless of +which centre supplies the final read. Therefore **at least 32 arrays/chains +are necessary** for every allowed collection of target permutations. + +This lower bound does not assume a common prefix tree, a bound on program +length, or the particular search algorithm used for the witness. + +### Upper bound: exact schedule and chronological feasibility + +`SCHEDULE.json` contains 116 parent edges on the eight-bit subset lattice. +An entry `[S,k]` means that the chosen path into `S` adds bit `k` to +`S without k`. Following parents to zero gives each target's read order. +Every parent edge is used by at least one target. Each centre's used read +frames are explicitly partitioned into nested chains: + +``` +centre 0 1 2 3 4 5 6 7 +number of chains 5 3 4 4 4 3 4 5 total 32 +``` + +The replay checks every frame, chain assignment, omitted/duplicate read, +and the full scalar coefficient matrix. It then executes events in increasing +`(frame dimension, frame mask, centre, target)` order. Each target dependency +strictly increases dimension. Each strict copy-chain dependency also increases +dimension; all reads at one fixed frame are consecutive within that chain. +Thus the event order satisfies both sets of dependencies and cannot contain +a chronological cycle. This is more than a disconnected collection of +minimum path covers. The receipt also exhibits two targets with incompatible +centre precedences, confirming that the changed hypothesis is actually used. + +The schedule plus the antichain lower bound proves **exactly 32**, in the +precise minimal-prefix, fixed-centre, no-redrop geometry above. + +## Complete invoice at the declared supplied-copy boundary + +This section deliberately does not call its subtotal a complete supplier +profile. Its boundary is: + +* one exact centre value is already available on each of the 32 arrays at + its singleton survivor frame; +* each target enters at frame zero with arbitrary target value; +* every array is completed to the full rank-nine frame after its last read; +* every target is completed to its rank-eight final hyperplane after its + last read. + +All positive frame increments at this boundary are counted. Rank-r transports +are denoted `H_r`. + +| Contribution | New per-target schedule | Replayed best-global-order witness | +|---|---|---| +| Delivery arrays, singleton entry to rank-nine exit | `85H1 + 17H2 + 19H3 + 20H4` | `101H1 + 27H2 + 24H3 + 28H4 + 11H5 + 4H6 + 2H7 + H8` | +| Delivery-array rank mass | **256** | **440** | +| Targets, zero entry to final hyperplane | `416H1 + 12H2 + 24H3 + 32H4 + 24H5 + 12H6` | same | +| Target rank mass | **832** | **832** | +| Scalar centre reads | **416**, coefficients `D[t,k]` | same | + +The new delivery subtotal is smaller **componentwise**: its saved histogram +is `{1:16, 2:10, 3:5, 4:8, 5:11, 6:4, 7:2, 8:1}`. Therefore its tail cost is +strictly smaller for every positive rank-cost function, not just at a sampled +exponent. The comparator is one explicit, independently reconstructed +55-chain cover of the predecessor's best global order. We do **not** claim +that its tail histogram minimizes the moment among all global-order covers. +The predecessor's exhaustive 40,320-order minimum is credited, not rerun; +its 55-chain witness and its single-cut 19-chains-per-centre control are +reproduced here. + +`RESULT.json` additionally gives certified rational intervals for the +normalized child subtotal `sum n_r (r/73)^(1-a)` at `a=0`, +`a=3351/2000000`, and `a=1/99`, using the pinned interval arithmetic engine +from `complex-local-word-ceiling`. There is **no role denominator W** in +this subtotal. The incumbent coverage-law ceiling is not applied to this +unfinished, changed interface. + +### What is not free or implemented + +The eight original gather-to-survivor drops still have rank charge 56. The +24 additional supplied centre values require a legal formation mechanism. +An ordinary addition into an arbitrary dirty helper produces `centre+dirty`, +not the boundary value required above. The verifier injects one independent +dirty symbol into **every** supplied copy in turn; all 32 contaminations +have a nonzero target response. Thus arbitrary dirty-copy formation or +cleanup cannot be silently omitted. + +A completed construction would have to charge, and prove compatibility of, + +``` +C_complete = C_gather + C_original_drops + C_form_24_exact_copies + + C_delivery_tails + C_target_tails + C_416_scalar_reads + + C_restore + C_side_corrections + C_hosting_and_precision. +``` + +Only the two tail profiles, the exact scalar read map, and the original +rank-seven drop geometry are established here. Source formation, dirty +lifetime restoration, phase/frame compatibility with the side corrections, +whole-call hosting, precision/tape work, and the all-size recursive interface +remain unresolved. The original 5%-above-selected complete-profile gate of +the chooser card is **not passed**. This is an explicitly declared changed-scope +result on a central missing delivery lemma, not a supplier improvement or +an updated frontier. + +PR1125's separate budget warning is unchanged: two extra ranks per call +already exceed its T37/T16 P104 knob budgets **if the remaining paid moment +retains or exceeds that knob profile**. Its theorem does not establish that +cost premise for every new word. Our 32-carrier witness does not evade the +at-most-26-path screen or discharge the remaining-cost premise; it only +attains the previously unconstructed monotone path threshold. + +## Reproduce and evidence + +From the repository root, CPython 3.12, standard library only: + +```sh +uv run --python 3.12 --no-project python -I -O -B research/p104-target-order-delivery/verify.py +uv run --python 3.12 --no-project python scripts/research_package.py --package research/p104-target-order-delivery +``` + +Expected verifier marker: + +``` +PASS_P104_TARGET_ORDER_DELIVERY chains=32 extra_arrays=24 reads=416 lower_bound=32 controls=8 no_new_kappa +``` + +Default replay does not modify files; `--write` regenerates only this +package's `RESULT.json`. Assertions are not used for acceptance. Negative +controls reject an omitted read, duplicate read, omitted chain, wrong +survivor frame, reversed chain, broken target path, and decoder coefficient +mutation. The eighth control verifies nonzero dirty sensitivity for all +copies. Positive controls rederive the exact decoder, 55-chain best-order +witness, and eight single-cut chain numbers equal to 19. + +Actual focused checks ran on **CPython 3.12.12**: exact receipt generation, +isolated optimized replay, and the registered package replay passed with +the markers above and `PASS_REGISTERED_RESEARCH_PACKAGE`. The planning +control printed `PASS_COMPLEX_LOCAL_WORD_CEILING`. No full selected-supplier +cold replay, native compiler, hosted CI or proof assistant was run. + +The witness was discovered with OR-Tools CP-SAT 9.14.6206, one worker and +search tie-break seed 3. An initial 180-second unrestricted optimization +found 70 chains, not an improvement. Adding the proved rank-four lower +bound and asking for its exact attainment produced the 32-chain certificate. +No solver optimality report or floating-point calculation is used for +acceptance; neither OR-Tools nor its dependencies are needed for replay. +The universal statement is the written antichain proof plus this exact +finite attainment, not a claim inferred from an unsuccessful search. + +## Provenance, novelty and credit + +* Exact baseline: `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. +* Independent chooser seed: `4e1451a884a6979cb599a332ccc7ad40`, track + `complex-mechanisms`; original card `complex-rank-shape-decoder`. + The full original draw is in `SELECTION.json`; `TASK.json` declares the + changed scope before synthesis. +* Precise claim: + [round-two discussion 1929](https://github.com/CrocSwap/integer-mult-bounds/discussions/1929#discussioncomment-18925825). +* Ali Romman / **PR1125**, head + `9f7c0679d64bab954b7161d8586dc626a59b92ee`: the 32-path terminal-read + lower bound, uniform cube-support classification across 7168 decoders, + and the paid-downward-move and retained-cost budget qualifications. + Its README and proof are pinned inputs. It explicitly does not construct + a schedule at 32 paths; that constructive gap is the new contribution. + Its substantial OpenAI Codex attribution is retained. +* Josie Elliston / **PR1071**, head + `ce9531beba1ce115fdcdc44925ded995a29b8bac`: the pinned P104 fixture, + survivor geometry, single-cut and global-order delivery bounds, and the + explicit open per-target question. Its research credited substantial + Claude Opus 5.5 assistance; that attribution is retained. +* themilkman216 / **PR968**, head + `6a99e7240b961ac5e115ae6aa0301ec7c4a45d77`: frame-pair theorem and + exact eight-term decoder floor. DreamingOfClouds / **PR717**, live head + `4a97676294f9fa413b65986e9984fddeda71e4cc`: the decoder model, P104 + witnesses, and prior pricing questions. DreamingOfClouds / PR446 and + PR595 supply the inherited copied-information model. GamingPuzzled / + Joel Pulikkan / PR620 supplies the coordinate decoder lineage. +* Douglas Colkitt / **PR1240** supplies the pinned exact interval calculator + and the selected-word planning control; no ceiling outside its hypotheses + is inferred here. The selected PR1094/PR589 constructions are unchanged. +* Shared cached overlap coverage contained 579 open PRs and 547 discussion + records with complete pagination at 2026-10-14 14:10/14:11 UTC. The initial + narrow searches missed merged PR1125. A final live `P104` search over PR + titles and bodies found it; its exact head, README and proof were read + before publication, and the scope/claim was corrected to constructive + attainment. Live heads of PR1071, PR968 and PR717 were also rechecked. + This is a metadata overlap screen, not an exhaustive code-diff novelty + certificate. + The final targeted offline search used the parent's refreshed cache: + 584 open PRs at 14:27:47 UTC and 565 discussion records at 14:29:09 UTC, + both with complete pagination; it recovered PR1125's local package. + +Prepared for Adam Gall with substantial OpenAI Codex (gpt-6-astra) +assistance in research, proof, implementation and writing. Apache-2.0. +No independent human proof review or formal proof-assistant verification +is claimed. No frozen predecessor, selected record, or shared index changes. + +## Open next questions + +1. **Can the 24 extra exact copies be formed and restored cheaply on arbitrary + dirty arrays?** This determines whether the chain reduction survives a real + invoice. Start by compiling one of the rank-four-ending chains, including + its dirty-state correction and full cleanup. The blocker is an admitted + P104 copy/restoration interface, not the path-cover combinatorics. +2. **Can side corrections coexist with the layer-by-layer target order?** + The schedule proves only the centre delivery. The first experiment is to + splice its actual 416 reads into a fully specified P104 correction word + and check each physical frame and chronological dependency. No such + complete correction word is supplied here. +3. **What is the minimum complete tail moment at 32 chains?** The chain count + is sharp, but our profile is only an attaining witness. Optimize chain + assignments with exact rank costs while retaining the same support paths; + any result still needs the physical contracts above before supplier use. diff --git a/research/p104-target-order-delivery/RESULT.json b/research/p104-target-order-delivery/RESULT.json new file mode 100644 index 0000000000..eb60a8ba97 --- /dev/null +++ b/research/p104-target-order-delivery/RESULT.json @@ -0,0 +1,698 @@ +{ + "binary_entries": 14400, + "claim": "exact 32-chain minimum in minimal-prefix per-target-order geometry", + "conditional_tail_price": { + "intervals_by_saving_a": { + "0": { + "global_order_control": [ + "348962460715199493057337215094675886681087625019738686146310527147135459188809/57896044618658097711785492504343953926634992332820282019728792003956564819968", + "87240615178799873264334303773668971670271906254934671536577631786783864797227/14474011154664524427946373126085988481658748083205070504932198000989141204992" + ], + "new": [ + "99137062703181674164016254288260195079854438926062126746110945212254391815/28269553036454149273332760011886696253239742350009903329945699220681916416", + "406065408832232137375810577564713759047083781841150471152070431589393988874381/115792089237316195423570985008687907853269984665640564039457584007913129639936" + ], + "saving": [ + "291859512598166848738863852624638014315091468198326901140550622704876929503237/115792089237316195423570985008687907853269984665640564039457584007913129639936", + "36482439074770856092357981578079751789386433524790862642568827838109616187947/14474011154664524427946373126085988481658748083205070504932198000989141204992" + ] + }, + "1/99": { + "global_order_control": [ + "721407602934658417737179718394859955687565936451852611488029589341796896713115/115792089237316195423570985008687907853269984665640564039457584007913129639936", + "721407602934658417737179718394859955687565936451852611488029589341796896713353/115792089237316195423570985008687907853269984665640564039457584007913129639936" + ], + "new": [ + "420772770982484913667165711038603692784449599504138017379024798268515830208353/115792089237316195423570985008687907853269984665640564039457584007913129639936", + "420772770982484913667165711038603692784449599504138017379024798268515830208511/115792089237316195423570985008687907853269984665640564039457584007913129639936" + ], + "saving": [ + "75158707988043376017503501839064065725779084236928648527251197768320266626151/28948022309329048855892746252171976963317496166410141009864396001978282409984", + "37579353994021688008751750919532032862889542118464324263625598884160133313125/14474011154664524427946373126085988481658748083205070504932198000989141204992" + ] + }, + "3351/2000000": { + "global_order_control": [ + "701764501116108187133178602525896859343032736268122900684156034934728843422787/115792089237316195423570985008687907853269984665640564039457584007913129639936", + "175441125279027046783294650631474214835758184067030725171039008733682210855753/28948022309329048855892746252171976963317496166410141009864396001978282409984" + ], + "new": [ + "204233973598142615784700823904699155049025754354091011184213301751407055150563/57896044618658097711785492504343953926634992332820282019728792003956564819968", + "102116986799071307892350411952349577524512877177045505592106650875703527575321/28948022309329048855892746252171976963317496166410141009864396001978282409984" + ], + "saving": [ + "293296553919822955563776954716498549244981227559940878315729431431914733121503/115792089237316195423570985008687907853269984665640564039457584007913129639936", + "146648276959911477781888477358249274622490613779970439157864715715957366560943/57896044618658097711785492504343953926634992332820282019728792003956564819968" + ] + } + }, + "role_denominator": "none: this is a child-sum subtotal", + "scope": "copy tails from supplied singleton frames to rank nine only", + "width": 73 + }, + "controls": { + "all_dirty_copies_detected": true, + "broken_target_path": true, + "decoder_coefficient": true, + "duplicate_read": true, + "omitted_copy_chain": true, + "omitted_read": true, + "reversed_chain": true, + "wrong_survivor_frame": true + }, + "copy_ranks": [ + 7, + 7, + 7, + 7, + 7, + 7, + 7, + 7 + ], + "decoder_entries": 10816, + "global_order_control": { + "chains": 55, + "chains_per_centre": [ + 1, + 1, + 2, + 3, + 6, + 14, + 9, + 19 + ], + "chronological_event_sha256": "514b3d04d0ad54b1db59a902f9f89445ce6f05239068d6d4319f6540195a1b5f", + "copy_tail_mass": 440, + "copy_tail_profile": { + "1": 101, + "2": 27, + "3": 24, + "4": 28, + "5": 11, + "6": 4, + "7": 2, + "8": 1 + }, + "dirty_copy_sensitivity": [ + { + "affected_targets": 52, + "centre": 0, + "chain": 0 + }, + { + "affected_targets": 52, + "centre": 1, + "chain": 0 + }, + { + "affected_targets": 36, + "centre": 2, + "chain": 0 + }, + { + "affected_targets": 16, + "centre": 2, + "chain": 1 + }, + { + "affected_targets": 26, + "centre": 3, + "chain": 0 + }, + { + "affected_targets": 16, + "centre": 3, + "chain": 1 + }, + { + "affected_targets": 10, + "centre": 3, + "chain": 2 + }, + { + "affected_targets": 13, + "centre": 4, + "chain": 0 + }, + { + "affected_targets": 10, + "centre": 4, + "chain": 1 + }, + { + "affected_targets": 11, + "centre": 4, + "chain": 2 + }, + { + "affected_targets": 9, + "centre": 4, + "chain": 3 + }, + { + "affected_targets": 8, + "centre": 4, + "chain": 4 + }, + { + "affected_targets": 1, + "centre": 4, + "chain": 5 + }, + { + "affected_targets": 6, + "centre": 5, + "chain": 0 + }, + { + "affected_targets": 4, + "centre": 5, + "chain": 1 + }, + { + "affected_targets": 6, + "centre": 5, + "chain": 2 + }, + { + "affected_targets": 4, + "centre": 5, + "chain": 3 + }, + { + "affected_targets": 5, + "centre": 5, + "chain": 4 + }, + { + "affected_targets": 4, + "centre": 5, + "chain": 5 + }, + { + "affected_targets": 3, + "centre": 5, + "chain": 6 + }, + { + "affected_targets": 5, + "centre": 5, + "chain": 7 + }, + { + "affected_targets": 3, + "centre": 5, + "chain": 8 + }, + { + "affected_targets": 3, + "centre": 5, + "chain": 9 + }, + { + "affected_targets": 2, + "centre": 5, + "chain": 10 + }, + { + "affected_targets": 2, + "centre": 5, + "chain": 11 + }, + { + "affected_targets": 3, + "centre": 5, + "chain": 12 + }, + { + "affected_targets": 2, + "centre": 5, + "chain": 13 + }, + { + "affected_targets": 11, + "centre": 6, + "chain": 0 + }, + { + "affected_targets": 8, + "centre": 6, + "chain": 1 + }, + { + "affected_targets": 8, + "centre": 6, + "chain": 2 + }, + { + "affected_targets": 6, + "centre": 6, + "chain": 3 + }, + { + "affected_targets": 4, + "centre": 6, + "chain": 4 + }, + { + "affected_targets": 5, + "centre": 6, + "chain": 5 + }, + { + "affected_targets": 4, + "centre": 6, + "chain": 6 + }, + { + "affected_targets": 3, + "centre": 6, + "chain": 7 + }, + { + "affected_targets": 3, + "centre": 6, + "chain": 8 + }, + { + "affected_targets": 5, + "centre": 7, + "chain": 0 + }, + { + "affected_targets": 4, + "centre": 7, + "chain": 1 + }, + { + "affected_targets": 4, + "centre": 7, + "chain": 2 + }, + { + "affected_targets": 4, + "centre": 7, + "chain": 3 + }, + { + "affected_targets": 3, + "centre": 7, + "chain": 4 + }, + { + "affected_targets": 3, + "centre": 7, + "chain": 5 + }, + { + "affected_targets": 3, + "centre": 7, + "chain": 6 + }, + { + "affected_targets": 3, + "centre": 7, + "chain": 7 + }, + { + "affected_targets": 3, + "centre": 7, + "chain": 8 + }, + { + "affected_targets": 2, + "centre": 7, + "chain": 9 + }, + { + "affected_targets": 3, + "centre": 7, + "chain": 10 + }, + { + "affected_targets": 3, + "centre": 7, + "chain": 11 + }, + { + "affected_targets": 3, + "centre": 7, + "chain": 12 + }, + { + "affected_targets": 2, + "centre": 7, + "chain": 13 + }, + { + "affected_targets": 2, + "centre": 7, + "chain": 14 + }, + { + "affected_targets": 2, + "centre": 7, + "chain": 15 + }, + { + "affected_targets": 1, + "centre": 7, + "chain": 16 + }, + { + "affected_targets": 1, + "centre": 7, + "chain": 17 + }, + { + "affected_targets": 1, + "centre": 7, + "chain": 18 + } + ], + "events": 416, + "extra_arrays_beyond_eight": 47, + "rank_four_antichain": [ + 89, + 75, + 83, + 23, + 15, + 30, + 166, + 180, + 172, + 58, + 106, + 43, + 113, + 57, + 108, + 45, + 101, + 102, + 54, + 142, + 198, + 197, + 212, + 149, + 153, + 201, + 210, + 147, + 154, + 232, + 225, + 240 + ], + "target_tail_mass": 832, + "target_tail_profile": { + "1": 416, + "2": 12, + "3": 24, + "4": 32, + "5": 24, + "6": 12 + } + }, + "incompatible_global_order_witness": { + "first_precedence": [ + 0, + 6 + ], + "first_target": 0, + "second_precedence": [ + 6, + 0 + ], + "second_target": 1 + }, + "new_kappa": false, + "physical_supplier": false, + "schedule": { + "chains": 32, + "chains_per_centre": [ + 5, + 3, + 4, + 4, + 4, + 3, + 4, + 5 + ], + "chronological_event_sha256": "7bddc7c3cdc47cac4f363ac57048e18ea7205936ca93e6d9bd6974852f997dbf", + "copy_tail_mass": 256, + "copy_tail_profile": { + "1": 85, + "2": 17, + "3": 19, + "4": 20 + }, + "dirty_copy_sensitivity": [ + { + "affected_targets": 15, + "centre": 0, + "chain": 0 + }, + { + "affected_targets": 14, + "centre": 0, + "chain": 1 + }, + { + "affected_targets": 3, + "centre": 0, + "chain": 2 + }, + { + "affected_targets": 3, + "centre": 0, + "chain": 3 + }, + { + "affected_targets": 17, + "centre": 0, + "chain": 4 + }, + { + "affected_targets": 29, + "centre": 1, + "chain": 0 + }, + { + "affected_targets": 14, + "centre": 1, + "chain": 1 + }, + { + "affected_targets": 9, + "centre": 1, + "chain": 2 + }, + { + "affected_targets": 16, + "centre": 2, + "chain": 0 + }, + { + "affected_targets": 5, + "centre": 2, + "chain": 1 + }, + { + "affected_targets": 24, + "centre": 2, + "chain": 2 + }, + { + "affected_targets": 7, + "centre": 2, + "chain": 3 + }, + { + "affected_targets": 23, + "centre": 3, + "chain": 0 + }, + { + "affected_targets": 11, + "centre": 3, + "chain": 1 + }, + { + "affected_targets": 12, + "centre": 3, + "chain": 2 + }, + { + "affected_targets": 6, + "centre": 3, + "chain": 3 + }, + { + "affected_targets": 24, + "centre": 4, + "chain": 0 + }, + { + "affected_targets": 18, + "centre": 4, + "chain": 1 + }, + { + "affected_targets": 8, + "centre": 4, + "chain": 2 + }, + { + "affected_targets": 2, + "centre": 4, + "chain": 3 + }, + { + "affected_targets": 40, + "centre": 5, + "chain": 0 + }, + { + "affected_targets": 9, + "centre": 5, + "chain": 1 + }, + { + "affected_targets": 3, + "centre": 5, + "chain": 2 + }, + { + "affected_targets": 27, + "centre": 6, + "chain": 0 + }, + { + "affected_targets": 7, + "centre": 6, + "chain": 1 + }, + { + "affected_targets": 2, + "centre": 6, + "chain": 2 + }, + { + "affected_targets": 16, + "centre": 6, + "chain": 3 + }, + { + "affected_targets": 24, + "centre": 7, + "chain": 0 + }, + { + "affected_targets": 11, + "centre": 7, + "chain": 1 + }, + { + "affected_targets": 7, + "centre": 7, + "chain": 2 + }, + { + "affected_targets": 7, + "centre": 7, + "chain": 3 + }, + { + "affected_targets": 3, + "centre": 7, + "chain": 4 + } + ], + "events": 416, + "extra_arrays_beyond_eight": 24, + "rank_four_antichain": [ + 89, + 75, + 83, + 23, + 15, + 30, + 166, + 180, + 172, + 58, + 106, + 43, + 113, + 57, + 108, + 45, + 101, + 102, + 54, + 142, + 198, + 197, + 212, + 149, + 153, + 201, + 210, + 147, + 154, + 232, + 225, + 240 + ], + "target_tail_mass": 832, + "target_tail_profile": { + "1": 416, + "2": 12, + "3": 24, + "4": 32, + "5": 24, + "6": 12 + } + }, + "schema_version": 1, + "single_cut_control": [ + 19, + 19, + 19, + 19, + 19, + 19, + 19, + 19 + ], + "source_inputs": [ + "research/biframe-decoder-ladder/README.md", + "research/biframe-decoder-ladder/RESULTS.json", + "research/p104-asynchronous-carrier-bound/README.md", + "research/p104-asynchronous-carrier-bound/PROOF.md", + "research/complex-local-word-ceiling/ceiling.py" + ], + "tail_profile_difference": { + "1": 16, + "2": 10, + "3": 5, + "4": 8, + "5": 11, + "6": 4, + "7": 2, + "8": 1 + }, + "target_layer_counts": { + "2": 12, + "3": 24, + "4": 32, + "5": 24, + "6": 12 + } +} diff --git a/research/p104-target-order-delivery/SCHEDULE.json b/research/p104-target-order-delivery/SCHEDULE.json new file mode 100644 index 0000000000..7d5039302d --- /dev/null +++ b/research/p104-target-order-delivery/SCHEDULE.json @@ -0,0 +1,675 @@ +{ + "schema_version": 1, + "encoding": "Eight independent survivor labels; bit k names centre k in pinned pairs_doubled_coordinates. Parent [mask,k] adds bit k to mask without k.", + "parent_edges": [ + [ + 2, + 1 + ], + [ + 4, + 2 + ], + [ + 6, + 1 + ], + [ + 8, + 3 + ], + [ + 9, + 0 + ], + [ + 10, + 1 + ], + [ + 11, + 1 + ], + [ + 14, + 2 + ], + [ + 15, + 2 + ], + [ + 16, + 4 + ], + [ + 17, + 0 + ], + [ + 18, + 4 + ], + [ + 19, + 0 + ], + [ + 22, + 2 + ], + [ + 23, + 0 + ], + [ + 25, + 4 + ], + [ + 26, + 3 + ], + [ + 30, + 2 + ], + [ + 32, + 5 + ], + [ + 36, + 2 + ], + [ + 38, + 1 + ], + [ + 40, + 3 + ], + [ + 41, + 0 + ], + [ + 42, + 5 + ], + [ + 43, + 0 + ], + [ + 44, + 3 + ], + [ + 45, + 0 + ], + [ + 54, + 4 + ], + [ + 55, + 0 + ], + [ + 57, + 4 + ], + [ + 58, + 5 + ], + [ + 59, + 0 + ], + [ + 61, + 4 + ], + [ + 63, + 2 + ], + [ + 64, + 6 + ], + [ + 65, + 0 + ], + [ + 73, + 3 + ], + [ + 75, + 1 + ], + [ + 79, + 2 + ], + [ + 81, + 6 + ], + [ + 83, + 6 + ], + [ + 87, + 6 + ], + [ + 89, + 6 + ], + [ + 96, + 5 + ], + [ + 97, + 5 + ], + [ + 100, + 2 + ], + [ + 101, + 2 + ], + [ + 102, + 1 + ], + [ + 103, + 1 + ], + [ + 104, + 3 + ], + [ + 106, + 6 + ], + [ + 108, + 3 + ], + [ + 110, + 3 + ], + [ + 111, + 3 + ], + [ + 113, + 5 + ], + [ + 115, + 5 + ], + [ + 117, + 2 + ], + [ + 118, + 4 + ], + [ + 122, + 6 + ], + [ + 123, + 6 + ], + [ + 128, + 7 + ], + [ + 132, + 7 + ], + [ + 134, + 7 + ], + [ + 142, + 7 + ], + [ + 143, + 7 + ], + [ + 144, + 7 + ], + [ + 145, + 7 + ], + [ + 146, + 1 + ], + [ + 147, + 0 + ], + [ + 148, + 2 + ], + [ + 149, + 2 + ], + [ + 153, + 7 + ], + [ + 154, + 3 + ], + [ + 155, + 0 + ], + [ + 157, + 2 + ], + [ + 159, + 2 + ], + [ + 164, + 7 + ], + [ + 166, + 7 + ], + [ + 172, + 3 + ], + [ + 173, + 0 + ], + [ + 180, + 5 + ], + [ + 181, + 5 + ], + [ + 182, + 7 + ], + [ + 185, + 7 + ], + [ + 186, + 5 + ], + [ + 188, + 3 + ], + [ + 190, + 3 + ], + [ + 192, + 6 + ], + [ + 193, + 0 + ], + [ + 196, + 6 + ], + [ + 197, + 0 + ], + [ + 198, + 6 + ], + [ + 199, + 0 + ], + [ + 201, + 3 + ], + [ + 203, + 1 + ], + [ + 205, + 3 + ], + [ + 206, + 6 + ], + [ + 208, + 4 + ], + [ + 210, + 1 + ], + [ + 212, + 4 + ], + [ + 215, + 4 + ], + [ + 218, + 3 + ], + [ + 219, + 0 + ], + [ + 224, + 7 + ], + [ + 225, + 7 + ], + [ + 229, + 7 + ], + [ + 232, + 7 + ], + [ + 234, + 7 + ], + [ + 237, + 3 + ], + [ + 238, + 7 + ], + [ + 240, + 4 + ], + [ + 242, + 1 + ], + [ + 245, + 7 + ], + [ + 246, + 7 + ], + [ + 248, + 4 + ], + [ + 249, + 6 + ] + ], + "chains": [ + [ + [ + 9, + 41, + 45, + 173 + ], + [ + 17, + 19, + 147, + 155, + 219 + ], + [ + 23, + 55 + ], + [ + 43, + 59 + ], + [ + 65, + 193, + 197, + 199 + ] + ], + [ + [ + 2, + 6, + 38, + 102, + 103 + ], + [ + 10, + 11, + 75, + 203 + ], + [ + 146, + 210, + 242 + ] + ], + [ + [ + 4, + 14, + 15, + 79 + ], + [ + 22, + 30, + 63 + ], + [ + 36, + 100, + 101, + 117 + ], + [ + 148, + 149, + 157, + 159 + ] + ], + [ + [ + 8, + 73, + 201, + 205, + 237 + ], + [ + 26, + 154, + 218 + ], + [ + 40, + 44, + 172, + 188, + 190 + ], + [ + 104, + 108, + 110, + 111 + ] + ], + [ + [ + 16, + 208, + 240, + 248 + ], + [ + 18, + 54, + 118 + ], + [ + 25, + 57, + 61 + ], + [ + 212, + 215 + ] + ], + [ + [ + 32, + 96, + 97, + 113, + 115 + ], + [ + 42, + 58, + 186 + ], + [ + 180, + 181 + ] + ], + [ + [ + 64, + 106, + 122, + 123 + ], + [ + 81, + 83, + 87 + ], + [ + 89, + 249 + ], + [ + 192, + 196, + 198, + 206 + ] + ], + [ + [ + 128, + 144, + 145, + 153, + 185 + ], + [ + 132, + 164, + 166, + 182, + 246 + ], + [ + 134, + 142, + 143 + ], + [ + 224, + 232, + 234, + 238 + ], + [ + 225, + 229, + 245 + ] + ] + ], + "discovery": { + "solver": "OR-Tools CP-SAT 9.14.6206", + "workers": 1, + "random_seed": 3, + "search": "Feasibility at the proved 32-chain rank-four-antichain lower bound; solver optimality is not trusted.", + "copy_chain_count": 32 + } +} diff --git a/research/p104-target-order-delivery/SELECTION.json b/research/p104-target-order-delivery/SELECTION.json new file mode 100644 index 0000000000..1285433379 --- /dev/null +++ b/research/p104-target-order-delivery/SELECTION.json @@ -0,0 +1,45 @@ +{ + "seed": "4e1451a884a6979cb599a332ccc7ad40", + "track": "complex-mechanisms", + "suggestions": [ + { + "task_id": "complex-rank-shape-decoder", + "scope_key": "02b31ebd160542c86299", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "method": "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "starting_points": ["research/complex-local-word-ceiling/README.md", "research/complex-decoder-field-extension-seed44/README.md", "research/complex-frame-pair-decoders/README.md"], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound.", + "first_step": {"command": ["python3", "-B", "research/complex-local-word-ceiling/verify.py"], "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."}, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": ["One masked, overcomplete or block decoder family with exact labels and supports.", "A scoped lower bound on effective rank for one alphabet.", "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."], + "scope_change_triggers": ["Repacking idle remainders of an unchanged word (covered by the packing ceiling).", "Repeating the eight-term all-pairs search inside its proved scope."], + "overlap_terms": ["rank shape", "block climb", "masked decoder", "overcomplete", "effective rank"], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + }, + { + "task_id": "complex-new-helper-inventory", + "scope_key": "5868e5281a1e63d41a22", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "method": "Propose a changed helper inventory and derive an optimistic exact moment.", + "starting_points": ["research/complex-local-word-ceiling/README.md", "research/heterogeneous-owner-assembly/README.md", "certificates/selected-result.json"], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model.", + "first_step": {"command": ["python3", "-B", "research/complex-local-word-ceiling/verify.py"], "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."}, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": ["Narrow to one changed boundary or helper type with explicit counts.", "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."], + "scope_change_triggers": ["Mixing only providers already inside the pinned catalogue."], + "overlap_terms": ["helper inventory", "heterogeneous-owner", "mutable leaver"], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + } + ], + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "catalog_assessed_on": "2026-10-13", + "priority_revision": 3, + "priority_log": "docs/research/research-priority-log.md", + "catalog_sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "selected": {"kappa": "836330098538459/500000000000000000", "review": "docs/research/community-batch1099-review.md", "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", "reproduce": "make frontier1094-verify"}, + "status": "SUGGESTIONS_ONLY_NOT_RESERVED", + "next_step": "Check live overlap, refine one question's object and domain, and record a bounded task card. A different seed or scope key is not evidence of novelty." +} diff --git a/research/p104-target-order-delivery/SOURCES.json b/research/p104-target-order-delivery/SOURCES.json new file mode 100644 index 0000000000..9613208685 --- /dev/null +++ b/research/p104-target-order-delivery/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/biframe-decoder-ladder/README.md", + "usage": "input", + "git_blob": "65afcf129309dc87e6090557e66d750d19bd5705", + "sha256": "95b71fb2e519e258811882d8d06359090da7a697aa77ba4c326c25a66d00bd36" + }, + { + "path": "research/biframe-decoder-ladder/RESULTS.json", + "usage": "input", + "git_blob": "2e16f99b295bb386fd13bd8fbd57b42ef54143a9", + "sha256": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4" + }, + { + "path": "research/p104-asynchronous-carrier-bound/README.md", + "usage": "input", + "git_blob": "85bd8278ec9725aa154bd846172f768a44b67612", + "sha256": "b65ebf972b24109ce40b36b92d372434c4a6ff0d07a1d464b2a36032536e7fef" + }, + { + "path": "research/p104-asynchronous-carrier-bound/PROOF.md", + "usage": "input", + "git_blob": "8e42ca7fd65557d57ab8ba5045e5cc8c9495794f", + "sha256": "63a915d06981eb6d85af8ff594de57bc86d2fabfa8b40563927ae67f75e4a355" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + } + ] +} diff --git a/research/p104-target-order-delivery/TASK.json b/research/p104-target-order-delivery/TASK.json new file mode 100644 index 0000000000..1ad237ec1b --- /dev/null +++ b/research/p104-target-order-delivery/TASK.json @@ -0,0 +1,91 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Construct a globally executable 32-chain per-target-order schedule attaining Ali Romman's PR1125 lower bound for the exact 104-port, eight-centre fixture in PR1071/biframe-decoder-ladder. Certify all chronological frame moves and the complete supplied-copy tail invoice; do not claim the existing 32 lower bound as new.", + "scope_change_reason": "The emitted card asks for a new block decoder and a complete supplier gain. The source-pinned P104 decoder already saves eight copy ranks but its delivery is unresolved. The investigation changes PR1071's global-order restriction. Final merged/local overlap revealed PR1125 already proves the stronger asynchronous 32-path obstruction, while explicitly excluding schedule attainment; the new contribution is the attaining witness and tail invoice only. No complete supplier or five-percent acceptance claim is made.", + "bottleneck_link": "The P104 decoder has copy rank 56 instead of 64, but incompatible survivor frames require additional delivery arrays. Reducing the exact chain count and pricing its monotone paths addresses this concrete barrier rather than repacking the selected word.", + "budget_minutes": 60, + "stop_rule": "Analyze the one pinned P104 fixture only; use bounded combinatorial synthesis with exact independently checked certificates. Stop with an exact geometric construction or obstruction, not an unpriced physical supplier.", + "outcome": "completed", + "evidence": "SCHEDULE.json gives 116 exact prefix edges and 32 chains. RESULT.json binds all 10816 decoder entries, 14400 binary pairings, eight rank-seven drops, 416 chronological reads, the 32-element rank-four antichain, complete supplied-boundary tail profiles, interval prices and eight controls. The supplied-copy dirty-state limitation is tested on every chain.", + "author": "Adam Gall, with substantial OpenAI Codex assistance", + "ai_assistance": "OpenAI Codex (gpt-6-astra) for research, implementation, proof and documentation.", + "selection_seed": "4e1451a884a6979cb599a332ccc7ad40", + "track": "complex-mechanisms", + "scope_key": "p104-pinned-biframe-independent-target-orders-monotone-delivery", + "method_domain": "All 104 targets and eight centre labels of section4_explicit_P104, separate permutations of each target's nonzero row support, each centre copy follows a nested sequence of exact read frames with no further drop.", + "optimistic_budget": "Inherited COPY56 remains. At the explicit boundary of 32 exact copies already at singleton survivor frames, delivery tails cost {1:85,2:17,3:19,4:20} (mass256), target tails {1:416,2:12,3:24,4:32,5:24,6:12} (mass832), and 416 scalar reads remain. Formation of 24 extra exact copies, gather, restoration, side corrections, hosting and precision are explicit unknown nonzero obligations. The selected-word ceiling is not applied to this incomplete interface.", + "success_falsification": "Success: an exact executable 32-chain schedule attaining the credited PR1125 lower bound, with all chronological and frame constraints. Falsification: an omitted/duplicated read, nonnested chain, cyclic dependency, failed decoder identity or hidden uncharged physical operation.", + "predecessors": [ + "Ali Romman / PR1125 head9f7c0679d64bab954b7161d8586dc626a59b92ee: existing asynchronous 32-path lower bound, all7168 cube supports, paid-drop and retained-cost qualifications; no attaining schedule constructed", + "biframe-decoder-ladder: fixed P104 decoder, 55-chain/47-extra-copy optimum over 40320 global orders; per-target orders explicitly excluded", + "themilkman216 / PR968 and DreamingOfClouds / PR717: frame-pair decoder floor and copied-rank56", + "DreamingOfClouds / PR446: copied-information frame model" + ], + "overlap": "Initial narrow search missed merged/local PR1125. Final live P104 title/body search found it; its README and proof were read and pinned before publication. Attribution/scope corrected to attaining its known32 bound. Live heads1071,968,717 also checked. Shared final cache:584 open PRs and565 discussion records, complete pagination at2026-10-14T14:27:47Z/14:29:09Z. Metadata and local evidence do not prove exhaustive novelty.", + "open_questions": [ + { + "question": "Can the certified delivery geometry be implemented with arbitrary dirty helper state, restored helpers and legal source/target timing?", + "why_it_matters": "A geometric chain saving is not a paid recursive supplier improvement.", + "first_step": "Compile one certified chain into the actual P104 gather/drop/read/restore interface and price all rank transport.", + "blocked_by": "No admitted P104 delivery/restoration contract is supplied by the predecessor." + }, + { + "question": "Can the layer-by-layer read order coexist with a physical P104 side-correction word?", + "why_it_matters": "Chronological centre delivery alone is not the complete unit.", + "first_step": "Splice the 416 certified reads into one specified correction word and check all physical frames and dependencies.", + "blocked_by": "A complete admitted P104 side-correction word is not supplied." + }, + { + "question": "What is the minimum supplied-boundary tail moment among 32-chain schedules?", + "why_it_matters": "The chain minimum is proved, but the attained rank histogram is not claimed moment-optimal.", + "first_step": "Optimize chain assignments for the fixed prefix paths with exact rank costs.", + "blocked_by": "Physical admission still requires the copy/restoration and correction interfaces." + } + ] +} diff --git a/research/p104-target-order-delivery/VERIFY.json b/research/p104-target-order-delivery/VERIFY.json new file mode 100644 index 0000000000..ee1e19af16 --- /dev/null +++ b/research/p104-target-order-delivery/VERIFY.json @@ -0,0 +1,26 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/biframe-decoder-ladder/README.md", + "research/biframe-decoder-ladder/RESULTS.json", + "research/p104-asynchronous-carrier-bound/README.md", + "research/p104-asynchronous-carrier-bound/PROOF.md", + "research/complex-local-word-ceiling/ceiling.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All P104 decoder entries and pairing ranks; 32-chain lower bound and exact chronological attainment; complete supplied-boundary frame profiles; predecessor positive controls and eight semantic negative/limitation controls" + } + ] +} diff --git a/research/p104-target-order-delivery/verify.py b/research/p104-target-order-delivery/verify.py new file mode 100755 index 0000000000..16e790d730 --- /dev/null +++ b/research/p104-target-order-delivery/verify.py @@ -0,0 +1,402 @@ +#!/usr/bin/env python3 +"""Exact certificate replay for one P104 per-target delivery geometry. + +Standard library only. All acceptance checks remain enabled under -O. +The supplied-copy boundary is explicit: no dirty-copy compiler is assumed. +""" +from __future__ import annotations + +import argparse +from collections import Counter, defaultdict +from copy import deepcopy +from hashlib import sha256 +from itertools import combinations, product +from fractions import Fraction +import importlib.util +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def basis(rows): + pivots = {} + for value in rows: + while value: + bit = value.bit_length() - 1 + if bit in pivots: + value ^= pivots[bit] + else: + pivots[bit] = value + break + return tuple(pivots.values()) + + +def in_span(value, vectors): + return len(basis((*vectors, value))) == len(basis(vectors)) + + +def rank(rows): + return len(basis(rows)) + + +def inner(a, b): + numerator = sum(x * y for x, y in zip(a, b)) + require(numerator % 4 == 0, "nonintegral E8 pairing") + return numerator // 4 + + +def roots(): + result = [] + for i, j in combinations(range(8), 2): + for sign in (-1, 1): + row = [0] * 8 + row[i], row[j] = 2, 2 * sign + result.append(tuple(row)) + for signs in product((-1, 1), repeat=7): + if signs.count(-1) % 2 == 0: + result.append((1, *signs)) + require(len(set(result)) == 120, "root count") + require(all(inner(r, r) == 2 for r in result), "root norm") + return sorted(result) + + +def source_check(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + pins = [] + for item in manifest["files"]: + if item["usage"] != "input": + continue + data = (ROOT / item["path"]).read_bytes() + require(sha256(data).hexdigest() == item["sha256"], "source hash: " + item["path"]) + pins.append(item["path"]) + return pins + + +def geometry(): + source = json.loads((ROOT / "research/biframe-decoder-ladder/RESULTS.json").read_text()) + fixture = source["section4_explicit_P104"] + lines = roots() + index = {r: i for i, r in enumerate(lines)} + pairs = [(tuple(a), tuple(b)) for a, b in fixture["pairs_doubled_coordinates"]] + require(len(pairs) == 8 and all(a in index and b in index for a, b in pairs), "centre roots") + removed = {tuple(r) for r in fixture["F0"] + fixture["C"]} + require(len(removed) == 16 and removed <= set(lines), "puncture") + ports = [r for r in lines if r not in removed] + gram = [[inner(a, b) for b in lines] for a in lines] + binary = [sum(((entry + 1) & 1) << j for j, entry in enumerate(row)) for row in gram] + indices = [] + independent = [] + for i, row in enumerate(binary): + if not in_span(row, independent): + independent.append(row) + indices.append(i) + require(len(indices) == 9, "binary pairing rank") + # Coordinate restriction to independent columns is injective on the row space. + labels = [sum(((row >> j) & 1) << k for k, j in enumerate(indices)) for row in binary] + require(rank(labels) == 9 and len(set(labels)) == 120, "label embedding") + for a in range(120): + for b in range(120): + require(((binary[a] >> b) & 1) == ((gram[a][b] + 1) & 1), "binary geometry") + centre_labels = [labels[index[a]] for a, _ in pairs] + require(rank(centre_labels) == 8, "eight independent survivor labels") + d = [[inner(r, a) for a, _ in pairs] for r in ports] + t = [] + for r in ports: + row = [] + for a, b in pairs: + ab = inner(a, b) + require(abs(ab) == 1, "mixed centre pair") + row.append(2 * inner(r, b) // ab) + t.append(row) + require(all(sum(d[i][k] * t[j][k] for k in range(8)) == 2 * inner(a, b) + for i, a in enumerate(ports) for j, b in enumerate(ports)), "decoder identity") + costs = [] + for k, (a, b) in enumerate(pairs): + readers = [i for i, r in enumerate(ports) if d[i][k]] + sources = [j for j, r in enumerate(ports) if t[j][k]] + require(len(readers) == len(sources) == 52, "centre support count") + rlabels = [labels[index[ports[i]]] for i in readers] + slabels = [labels[index[ports[j]]] for j in sources] + require(rank(rlabels) == rank(slabels) == 8, "centre hyperplanes") + require(in_span(centre_labels[k], slabels), "survivor in gather span") + require(all((inner(a, ports[i]) + 1) % 2 == 0 for i in readers), "survivor orthogonal to readers") + pairing = [sum(((inner(ports[i], ports[j]) + 1) & 1) << v + for v, j in enumerate(sources)) for i in readers] + costs.append(rank(pairing)) + require(costs == [7] * 8, "COPY56") + masks = [sum(bool(value) << k for k, value in enumerate(row)) for row in d] + require(len(set(masks)) == 104, "distinct target masks") + require(Counter(m.bit_count() for m in masks) == {2: 12, 3: 24, 4: 32, 5: 24, 6: 12}, "target layers") + return {"ports": ports, "pairs": pairs, "d": d, "t": t, "masks": masks, + "labels": centre_labels, "best_global_order": fixture["staggered_best_global_order"]} + + +def minimum_chains(vertices): + """Bipartite matching supplies an explicit minimum chain cover of subsets.""" + vertices = sorted(set(vertices), key=lambda s: (s.bit_count(), s)) + successors = [[j for j, b in enumerate(vertices) if a != b and a & b == a] + for a in vertices] + matched = {} + + def augment(i, seen): + for j in successors[i]: + if j not in seen: + seen.add(j) + if j not in matched or augment(matched[j], seen): + matched[j] = i + return True + return False + + for i in range(len(vertices)): + augment(i, set()) + forward = {i: j for j, i in matched.items()} + chains = [] + for i in range(len(vertices)): + if i not in matched: + chain = [vertices[i]] + while i in forward: + i = forward[i] + chain.append(vertices[i]) + chains.append(chain) + require(sum(map(len, chains)) == len(vertices), "matching cover") + return chains + + +def orders_from_tree(certificate, masks): + edges = certificate["parent_edges"] + parent = {} + for s, k in edges: + require(isinstance(s, int) and 0 < s < 256 and isinstance(k, int) and 0 <= k < 8, + "parent edge domain") + require(s >> k & 1 and s not in parent, "parent edge uniqueness") + parent[s] = k + used = set() + orders = [] + for mask in masks: + reverse = [] + s = mask + while s: + require(s in parent, "missing path prefix") + used.add(s) + k = parent[s] + reverse.append(k) + s ^= 1 << k + orders.append(list(reversed(reverse))) + require(used == set(parent), "unused tree edges") + return orders + + +def events_from_orders(orders, masks): + require(len(orders) == len(masks), "target order count") + events = [] + for target, (order, expected) in enumerate(zip(orders, masks)): + mask = 0 + for k in order: + require(isinstance(k, int) and 0 <= k < 8 and not (mask >> k & 1), "repeated or invalid read") + mask |= 1 << k + events.append((mask.bit_count(), mask, k, target)) + require(mask == expected, "missing or extra target read") + require(len(events) == 416, "read event count") + return sorted(events) + + +def evaluate(orders, chains, geo): + events = events_from_orders(orders, geo["masks"]) + require(len(chains) == 8 and all(chains), "centre chain inventory") + used = {(s, k) for _, s, k, _ in events} + assignment = {} + for k, centre_chains in enumerate(chains): + for ci, chain in enumerate(centre_chains): + require(chain, "empty chain") + previous = 1 << k + for s in chain: + require(isinstance(s, int) and 0 < s < 256 and s >> k & 1, "chain frame domain") + require(previous & s == previous, "nonnested copy chain") + require((s, k) not in assignment, "duplicate chain frame") + assignment[s, k] = ci + previous = s + require(set(assignment) == used, "chain event coverage") + # Direct replay provides a chronological certificate, not just a path cover. + target_frame = [0] * 104 + copy_frame = [[1 << k for _ in c] for k, c in enumerate(chains)] + h_copy, h_target = Counter(), Counter() + delivered = [[0] * 8 for _ in range(104)] + reads_per_copy = defaultdict(list) + for dimension, frame, k, target in events: + require(frame == (target_frame[target] | (1 << k)), "target chronological frame") + require(target_frame[target] != frame, "target read duplicated") + ci = assignment[frame, k] + previous = copy_frame[k][ci] + require(previous & frame == previous, "copy chronological frame") + delta = dimension - previous.bit_count() + if delta: + h_copy[delta] += 1 + h_target[dimension - target_frame[target].bit_count()] += 1 + copy_frame[k][ci] = frame + target_frame[target] = frame + delivered[target][k] += geo["d"][target][k] + reads_per_copy[k, ci].append(target) + require(delivered == geo["d"], "scalar delivery map") + for k, frames in enumerate(copy_frame): + for frame in frames: + h_copy[9 - frame.bit_count()] += 1 + for mask in target_frame: + h_target[8 - mask.bit_count()] += 1 + chain_count = sum(map(len, chains)) + require(sum(r * n for r, n in h_copy.items()) == 8 * chain_count, "copy tail mass") + require(sum(r * n for r, n in h_target.items()) == 8 * 104, "target tail mass") + # Every final target frame of rank four is a distinct required visit. + rank_four = [m for m in geo["masks"] if m.bit_count() == 4] + require(len(rank_four) == 32 and len(set(rank_four)) == 32, "rank-four antichain") + require(all(a & b != a and a & b != b for a, b in combinations(rank_four, 2)), "antichain inclusion") + # Extra dirty input on a supplied copy reaches a target with nonzero coefficient. + # This certifies the boundary limitation, not a dirty-copy implementation. + require(len(reads_per_copy) == chain_count, "unused copy") + dirty_sensitivity = [] + for (k, ci), targets in sorted(reads_per_copy.items()): + residual = [0] * 104 + for target in targets: + residual[target] += geo["d"][target][k] + require(any(residual), "dirty sensitivity unexpectedly zero") + dirty_sensitivity.append({"centre": k, "chain": ci, "affected_targets": sum(bool(v) for v in residual)}) + return {"chains": chain_count, "chains_per_centre": list(map(len, chains)), + "extra_arrays_beyond_eight": chain_count - 8, + "events": len(events), "rank_four_antichain": rank_four, + "copy_tail_profile": {str(k): v for k, v in sorted(h_copy.items())}, + "target_tail_profile": {str(k): v for k, v in sorted(h_target.items())}, + "copy_tail_mass": 8 * chain_count, "target_tail_mass": 832, + "dirty_copy_sensitivity": dirty_sensitivity, + "chronological_event_sha256": sha256(json.dumps(events, separators=(",", ":")).encode()).hexdigest()} + +def conditional_price(new, old): + """Price only the declared delivered-copy tails, not a supplier moment.""" + path = ROOT / "research/complex-local-word-ceiling/ceiling.py" + spec = importlib.util.spec_from_file_location("p104_pinned_intervals", path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + prices = {} + for a in (Fraction(0), Fraction(3351, 2000000), Fraction(1, 99)): + intervals = {} + for name, profile in (("new", new), ("global_order_control", old)): + lo = hi = Fraction(0) + for r, count in profile.items(): + low, high = module.child_cost(int(r), 73, a) + lo += count * low + hi += count * high + intervals[name] = (lo, hi) + nlo, nhi = intervals["new"] + olo, ohi = intervals["global_order_control"] + require(nhi < olo, "conditional delivery-tail moment improvement") + prices[str(a)] = { + "new": [str(nlo), str(nhi)], + "global_order_control": [str(olo), str(ohi)], + "saving": [str(olo - nhi), str(ohi - nlo)], + } + return {"width": 73, "role_denominator": "none: this is a child-sum subtotal", + "scope": "copy tails from supplied singleton frames to rank nine only", + "intervals_by_saving_a": prices} + + + +def global_control(geo): + order = geo["best_global_order"] + orders = [[k for k in order if mask >> k & 1] for mask in geo["masks"]] + events = events_from_orders(orders, geo["masks"]) + chains = [minimum_chains([s for _, s, key, _ in events if key == k]) for k in range(8)] + receipt = evaluate(orders, chains, geo) + require(receipt["chains"] == 55, "predecessor global-order control") + return receipt + + +def rejected(fn): + try: + fn() + except (ValueError, KeyError): + return True + raise ValueError("mutation was accepted") + + +def run(): + pins = source_check() + geo = geometry() + certificate = json.loads((HERE / "SCHEDULE.json").read_text()) + orders = orders_from_tree(certificate, geo["masks"]) + chains = certificate["chains"] + result = evaluate(orders, chains, geo) + require(result["chains"] == 32, "sharp antichain attainment") + directions = {} + conflict = None + for target, order in enumerate(orders): + for i, k in enumerate(order): + for other in order[i + 1:]: + if (other, k) in directions and conflict is None: + conflict = {"first_target": directions[other, k], "second_target": target, + "first_precedence": [other, k], "second_precedence": [k, other]} + directions[k, other] = target + require(conflict is not None, "per-target order genuinely differs from global order") + control = global_control(geo) + difference = {r: control["copy_tail_profile"].get(r, 0) - result["copy_tail_profile"].get(r, 0) + for r in set(control["copy_tail_profile"]) | set(result["copy_tail_profile"])} + require(all(count >= 0 for count in difference.values()) and any(difference.values()), + "componentwise conditional tail dominance") + single_cut = [len(minimum_chains([m for m in geo["masks"] if m >> k & 1])) for k in range(8)] + require(single_cut == [19] * 8, "single-cut predecessor control") + # Rebinding the matrix identity catches a coefficient error independently of scheduling. + bad_d = deepcopy(geo["d"]) + bad_d[0][next(k for k, value in enumerate(bad_d[0]) if value)] += 1 + require(any(sum(bad_d[i][k] * geo["t"][j][k] for k in range(8)) != 2 * inner(a, b) + for i, a in enumerate(geo["ports"]) for j, b in enumerate(geo["ports"])), "coefficient mutation") + bad_orders = deepcopy(orders) + bad_orders[0].pop() + controls = {"omitted_read": rejected(lambda: evaluate(bad_orders, chains, geo))} + repeated = deepcopy(orders) + repeated[0].append(repeated[0][0]) + controls["duplicate_read"] = rejected(lambda: evaluate(repeated, chains, geo)) + missing = deepcopy(chains) + missing[0].pop() + controls["omitted_copy_chain"] = rejected(lambda: evaluate(orders, missing, geo)) + wrong = deepcopy(chains) + wrong[0][0][0] ^= 1 + controls["wrong_survivor_frame"] = rejected(lambda: evaluate(orders, wrong, geo)) + reverse = deepcopy(chains) + k, ci = next((k, ci) for k, cs in enumerate(reverse) for ci, c in enumerate(cs) if len(c) > 1) + reverse[k][ci] = list(reversed(reverse[k][ci])) + controls["reversed_chain"] = rejected(lambda: evaluate(orders, reverse, geo)) + bad_tree = deepcopy(certificate) + bad_tree["parent_edges"].pop() + controls["broken_target_path"] = rejected(lambda: orders_from_tree(bad_tree, geo["masks"])) + controls["decoder_coefficient"] = True + controls["all_dirty_copies_detected"] = len(result["dirty_copy_sensitivity"]) == 32 + return {"schema_version": 1, "claim": "exact 32-chain minimum in minimal-prefix per-target-order geometry", + "source_inputs": pins, "decoder_entries": 10816, "binary_entries": 14400, + "copy_ranks": [7] * 8, "target_layer_counts": {str(k): v for k, v in sorted(Counter(m.bit_count() for m in geo["masks"]).items())}, + "schedule": result, "global_order_control": control, + "conditional_tail_price": conditional_price(result["copy_tail_profile"], control["copy_tail_profile"]), + "tail_profile_difference": dict(sorted(difference.items(), key=lambda kv: int(kv[0]))), + "incompatible_global_order_witness": conflict, + "single_cut_control": single_cut, "controls": controls, + "physical_supplier": False, "new_kappa": False} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="regenerate this package's exact receipt") + args = parser.parse_args() + result = run() + destination = HERE / "RESULT.json" + if args.write: + destination.write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + require(json.loads(destination.read_text()) == result, "stored result mismatch") + print("PASS_P104_TARGET_ORDER_DELIVERY chains=32 extra_arrays=24 reads=416 lower_bound=32 controls=8 no_new_kappa") + + +if __name__ == "__main__": + main()