From 9bdba17f90e7c2a3092186f55f06d019c2823546 Mon Sep 17 00:00:00 2001 From: josecarlosgonzalezroque-design Date: Sat, 17 Oct 2026 07:26:17 -0600 Subject: [PATCH] Audit ten rank7 departure obstructions with independent minors Reconstruct coordinates and frame bounds from both pinned PR3042 words. Add ten explicit determinant witnesses, row-restriction null controls, and registered source-bound replay. Scoped audit of PR3114; no new kappa. --- .../rank7-departure-minor-audit/README.md | 188 ++ .../rank7-departure-minor-audit/RESULT.json | 1903 +++++++++++++++++ .../rank7-departure-minor-audit/SOURCES.json | 35 + .../rank7-departure-minor-audit/TASK.json | 102 + .../rank7-departure-minor-audit/VERIFY.json | 31 + .../test_verify.py | 109 + .../rank7-departure-minor-audit/verify.py | 422 ++++ 7 files changed, 2790 insertions(+) create mode 100644 research/rank7-departure-minor-audit/README.md create mode 100644 research/rank7-departure-minor-audit/RESULT.json create mode 100644 research/rank7-departure-minor-audit/SOURCES.json create mode 100644 research/rank7-departure-minor-audit/TASK.json create mode 100644 research/rank7-departure-minor-audit/VERIFY.json create mode 100644 research/rank7-departure-minor-audit/test_verify.py create mode 100644 research/rank7-departure-minor-audit/verify.py diff --git a/research/rank7-departure-minor-audit/README.md b/research/rank7-departure-minor-audit/README.md new file mode 100644 index 0000000000..5876acd6b7 --- /dev/null +++ b/research/rank7-departure-minor-audit/README.md @@ -0,0 +1,188 @@ +# Independent departure-minor audit for PR3114 + +**Scoped audit: ten departure obstructions reproduced on both PR3042 words.** +This package gives explicit nonzero rational minors for the eight proposed +`(1,3)` replacements of `(2,2)` restore climbs and the two departure-forced +visits in Marius-Paul Dumitrean's [PR3114](https://github.com/CrocSwap/integer-mult-bounds/pull/3114), +at head `c88769c350977d9ed4f90fe5c652d582cfe2782a`. +The result is evidence for that particular implication of the fixed-A/B model, +not a verification of the complete restore-optimality theorem or an admitted supplier. + +The only computational inputs are dcharb78's two PR3042 words, with Git blob and +SHA256 pins in [SOURCES.json](SOURCES.json). No predecessor Python module, +frame optimizer, cost engine or stored certificate is imported or executed. +The proof and source implementation were read before writing this separate +implementation; this is not a blind audit or a new departure lemma. + +## Result + +For each provider, the checker verifies all **91** restored-helper coordinate +identities against **520** independently replayed non-target input rows. It +reconstructs entry-frame bounds from the scalar/warp chronology and enumerates +**27** candidate frames: **17** have no possible reader and **10** have a full +column-rank departure matrix. The complete results for the two providers agree. + +The following determinants refer to the ordered columns and selected rows in +[RESULT.json](RESULT.json). Integer minors clear each selected row's positive +denominator; the rational determinant divides by the product of those scales. + +| Register | Candidate frames | Columns | Integer determinant | Rational determinant | Restricted-row rank | +|---|---:|---:|---:|---:|---:| +| 5 | 3 | 10 | 1 | 1/4 | 2 | +| 34 | 3 | 8 | -2 | -1/2 | 2 | +| 44 | 3 | 6 | -1 | -1 | 2 | +| 54 | 3 | 6 | 2 | 1/2 | 2 | +| 73 | 3 | 10 | -1 | -1/4 | 2 | +| 105 | 3 | 6 | -1 | -1 | 2 | +| 414 | 3 | 6 | -1 | -1 | 2 | +| 430 | 3 | 6 | -1 | -1 | 2 | +| 69 | 2 | 2 | -1 | -1 | 1 | +| 444 | 1 | 2 | -1 | -1 | 1 | + +There is exactly one rank-obstructed frame per register. All remaining +candidates have no reader. The eight split registers have forced dimension-5 +entry frames, no reader at entry, dimension-9 ends, and three possible +dimension-6 first frames inside their dimension-7 receiver caps. +Thus none admits a two-jump `5 -> 6 -> 9` restore chain in the stated model. +For 69 and 444, every admissible entry frame excludes a direct departure to +FULL without an intermediate visit. + +Restricting the departure rows to receivers whose ends contain the candidate +frame loses rank in **all ten** cases. Each receipt includes an explicit +nonzero null vector for that restricted matrix, and verifies that the full +matrix detects it. This independently reconstructs and makes inspectable the +row-restriction failure control of PR3114; the control itself is credited to +that predecessor. + +## Why these matrices give an obstruction + +Use the fixed-prefix, fixed-end, monotone scalar-restore model of +[PR3114's proof](https://github.com/CrocSwap/integer-mult-bounds/blob/c88769c350977d9ed4f90fe5c652d582cfe2782a/research/rank7-skip-restore-optimum/README.md#proof). +Let `e_q` be the non-target rows at restore entry, `L_q` their entry-frame +lower bounds, and `E_q` their fixed end frames. A restored helper `c` must end +at its own arbitrary input `x_c`. + +1. **Forced coordinates.** Independently replay the non-target A/B prefix over + sparse rational free-warp words. Each ADD has distinct operands, each SCALE + is nonzero, and each warp is an invertible free-group symbol. Target-only + corrections/wrappers/cut cannot feed back into these rows. The resulting + 520 non-target rows are therefore independent. The literal restore supplies + candidate coefficients `M[c]`, but the checker separately verifies + `sum_q M[c,q] e_q = x_c` for every restored helper. Uniqueness makes these + coefficients necessary for every exact restore. An empty or damaged restore + fails this identity; it cannot define its own acceptance condition. + +2. **Frame constraints.** A nonzero `M[c,q]` with `q != c` requires a + chronological gate path from `q` to `c`, so the entry frame of `q` + lies inside `E_c`. Build an event DAG with shared vertices for ADD operands, + warp resets and cut/warp last-use equalities. Forward unions give lower + bounds; backward intersections propagate end frames, these forced caps + and fixed equalities. Both operands' subsequent uses matter: in particular, + the dimension-8 receiver caps of 69/444 alone are insufficient, while their + reconstructed entry upper bounds have dimension 7. This is set dataflow, + not cost minimization. A possible reader at `G` must satisfy + `L_y <= G <= E_y`; absence is a necessary-condition rejection. + +3. **Departure.** Suppose register `r` stays inside `G` until it departs to + `E_r`. For the invertible restore-prefix matrix `A_t`, its inverse column + `d_r = A_t^-1 e_r` is nonzero. An ADD `t += k*s` replaces inverse column + `d_s` by `d_s - k*d_t`. Recursing backward through these updates, every + contributing register has an earlier frame inside `G`; monotonicity gives + support in `Z = {r} union {y != r : L_y <= G}`. Targets are excluded because + they cannot feed into a non-target restore. + + Let `O = {c restored : c != r and E_r not<= E_c}`. After departure there + can be no gate path from `r` to any `c in O`. The remaining restore matrix + therefore has zero `(c,r)` entries, equivalently `M[O][Z] d_r = 0`. + A nonzero square minor with all `|Z|` columns contradicts this nonzero + kernel vector. Crucially, `O` includes receivers that cannot themselves + sit at `G`, and `Z` includes registers that can sit strictly below `G`. + +4. **Bounded application.** For the eight split registers the entry frame is + forced and has no reader. A two-jump split with first dimension 6 must + deliver its required contents at that intermediate frame. The receiver + intersections give all three candidates, each excluded above. For 69/444, + enumerate the entire admissible entry interval and exclude each possible + skip in the same way. This does not enumerate arbitrary restore programs: + the inverse-column argument supplies the necessary condition for them. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/rank7-departure-minor-audit --check-only +python3.12 -B scripts/research_package.py --package research/rank7-departure-minor-audit +``` + +The first registered command recomputes and byte-compares the deterministic +receipt. The second runs eight behavioral test groups under optimized Python. +Those include a separate rational Gaussian determinant calculation for every +minor, singular-minor controls, corrupt source bytes, an empty restore, a wrong +restored-helper coefficient, a changed prefix with unchanged restore, target +feedback and singular gates, an inconsistent cut equality, and deletion of a +required departure coordinate. Mathematical null controls run in every replay. + +To regenerate the receipt after an intentional code change: + +```sh +python3.12 -B research/rank7-departure-minor-audit/verify.py --write +``` + +Observed locally with CPython 3.12.14 on Windows. Checks use explicit exceptions, +so `-O` does not disable acceptance conditions. No full PR3114 replay, native +transport/phase validation, complete target endpoint, cleanup/allocation invoice, +moment enclosure, or selected cold replay is included. The model's legal gate +and restored-helper endpoint requirements are inherited from the cited proof; +this checker is not a replacement for the full BORROW-WORD auditor. + +## Selection and overlap + +Base: canonical main `997e6a9ca7b4f95d50e366f61412fd640d72a88a`, refreshed +unchanged before submission; priority revision 6. Card `independent-moment`, +scope key `c191650c0fa8d2fa514e`; the preserved original card and refinement +are in [TASK.json](TASK.json). The card's baseline command stopped at a missing +selected assembly in the sparse checkout; no baseline PASS is claimed. + +[PR3050](https://github.com/CrocSwap/integer-mult-bounds/pull/3050) already covers +the PR3042 restore-splice audit initially considered, so that duplicate was +stopped. [PR3056](https://github.com/CrocSwap/integer-mult-bounds/pull/3056) +covers a local contraction; [PR3057](https://github.com/CrocSwap/integer-mult-bounds/pull/3057) +and [PR3065](https://github.com/CrocSwap/integer-mult-bounds/pull/3065) cover frame +optimization with fixed scalar order. PR3114 adds the arbitrary-restore claim +and its own checks. This package adds separate coordinate/frame reconstruction, +explicit determinant witnesses and null vectors for ten of its obstructions. +It does not reproduce its full bound, classification or payer-group proof. + +The handoff/start-here/active Discussion pages and targeted live PR searches +were inspected. The offline overlap helper had sparse local coverage and no +remote cache; Discussion pagination and arbitrary code diffs were not exhaustively +searched. No-match is not a novelty guarantee. +[PR3133](https://github.com/CrocSwap/integer-mult-bounds/pull/3133) changes helper +ends and B routing; the fixed-end result here makes no claim about that word. + +## Open next questions + +The structured questions in [TASK.json](TASK.json) identify two useful follow-ups: + +- Independently reconstruct PR3114's remaining lower-bound terms and the + disjoint charging proof. Start with the pinned empty-restore optimum and + remaining blocked/zero-sum/lift groups. These require a separate exact + optimizer and proof review; the ten minors do not settle them. +- For a concrete A/B or helper-end rewrite, first identify the changed + coordinates and frame intervals. Old witnesses only apply if their premises + remain true; a new source-bound word and its admission evidence are needed. + +## Credit + +The departure lemma, ten cases and original restriction control are due to +Marius-Paul Dumitrean (PR3114, with Claude Code); the two words are dcharb78's +PR3042. Retain credit for the PR2979 joint construction (Marius-Paul Dumitrean), +PR3015 and its declared-edit lineage (Jeremy Kothe), PR2917 (Mason Hale), +PR2908 (Jeremy Diviney), and the PR2833 free-algebra auditor (icekylinx). +Nick Petalas's independent audits in PR3050/3056/3057/3065 supply the overlapping +coverage described above. + +Prepared for josecarlosgonzalezroque-design with substantial OpenAI Codex +assistance in analysis, implementation, tests and exposition. No separate agent, +independent human or proof-assistant review is claimed. New work: Apache-2.0. diff --git a/research/rank7-departure-minor-audit/RESULT.json b/research/rank7-departure-minor-audit/RESULT.json new file mode 100644 index 0000000000..a55d0de80d --- /dev/null +++ b/research/rank7-departure-minor-audit/RESULT.json @@ -0,0 +1,1903 @@ +{ + "providers": 2, + "result": { + "departure_witnesses": [ + { + "columns": [ + 5, + 369, + 371, + 373, + 378, + 385, + 387, + 389, + 394, + 395 + ], + "frame": [ + 8, + 22, + 37, + 67, + 131, + 259 + ], + "integer_determinant": 1, + "integer_minor": [ + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -1 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -1 + ] + ], + "rational_determinant": "1/4", + "register": 5, + "restricted_receivers": [ + 363, + 395, + 408, + 424, + 454, + 455, + 554, + 555, + 556, + 557, + 566, + 567, + 584, + 585, + 590, + 591 + ], + "restricted_row_null_vector": [ + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + "restricted_row_rank": 2, + "row_denominator_scales": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 4, + 1 + ], + "selected_receivers": [ + 369, + 371, + 373, + 378, + 385, + 387, + 389, + 394, + 395, + 556 + ] + }, + { + "columns": [ + 34, + 307, + 309, + 314, + 323, + 325, + 330, + 331 + ], + "frame": [ + 1, + 30, + 44, + 74, + 138, + 266 + ], + "integer_determinant": -2, + "integer_minor": [ + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + -1 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ] + ], + "rational_determinant": "-1/2", + "register": 34, + "restricted_receivers": [ + 226, + 228, + 230, + 331, + 408, + 424, + 450, + 451, + 508, + 509, + 531, + 543, + 586, + 587, + 588, + 589 + ], + "restricted_row_null_vector": [ + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0" + ], + "restricted_row_rank": 2, + "row_denominator_scales": [ + 4, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "selected_receivers": [ + 228, + 307, + 309, + 314, + 323, + 325, + 330, + 331 + ] + }, + { + "columns": [ + 44, + 369, + 371, + 373, + 378, + 424 + ], + "frame": [ + 2, + 8, + 20, + 37, + 65, + 384 + ], + "integer_determinant": -1, + "integer_minor": [ + [ + 0, + 1, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 1, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 1, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 1, + 0 + ], + [ + 1, + 0, + 0, + 0, + 0, + 1 + ], + [ + 0, + 0, + 0, + 0, + 0, + -1 + ] + ], + "rational_determinant": "-1", + "register": 44, + "restricted_receivers": [ + 327, + 408, + 424, + 510, + 511, + 580, + 581 + ], + "restricted_row_null_vector": [ + "0", + "1", + "0", + "0", + "0", + "0" + ], + "restricted_row_rank": 2, + "row_denominator_scales": [ + 1, + 1, + 1, + 1, + 1, + 1 + ], + "selected_receivers": [ + 369, + 371, + 373, + 378, + 424, + 580 + ] + }, + { + "columns": [ + 54, + 277, + 282, + 293, + 298, + 299 + ], + "frame": [ + 4, + 26, + 41, + 75, + 139, + 267 + ], + "integer_determinant": 2, + "integer_minor": [ + [ + 1, + 0, + 0, + 0, + 0, + 1 + ], + [ + 0, + 1, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 1, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 1, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 1, + 0 + ], + [ + -1, + 0, + 0, + 0, + 0, + 1 + ] + ], + "rational_determinant": "1/2", + "register": 54, + "restricted_receivers": [ + 226, + 228, + 230, + 299, + 448, + 449, + 484, + 485, + 554, + 555, + 566, + 567, + 584, + 585, + 590, + 591 + ], + "restricted_row_null_vector": [ + "0", + "1", + "0", + "0", + "0", + "0" + ], + "restricted_row_rank": 2, + "row_denominator_scales": [ + 4, + 1, + 1, + 1, + 1, + 1 + ], + "selected_receivers": [ + 226, + 277, + 282, + 293, + 298, + 299 + ] + }, + { + "columns": [ + 73, + 337, + 339, + 341, + 346, + 353, + 355, + 357, + 362, + 363 + ], + "frame": [ + 13, + 19, + 32, + 70, + 134, + 262 + ], + "integer_determinant": -1, + "integer_minor": [ + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0 + ], + [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -1 + ] + ], + "rational_determinant": "-1/4", + "register": 73, + "restricted_receivers": [ + 363, + 395, + 452, + 453, + 531, + 532, + 533, + 543, + 586, + 587, + 588, + 589 + ], + "restricted_row_null_vector": [ + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + "restricted_row_rank": 2, + "row_denominator_scales": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 4, + 1 + ], + "selected_receivers": [ + 337, + 339, + 341, + 346, + 353, + 355, + 357, + 362, + 363, + 532 + ] + }, + { + "columns": [ + 105, + 369, + 371, + 373, + 378, + 408 + ], + "frame": [ + 8, + 22, + 37, + 67, + 129, + 257 + ], + "integer_determinant": -1, + "integer_minor": [ + [ + 0, + 1, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 1, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 1, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 1, + 0 + ], + [ + 1, + 0, + 0, + 0, + 0, + 1 + ], + [ + 0, + 0, + 0, + 0, + 0, + -1 + ] + ], + "rational_determinant": "-1", + "register": 105, + "restricted_receivers": [ + 304, + 408, + 424, + 500, + 501, + 572, + 573 + ], + "restricted_row_null_vector": [ + "0", + "1", + "0", + "0", + "0", + "0" + ], + "restricted_row_rank": 2, + "row_denominator_scales": [ + 1, + 1, + 1, + 1, + 1, + 1 + ], + "selected_receivers": [ + 369, + 371, + 373, + 378, + 408, + 572 + ] + }, + { + "columns": [ + 414, + 385, + 387, + 389, + 394, + 412 + ], + "frame": [ + 10, + 20, + 39, + 65, + 131, + 259 + ], + "integer_determinant": -1, + "integer_minor": [ + [ + 0, + 1, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 1, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 1, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 1, + 0 + ], + [ + 1, + 0, + 0, + 0, + 0, + -1 + ], + [ + 0, + 0, + 0, + 0, + 0, + -1 + ] + ], + "rational_determinant": "-1", + "register": 414, + "restricted_receivers": [ + 320, + 408, + 412, + 424, + 512, + 513, + 574, + 575 + ], + "restricted_row_null_vector": [ + "0", + "1", + "0", + "0", + "0", + "0" + ], + "restricted_row_rank": 2, + "row_denominator_scales": [ + 1, + 1, + 1, + 1, + 1, + 1 + ], + "selected_receivers": [ + 385, + 387, + 389, + 394, + 412, + 574 + ] + }, + { + "columns": [ + 430, + 385, + 387, + 389, + 394, + 428 + ], + "frame": [ + 2, + 28, + 45, + 73, + 129, + 257 + ], + "integer_determinant": -1, + "integer_minor": [ + [ + 0, + 1, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 1, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 1, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 1, + 0 + ], + [ + 1, + 0, + 0, + 0, + 0, + -1 + ], + [ + 0, + 0, + 0, + 0, + 0, + -1 + ] + ], + "rational_determinant": "-1", + "register": 430, + "restricted_receivers": [ + 311, + 408, + 424, + 428, + 498, + 499, + 582, + 583 + ], + "restricted_row_null_vector": [ + "0", + "1", + "0", + "0", + "0", + "0" + ], + "restricted_row_rank": 2, + "row_denominator_scales": [ + 1, + 1, + 1, + 1, + 1, + 1 + ], + "selected_receivers": [ + 385, + 387, + 389, + 394, + 428, + 582 + ] + }, + { + "columns": [ + 69, + 231 + ], + "frame": [ + 4, + 8, + 17, + 34, + 64, + 128, + 259 + ], + "integer_determinant": -1, + "integer_minor": [ + [ + 0, + -1 + ], + [ + -1, + 0 + ] + ], + "rational_determinant": "-1", + "register": 69, + "restricted_receivers": [ + 554, + 555, + 566, + 567, + 584, + 585, + 590, + 591 + ], + "restricted_row_null_vector": [ + "0", + "1" + ], + "restricted_row_rank": 1, + "row_denominator_scales": [ + 1, + 1 + ], + "selected_receivers": [ + 448, + 566 + ] + }, + { + "columns": [ + 444, + 238 + ], + "frame": [ + 3, + 4, + 8, + 48, + 64, + 128, + 273 + ], + "integer_determinant": -1, + "integer_minor": [ + [ + 0, + -1 + ], + [ + -1, + 0 + ] + ], + "rational_determinant": "-1", + "register": 444, + "restricted_receivers": [ + 554, + 555, + 566, + 567, + 584, + 585, + 590, + 591 + ], + "restricted_row_null_vector": [ + "0", + "1" + ], + "restricted_row_rank": 1, + "row_denominator_scales": [ + 1, + 1 + ], + "selected_receivers": [ + 455, + 590 + ] + } + ], + "domains": [ + { + "candidate_frames": [ + [ + 3, + 29, + 45, + 64, + 128, + 256 + ], + [ + 8, + 22, + 37, + 67, + 131, + 259 + ], + [ + 11, + 21, + 38, + 67, + 131, + 259 + ] + ], + "entry_lower": [ + 30, + 45, + 67, + 131, + 259 + ], + "entry_upper": [ + 30, + 45, + 67, + 131, + 259 + ], + "receiver_cap": [ + 3, + 8, + 21, + 37, + 64, + 128, + 256 + ], + "register": 5 + }, + { + "candidate_frames": [ + [ + 1, + 30, + 44, + 74, + 138, + 266 + ], + [ + 10, + 20, + 39, + 64, + 128, + 256 + ], + [ + 11, + 21, + 38, + 65, + 129, + 257 + ] + ], + "entry_lower": [ + 30, + 45, + 74, + 138, + 266 + ], + "entry_upper": [ + 30, + 45, + 74, + 138, + 266 + ], + "receiver_cap": [ + 1, + 10, + 20, + 38, + 64, + 128, + 256 + ], + "register": 34 + }, + { + "candidate_frames": [ + [ + 2, + 8, + 20, + 37, + 65, + 384 + ], + [ + 2, + 8, + 20, + 65, + 128, + 293 + ], + [ + 2, + 8, + 20, + 65, + 165, + 256 + ] + ], + "entry_lower": [ + 2, + 8, + 20, + 65, + 421 + ], + "entry_upper": [ + 2, + 8, + 20, + 65, + 421 + ], + "receiver_cap": [ + 2, + 8, + 20, + 37, + 65, + 128, + 256 + ], + "register": 44 + }, + { + "candidate_frames": [ + [ + 4, + 11, + 17, + 34, + 192, + 320 + ], + [ + 4, + 26, + 41, + 64, + 128, + 256 + ], + [ + 4, + 26, + 41, + 75, + 139, + 267 + ] + ], + "entry_lower": [ + 4, + 26, + 41, + 192, + 320 + ], + "entry_upper": [ + 4, + 26, + 41, + 192, + 320 + ], + "receiver_cap": [ + 4, + 11, + 17, + 34, + 64, + 128, + 256 + ], + "register": 54 + }, + { + "candidate_frames": [ + [ + 6, + 11, + 19, + 32, + 192, + 320 + ], + [ + 13, + 19, + 32, + 64, + 128, + 256 + ], + [ + 13, + 19, + 32, + 70, + 134, + 262 + ] + ], + "entry_lower": [ + 13, + 19, + 32, + 192, + 320 + ], + "entry_upper": [ + 13, + 19, + 32, + 192, + 320 + ], + "receiver_cap": [ + 6, + 11, + 19, + 32, + 64, + 128, + 256 + ], + "register": 73 + }, + { + "candidate_frames": [ + [ + 1, + 8, + 22, + 102, + 128, + 256 + ], + [ + 8, + 22, + 36, + 66, + 129, + 257 + ], + [ + 8, + 22, + 37, + 67, + 129, + 257 + ] + ], + "entry_lower": [ + 8, + 22, + 102, + 129, + 257 + ], + "entry_upper": [ + 8, + 22, + 102, + 129, + 257 + ], + "receiver_cap": [ + 1, + 8, + 22, + 36, + 66, + 128, + 256 + ], + "register": 105 + }, + { + "candidate_frames": [ + [ + 3, + 9, + 20, + 65, + 164, + 256 + ], + [ + 10, + 20, + 36, + 65, + 128, + 259 + ], + [ + 10, + 20, + 39, + 65, + 131, + 259 + ] + ], + "entry_lower": [ + 10, + 20, + 65, + 164, + 259 + ], + "entry_upper": [ + 10, + 20, + 65, + 164, + 259 + ], + "receiver_cap": [ + 3, + 9, + 20, + 36, + 65, + 128, + 256 + ], + "register": 414 + }, + { + "candidate_frames": [ + [ + 1, + 30, + 46, + 72, + 128, + 256 + ], + [ + 2, + 28, + 45, + 73, + 129, + 257 + ], + [ + 3, + 29, + 44, + 73, + 129, + 257 + ] + ], + "entry_lower": [ + 30, + 47, + 73, + 129, + 257 + ], + "entry_upper": [ + 30, + 47, + 73, + 129, + 257 + ], + "receiver_cap": [ + 1, + 2, + 28, + 44, + 72, + 128, + 256 + ], + "register": 430 + }, + { + "candidate_frames": [ + [ + 12, + 17, + 34, + 68, + 128, + 259 + ], + [ + 4, + 8, + 17, + 34, + 64, + 128, + 259 + ] + ], + "entry_lower": [ + 12, + 17, + 34, + 68, + 128, + 259 + ], + "entry_upper": [ + 4, + 8, + 17, + 34, + 64, + 128, + 259 + ], + "receiver_cap": [ + 3, + 4, + 8, + 17, + 33, + 64, + 128, + 256 + ], + "register": 69 + }, + { + "candidate_frames": [ + [ + 3, + 4, + 8, + 48, + 64, + 128, + 273 + ] + ], + "entry_lower": [ + 3, + 4, + 8, + 48, + 64, + 128, + 273 + ], + "entry_upper": [ + 3, + 4, + 8, + 48, + 64, + 128, + 273 + ], + "receiver_cap": [ + 3, + 4, + 8, + 17, + 33, + 64, + 128, + 256 + ], + "register": 444 + } + ], + "no_reader_cases": [ + { + "frame": [ + 3, + 29, + 45, + 64, + 128, + 256 + ], + "register": 5 + }, + { + "frame": [ + 11, + 21, + 38, + 67, + 131, + 259 + ], + "register": 5 + }, + { + "frame": [ + 10, + 20, + 39, + 64, + 128, + 256 + ], + "register": 34 + }, + { + "frame": [ + 11, + 21, + 38, + 65, + 129, + 257 + ], + "register": 34 + }, + { + "frame": [ + 2, + 8, + 20, + 65, + 128, + 293 + ], + "register": 44 + }, + { + "frame": [ + 2, + 8, + 20, + 65, + 165, + 256 + ], + "register": 44 + }, + { + "frame": [ + 4, + 11, + 17, + 34, + 192, + 320 + ], + "register": 54 + }, + { + "frame": [ + 4, + 26, + 41, + 64, + 128, + 256 + ], + "register": 54 + }, + { + "frame": [ + 6, + 11, + 19, + 32, + 192, + 320 + ], + "register": 73 + }, + { + "frame": [ + 13, + 19, + 32, + 64, + 128, + 256 + ], + "register": 73 + }, + { + "frame": [ + 1, + 8, + 22, + 102, + 128, + 256 + ], + "register": 105 + }, + { + "frame": [ + 8, + 22, + 36, + 66, + 129, + 257 + ], + "register": 105 + }, + { + "frame": [ + 3, + 9, + 20, + 65, + 164, + 256 + ], + "register": 414 + }, + { + "frame": [ + 10, + 20, + 36, + 65, + 128, + 259 + ], + "register": 414 + }, + { + "frame": [ + 1, + 30, + 46, + 72, + 128, + 256 + ], + "register": 430 + }, + { + "frame": [ + 3, + 29, + 44, + 73, + 129, + 257 + ], + "register": 430 + }, + { + "frame": [ + 12, + 17, + 34, + 68, + 128, + 259 + ], + "register": 69 + } + ], + "non_target_prefix_rows": 520, + "restored_coordinates_checked": 91 + }, + "scope": "Ten departure rank obstructions, not the complete restore-optimality theorem or supplier admission.", + "source_head": "c88769c350977d9ed4f90fe5c652d582cfe2782a", + "source_pr": 3114, + "status": "PASS_RANK7_DEPARTURE_MINOR_AUDIT" +} diff --git a/research/rank7-departure-minor-audit/SOURCES.json b/research/rank7-departure-minor-audit/SOURCES.json new file mode 100644 index 0000000000..f353db6d59 --- /dev/null +++ b/research/rank7-departure-minor-audit/SOURCES.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/rank7-restore-carrier-skips/edits/FINAL-WORD-base.json.gz", + "usage": "input", + "git_blob": "2ee02e318c98281a71445b954feccd55c153827c", + "sha256": "7e98f6f2a6c9ce9e7e04b515bd8ce4a4a533ff05f01ea265be2a1a994695260e" + }, + { + "path": "research/rank7-restore-carrier-skips/edits/FINAL-WORD-extra.json.gz", + "usage": "input", + "git_blob": "33ba5f34996a31edd197cb58eca575645575e529", + "sha256": "1396410de482883416fc7f534062ab005b484056b035fdcfa3b5cc065536ba35" + } + ], + "claim_under_review": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/3114", + "head": "c88769c350977d9ed4f90fe5c652d582cfe2782a", + "role": "Bibliographic comparison only; no PR3114 executable, certificate or cost output is a replay input." + } +} diff --git a/research/rank7-departure-minor-audit/TASK.json b/research/rank7-departure-minor-audit/TASK.json new file mode 100644 index 0000000000..1dbccca804 --- /dev/null +++ b/research/rank7-departure-minor-audit/TASK.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "refined", + "actual_scope": "Independently reconstruct PR3114's ten departure-rank obstructions on the pinned PR3042 base/extra words, with explicit nonzero minors and row-restriction countercontrols.", + "scope_change_reason": "The initial bounded PR3042 restore-splice audit was already covered by PR3050; stop that duplicate and make one pivot to the new departure-lemma implication in PR3114. This does not complete the card's full physical-ledger/supplier-admission objective.", + "bottleneck_link": "Scoped independent evidence for a new fixed-A/B restore-only obstruction, before treating the author-checked optimum as a reason to redirect construction work. This is a local proof audit, not independent supplier pricing.", + "budget_minutes": 60, + "stop_rule": "Stop after the ten obstructions on both providers, source binding and semantic failure controls. Do not extend a lowering census, optimize A/B, or claim the complete restore-only optimum or a new kappa.", + "outcome": "partial", + "evidence": "RESULT.json, verify.py and test_verify.py. Both providers have 27 candidate frames: 17 have no reader and 10 have an explicit nonzero minor. All 91 restored-helper coordinate identities are checked against an independently replayed 520-row non-target prefix. Eight test groups exercise positive cases, a second determinant algorithm and rejecting semantic/source faults.", + "author": "josecarlosgonzalezroque-design (OpenAI Codex assisted)", + "ai_assistance": "Substantial OpenAI Codex assistance in source reading, proof analysis, implementation, testing and writing. No separate agent, independent human or proof-assistant review is claimed.", + "open_questions": [ + { + "question": "Does the complete fixed-A/B restore-only lower bound of PR3114 survive a separate reconstruction of its remaining terms?", + "why_it_matters": "These ten obstructions do not establish the empty-restore optimum or the complete disjoint charging argument.", + "first_step": "At head c88769c350977d9ed4f90fe5c652d582cfe2782a, independently check LB_forced and the remaining blocked/zero-sum/lift groups, retaining these minors as a scoped positive control.", + "blocked_by": "A separate exact cost/frame optimizer and review of group disjointness; neither is implemented here." + }, + { + "question": "Which coordinate or frame constraint actually changes in a proposed A/B or helper-end rewrite?", + "why_it_matters": "The audited result has fixed-prefix and fixed-end hypotheses; it cannot rule out later changes to those hypotheses.", + "first_step": "Recompute the 91 own-input identities and affected L/U/end spaces on one precisely pinned proposed rewrite before applying any of the ten old witnesses.", + "blocked_by": "A concrete changed word with full source pins and its own admission evidence." + } + ], + "selection": { + "seed": "eb64135aaa17ef3bfde3538fe5983a52", + "scope_key": "c191650c0fa8d2fa514e", + "track": "independent-verification", + "priority_revision": 6 + }, + "baseline": { + "command": "python -B scripts/research_baseline.py", + "status": "unavailable-in-sparse-checkout", + "reason": "The source-bound orientation command stopped at missing research/community-frontier1094-audit/ASSEMBLY.json. No baseline PASS or selected cold replay is claimed." + }, + "overlap": { + "coverage": "Read the handoff/start-here/active Discussion pages and targeted live PR searches; the offline helper had only the sparse local ledger and no gh/cache snapshot. Discussion pagination and arbitrary source diffs were not comprehensively searched.", + "duplicate_avoided": "PR3050 already independently checks PR3042 restore splices and the 29976-unit correction.", + "comparison_prs": [ + 3050, + 3056, + 3057, + 3065, + 3114, + 3133 + ], + "final_queries": [ + "3114", + "departure" + ], + "canonical_main": "997e6a9ca7b4f95d50e366f61412fd640d72a88a", + "claim_under_review_head": "c88769c350977d9ed4f90fe5c652d582cfe2782a", + "limitation": "No targeted match for another audit of these ten minors was found; this is not a proof of novelty. PR3133 changes helper endpoints and is outside the fixed-end hypothesis." + } +} diff --git a/research/rank7-departure-minor-audit/VERIFY.json b/research/rank7-departure-minor-audit/VERIFY.json new file mode 100644 index 0000000000..922e54c945 --- /dev/null +++ b/research/rank7-departure-minor-audit/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/rank7-restore-carrier-skips/edits/FINAL-WORD-base.json.gz", + "research/rank7-restore-carrier-skips/edits/FINAL-WORD-extra.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate both words; reconstruct coordinate identities and frame intervals; recompute and byte-compare ten determinant witnesses and seventeen no-reader cases per provider, including row-restriction null controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Eight behavioral groups with optimized Python: both providers, a separate rational determinant, corrupted bytes, empty restore, changed coefficients/prefix, illegal feedback or singular gates, inconsistent cut frame, and missing departure coordinate." + } + ] +} diff --git a/research/rank7-departure-minor-audit/test_verify.py b/research/rank7-departure-minor-audit/test_verify.py new file mode 100644 index 0000000000..a19461e7d7 --- /dev/null +++ b/research/rank7-departure-minor-audit/test_verify.py @@ -0,0 +1,109 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Fault controls for the independent departure audit (standard library only).""" +import copy +import json +import unittest +from fractions import Fraction as Q + +import verify as v + + +def rational_det(matrix): + """Separate Gaussian determinant, without Bareiss or row-basis selection.""" + a = [list(map(Q, row)) for row in matrix] + answer = Q(1) + for j in range(len(a)): + p = next((i for i in range(j, len(a)) if a[i][j]), None) + if p is None: + return Q(0) + if p != j: + a[j], a[p] = a[p], a[j] + answer = -answer + pivot = a[j][j] + answer *= pivot + for i in range(j + 1, len(a)): + factor = a[i][j] / pivot + for k in range(j, len(a)): + a[i][k] -= factor * a[j][k] + return answer + + +class AuditControls(unittest.TestCase): + @classmethod + def setUpClass(cls): + sources = json.loads((v.HERE / 'SOURCES.json').read_bytes())['files'] + cls.source = next(s for s in sources if s['usage'] == 'input') + cls.raw = (v.ROOT / cls.source['path']).read_bytes() + cls.word = v.decode_word(cls.raw, cls.source['sha256']) + cls.result = v.run()['result'] + + def test_both_providers_and_all_minor_determinants(self): + self.assertEqual(len(self.result['departure_witnesses']), 10) + self.assertEqual(len(self.result['no_reader_cases']), 17) + for w in self.result['departure_witnesses']: + with self.subTest(register=w['register']): + a = w['integer_minor'] + self.assertEqual(rational_det(a), w['integer_determinant']) + self.assertNotEqual(rational_det(a), 0) + bad = copy.deepcopy(a) + bad[-1] = bad[0][:] + self.assertEqual(rational_det(bad), 0) + self.assertEqual(v.determinant(bad), 0) + + def test_corrupt_bytes_fail_before_parsing(self): + with self.assertRaisesRegex(ValueError, 'source digest mismatch'): + v.decode_word(self.raw[:-1] + bytes([self.raw[-1] ^ 1]), self.source['sha256']) + + def test_empty_restore_cannot_supply_its_own_coordinates(self): + w = copy.deepcopy(self.word) + w['restore'] = [] + with self.assertRaisesRegex(ValueError, 'forced coordinate fails prefix identity'): + v.forced_coordinates(w) + + def test_wrong_restored_helper_coefficient(self): + w = copy.deepcopy(self.word) + gate = next(g for g in reversed(w['restore']) + if g[0] == 'scale' and str(g[1]) in w['helper_final']) + gate[2] = -gate[2] + with self.assertRaisesRegex(ValueError, 'forced coordinate fails prefix identity'): + v.forced_coordinates(w) + + def test_changed_prefix_with_unchanged_restore(self): + w = copy.deepcopy(self.word) + helper = min(map(int, w['helper_final'])) + w['B'].append(['add', helper, 0, 1, 1, []]) + with self.assertRaisesRegex(ValueError, 'forced coordinate fails prefix identity'): + v.forced_coordinates(w) + + def test_target_feedback_and_singular_gate(self): + w = copy.deepcopy(self.word) + w['B'].append(['add', 0, 112, 1, 1, []]) + with self.assertRaisesRegex(ValueError, 'illegal ADD operands'): + v.forced_coordinates(w) + for gate, message in ((['scale', 0, 0, 1], 'noninvertible SCALE'), + (['add', 0, 0, 1, 1], 'illegal ADD operands')): + with self.subTest(gate=gate), self.assertRaisesRegex(ValueError, message): + v.scalar(gate, {0: {0: Q(1)}}) + rows = {0: {0: Q(1)}} + v.scalar(['scale', 0, 1, -4], rows) + self.assertEqual(rows, {0: {0: Q(-1, 4)}}) + + def test_inconsistent_cut_frame(self): + w = copy.deepcopy(self.word) + w['center_frames'][0] = [] + with self.assertRaisesRegex(ValueError, 'below its lower bound'): + v.entry_bounds(w, v.forced_coordinates(w), v.ends(w)) + + def test_missing_coordinate_destroys_departure_obstruction(self): + m, end = v.forced_coordinates(self.word), v.ends(self.word) + lower, _ = v.entry_bounds(self.word, m, end) + frame = next(w['frame'] for w in self.result['departure_witnesses'] if w['register'] == 69) + for row in m.values(): + row.pop(69, None) + with self.assertRaisesRegex(ValueError, 'departure matrix not full rank'): + v.rank_witness(m, lower, end, 69, v.space(frame)) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/rank7-departure-minor-audit/verify.py b/research/rank7-departure-minor-audit/verify.py new file mode 100644 index 0000000000..167328e609 --- /dev/null +++ b/research/rank7-departure-minor-audit/verify.py @@ -0,0 +1,422 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent, bounded audit of PR3114's ten departure obstructions. + +No predecessor Python module is imported or executed. Inputs are the two +immutable PR3042 words. See README.md for the proof and exact scope. +Prepared for josecarlosgonzalezroque-design with OpenAI Codex assistance. +""" +import argparse +import gzip +import hashlib +import json +import math +from fractions import Fraction as Q +from functools import lru_cache +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +FULL = frozenset(range(512)) +ZERO = frozenset({0}) +SPLIT_REGISTERS = (5, 34, 44, 54, 73, 105, 414, 430) +SKIP_REGISTERS = (69, 444) + + +def require(ok, reason): + if not ok: + raise ValueError(reason) + + +def space(vectors): + out = {0} + for x in vectors: + require(type(x) is int and 0 <= x < 512, 'invalid binary vector') + if x not in out: + out |= {y ^ x for y in out} + return frozenset(out) + + +@lru_cache(None) +def join(a, b): + return a if b <= a else b if a <= b else space(sorted(a | b)) + + +def dim(s): + require(len(s) > 0 and len(s) & (len(s) - 1) == 0, 'not a subspace size') + return len(s).bit_length() - 1 + + +def basis(s): + """Greedy finite-set basis, ascending, independent of the source RREF.""" + out, seen = [], ZERO + for x in sorted(s): + if x not in seen: + out.append(x) + seen = join(seen, space([x])) + require(seen == s, 'not an XOR-closed subspace') + return out + + +def all_subspaces(lo, hi): + require(lo <= hi, 'empty subspace interval') + seen, pending = {lo}, [lo] + while pending: + a = pending.pop() + for x in sorted(hi - a): + b = join(a, space([x])) + if b not in seen: + seen.add(b) + pending.append(b) + return sorted(seen, key=lambda s: (len(s), sorted(s))) + + +def live(w): + return sorted(set(range(224 + w['report']['R'])) - set(w['removed'])) + + +def target(r): + return 112 <= r < 224 + + +def ends(w): + e = {r: FULL for r in live(w)} + for i, p in enumerate(w['ports']): + e[112 + i] = frozenset(x for x in FULL if (x & p).bit_count() % 2 == 0) + e.update({int(r): space(f) for r, f in w['helper_final'].items()}) + return e + + +def b_events(w): + at = {} + for op, rec in enumerate(w['warps'], 1): + at.setdefault(rec[0], []).append(['warp', rec[1], op, rec[3], rec[4]]) + require(all(0 <= p <= len(w['B']) for p in at), 'warp position') + for i in range(len(w['B']) + 1): + yield from at.get(i, []) + if i < len(w['B']): + yield w['B'][i] + + +def entry_bounds(w, m, end): + """Set dataflow; cut/warp equalities anchor the last uses. + + Build the whole DAG before propagating. A last-use equality can affect + later operations on the OTHER operand of that earlier gate. No source + frame solver, cost function or optimized assignment is used. Backward + intersections enforce the other operand's subsequent frame constraints. + """ + nodes, last = [], {} + + def fixed(r, f, parent=None): + last[r] = len(nodes) + nodes.append({'parents': [] if parent is None else [parent], 'fixed': f, 'equal': None}) + + for r in range(224 + w['report']['R']): + f = space([w['ports'][r]]) if r < 112 else ZERO + fixed(r, space(w['start_extra'][str(r)]) if str(r) in w['start_extra'] else f) + + def anchor(r, f): + node = nodes[last[r]] + old = node['equal'] + require(old is None or old == f, 'inconsistent last-use equalities') + node['equal'] = f + + def event(g): + if g[0] == 'warp': + anchor(g[1], space(g[3])) + fixed(g[1], space(g[4])) + return + require(g[0] in ('add', 'scale'), 'unknown frame event') + regs = g[1:3] if g[0] == 'add' else g[1:2] + k = len(nodes) + nodes.append({'parents': [last[r] for r in regs], 'fixed': None, 'equal': None}) + for r in regs: + last[r] = k + + for g in w['A']: + event(g) + cuts = list(zip(w['centers'], w['center_frames'])) + cuts += [(112 + i, w['target_levels'].get(str(i), [])) for i in range(112)] + for r, f in cuts: + f = space(f) + anchor(r, f) + fixed(r, f, last[r]) + for g in b_events(w): + event(g) + values = [] + for node in nodes: + f = ZERO + for p in node['parents']: + f = join(f, values[p]) + if node['fixed'] is not None: + require(f <= node['fixed'], 'fixed frame below its incoming lower bound') + f = node['fixed'] + if node['equal'] is not None: + require(f <= node['equal'], 'last-use equality below its lower bound') + f = node['equal'] + values.append(f) + ceilings = [FULL for _ in nodes] + for k, node in enumerate(nodes): + for f in (node['fixed'], node['equal']): + if f is not None: + ceilings[k] &= f + for r in live(w): + ceilings[last[r]] &= end[r] + for c, row in m.items(): + for r, coefficient in row.items(): + if r != c and coefficient: + ceilings[last[r]] &= end[c] + # A final shared gate is constrained by the subsequent uses of BOTH + # operands. Propagate their end/cap/equality constraints backward. + for k in reversed(range(len(nodes))): + require(values[k] <= ceilings[k], 'inconsistent frame interval') + for p in nodes[k]['parents']: + ceilings[p] &= ceilings[k] + return ({r: values[last[r]] for r in live(w)}, + {r: ceilings[last[r]] for r in live(w)}) + + +def add_row(a, b, c): + out = dict(a) + for k, v in b.items(): + out[k] = out.get(k, Q(0)) + c * v + if not out[k]: + del out[k] + return out + + +def scalar(g, rows): + if g[0] == 'add': + t, s = g[1:3] + require(t != s and t in rows and s in rows, 'illegal ADD operands') + rows[t] = add_row(rows[t], rows[s], Q(g[3], g[4])) + else: + require(g[0] == 'scale' and g[1] in rows, 'unknown scalar gate') + c = Q(g[2], g[3]) + require(c != 0, 'noninvertible SCALE') + rows[g[1]] = {k: c * v for k, v in rows[g[1]].items()} + + +def forced_coordinates(w): + """Derive M from restore, then prove its coordinates against the A/B prefix. + + Target writes cannot feed back into non-targets. The non-target prefix is + a product of invertible ADD/SCALE/free-warp maps, so its rows are independent. + M*entry = own-input therefore establishes UNIQUE forced coordinates. + A malformed restore cannot define its own acceptance condition. + """ + regs = [r for r in live(w) if not target(r)] + rows = {r: {(r, ()): Q(1)} for r in regs} + for c in w['initial_corrections']: + require(target(c['target']), 'correction changes a non-target') + for g in w['precondition'] + w['compensation'] + w['cut']: + require(target(g[1]), 'wrapper changes a non-target') + for g in list(w['A']) + list(b_events(w)): + if target(g[1]): + require(g[0] in ('add', 'scale'), 'target warp not covered') + continue + if g[0] == 'warp': + op = g[2] + require(type(op) is int and op != 0, 'invalid warp symbol') + changed = {} + for (r, word), c in rows[g[1]].items(): + word = word[1:] if word and word[0] == -op else (op,) + word + changed[(r, word)] = c + rows[g[1]] = changed + else: + scalar(g, rows) + m = {r: {r: Q(1)} for r in regs} + for g in w['restore']: + scalar(g, m) + result = {} + for c in sorted(map(int, w['helper_final'])): + row = {} + for q, coefficient in m[c].items(): + row = add_row(row, rows[q], coefficient) + require(row == {(c, ()): Q(1)}, f'forced coordinate fails prefix identity for {c}') + result[c] = m[c] + return result + + +def integer_rows(matrix): + out, scales = [], [] + for row in matrix: + scale = math.lcm(*(x.denominator for x in row)) + out.append([int(x * scale) for x in row]) + scales.append(scale) + return out, scales + + +def pivot_rows(a): + """Fraction-free row-space basis, retaining original row indices.""" + pivots, selected = {}, [] + for i, row in enumerate(a): + row = list(row) + for j, p in sorted(pivots.items()): + x = row[j] + if x: + row = [p[j] * u - x * v for u, v in zip(row, p)] + g = math.gcd(*row) + if g: + row = [v // g for v in row] + j = next((j for j, v in enumerate(row) if v), None) + if j is not None: + pivots[j] = row + selected.append(i) + return selected + + +def determinant(a): + """Bareiss determinant of a square integer witness.""" + n = len(a) + require(n > 0 and all(len(r) == n for r in a), 'minor must be square') + a, sign, prev = [list(r) for r in a], 1, 1 + for k in range(n - 1): + p = next((i for i in range(k, n) if a[i][k]), None) + if p is None: + return 0 + if p != k: + a[k], a[p] = a[p], a[k] + sign = -sign + pivot = a[k][k] + for i in range(k + 1, n): + for j in range(k + 1, n): + v = a[i][j] * pivot - a[i][k] * a[k][j] + require(v % prev == 0, 'nonexact Bareiss division') + a[i][j] = v // prev + a[i][k] = 0 + prev = pivot + return sign * a[-1][-1] + + +def kernel_vector(matrix, n): + """Rational representation for the row-restriction failure control.""" + a = [list(map(Q, r)) for r in matrix] + used, k = [], 0 + for j in range(n): + p = next((i for i in range(k, len(a)) if a[i][j]), None) + if p is None: + continue + a[k], a[p] = a[p], a[k] + c = a[k][j] + a[k] = [v / c for v in a[k]] + for i in range(len(a)): + if i != k and a[i][j]: + c = a[i][j] + a[i] = [u - c * v for u, v in zip(a[i], a[k])] + used.append(j) + k += 1 + free = next((j for j in range(n) if j not in used), None) + if free is None: + return None + v = [Q(0)] * n + v[free] = 1 + for i, j in enumerate(used): + v[j] = -a[i][free] + return v + + +def rank_witness(m, lower, end, r, frame): + z = [r] + [q for q in sorted(lower) if q != r and not target(q) and lower[q] <= frame] + o = [c for c in sorted(m) if c != r and not end[r] <= end[c]] + matrix = [[m[c].get(q, Q(0)) for q in z] for c in o] + ints, scales = integer_rows(matrix) + chosen = pivot_rows(ints) + require(len(chosen) == len(z), f'departure matrix not full rank for {r}') + minor = [ints[i] for i in chosen] + det = determinant(minor) + require(det != 0, 'zero witness determinant') + weak = [row for c, row in zip(o, matrix) if frame <= end[c]] + null = kernel_vector(weak, len(z)) + require(null is not None, 'row restriction unexpectedly retains full rank') + require(all(sum(x * y for x, y in zip(row, null)) == 0 for row in weak), 'false kernel witness') + require(any(sum(x * y for x, y in zip(row, null)) != 0 for row in matrix), 'full rows fail to detect weak-kernel vector') + return {'register': r, 'frame': basis(frame), 'columns': z, + 'selected_receivers': [o[i] for i in chosen], + 'row_denominator_scales': [scales[i] for i in chosen], + 'integer_minor': minor, 'integer_determinant': det, + 'rational_determinant': str(Q(det, math.prod(scales[i] for i in chosen))), + 'restricted_receivers': [c for c in o if frame <= end[c]], + 'restricted_row_rank': len(pivot_rows(integer_rows(weak)[0])), + 'restricted_row_null_vector': list(map(str, null))} + + +def inspect_word(w): + require(w['report']['v'] == 112 and w['report']['h'] == 9, 'unexpected word interface') + end, m = ends(w), forced_coordinates(w) + lower, upper = entry_bounds(w, m, end) + witnesses, no_readers, domains = [], [], [] + for r in SPLIT_REGISTERS + SKIP_REGISTERS: + require(r not in m and end[r] == FULL, 'expected a non-restored full-ended register') + receivers = [c for c in m if c != r and m[c].get(r)] + require(receivers, 'missing receivers') + cap = end[r] + for c in receivers: + cap &= end[c] + ceiling = cap if r in SPLIT_REGISTERS else cap & upper[r] + candidates = all_subspaces(lower[r], ceiling) + if r in SPLIT_REGISTERS: + require(dim(lower[r]) == 5 and dim(cap) == 7, 'split geometry changed') + require(lower[r] == upper[r], 'split entry frame is not forced') + require(not any(q != r and not target(q) and lower[q] <= lower[r] <= end[q] + for q in lower), 'split register has an entry-frame reader') + candidates = [s for s in candidates if dim(s) == 6] + require(len(candidates) == 3, 'incomplete six-dimensional frame enumeration') + domains.append({'register': r, 'entry_lower': basis(lower[r]), + 'receiver_cap': basis(cap), 'entry_upper': basis(upper[r]), + 'candidate_frames': [basis(s) for s in candidates]}) + local = [] + for frame in candidates: + readers = [q for q in lower if q != r and not target(q) and lower[q] <= frame <= end[q]] + if not readers: + no_readers.append({'register': r, 'frame': basis(frame)}) + else: + local.append(rank_witness(m, lower, end, r, frame)) + require(len(local) == 1, f'expected one departure rank witness for {r}') + witnesses.extend(local) + require(len(no_readers) == 17, 'reader-free frame count changed') + require(len(lower) - 112 == 520 and len(m) == 91, 'word population changed') + return {'non_target_prefix_rows': len(lower) - 112, 'restored_coordinates_checked': len(m), + 'domains': domains, 'no_reader_cases': no_readers, 'departure_witnesses': witnesses} + + +def canonical(x): + return json.dumps(x, indent=2, sort_keys=True) + '\n' + + +def decode_word(raw, digest): + require(hashlib.sha256(raw).hexdigest() == digest, 'source digest mismatch') + return json.loads(gzip.decompress(raw)) + + +def run(): + manifest = json.loads((HERE / 'SOURCES.json').read_bytes()) + sources = [s for s in manifest['files'] if s['usage'] == 'input'] + require(len(sources) == 2, 'expected the two pinned provider inputs') + reports = {} + for s, variant in zip(sources, ('base', 'extra')): + raw = (ROOT / s['path']).read_bytes() + reports[variant] = inspect_word(decode_word(raw, s['sha256'])) + require(reports['base'] == reports['extra'], 'provider geometry or obstruction differs') + return {'status': 'PASS_RANK7_DEPARTURE_MINOR_AUDIT', 'providers': 2, + 'source_pr': 3114, 'source_head': 'c88769c350977d9ed4f90fe5c652d582cfe2782a', + 'scope': 'Ten departure rank obstructions, not the complete restore-optimality theorem or supplier admission.', + 'result': reports['base']} + + +def main(): + p = argparse.ArgumentParser(description=__doc__) + p.add_argument('--write', action='store_true', help='write the deterministic receipt after all checks') + args = p.parse_args() + result = run() + raw = canonical(result).encode() + if args.write: + (HERE / 'RESULT.json').write_bytes(raw) + else: + require((HERE / 'RESULT.json').read_bytes() == raw, 'stored receipt differs from recomputation') + print(result['status'] + ' providers=2 rank_witnesses=20 no_reader_cases=34 restored_coordinates=182') + + +if __name__ == '__main__': + main()