diff --git a/research/p104-joint-endpoint-obstruction/README.md b/research/p104-joint-endpoint-obstruction/README.md new file mode 100644 index 0000000000..e738e6aa46 --- /dev/null +++ b/research/p104-joint-endpoint-obstruction/README.md @@ -0,0 +1,235 @@ +# P104 joint endpoint obstruction for the 423-lifetime profile + +The named profile in [PR2941][2941], **232 cheap lifetimes, 180 unit-step +lifetimes and 11 lifetimes skipping dimension three**, cannot realize the +frozen X-only monotone correction. The two endpoint systems must use the same +cheap source-to-target flags. A finite necessary-condition certificate then +requires at least 235 distinct flags under the assumed 232-flag budget. + +This rejects that profile even though PR2941 reports a passing optimistic +moment and passing separate endpoint screens. It does not correct an error in +PR2941, which explicitly leaves joint realization open. It supplies no new +universal lifetime threshold, feasible correction, supplier or kappa. The +selected result and predecessor packages are unchanged. + +## Model and exact question + +Use the original 4,058-event P104 `G/2` channel retained by PR1991. The added +correction must implement `I-G/2` on independent immutable X inputs, with +write-only targets Y. Original data-frame paths are fixed. New helpers start +at ZERO with source-independent arbitrary dirty values, move only through +increasing binary subspaces, end at FULL and restore their logical dirt. +Reinitialization starts another lifetime. Same-frame linear operations, +relays, cancellation and singular mixing are allowed. Reading Y or original +helper/private fields, writing X, descending, or source-dependent initial +state is outside this model. + +A cheap lifetime has dimension jumps `(1,7,1)`. The other 191 lifetimes have +jumps `(1,1,1,1,1,1,1,1,1)` or `(1,1,2,1,1,1,1,1)`. Call these broad lifetimes. +The proof generously gives every broad endpoint contact its maximum proper +subspace capacity; it does not use the missing dimension-three contact. +Thus replacing that history by a unit-step history does not evade this test +at the same cheap/broad counts. + +Scientific base main is `05eee6613f843dd754528c9b2da8049757382ef6`, priority +revision 5. The named pending predecessor is PR2941 at +`df29f70185979e32c73efc5f6e2903652d744ae7`; its price is not recomputed here. +[The canonical claim][claim] records live coordination. [SOURCES.json](SOURCES.json) +pins the original JSON inputs and the reused geometry implementation. No +pending construction is promoted to a reviewed supplier. + +## From programs to one shared edge set + +Retain the residual sets of PR2896/2909/2920. For target t, `N_t` contains +required source labels absent from every earlier proper Y frame, after +forgiving all direct X-to-final-Y contacts. For source s, `F_s` contains +required target normals for which no later proper X frame lies in that target +hyperplane. The executable reconstructs these sets from the original word, +not a stored endpoint table. Each orientation has 4,656 demands. + +The inherited source-support invariant says that a helper's X coefficient +row is supported on labels in its current binary frame. A cheap lifetime +therefore carries at most one designated X source before its direct +line-to-hyperplane transport. After entering a dimension-eight hyperplane, +its only larger frame is FULL. It can reach at most one designated target +hyperplane. Record this source/target pair when both exist. Let E be the set +of distinct such pairs of all cheap lifetimes. Then `|E| <= 232`. + +The same E bounds both endpoint systems. A residual arrival that uses a +cheap entrance must use its recorded source and target. A residual departure +that first leaves its source on a cheap lifetime reaches that lifetime's +hyperplane, and cannot subsequently reach a different target hyperplane +without descending. Mixing at a target hyperplane can move broad information +through a cheap helper, but that information is still accounted for at its +broad entrance. Expanding the chronological linear dependency graph handles +relays and cancellation without creating another cheap flag. + +At an endpoint let d be its residual demand, b the maximum intersection with +a proper subspace, and u the number of broad contacts. The cheap flags must +cover at least `max(0,d-b*u)` distinct residual demands. The source-side +statement uses the annihilator of the first broad departure. A nested +lifetime has at most one designated source line and one designated target +hyperplane, so the broad counts sum to at most 191 in each orientation. + +All endpoints have `b < d <= 2b`. Truncate u at two and, if needed, add +fictitious broad contacts until the sum is 191. This only weakens the +requirements. There are then exactly 17 missing contacts relative to two +per endpoint. This padding is separate in the two orientations and grants +more freedom than a joint physical program. + +Choose subsets `E_A, E_D` of E containing exactly the required number of +arrival and departure flags at each endpoint. Their intersection lies in the +mutual residual graph, whose edges satisfy both `s in N_t` and `t in F_s`. +If the total required subset sizes are `L_A,L_D` and their overlap is at most U, + +```text +|E| >= |E_A union E_D| >= L_A + L_D - U. +``` + +This is the new joint condition. Independent endpoint budgets do not impose it. + +## Small integer certificate + +Classify positive-deficiency endpoints, those with u less than two, as follows. +Each orientation has 12 available P endpoints, 8 Q endpoints and 84 R endpoints. + +```text +P: (d,b) = (36,24), first missing-contact price 12 +Q: (d,b) = (45,30), first missing-contact price 15 +R: d-b >= 16 +Every second missing contact costs at least another 24. +``` + +The reconstructed mutual graph has 4,368 edges. Its only facts needed below are: + +- Between the two P classes, every vertex has degree at most four. +- A Q vertex has at most six neighbors in the opposite P class. +- There are no Q-to-Q edges. + +Let p,q,r count selected endpoints in those classes, and z count selected +endpoints with u zero. Then `p+q+r+z=17`, and + +```text +L >= ell(p,q,r,z) = 12p + 15q + 16r + 24z. +``` + +A solution with at most 232 cheap flags needs `ell <= 232` in each orientation. +Enumerate `0<=z<=8`, `0<=p<=12`, `0<=q<=8`, set `r=17-z-p-q`, and retain +`0<=r<=84`, `z<=p+q+r`, `ell<=232`. Exactly 34 relaxed states survive. +The relaxation permits unrealizable placements of the second deficiency, +which favors the proposed program. + +For source state `(p,q,r,z)` and target state `(a,b,c,w)`, write +`k=p+q+r`, `h=a+b+c`. Allow every possible edge touching R. The mutual-edge +upper bound is + +```text +U = k*c + h*r - r*c + 4*min(p,a) + 6*(q+b). +``` + +All 1,156 state pairs satisfy `ell_source + ell_target - U >= 235`. +The minimum occurs at `(p,q,r,z)=(10,0,7,0)` on both sides, with lower costs +232 each and overlap allowance 229. Consequently `|E| >= 235 > 232`, a +contradiction. [RESULT.json](RESULT.json) retains every state and the full +geometric census. + +**The 235 is conditional on the assumed 232 budget.** It is a contradiction +certificate, not the optimum cheap count when a larger budget is allowed. +The independently implemented six-type check retains the exact endpoint +prices and block degree maxima. Its 337 squared state pairs give the stronger +conditional bound 300 under the same budget. The smaller proof above suffices. +Neither computation optimizes actual correction circuits. + +## Reproduce and evidence + +Python 3.12 or later, standard library only, from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/p104-joint-endpoint-obstruction +``` + +Direct read-only checks also work in a Git-free source export: + +```sh +python3.12 -I -O -Werror -B research/p104-joint-endpoint-obstruction/verify.py +python3.12 -I -O -Werror -B research/p104-joint-endpoint-obstruction/independent.py +python3.12 -I -O -Werror -B research/p104-joint-endpoint-obstruction/test_verify.py +``` + +The primary marker is +`PASS_P104_JOINT_ENDPOINT cheap=232 broad=191 bound=235 states=34 pairs=1156`. +`verify.py --emit` recomputes the complete receipt without writing files. +The primary checker reuses the authenticated PR2909 geometry module. Its +loader compiles those authenticated bytes directly, so a preexisting bytecode +cache cannot replace that module. The independent checker imports no +predecessor implementation and computes capacities using integer character +transforms instead of direct functional intersections. + +The tests exercise the actual CLI, Git-free read-only replay, false P-P and +Q-Q graph premises, a weakened degree bound that no longer excludes the +profile, a false class gap, input corruption before code execution, poisoned +bytecode, duplicate keys and typed receipt corruption. An exploratory CP-SAT +run returned UNKNOWN after 45 seconds; no solver status or solver dependency +is used as evidence. The two finite implementations and a separate internal +mathematical review support the result. The program-to-edge implication is a +written proof, not a formal-kernel theorem or independent human review. + +Native identities, precision, full-word execution, physical routing/hosting, +complete consumer costs, all-size lifting and the selected cold replay are +unrun. They are unnecessary for this exclusion within the stated model, and +remain obligations for a changed candidate. Local commands and environments +are recorded in [TASK.json](TASK.json). Hosted CI is separate. + +## Open next questions + +A changed candidate must pass a **joint** endpoint flag test before further +scalar or native implementation. One feasible next test is to name a different +cheap/broad histogram and check actual residual-edge subsets in both +orientations, retaining the same flags, or to change a stated source/consumer +contract. This result does not supply a new optimum or authorize treating +unknown acquisition, coefficient, restoration and physical costs as zero. + +Family decision: finish this named-profile obstruction and stop. No additional +threshold search or construction expansion is included. The structured next +question in TASK.json preserves that boundary. + +## Credit and engineering notes + +Nick Petalas. Apache-2.0. Substantial automated assistance was used in the +mathematics, code, independent implementation, review and writing. No independent +human review is claimed. + +Credit Nick Petalas/PR2941 for the named three-history profile and handoff, +Sudarsh Chaturvedi/PR2924 for the two-history floor screen, Nick Petalas/PR2920, +PR2909 and PR2896 for separate covers, endpoint prices and residual capacities, +Hiroki Kumazaki/PR2889 and PR2353 for endpoint spans and the monotone model, +Arham Tahir/PR2675 and PR2682 for the coupled price model, ywz65/PR2614 for +later-read-aware departures, Sagar Thakrar's mixer handoff and Philippe Van +Velzen's relay work. Retain Rohan Arun/PR1972, Chafik Boukhalfa/PR1991, +Adam Gall/PR1940, Josie Elliston/PR1071, Ali Romman/PR1125 and their retained +geometry/native/compiler lineage. No predecessor construction or earlier +one-sided bound is claimed as new. + +Build the Lever led to the replayable integer certificate. Prove It Works +required original-input reconstruction and a separate implementation. Test +Behavior, Not Implementation led to CLI and semantic fault tests. Unslop guided +the prose. The finite domains are 104 endpoints per orientation, 512 labels, +4,058 source events, 34 squared primary pairs and 337 squared independent pairs. +All changed functions are below 60 lines. Explicit checks remain enabled under +optimized Python. + +Power of Ten rule 3 deviation: these bounded Python computations allocate +managed objects. Source files are capped at 2 MB, spans at 512 members, and +the independent staged state list at one million entries. A resident or +untrusted general-purpose checker would need a fixed-capacity implementation. +Rule 8/9 deviation: the primary loader uses Python module dispatch for one +SHA256-authenticated geometry source. Its code path bypasses bytecode-cache +reads, with a valid poisoned-cache control. The test runner has one explicit +module import and bounded subprocesses with 30-second timeouts and scoped +temporary cleanup. A standalone static geometry API with source binding could +remove that loader in a separate change. Registered warnings-as-errors, lint +and source compilation cover the changed code. Shared repository configuration +and frozen sources are unchanged. + +[2941]: https://github.com/CrocSwap/integer-mult-bounds/blob/df29f70185979e32c73efc5f6e2903652d744ae7/research/p104-three-history-threshold/README.md +[claim]: https://github.com/CrocSwap/integer-mult-bounds/discussions/2245#discussioncomment-18975014 diff --git a/research/p104-joint-endpoint-obstruction/RESULT.json b/research/p104-joint-endpoint-obstruction/RESULT.json new file mode 100644 index 0000000000..f9dfbc25fd --- /dev/null +++ b/research/p104-joint-endpoint-obstruction/RESULT.json @@ -0,0 +1,1340 @@ +{ + "certificate": { + "attaining_relaxed_pair": { + "arrival": [ + 10, + 0, + 7, + 0, + 232 + ], + "departure": [ + 10, + 0, + 7, + 0, + 232 + ], + "overlap_cap": 229 + }, + "cheap_budget": 232, + "contradiction": 3, + "minimum_conditional_union_bound": 235, + "pairs_checked": 1156, + "states": [ + [ + 8, + 8, + 1, + 0, + 232 + ], + [ + 9, + 4, + 4, + 0, + 232 + ], + [ + 9, + 5, + 3, + 0, + 231 + ], + [ + 9, + 6, + 2, + 0, + 230 + ], + [ + 9, + 7, + 1, + 0, + 229 + ], + [ + 9, + 8, + 0, + 0, + 228 + ], + [ + 10, + 0, + 7, + 0, + 232 + ], + [ + 10, + 1, + 6, + 0, + 231 + ], + [ + 10, + 2, + 5, + 0, + 230 + ], + [ + 10, + 3, + 4, + 0, + 229 + ], + [ + 10, + 4, + 3, + 0, + 228 + ], + [ + 10, + 5, + 2, + 0, + 227 + ], + [ + 10, + 6, + 1, + 0, + 226 + ], + [ + 10, + 7, + 0, + 0, + 225 + ], + [ + 11, + 0, + 6, + 0, + 228 + ], + [ + 11, + 1, + 5, + 0, + 227 + ], + [ + 11, + 2, + 4, + 0, + 226 + ], + [ + 11, + 3, + 3, + 0, + 225 + ], + [ + 11, + 4, + 2, + 0, + 224 + ], + [ + 11, + 5, + 1, + 0, + 223 + ], + [ + 11, + 6, + 0, + 0, + 222 + ], + [ + 12, + 0, + 5, + 0, + 224 + ], + [ + 12, + 1, + 4, + 0, + 223 + ], + [ + 12, + 2, + 3, + 0, + 222 + ], + [ + 12, + 3, + 2, + 0, + 221 + ], + [ + 12, + 4, + 1, + 0, + 220 + ], + [ + 12, + 5, + 0, + 0, + 219 + ], + [ + 11, + 4, + 1, + 1, + 232 + ], + [ + 11, + 5, + 0, + 1, + 231 + ], + [ + 12, + 0, + 4, + 1, + 232 + ], + [ + 12, + 1, + 3, + 1, + 231 + ], + [ + 12, + 2, + 2, + 1, + 230 + ], + [ + 12, + 3, + 1, + 1, + 229 + ], + [ + 12, + 4, + 0, + 1, + 228 + ] + ] + }, + "geometry": { + "arrival_classes": [ + [ + 26, + 27, + 31, + 33, + 55, + 62, + 66, + 67, + 90, + 93, + 97, + 103 + ], + [ + 0, + 21, + 22, + 38, + 47, + 75, + 88, + 99 + ], + [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 23, + 24, + 25, + 28, + 29, + 30, + 32, + 34, + 35, + 36, + 37, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 56, + 57, + 58, + 59, + 60, + 61, + 63, + 64, + 65, + 68, + 69, + 70, + 71, + 72, + 73, + 74, + 76, + 77, + 78, + 79, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 89, + 91, + 92, + 94, + 95, + 96, + 98, + 100, + 101, + 102 + ] + ], + "arrival_endpoints": [ + [ + 45, + 30 + ], + [ + 48, + 30 + ], + [ + 47, + 30 + ], + [ + 48, + 30 + ], + [ + 47, + 30 + ], + [ + 47, + 30 + ], + [ + 48, + 30 + ], + [ + 48, + 30 + ], + [ + 47, + 30 + ], + [ + 46, + 29 + ], + [ + 46, + 29 + ], + [ + 47, + 30 + ], + [ + 48, + 30 + ], + [ + 47, + 30 + ], + [ + 48, + 30 + ], + [ + 47, + 30 + ], + [ + 46, + 29 + ], + [ + 44, + 28 + ], + [ + 44, + 28 + ], + [ + 46, + 29 + ], + [ + 47, + 30 + ], + [ + 45, + 30 + ], + [ + 45, + 30 + ], + [ + 47, + 30 + ], + [ + 46, + 29 + ], + [ + 44, + 28 + ], + [ + 36, + 24 + ], + [ + 36, + 24 + ], + [ + 44, + 28 + ], + [ + 46, + 29 + ], + [ + 44, + 28 + ], + [ + 36, + 24 + ], + [ + 44, + 28 + ], + [ + 36, + 24 + ], + [ + 44, + 28 + ], + [ + 46, + 29 + ], + [ + 46, + 29 + ], + [ + 47, + 30 + ], + [ + 45, + 30 + ], + [ + 44, + 28 + ], + [ + 47, + 30 + ], + [ + 48, + 30 + ], + [ + 47, + 30 + ], + [ + 46, + 29 + ], + [ + 46, + 29 + ], + [ + 47, + 30 + ], + [ + 48, + 30 + ], + [ + 45, + 30 + ], + [ + 47, + 30 + ], + [ + 46, + 29 + ], + [ + 44, + 28 + ], + [ + 44, + 28 + ], + [ + 46, + 29 + ], + [ + 47, + 30 + ], + [ + 48, + 30 + ], + [ + 36, + 24 + ], + [ + 44, + 28 + ], + [ + 46, + 29 + ], + [ + 47, + 30 + ], + [ + 44, + 28 + ], + [ + 46, + 29 + ], + [ + 44, + 28 + ], + [ + 36, + 24 + ], + [ + 44, + 28 + ], + [ + 46, + 29 + ], + [ + 44, + 28 + ], + [ + 36, + 24 + ], + [ + 36, + 24 + ], + [ + 44, + 28 + ], + [ + 46, + 29 + ], + [ + 47, + 30 + ], + [ + 44, + 28 + ], + [ + 46, + 29 + ], + [ + 47, + 30 + ], + [ + 48, + 30 + ], + [ + 45, + 30 + ], + [ + 47, + 30 + ], + [ + 46, + 29 + ], + [ + 44, + 28 + ], + [ + 46, + 29 + ], + [ + 47, + 30 + ], + [ + 48, + 30 + ], + [ + 47, + 30 + ], + [ + 48, + 30 + ], + [ + 47, + 30 + ], + [ + 46, + 29 + ], + [ + 46, + 29 + ], + [ + 47, + 30 + ], + [ + 45, + 30 + ], + [ + 44, + 28 + ], + [ + 36, + 24 + ], + [ + 44, + 28 + ], + [ + 46, + 29 + ], + [ + 36, + 24 + ], + [ + 44, + 28 + ], + [ + 46, + 29 + ], + [ + 44, + 28 + ], + [ + 36, + 24 + ], + [ + 44, + 28 + ], + [ + 45, + 30 + ], + [ + 47, + 30 + ], + [ + 46, + 29 + ], + [ + 44, + 28 + ], + [ + 36, + 24 + ] + ], + "departure_classes": [ + [ + 1, + 3, + 6, + 7, + 12, + 14, + 41, + 46, + 54, + 74, + 81, + 83 + ], + [ + 0, + 21, + 22, + 38, + 47, + 75, + 88, + 99 + ], + [ + 2, + 4, + 5, + 8, + 9, + 10, + 11, + 13, + 15, + 16, + 17, + 18, + 19, + 20, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 39, + 40, + 42, + 43, + 44, + 45, + 48, + 49, + 50, + 51, + 52, + 53, + 55, + 56, + 57, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 72, + 73, + 76, + 77, + 78, + 79, + 80, + 82, + 84, + 85, + 86, + 87, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 100, + 101, + 102, + 103 + ] + ], + "departure_endpoints": [ + [ + 45, + 30 + ], + [ + 36, + 24 + ], + [ + 44, + 28 + ], + [ + 36, + 24 + ], + [ + 44, + 28 + ], + [ + 44, + 28 + ], + [ + 36, + 24 + ], + [ + 36, + 24 + ], + [ + 44, + 28 + ], + [ + 46, + 29 + ], + [ + 46, + 29 + ], + [ + 44, + 28 + ], + [ + 36, + 24 + ], + [ + 44, + 28 + ], + [ + 36, + 24 + ], + [ + 44, + 28 + ], + [ + 46, + 29 + ], + [ + 47, + 30 + ], + [ + 47, + 30 + ], + [ + 46, + 29 + ], + [ + 44, + 28 + ], + [ + 45, + 30 + ], + [ + 45, + 30 + ], + [ + 44, + 28 + ], + [ + 46, + 29 + ], + [ + 47, + 30 + ], + [ + 48, + 30 + ], + [ + 48, + 30 + ], + [ + 47, + 30 + ], + [ + 46, + 29 + ], + [ + 47, + 30 + ], + [ + 48, + 30 + ], + [ + 47, + 30 + ], + [ + 48, + 30 + ], + [ + 47, + 30 + ], + [ + 46, + 29 + ], + [ + 46, + 29 + ], + [ + 44, + 28 + ], + [ + 45, + 30 + ], + [ + 47, + 30 + ], + [ + 44, + 28 + ], + [ + 36, + 24 + ], + [ + 44, + 28 + ], + [ + 46, + 29 + ], + [ + 46, + 29 + ], + [ + 44, + 28 + ], + [ + 36, + 24 + ], + [ + 45, + 30 + ], + [ + 44, + 28 + ], + [ + 46, + 29 + ], + [ + 47, + 30 + ], + [ + 47, + 30 + ], + [ + 46, + 29 + ], + [ + 44, + 28 + ], + [ + 36, + 24 + ], + [ + 48, + 30 + ], + [ + 47, + 30 + ], + [ + 46, + 29 + ], + [ + 44, + 28 + ], + [ + 47, + 30 + ], + [ + 46, + 29 + ], + [ + 47, + 30 + ], + [ + 48, + 30 + ], + [ + 47, + 30 + ], + [ + 46, + 29 + ], + [ + 47, + 30 + ], + [ + 48, + 30 + ], + [ + 48, + 30 + ], + [ + 47, + 30 + ], + [ + 46, + 29 + ], + [ + 44, + 28 + ], + [ + 47, + 30 + ], + [ + 46, + 29 + ], + [ + 44, + 28 + ], + [ + 36, + 24 + ], + [ + 45, + 30 + ], + [ + 44, + 28 + ], + [ + 46, + 29 + ], + [ + 47, + 30 + ], + [ + 46, + 29 + ], + [ + 44, + 28 + ], + [ + 36, + 24 + ], + [ + 44, + 28 + ], + [ + 36, + 24 + ], + [ + 44, + 28 + ], + [ + 46, + 29 + ], + [ + 46, + 29 + ], + [ + 44, + 28 + ], + [ + 45, + 30 + ], + [ + 47, + 30 + ], + [ + 48, + 30 + ], + [ + 47, + 30 + ], + [ + 46, + 29 + ], + [ + 48, + 30 + ], + [ + 47, + 30 + ], + [ + 46, + 29 + ], + [ + 47, + 30 + ], + [ + 48, + 30 + ], + [ + 47, + 30 + ], + [ + 45, + 30 + ], + [ + 44, + 28 + ], + [ + 46, + 29 + ], + [ + 47, + 30 + ], + [ + 48, + 30 + ] + ], + "incidence_sha256": "1988c7e51c86577647febce961ac43d3500e533c388b63b22f25faeade222bd4", + "mutual_edges": 4368, + "pp_column_max": 4, + "pp_row_max": 4, + "pq_column_max": 6, + "qp_row_max": 6, + "qq_edges": 0 + }, + "profile": { + "cheap": 232, + "skip_dimension_three": 11, + "unit": 180 + }, + "scope": "Reject named profile in frozen X-only monotone model; no supplier or kappa" +} diff --git a/research/p104-joint-endpoint-obstruction/SOURCES.json b/research/p104-joint-endpoint-obstruction/SOURCES.json new file mode 100644 index 0000000000..5b358d843f --- /dev/null +++ b/research/p104-joint-endpoint-obstruction/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "05eee6613f843dd754528c9b2da8049757382ef6", + "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-endpoint-saturation/geometry.py", + "usage": "input", + "git_blob": "a08360057fede369e748c57b1db55db0c7f23129", + "sha256": "c901d2e72194529e15e24c20629a3ffedbc792f397151e67ea8d1a51cfefd9fb" + }, + { + "path": "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "usage": "input", + "git_blob": "86beaf424e9f0f800ae3a62797d94ec9386b7706", + "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e" + }, + { + "path": "research/p104-native-channel/inputs/P104-FIXTURE.json", + "usage": "input", + "git_blob": "2e16f99b295bb386fd13bd8fbd57b42ef54143a9", + "sha256": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4" + } + ] +} diff --git a/research/p104-joint-endpoint-obstruction/TASK.json b/research/p104-joint-endpoint-obstruction/TASK.json new file mode 100644 index 0000000000..4e52485cc4 --- /dev/null +++ b/research/p104-joint-endpoint-obstruction/TASK.json @@ -0,0 +1,173 @@ +{ + "schema_version": 1, + "task_id": "p104-side-correction", + "priority_revision": 5, + "base_commit": "05eee6613f843dd754528c9b2da8049757382ef6", + "original_card": { + "id": "p104-side-correction", + "question": "Which unresolved physical correction, endpoint transport or hosting obligation in a pinned P104 follow-up can be closed or decisively rejected?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/p104-native-channel/README.md", + "research/p104-native-channel/PROOF.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct one side-correction word at an explicit chronological cut with the needed frames still available.", + "Derive a lower bound on the side correction and hosting costs that decides whether this channel can beat the selected budget." + ], + "acceptance_gate": "An exact arbitrary-input identity, source/target frame availability and restoration at the chosen cut, plus the complete channel+correction+idle/hosting bill or an explicit favorable bound. The native channel alone is not a supplier. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the P104 row in research-family-status.md and its exact pending source heads before choosing a task. #1991 is the reviewed channel; #2586 is a pending physical dual with explicit added transport costs, not an admitted supplier.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Check live claims, pin the chosen follow-up and reproduce only the evidence needed for one unresolved obligation. Compare its complete correction/transport/hosting invoice with the target budget; test legal chronological access. Do not rebuild #1991 or assume #2586 has solved global admission.", + "bottleneck_link": "Completing an already realized changed channel tests a concrete construction opportunity, instead of refining the incumbent packing. A positive local result still needs global and all-size admission.", + "allowed_variations": [ + "One correction factorization, one chronological cut, or one explicit hosting obstruction.", + "A changed correction schedule with an updated full bill and native frame contract." + ], + "scope_change_triggers": [ + "Recompiling the already certified low-rank channel without closing a new obligation.", + "Treating a pending ancestor, local histogram or unpriced side correction as an admitted global supplier.", + "Repeating a correction or physical conversion already supplied by a pending follow-up without adding independent coverage or a different unresolved obligation." + ], + "overlap_terms": [ + "P104", + "I-G/2", + "side correction", + "native channel", + "1972", + "1991", + "2586", + "endpoint transport", + "physical dual", + "relay composition" + ] + }, + "scope_status": "refined", + "actual_scope": "Reject PR2941's named 232-cheap/191-broad correction profile through a shared residual-edge budget at both endpoint orientations.", + "scope_change_reason": "The live PR2920/2941 handoff leaves joint endpoint/dependency realization open after separate endpoint and price screens passed. This audit closes one necessary joint compatibility condition without extending construction.", + "bottleneck_link": "A passing optimistic moment is useful only if a complete source/target correction can realize its helper profile. Binding cheap lifetimes to one shared edge set rejects a currently affordable candidate before native or hosting work.", + "budget_minutes": 60, + "stop_rule": "Stop after checking the named profile and independently reviewing its shared-edge obstruction. No threshold sweep, new circuit campaign or frontier update.", + "outcome": "negative-result", + "evidence": "RESULT.json reconstructs all 208 endpoint records, 4,368 mutual residual edges, 34 states and 1,156 pairs with a conditional 235 > 232 contradiction. independent.py reconstructs original inputs separately and checks 337 squared six-type pairs with conditional bound 300 > 232.", + "author": "Nick Petalas", + "ai_assistance": "Substantial automated assistance was used in mathematics, code, separate implementation, internal review and writing. No independent human or formal-kernel review is claimed.", + "open_questions": [ + { + "question": "Can one named changed histogram or contract satisfy a shared endpoint flag assignment before scalar synthesis?", + "why_it_matters": "Separate source/target allocations can double-count the same cheap lifetimes and admit incompatible profiles.", + "first_step": "Pin one changed candidate and require the same cheap flags to cover both actual residual incidence matrices. Preserve the source/consumer boundary and state every unpriced obligation.", + "blocked_by": "No changed candidate is constructed here. Passing necessary flags would still leave coefficients, relays, chronology, restoration, precision, physical hosting and the complete consumer bill." + } + ], + "chooser_nonce": "237b7b36d5393aad3e49b3dcc8bbea8d", + "scope_key": "c5367b1a1b7bed20db53", + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2245#discussioncomment-18975014", + "predecessors": [ + { + "pr": 2941, + "head": "df29f70185979e32c73efc5f6e2903652d744ae7", + "author": "Nick Petalas", + "scope": "Named profile and passing separate endpoint/optimistic price screen; no joint realization claimed." + }, + { + "pr": 2920, + "head": "b9ea9def949f9d71d59e21294d0e6cfbe0692a73", + "author": "Nick Petalas", + "scope": "Separate endpoint geometric covers and prices." + }, + { + "pr": 2924, + "head": "d1660ed0a17b66ad0c86cd4aaea724926134e362", + "author": "Sudarsh Chaturvedi", + "scope": "Explicitly two-history lifetime-floor price screen." + } + ], + "family_decision": "Stop after named-profile obstruction. A changed candidate must pass joint endpoint flags and still provide chronology, coefficients, dirty restoration and a complete consumer/physical cost ledger.", + "entry_freshness": { + "upstream_commit": "05eee6613f843dd754528c9b2da8049757382ef6", + "priority_revision": 5, + "open_prs": 368, + "open_prs_checked_utc": "2026-10-16T13:53:18Z", + "closed_prs": 2271, + "closed_prs_checked_utc": "2026-10-16T13:54:09Z", + "discussion_records": 1642, + "discussions_checked_utc": "2026-10-16T13:53:46Z", + "complete_pagination": true, + "limits": "Cached body/comment/local-note search excludes arbitrary diffs and unpublished work." + }, + "verification": { + "environment": "macOS arm64, CPython3.12.15 and3.14.8, standard library", + "commands": [ + { + "command": "python3.12 -B scripts/research_package.py --package research/p104-joint-endpoint-obstruction", + "result": "PASS_REGISTERED_RESEARCH_PACKAGE outcome=negative-result, including seven behavioral test groups." + }, + { + "command": "python3.14 -I -O -Werror -B research/p104-joint-endpoint-obstruction/{verify,independent,test_verify}.py, each separately", + "result": "Both checkers and all seven behavioral test groups pass." + }, + { + "command": "uv run --python 3.12 --with ruff ruff check research/p104-joint-endpoint-obstruction", + "result": "All checks passed." + }, + { + "command": "python3.12 -Werror source compilation and AST function-length census", + "result": "All three sources compile. Maximum function lengths are 19, 21 and 22 lines for primary, independent and test code." + } + ], + "unrun": [ + "native reconstruction", + "physical corrected-word execution", + "precision/tape", + "global hosting and complete consumer invoice", + "all-size lifting", + "selected cold replay" + ], + "exploratory_solver": "OR-Tools 9.15.6755 CP-SAT returned UNKNOWN after 45 seconds. Not a proof dependency; no solver status supports the result.", + "internal_reviews": [ + { + "task": "joint_endpoint_review", + "scope": "Separately derived shared-edge implication and three-class235 certificate; implemented independent original-input six-class300 checker; no correctness flags." + }, + { + "task": "final_proof_audit", + "scope": "Fresh read-only proof/implementation and local decision-log audit, reran both checkers and seven tests; no correctness flags. Metadata finalization was outside that audit." + } + ], + "ruff_version": "0.17.1" + }, + "pre_submission_freshness": { + "checked_utc": "2026-10-16T14:05:03.204447+00:00", + "upstream_commit": "389fa10d714f5b40afe624908e487eb5e424498d", + "scientific_base": "05eee6613f843dd754528c9b2da8049757382ef6", + "changed_guidance_or_inputs": [], + "overlap": { + "open_prs": { + "fetched_at": "2026-10-16T14:04:58.811091+00:00", + "complete_pagination": true, + "records": 306 + }, + "discussions": { + "fetched_at": "2026-10-16T14:05:27.481112+00:00", + "complete_pagination": true, + "records": 1644 + }, + "closed_prs": { + "fetched_at": "2026-10-16T14:05:51.028495+00:00", + "complete_pagination": true, + "records": 2334 + } + }, + "interpretation": "Relevant guidance and all three live inputs are byte-identical to the scientific base. Fresh overlap finds the credited handoffs and this own claim; no completed shared cheap-edge result appears in the searched bodies/comments/local notes. Arbitrary diffs and unpublished work remain outside coverage." + } +} diff --git a/research/p104-joint-endpoint-obstruction/VERIFY.json b/research/p104-joint-endpoint-obstruction/VERIFY.json new file mode 100644 index 0000000000..dfe220fdd4 --- /dev/null +++ b/research/p104-joint-endpoint-obstruction/VERIFY.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-endpoint-saturation/geometry.py", + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "research/p104-native-channel/inputs/P104-FIXTURE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Authenticated original-input reconstruction, 34 squared integer certificate and complete typed receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Separate bitset/character-transform reconstruction, 337 squared six-type bound and independent 34 squared coarse check." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Seven actual CLI/semantic groups, graph/class faults, weakened proof control, Git-free read-only replay, source-before-execution, poisoned cache, duplicate keys and typed receipt faults." + } + ] +} diff --git a/research/p104-joint-endpoint-obstruction/independent.py b/research/p104-joint-endpoint-obstruction/independent.py new file mode 100644 index 0000000000..d6c61f4a2b --- /dev/null +++ b/research/p104-joint-endpoint-obstruction/independent.py @@ -0,0 +1,257 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Independent finite joint-endpoint audit, using only authenticated JSON.""" + +import argparse +import hashlib +import json +from itertools import combinations, product +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PINS = { + 'LOWRANK-WITNESS.json': + '0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e', + 'P104-FIXTURE.json': + '516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4', +} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def load_input(name): + path = ROOT / 'research/p104-native-channel/inputs' / name + require(path.stat().st_size <= 2_000_000, 'oversized original JSON') + raw = path.read_bytes() + require(len(raw) <= 2_000_000, 'oversized original JSON read') + require(hashlib.sha256(raw).hexdigest() == PINS[name], 'original input hash') + return json.loads(raw) + + +def frame(basis): + """Encode a binary span as an integer with 512 membership bits.""" + require(isinstance(basis, list) and len(basis) <= 9, 'binary basis length') + members = [0] + for v in basis: + require(type(v) is int and 0 < v < 512 and v not in members, + 'independent binary basis vector') + members += [old ^ v for old in tuple(members)] + return sum(1 << v for v in members) + + +def ordered_ports(fixture): + roots = set() + for i, j in combinations(range(8), 2): + for sign in (-1, 1): + point = [0] * 8 + point[i], point[j] = 2, sign * 2 + roots.add(tuple(point)) + for tail in product((-1, 1), repeat=7): + if sum(x == -1 for x in tail) % 2 == 0: + roots.add((1, *tail)) + section = fixture['section4_explicit_P104'] + deleted = {tuple(point) for point in section['F0'] + section['C']} + require(len(roots) == 120 and len(deleted) == 16, 'E8 puncture cardinalities') + ports = sorted(roots - deleted) + require(len(ports) == 104, 'P104 port cardinality') + return ports + + +def data_paths(witness): + names = [f'{kind}{i}' for kind in 'XY' for i in range(104)] + paths = {name: [frame(witness['initial_frames'][name])] for name in names} + require(len(witness['program']) == 4058, 'frozen program length') + for event in witness['program']: + if event[0] != 'transport': + continue + _, name, old_basis, new_basis, rank = event + if name not in paths: + continue + old, new = frame(old_basis), frame(new_basis) + require(paths[name][-1] == old and old != new and old & ~new == 0, + 'data transport inclusion and continuity') + require(rank == len(new_basis) - len(old_basis), 'data transport rank') + paths[name].append(new) + for name in names: + require(paths[name][-1] == frame(witness['final_frames'][name]), + 'frozen final data frame') + require(len(paths[name]) <= 10, 'monotone path bound') + return paths + + +def endpoint_data(paths): + sources = [paths[f'X{s}'] for s in range(104)] + targets = [paths[f'Y{t}'] for t in range(104)] + require(all(p[0].bit_count() == 2 and p[-1].bit_count() == 512 + for p in sources), 'source endpoint dimensions') + require(all(p[0] == 1 and p[-1].bit_count() == 256 + for p in targets), 'target endpoint dimensions') + labels = [(p[0] ^ 1).bit_length() - 1 for p in sources] + normals = [] + for path in targets: + final = path[-1] + perpendicular = [n for n in range(1, 512) + if all(not (n & v).bit_count() % 2 + for v in range(512) if final >> v & 1)] + require(len(perpendicular) == 1, 'unique target normal') + normals.append(perpendicular[0]) + require(len(set(labels)) == len(set(normals)) == 104, 'distinct endpoints') + return sources, targets, labels, normals + + +def demand_graph(ports, sources, targets, labels, normals): + arrivals, departures = [0] * 104, [0] * 104 + original_demands = 0 + for s, t in product(range(104), repeat=2): + dot = sum(ports[s][i] * ports[t][i] for i in range(8)) + require(bool(targets[t][-1] >> labels[s] & 1) == (dot % 8 == 4), + 'root incidence agrees with frame incidence') + if dot == 8 * int(s == t): + continue + original_demands += 1 + require(targets[t][-1] not in sources[s] and sources[s][0] not in targets[t], + 'no direct source/target endpoint contact') + if not any(v >> labels[s] & 1 for v in targets[t][:-1]): + arrivals[t] |= 1 << s + if not any(v.bit_count() > 2 and v & ~targets[t][-1] == 0 + for v in sources[s]): + departures[s] |= 1 << t + require(original_demands == 4992, 'frozen correction support size') + require(sum(v.bit_count() for v in arrivals) == 4656, 'arrival residual count') + require(sum(v.bit_count() for v in departures) == 4656, 'departure residual count') + return arrivals, departures + + +def capacity(indices, vectors, normal): + """Count every proper section using an integer character transform.""" + points = [vectors[i] for i in range(104) if indices >> i & 1] + require(0 < len(points) <= 48, 'residual endpoint bound') + require(all(not (v & normal).bit_count() % 2 for v in points), + 'residual endpoint containment') + chars = [0] * 512 + for v in points: + chars[v] += 1 + for stage in range(9): + width = 1 << stage + for start in range(0, 512, 2 * width): + for offset in range(width): + i, j = start + offset, start + offset + width + chars[i], chars[j] = chars[i] + chars[j], chars[i] - chars[j] + best = max((len(points) + chars[n]) // 2 + for n in range(1, 512) if n != normal) + require(best < len(points) <= 2 * best, 'proper capacity and two-carrier bound') + return best + + +def type_groups(residual, capacities, types): + groups = [[i for i in range(104) if (residual[i].bit_count(), capacities[i]) == t] + for t in types] + require([len(group) for group in groups] == [12, 8, 24, 24, 24, 12], + 'six endpoint type populations') + return groups + + +def mutual_blocks(arrivals, departures, source_groups, target_groups): + rows = [sum(1 << t for t in range(104) + if departures[s] >> t & 1 and arrivals[t] >> s & 1) + for s in range(104)] + require(sum(row.bit_count() for row in rows) == 4368, 'mutual residual count') + columns = [sum(1 << s for s in range(104) if rows[s] >> t & 1) + for t in range(104)] + source_masks = [sum(1 << s for s in group) for group in source_groups] + target_masks = [sum(1 << t for t in group) for group in target_groups] + row_max = [[max((rows[s] & mask).bit_count() for s in group) + for mask in target_masks] for group in source_groups] + column_max = [[max((columns[t] & mask).bit_count() for t in group) + for group in target_groups] for mask in source_masks] + return row_max, column_max + + +def deficiency_patterns(types, populations): + """Assign 17 missing broad contacts relative to two at every endpoint.""" + partial = [((), 0, 0)] + for (demand, cap), population in zip(types, populations, strict=True): + next_partial = [] + for counts, missing, price in partial: + for zero in range(min(population, (17 - missing) // 2) + 1): + for one in range(min(population - zero, 17 - missing - 2 * zero) + 1): + new_missing = missing + 2 * zero + one + new_price = price + demand * zero + (demand - cap) * one + if new_price <= 232: + next_partial.append((counts + (zero + one,), + new_missing, new_price)) + require(len(next_partial) <= 1_000_000, + 'bounded deficiency state count') + partial = next_partial + patterns = [(counts, price) for counts, missing, price in partial if missing == 17] + require(len(patterns) == 337, 'feasible six-type deficiency pattern count') + return patterns + + +def overlap_audit(patterns, row_max, column_max): + best, witness = None, None + for (source, source_cost), (target, target_cost) in product(patterns, repeat=2): + overlap = sum(min(source[i] * target[j], source[i] * row_max[i][j], + target[j] * column_max[i][j]) + for i, j in product(range(6), repeat=2)) + required = source_cost + target_cost - overlap + if best is None or required < best: + best = required + witness = [list(source), list(target), source_cost, target_cost, overlap] + require(best == 300, 'conditional joint cheap union lower bound') + return best, witness + + +def three_class_audit(): + states = [] + for p, q, z in product(range(13), range(9), range(9)): + r = 17 - z - p - q + price = 12 * p + 15 * q + 16 * r + 24 * z + if r >= 0 and price <= 232: + states.append((p, q, r, price)) + require(len(states) == 34, 'three-class deficiency count') + lower = 1000 + for (p, q, r, price), (pp, qq, rr, other_price) in product(states, repeat=2): + overlap = ((p + q + r) * rr + (pp + qq + rr) * r - r * rr + + 4 * min(p, pp) + 6 * (q + qq)) + lower = min(lower, price + other_price - overlap) + require(lower == 235, 'three-class conditional union lower bound') + return lower + + +def audit(): + witness, fixture = load_input('LOWRANK-WITNESS.json'), load_input('P104-FIXTURE.json') + paths = data_paths(witness) + sources, targets, labels, normals = endpoint_data(paths) + arrivals, departures = demand_graph(ordered_ports(fixture), sources, targets, + labels, normals) + ac = [capacity(arrivals[t], labels, normals[t]) for t in range(104)] + dc = [capacity(departures[s], normals, labels[s]) for s in range(104)] + types = [(36, 24), (45, 30), (44, 28), (46, 29), (47, 30), (48, 30)] + ag, dg = type_groups(arrivals, ac, types), type_groups(departures, dc, types) + row_max, column_max = mutual_blocks(arrivals, departures, dg, ag) + require(row_max[0][0] == column_max[0][0] == 4 + and row_max[1][1] == 0 and row_max[1][0] == column_max[0][1] == 6, + 'three-class graph premises') + patterns = deficiency_patterns(types, [len(group) for group in ag]) + lower, attaining = overlap_audit(patterns, row_max, column_max) + return {'patterns': len(patterns), 'lower': lower, 'attaining': attaining, + 'row_max': row_max, 'column_max': column_max, + 'three_class_patterns': 34, 'three_class_lower': three_class_audit()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--emit', action='store_true', help='print a recomputed JSON receipt') + args = parser.parse_args() + result = audit() + if args.emit: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + print('PASS_P104_JOINT_ENDPOINT_INDEPENDENT patterns=337 lower=300') + + +if __name__ == '__main__': + main() diff --git a/research/p104-joint-endpoint-obstruction/test_verify.py b/research/p104-joint-endpoint-obstruction/test_verify.py new file mode 100644 index 0000000000..79f5d48425 --- /dev/null +++ b/research/p104-joint-endpoint-obstruction/test_verify.py @@ -0,0 +1,153 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Exercise the actual checker, its geometric hypotheses and failure paths.""" + +import importlib.util +import json +import marshal +import shutil +import struct +import subprocess +import sys +import tempfile +import unittest +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +SPEC = importlib.util.spec_from_file_location('joint_endpoint_under_test', PACKAGE / 'verify.py') +V = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(V) +MARKER = 'PASS_P104_JOINT_ENDPOINT cheap=232 broad=191 bound=235 states=34 pairs=1156' + + +def run(root, *options): + command = [sys.executable, '-I', '-O', '-Werror', '-B', + str(root / 'research/p104-joint-endpoint-obstruction/verify.py'), *options] + return subprocess.run(command, capture_output=True, text=True, timeout=30, check=False) + + +def export(root): + destination = root / 'research/p104-joint-endpoint-obstruction' + destination.mkdir(parents=True) + for name in ('verify.py', 'RESULT.json', 'SOURCES.json'): + shutil.copyfile(PACKAGE / name, destination / name) + for row in json.loads((PACKAGE / 'SOURCES.json').read_text())['files']: + if row['usage'] == 'input': + target = root / row['path'] + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / row['path'], target) + return destination + + +class Behavior(unittest.TestCase): + def test_cli_and_recomputed_receipt(self): + result = run(ROOT) + self.assertEqual((result.returncode, result.stdout.strip()), (0, MARKER)) + emitted = run(ROOT, '--emit') + self.assertEqual(emitted.returncode, 0, emitted.stderr) + data = json.loads(emitted.stdout) + self.assertEqual(data['certificate']['minimum_conditional_union_bound'], 235) + self.assertEqual(data['geometry']['mutual_edges'], 4368) + + def test_degree_hypothesis_is_essential(self): + candidates = V.states() + weaker = min(a[4] + b[4] - V.overlap_cap(a, b, pp=5) + for a in candidates for b in candidates) + self.assertEqual(weaker, 225) + self.assertLessEqual(weaker, 232) + data = V.calculate()['geometry'] + ae = [tuple(row) for row in data['arrival_endpoints']] + ae[V.classes(ae)[2][0]] = (44, 29) + with self.assertRaisesRegex(ValueError, 'R gap'): + V.classes(ae) + + def test_false_mutual_graph_facts_reject(self): + module, word, fixture = V.inputs() + paths = module['paths'](word) + (aa, normals), (dd, labels) = module['endpoint_data'](paths, module['ports'](fixture)) + ag = V.classes(module['census'](aa, normals)) + dg = V.classes(module['census'](dd, labels)) + arrival = [{s for s in range(104) if labels[s] in row} for row in aa] + departure = [{t for t in range(104) if normals[t] in row} for row in dd] + self.assertEqual(V.degree_facts(arrival, departure, ag, dg)['qq_edges'], 0) + s, t = dg[1][0], ag[1][0] + arrival[t].add(s) + departure[s].add(t) + with self.assertRaisesRegex(ValueError, 'Q-Q'): + V.degree_facts(arrival, departure, ag, dg) + arrival[t].remove(s) + departure[s].remove(t) + s = dg[0][0] + t = next(t for t in ag[0] if s not in arrival[t] or t not in departure[s]) + arrival[t].add(s) + departure[s].add(t) + with self.assertRaisesRegex(ValueError, 'P-P'): + V.degree_facts(arrival, departure, ag, dg) + + def test_git_free_export_is_read_only(self): + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + export(root) + before = {p.relative_to(root): p.read_bytes() for p in root.rglob('*') if p.is_file()} + result = run(root) + self.assertEqual((result.returncode, result.stdout.strip()), (0, MARKER)) + after = {p.relative_to(root): p.read_bytes() for p in root.rglob('*') if p.is_file()} + self.assertEqual(after, before) + + def test_source_rejection_precedes_execution(self): + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + export(root) + marker = root / 'executed' + (root / V.GEOMETRY).write_text(f'open({str(marker)!r}, "w").write("bad")\n') + result = run(root) + self.assertNotEqual(result.returncode, 0) + self.assertIn('input SHA256', result.stderr) + self.assertFalse(marker.exists()) + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + export(root) + (root / V.WORD).write_text('{}') + result = run(root) + self.assertNotEqual(result.returncode, 0) + self.assertIn('input SHA256', result.stderr) + + def test_authenticated_source_ignores_a_valid_poisoned_cache(self): + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + export(root) + path = root / V.GEOMETRY + stat = path.stat() + code = compile("raise RuntimeError('poisoned cache executed')", str(path), 'exec') + payload = (importlib.util.MAGIC_NUMBER + struct.pack('= 16 for i in groups[2]), + 'R gap at least sixteen') + return groups + + +def degree_facts(arrival, departure, ag, dg): + require(len(arrival) == len(departure) == 104, 'incidence dimensions') + mutual = {(s, t) for s in range(104) for t in departure[s] if s in arrival[t]} + pp_row = max(sum((s, t) in mutual for t in ag[0]) for s in dg[0]) + pp_column = max(sum((s, t) in mutual for s in dg[0]) for t in ag[0]) + qp_row = max(sum((s, t) in mutual for t in ag[0]) for s in dg[1]) + pq_column = max(sum((s, t) in mutual for s in dg[0]) for t in ag[1]) + qq = sum((s, t) in mutual for s in dg[1] for t in ag[1]) + require(pp_row <= 4 and pp_column <= 4, 'P-P degree at most four') + require(qp_row <= 6 and pq_column <= 6, 'Q-P degree at most six per Q') + require(qq == 0, 'no Q-Q mutual residual edges') + return {'mutual_edges': len(mutual), 'pp_row_max': pp_row, + 'pp_column_max': pp_column, 'qp_row_max': qp_row, + 'pq_column_max': pq_column, 'qq_edges': qq} + + +def reconstruct(): + module, word, fixture = inputs() + paths = module['paths'](word) + ports = module['ports'](fixture) + (arrival, normals), (departure, labels) = module['endpoint_data'](paths, ports) + ae = module['census'](arrival, normals) + de = module['census'](departure, labels) + ag, dg = classes(ae), classes(de) + a = [{s for s in range(104) if labels[s] in row} for row in arrival] + d = [{t for t in range(104) if normals[t] in row} for row in departure] + facts = degree_facts(a, d, ag, dg) + require(facts['mutual_edges'] == 4368, 'literal mutual incidence census') + encoded = json.dumps([list(map(sorted, a)), list(map(sorted, d))], + separators=(',', ':')).encode() + return {'arrival_endpoints': [list(row) for row in ae], + 'departure_endpoints': [list(row) for row in de], + 'arrival_classes': ag, 'departure_classes': dg, + 'incidence_sha256': hashlib.sha256(encoded).hexdigest(), **facts} + + +def states(): + """Overapproximate endpoint counts with seventeen missing broad slots.""" + result = [] + deficit = 2 * 104 - BROAD + require(deficit == 17, 'named broad count') + for z in range(deficit // 2 + 1): + for p in range(13): + for q in range(9): + r = deficit - z - p - q + if not 0 <= r <= 84 or z > p + q + r: + continue + lower = 12 * p + 15 * q + 16 * r + 24 * z + if lower <= BUDGET: + result.append([p, q, r, z, lower]) + require(len(result) == 34, 'complete relaxed state count') + return result + + +def overlap_cap(left, right, pp=4, qp=6): + p, q, r, _, _ = left + a, b, c, _, _ = right + return ((p + q + r) * c + (a + b + c) * r - r * c + + pp * min(p, a) + qp * (q + b)) + + +def joint_certificate(candidates): + require(len(candidates) == 34, 'bounded pair census') + minimum, witness = 10_000, None + for left in candidates: + for right in candidates: + overlap = overlap_cap(left, right) + lower = left[4] + right[4] - overlap + if lower < minimum: + minimum = lower + witness = {'departure': left, 'arrival': right, 'overlap_cap': overlap} + require(minimum == 235 and minimum > BUDGET, 'joint cheap union contradiction') + return {'states': candidates, 'pairs_checked': len(candidates) ** 2, + 'minimum_conditional_union_bound': minimum, + 'cheap_budget': BUDGET, 'contradiction': minimum - BUDGET, + 'attaining_relaxed_pair': witness} + + +def calculate(): + return {'geometry': reconstruct(), 'certificate': joint_certificate(states()), + 'profile': {'cheap': BUDGET, 'unit': 180, 'skip_dimension_three': 11}, + 'scope': 'Reject named profile in frozen X-only monotone model; no supplier or kappa'} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--emit', action='store_true') + args = parser.parse_args() + result = calculate() + if args.emit: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + require(json.dumps(result, sort_keys=True) == json.dumps( + read_json(PACKAGE / 'RESULT.json'), sort_keys=True), 'typed receipt equality') + print('PASS_P104_JOINT_ENDPOINT cheap=232 broad=191 bound=235 states=34 pairs=1156') + + +if __name__ == '__main__': + try: + main() + except (OSError, ValueError, KeyError, TypeError) as error: + raise SystemExit(f'FAIL_P104_JOINT_ENDPOINT: {error}') from error