diff --git a/research/qq16-l2-minimal-retention/PREDECESSORS.json b/research/qq16-l2-minimal-retention/PREDECESSORS.json new file mode 100644 index 0000000000..9eebdd32c1 --- /dev/null +++ b/research/qq16-l2-minimal-retention/PREDECESSORS.json @@ -0,0 +1,71 @@ +[ + { + "pr": 2470, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2470", + "head": "1b2eee3bf1ec67e68c0b0fa7f47c7b2a66febe56", + "usage": "consulted predecessor provenance, not runtime code", + "files": [ + { + "path": "research/qq16-cut-retention-census/README.md", + "git_blob": "83d2b42eed128a7a9e2151e47990ac8966b6d4f9", + "sha256": "796636d4d9824bc4959b00d9d2cbbfafec07c14e6845a1e238fb668a2f3d8adf" + }, + { + "path": "research/qq16-cut-retention-census/verify.py", + "git_blob": "1a699e2608dd8e884e6a4ff924f2b78eb8564126", + "sha256": "fd3b95f9dd2373d57b07328a2c98fe53e45810f4bbe85acf34bdbabe6686278e" + }, + { + "path": "research/qq16-cut-retention-census/SOURCES.json", + "git_blob": "49ba699e4fa38c1e15843217864e2af84a3dcd30", + "sha256": "42fd562335168f41becda254431b3230bfc134e16d84b19473af1448b2fef1ed" + } + ] + }, + { + "pr": 2443, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2443", + "head": "545c05e17243c962b112b91e7f84b4c1a41de7b8", + "usage": "consulted predecessor provenance, not runtime code", + "files": [ + { + "path": "research/qq16-coordinate-cut-decoder/README.md", + "git_blob": "1ae3d3eb976ed85f795da2c211b58577ed7e8a82", + "sha256": "91d68f5d01d89ee78802ee5f76e8b901199a686aaa62341090eb70c458fd070e" + }, + { + "path": "research/qq16-coordinate-cut-decoder/verify.py", + "git_blob": "e4bcea403a0db78115eba60ab8ec78294cea0c5c", + "sha256": "7decbde0922eb8b1473e1cf4ad0b65eee69f040c40ad0bea3b415e82bd129dc7" + }, + { + "path": "research/qq16-coordinate-cut-decoder/SOURCES.json", + "git_blob": "69b9533b9dbefe9639a7150be1c93d9001d75944", + "sha256": "54a00dadab40a5a39100a1b16f2e86c7b4bea33d9d1fcbb4f62897ae83b5f0d8" + } + ] + }, + { + "pr": 2456, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2456", + "head": "665ba8d7bffab92a434413096e9d5c0df7db40bd", + "usage": "consulted predecessor provenance, not runtime code", + "files": [ + { + "path": "research/qq16-cut-operator-audit/README.md", + "git_blob": "de6288549cbfd5c1c00fafc0b9b7ba131d7c354e", + "sha256": "6bff81589ff5d58bbeecd7798dce3ba4cf03b803caefccf543ac996e7c9605de" + }, + { + "path": "research/qq16-cut-operator-audit/verify.py", + "git_blob": "ddd2dbec0806e5a73b7f8fcb1986d7322a98436f", + "sha256": "4cd6d4e82662eb80bc6a161a81813947895534d085c3ab715177634d3230dc8f" + }, + { + "path": "research/qq16-cut-operator-audit/SOURCES.json", + "git_blob": "e9d7facc0bdf93834baed0e4fc10575829aa2197", + "sha256": "f3e0e580d358ddec7209fb4cee55a6a5880f397a7058ceba2bdfe562ae31bc78" + } + ] + } +] diff --git a/research/qq16-l2-minimal-retention/README.md b/research/qq16-l2-minimal-retention/README.md new file mode 100644 index 0000000000..369c7f7a79 --- /dev/null +++ b/research/qq16-l2-minimal-retention/README.md @@ -0,0 +1,208 @@ +# QQ16 L2 recovery with exactly 24 retained arrays + +**Scoped information lemma; no supplier or new kappa.** Given the fixed live +post-B1 observations `X2_U, Y2_U, Y2_A`, exactly **24** rational-linear retained +complete arrays are necessary and sufficient to recover all 224 arbitrary +pair-0 input arrays. Retain `x1_A, x1_T, y1_T` after F0. The eight `y1_A` arrays +in PR2470's 32-array L2 lead are reconstructible from its already granted future +logger output. This removes eight retained arrays in that information contract; +it does not establish a physical storage, recursive-work or native-cost saving. + +A separate specialist derived the inverse and kernel and wrote an independent +noncommuting-matrix check; see [REVIEW.md](REVIEW.md). + +## Exact contract and predecessor delta + +Let `(x1,y1)=F0(x,y)` and `(x2,y2)=B_1_2(x1,y1)`, with **no intervening event**. +Use the pinned disjoint sets + +``` +A = [0,7,20,27,36,46,57,111] +T = [21,37,47,76,81,87,92,110] +U = {0,...,111} minus (A union T), |U|=96. +``` + +All arrays lie in the same space `W=Q^n`, for any finite `n>=1`. Owner, payload, +tensor and spectator coordinates belong to the complete array. Every initial +X/Y array is arbitrary. Each retained record is a fixed rational-linear map to +one copy of W and may mix coordinates or ports. No nonlinear encoding, enlarged +array, extra read or adaptive nonlinear observation is granted. The lower bound +even permits a nonlinear decoder of these linear records. Other bank pairs are +arbitrary but neither read nor decoded; they do not participate in these events. + +| Observation | Cut | Complete arrays | +|---|---|---:| +| `r=x1_A`, `t=x1_T`, `h=y1_T` | retained after F0 | 24 | +| `C=x2_U`, `V=y2_U`, `Z=y2_A` | live immediately after B1 | 200 | +| Total independent records | two cuts | 224 | + +PR2470's L2 lead grants the same 200 live arrays and retains 32 F0 arrays. +We remove its `y1_A` block. PR2443 instead grants 88 ordinary F0 reads and +104 B1 arrays; its contract expressly excludes `y2_U`. Our 96 `y2_U` arrays +change that contract, so its 88-read threshold and any native-cost comparison +do not transfer. Without Z, only 192 live arrays remain and the same dimension +argument would require at least 32 retained arrays. + +Exact consulted file hashes and heads are in [PREDECESSORS.json](PREDECESSORS.json): + +- [PR2470](https://github.com/CrocSwap/integer-mult-bounds/pull/2470), + `1b2eee3bf1ec67e68c0b0fa7f47c7b2a66febe56`: Sagar Thakrar's retention census, + L2 reconstruction and 32-array sufficient record; these results retain credit. +- [PR2443](https://github.com/CrocSwap/integer-mult-bounds/pull/2443), + `545c05e17243c962b112b91e7f84b4c1a41de7b8`: starship-s's ordered cut decoder + and arbitrary-input F0 inverse. +- [PR2456](https://github.com/CrocSwap/integer-mult-bounds/pull/2456), + `665ba8d7bffab92a434413096e9d5c0df7db40bd`: ywz65's operator audit and + chart-fault warning. Its affine-operator implementation is not imported. +- Ali Romman's [PR1969 conserved contract](../joint-query/evidence/CONSERVED-QQ16.md) + supplies the inherited F/B maps, retained unchanged on the pinned base. + +## Ordered sufficiency proof + +Let `B_(s,U)=R_U D_(s,U)`, `ell_(s,V)=R_V D_(s,V)` for V=A,T, +`P_(s,V)=D_(s,V)^(-1) R_V^(-1)`, and `K_(s,U)=D_(s,U)^(-1)R_U^T/4`. +The selected Grams are `R_A R_A^T=R_T R_T^T=4I`. Each D is an invertible +port-diagonal operator; `D_0=I`. Products act from right to left. Positive-stage +charts need not commute. D denotes the logical owner route, not the physical +alignment A with its payload translation; the bridge is inherited from the +pinned [cover-action note](../joint-query/evidence/QQ16-COVER-ACTION-ADDENDUM.md). + +The relevant backward rows are + +``` +a = ell_(1,T) x1_T +C = x1_U - y1_U +V = y1_U + K_(1,U) a +Z = y1_A + P_(2,A)(B_(2,U) y1_U + ell_(2,T) y1_T). +``` + +Recover the entire post-F0 state in order: + +``` +a = ell_(1,T) t +y1_U = V - K_(1,U) a +x1_U = C + y1_U +y1_A = Z - P_(2,A)(B_(2,U) y1_U + ell_(2,T) h) +x1_A = r; x1_T = t; y1_T = h. +``` + +The logger correction has no y1_A input, so there is no circular dependence. +The mixed product `P_(2,A) B_(2,U) K_(1,U) ell_(1,T)` retains this order. +No 88-coordinate F0 read or unread-minor inverse is needed for this changed map. +Apply the credited F0 inverse: + +``` +f = ell_(0,T) x1_T +c = ell_(0,A) x1_A +x_U = x1_U + K_(0,U) f +x_T = P_(0,T) c +x_A = P_(0,A)(f - B_(0,U) x_U - c) +y_U = y1_U - x1_U +y_p = x1_p + y1_p - x_p, p in A union T. +``` + +Substitution proves both inverse orders for F0 and for the observation map. +This is an all-finite-dimension written operator proof under the stated local +contract, distinct from executable finite verification or a formal-kernel proof. + +## Sharp lower bound + +A record of 200 live arrays and q retained arrays is a linear map +`W^224 -> W^(200+q)`. Recovery of every input forces this map to be injective, +even if the decoder is nonlinear. Thus `(200+q)n>=224n`, so `q>=24`. +The construction attains equality. This permits arbitrary fixed rational-linear +compression, not just selection of coordinates. + +The live observation H has an explicit kernel. Choose arbitrary `r,t,h in W^8` +and set + +``` +x1_A=r, x1_T=t, y1_T=h +x1_U=y1_U=-K_(1,U)ell_(1,T)t +y1_A=-P_(2,A)(B_(2,U)y1_U + ell_(2,T)h). +``` + +These are exactly all states with C=V=Z=0, so `ker H` is isomorphic to `W^24` +and `rank H=200n`. F0 is invertible, transferring this kernel dimension to the +original inputs. No conclusion for infinite array spaces, nonlinear encodings +or a different live-read set is intended. + +## Reproduction and coverage + +From a full checkout, with standard-library Python: + +```sh +python3.12 -I -B scripts/research_package.py --package research/qq16-l2-minimal-retention +python3 -I -B research/qq16-l2-minimal-retention/verify.py +python3 -I -B research/qq16-l2-minimal-retention/independent_check.py +``` + +The primary verifier consumes pinned R/K and checks selected Grams, the first +two chronological events, and both inverse orders of 224 registered owner-route +pairs, including their native translation inverse equations. This binds packet +registrations; it does not freshly derive phase geometry, reconstruct R from the +scalar prefix, execute native words, or audit their full cost/precision invoice. + +Every input array is independent, and a second pass uses 224 independently +specified observation arrays. Six complete identities are checked in the rational +free-group ring on 224 chart/port symbols, allowing only adjacent inverse +cancellation. Zero formal residual specializes to zero for every invertible +choice of the maps. This stronger symbolic model applies to the pinned logical +maps, but the executable is not a proof assistant. + +[RESULT.json](RESULT.json) is the complete deterministic receipt. It records +32 semantic fault residuals: 24 individual retained-coordinate omissions plus +eight driver, sign, logger, chart, missing-read or wrong-cut mutations. They are +free-operator controls; a nonzero formal residual need not survive every concrete +specialization. The chart substitution becomes invisible when every D is set to +identity. No source-specific native counterexample is claimed. Reordered terms +and equivalent rational splitting are accepted. Missing or changed receipts fail; +explicit generation (`--write-result`) refuses to overwrite an existing receipt. + +The independent checker uses the same R but separately constructed noncommuting +2x2 rational maps. It covers 448 independent input coordinates and 448 independent +observation coordinates, both inverse orders and five faults. Those finite +fixtures supplement the separate written proof, not an exhaustive chart census. +Behavioral tests exercise source/receipt integrity and ineffective-control +rejection. The registered Python 3.12 replay passes all four declared commands; +REVIEW.md separately records the specialist's direct replays. Hosted CI is a +separate gate. + +## Open next questions and limits + +1. Can these 24 retained arrays and 200 live arrays be accessed and retired + legally at d1? Trace post-F0/B1 endpoint frames, especially the extra Y2_U + read, then price current-driver and future-logger reconstruction together + with output storage and literal cleanup. Native access and restoration are + the blockers, not information sufficiency. +2. Can the d1 record serve the full controller? Follow the next bridge and F2 + before proposing final-cut recovery. The remaining 17 events and their costs + have not been checked here. + +Concurrent work: ywz65's [12:12 UTC native L2 claim](https://github.com/CrocSwap/integer-mult-bounds/pull/2470#issuecomment-6191762591) +targets the native reconstruction of x1_U with restored sources and owned outputs. +It explicitly excludes this 24-array information minimum and full decoder. +That claim is an adjacent lead, not verified native evidence for this package. + +This decoder is an information map, not a reversible implementation restoring +separate record workspace from arbitrary dirt. Physical retention, native reads, +helper cleanup, ownership, rounding, precision, tape costs, global hosting and the +complete invoice remain open. A smaller record can cost more to reconstruct. +No selected cold replay, hosted CI pass, full multiplication theorem or improved +kappa is implied. + +## Provenance and credit + +Base `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority revision 4; +[SOURCES.json](SOURCES.json) pins inputs and historical guidance. The independent +verification card is explicitly changed from ledger reconstruction to this +retention implication; see [TASK.json](TASK.json). +[Canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/2424#discussioncomment-18948536). + +Credit Sagar Thakrar/PR2470, starship-s/PR2443, ywz65/PR2456, Ali Romman/PR1969, +Gareth Davidson/PR2432, commdata2338/PR2174 and the retained QQ16/supplier lineage, +including Rohan Arun, Jeremy Kothe and DreamingOfClouds. Existing sources and +notices are unchanged. New work is Apache-2.0, prepared by Ross Richardson with +substantial OpenAI Codex assistance for derivation, implementation and writing; +a separate Codex recursive-interface specialist performed the independent proof +and matrix check. No independent human or formal-kernel review is claimed. diff --git a/research/qq16-l2-minimal-retention/RESULT.json b/research/qq16-l2-minimal-retention/RESULT.json new file mode 100644 index 0000000000..e4ba9dbf31 --- /dev/null +++ b/research/qq16-l2-minimal-retention/RESULT.json @@ -0,0 +1,1815 @@ +{ + "algebra": "Q free-group ring on 224 invertible chart/port symbols; D0=I", + "chart_fault_invisible_at_identity_specialization": true, + "identities": [ + "F0^-1 F0=I", + "F0 F0^-1=I", + "decode observe=I", + "observe decode=I", + "full decoder full observation=I", + "full observation full decoder=I" + ], + "input_arrays": 224, + "live_arrays": 200, + "live_blocks": [ + "X2_U", + "Y2_U", + "Y2_A" + ], + "lower_bound": "For finite array dimension n>0, (200+q)n>=224n; hence q>=24", + "no_new_kappa": true, + "positive_controls": [ + "reordered terms/ports", + "rational splitting" + ], + "predecessor_L2_retained_arrays": 32, + "registered_route_pairs": [ + [ + 2, + 0, + "m89", + "m201" + ], + [ + 1, + 0, + "m1", + "m3" + ], + [ + 2, + 1, + "m90", + "m202" + ], + [ + 1, + 1, + "m313", + "m409" + ], + [ + 2, + 2, + "m91", + "m203" + ], + [ + 1, + 2, + "m314", + "m410" + ], + [ + 2, + 3, + "m92", + "m204" + ], + [ + 1, + 3, + "m315", + "m411" + ], + [ + 2, + 4, + "m93", + "m205" + ], + [ + 1, + 4, + "m316", + "m412" + ], + [ + 2, + 5, + "m94", + "m206" + ], + [ + 1, + 5, + "m317", + "m413" + ], + [ + 2, + 6, + "m95", + "m207" + ], + [ + 1, + 6, + "m318", + "m414" + ], + [ + 2, + 7, + "m96", + "m208" + ], + [ + 1, + 7, + "m15", + "m16" + ], + [ + 2, + 8, + "m97", + "m209" + ], + [ + 1, + 8, + "m319", + "m415" + ], + [ + 2, + 9, + "m98", + "m210" + ], + [ + 1, + 9, + "m320", + "m416" + ], + [ + 2, + 10, + "m99", + "m211" + ], + [ + 1, + 10, + "m321", + "m417" + ], + [ + 2, + 11, + "m100", + "m212" + ], + [ + 1, + 11, + "m322", + "m418" + ], + [ + 2, + 12, + "m101", + "m213" + ], + [ + 1, + 12, + "m323", + "m419" + ], + [ + 2, + 13, + "m102", + "m214" + ], + [ + 1, + 13, + "m324", + "m420" + ], + [ + 2, + 14, + "m103", + "m215" + ], + [ + 1, + 14, + "m325", + "m421" + ], + [ + 2, + 15, + "m104", + "m216" + ], + [ + 1, + 15, + "m326", + "m422" + ], + [ + 2, + 16, + "m105", + "m217" + ], + [ + 1, + 16, + "m327", + "m423" + ], + [ + 2, + 17, + "m106", + "m218" + ], + [ + 1, + 17, + "m328", + "m424" + ], + [ + 2, + 18, + "m107", + "m219" + ], + [ + 1, + 18, + "m329", + "m425" + ], + [ + 2, + 19, + "m108", + "m220" + ], + [ + 1, + 19, + "m330", + "m426" + ], + [ + 2, + 20, + "m109", + "m221" + ], + [ + 1, + 20, + "m25", + "m27" + ], + [ + 2, + 21, + "m110", + "m222" + ], + [ + 1, + 21, + "m26", + "m427" + ], + [ + 2, + 22, + "m111", + "m223" + ], + [ + 1, + 22, + "m331", + "m428" + ], + [ + 2, + 23, + "m112", + "m224" + ], + [ + 1, + 23, + "m332", + "m429" + ], + [ + 2, + 24, + "m113", + "m225" + ], + [ + 1, + 24, + "m333", + "m430" + ], + [ + 2, + 25, + "m114", + "m226" + ], + [ + 1, + 25, + "m334", + "m431" + ], + [ + 2, + 26, + "m115", + "m227" + ], + [ + 1, + 26, + "m335", + "m432" + ], + [ + 2, + 27, + "m116", + "m228" + ], + [ + 1, + 27, + "m39", + "m40" + ], + [ + 2, + 28, + "m117", + "m229" + ], + [ + 1, + 28, + "m336", + "m433" + ], + [ + 2, + 29, + "m118", + "m230" + ], + [ + 1, + 29, + "m337", + "m434" + ], + [ + 2, + 30, + "m119", + "m231" + ], + [ + 1, + 30, + "m338", + "m435" + ], + [ + 2, + 31, + "m120", + "m232" + ], + [ + 1, + 31, + "m339", + "m436" + ], + [ + 2, + 32, + "m121", + "m233" + ], + [ + 1, + 32, + "m340", + "m437" + ], + [ + 2, + 33, + "m122", + "m234" + ], + [ + 1, + 33, + "m341", + "m438" + ], + [ + 2, + 34, + "m123", + "m235" + ], + [ + 1, + 34, + "m342", + "m439" + ], + [ + 2, + 35, + "m124", + "m236" + ], + [ + 1, + 35, + "m343", + "m440" + ], + [ + 2, + 36, + "m125", + "m237" + ], + [ + 1, + 36, + "m49", + "m50" + ], + [ + 2, + 37, + "m126", + "m238" + ], + [ + 1, + 37, + "m29", + "m441" + ], + [ + 2, + 38, + "m127", + "m239" + ], + [ + 1, + 38, + "m344", + "m442" + ], + [ + 2, + 39, + "m128", + "m240" + ], + [ + 1, + 39, + "m345", + "m443" + ], + [ + 2, + 40, + "m129", + "m241" + ], + [ + 1, + 40, + "m346", + "m444" + ], + [ + 2, + 41, + "m130", + "m242" + ], + [ + 1, + 41, + "m347", + "m445" + ], + [ + 2, + 42, + "m131", + "m243" + ], + [ + 1, + 42, + "m348", + "m446" + ], + [ + 2, + 43, + "m132", + "m244" + ], + [ + 1, + 43, + "m349", + "m447" + ], + [ + 2, + 44, + "m133", + "m245" + ], + [ + 1, + 44, + "m350", + "m448" + ], + [ + 2, + 45, + "m134", + "m246" + ], + [ + 1, + 45, + "m351", + "m449" + ], + [ + 2, + 46, + "m135", + "m247" + ], + [ + 1, + 46, + "m59", + "m60" + ], + [ + 2, + 47, + "m136", + "m248" + ], + [ + 1, + 47, + "m31", + "m450" + ], + [ + 2, + 48, + "m137", + "m249" + ], + [ + 1, + 48, + "m352", + "m451" + ], + [ + 2, + 49, + "m138", + "m250" + ], + [ + 1, + 49, + "m353", + "m452" + ], + [ + 2, + 50, + "m139", + "m251" + ], + [ + 1, + 50, + "m354", + "m453" + ], + [ + 2, + 51, + "m140", + "m252" + ], + [ + 1, + 51, + "m355", + "m454" + ], + [ + 2, + 52, + "m141", + "m253" + ], + [ + 1, + 52, + "m356", + "m455" + ], + [ + 2, + 53, + "m142", + "m254" + ], + [ + 1, + 53, + "m357", + "m456" + ], + [ + 2, + 54, + "m143", + "m255" + ], + [ + 1, + 54, + "m358", + "m457" + ], + [ + 2, + 55, + "m144", + "m256" + ], + [ + 1, + 55, + "m359", + "m458" + ], + [ + 2, + 56, + "m145", + "m257" + ], + [ + 1, + 56, + "m360", + "m459" + ], + [ + 2, + 57, + "m146", + "m258" + ], + [ + 1, + 57, + "m69", + "m70" + ], + [ + 2, + 58, + "m147", + "m259" + ], + [ + 1, + 58, + "m361", + "m460" + ], + [ + 2, + 59, + "m148", + "m260" + ], + [ + 1, + 59, + "m362", + "m461" + ], + [ + 2, + 60, + "m149", + "m261" + ], + [ + 1, + 60, + "m363", + "m462" + ], + [ + 2, + 61, + "m150", + "m262" + ], + [ + 1, + 61, + "m364", + "m463" + ], + [ + 2, + 62, + "m151", + "m263" + ], + [ + 1, + 62, + "m365", + "m464" + ], + [ + 2, + 63, + "m152", + "m264" + ], + [ + 1, + 63, + "m366", + "m465" + ], + [ + 2, + 64, + "m153", + "m265" + ], + [ + 1, + 64, + "m367", + "m466" + ], + [ + 2, + 65, + "m154", + "m266" + ], + [ + 1, + 65, + "m368", + "m467" + ], + [ + 2, + 66, + "m155", + "m267" + ], + [ + 1, + 66, + "m369", + "m468" + ], + [ + 2, + 67, + "m156", + "m268" + ], + [ + 1, + 67, + "m370", + "m469" + ], + [ + 2, + 68, + "m157", + "m269" + ], + [ + 1, + 68, + "m371", + "m470" + ], + [ + 2, + 69, + "m158", + "m270" + ], + [ + 1, + 69, + "m372", + "m471" + ], + [ + 2, + 70, + "m159", + "m271" + ], + [ + 1, + 70, + "m373", + "m472" + ], + [ + 2, + 71, + "m160", + "m272" + ], + [ + 1, + 71, + "m374", + "m473" + ], + [ + 2, + 72, + "m161", + "m273" + ], + [ + 1, + 72, + "m375", + "m474" + ], + [ + 2, + 73, + "m162", + "m274" + ], + [ + 1, + 73, + "m376", + "m475" + ], + [ + 2, + 74, + "m163", + "m275" + ], + [ + 1, + 74, + "m377", + "m476" + ], + [ + 2, + 75, + "m164", + "m276" + ], + [ + 1, + 75, + "m378", + "m477" + ], + [ + 2, + 76, + "m165", + "m277" + ], + [ + 1, + 76, + "m2", + "m478" + ], + [ + 2, + 77, + "m166", + "m278" + ], + [ + 1, + 77, + "m379", + "m479" + ], + [ + 2, + 78, + "m167", + "m279" + ], + [ + 1, + 78, + "m380", + "m480" + ], + [ + 2, + 79, + "m168", + "m280" + ], + [ + 1, + 79, + "m381", + "m481" + ], + [ + 2, + 80, + "m169", + "m281" + ], + [ + 1, + 80, + "m382", + "m482" + ], + [ + 2, + 81, + "m170", + "m282" + ], + [ + 1, + 81, + "m5", + "m483" + ], + [ + 2, + 82, + "m171", + "m283" + ], + [ + 1, + 82, + "m383", + "m484" + ], + [ + 2, + 83, + "m172", + "m284" + ], + [ + 1, + 83, + "m384", + "m485" + ], + [ + 2, + 84, + "m173", + "m285" + ], + [ + 1, + 84, + "m385", + "m486" + ], + [ + 2, + 85, + "m174", + "m286" + ], + [ + 1, + 85, + "m386", + "m487" + ], + [ + 2, + 86, + "m175", + "m287" + ], + [ + 1, + 86, + "m387", + "m488" + ], + [ + 2, + 87, + "m176", + "m288" + ], + [ + 1, + 87, + "m7", + "m489" + ], + [ + 2, + 88, + "m177", + "m289" + ], + [ + 1, + 88, + "m388", + "m490" + ], + [ + 2, + 89, + "m178", + "m290" + ], + [ + 1, + 89, + "m389", + "m491" + ], + [ + 2, + 90, + "m179", + "m291" + ], + [ + 1, + 90, + "m390", + "m492" + ], + [ + 2, + 91, + "m180", + "m292" + ], + [ + 1, + 91, + "m391", + "m493" + ], + [ + 2, + 92, + "m181", + "m293" + ], + [ + 1, + 92, + "m9", + "m494" + ], + [ + 2, + 93, + "m182", + "m294" + ], + [ + 1, + 93, + "m392", + "m495" + ], + [ + 2, + 94, + "m183", + "m295" + ], + [ + 1, + 94, + "m393", + "m496" + ], + [ + 2, + 95, + "m184", + "m296" + ], + [ + 1, + 95, + "m394", + "m497" + ], + [ + 2, + 96, + "m185", + "m297" + ], + [ + 1, + 96, + "m395", + "m498" + ], + [ + 2, + 97, + "m186", + "m298" + ], + [ + 1, + 97, + "m396", + "m499" + ], + [ + 2, + 98, + "m187", + "m299" + ], + [ + 1, + 98, + "m397", + "m500" + ], + [ + 2, + 99, + "m188", + "m300" + ], + [ + 1, + 99, + "m398", + "m501" + ], + [ + 2, + 100, + "m189", + "m301" + ], + [ + 1, + 100, + "m399", + "m502" + ], + [ + 2, + 101, + "m190", + "m302" + ], + [ + 1, + 101, + "m400", + "m503" + ], + [ + 2, + 102, + "m191", + "m303" + ], + [ + 1, + 102, + "m401", + "m504" + ], + [ + 2, + 103, + "m192", + "m304" + ], + [ + 1, + 103, + "m402", + "m505" + ], + [ + 2, + 104, + "m193", + "m305" + ], + [ + 1, + 104, + "m403", + "m506" + ], + [ + 2, + 105, + "m194", + "m306" + ], + [ + 1, + 105, + "m404", + "m507" + ], + [ + 2, + 106, + "m195", + "m307" + ], + [ + 1, + 106, + "m405", + "m508" + ], + [ + 2, + 107, + "m196", + "m308" + ], + [ + 1, + 107, + "m406", + "m509" + ], + [ + 2, + 108, + "m197", + "m309" + ], + [ + 1, + 108, + "m407", + "m510" + ], + [ + 2, + 109, + "m198", + "m310" + ], + [ + 1, + 109, + "m408", + "m511" + ], + [ + 2, + 110, + "m199", + "m311" + ], + [ + 1, + 110, + "m33", + "m512" + ], + [ + 2, + 111, + "m200", + "m312" + ], + [ + 1, + 111, + "m79", + "m80" + ] + ], + "retained_arrays": 24, + "retained_blocks": [ + "x1_A", + "x1_T", + "y1_T" + ], + "retained_coordinate_omissions": [ + { + "block": 0, + "port": 0, + "witness": { + "block": 0, + "coefficient": "-1", + "input_array": 0, + "port": 0, + "row_terms": 1, + "word": [] + } + }, + { + "block": 0, + "port": 7, + "witness": { + "block": 0, + "coefficient": "-1", + "input_array": 7, + "port": 7, + "row_terms": 1, + "word": [] + } + }, + { + "block": 0, + "port": 20, + "witness": { + "block": 0, + "coefficient": "-1", + "input_array": 20, + "port": 20, + "row_terms": 1, + "word": [] + } + }, + { + "block": 0, + "port": 27, + "witness": { + "block": 0, + "coefficient": "-1", + "input_array": 27, + "port": 27, + "row_terms": 1, + "word": [] + } + }, + { + "block": 0, + "port": 36, + "witness": { + "block": 0, + "coefficient": "-1", + "input_array": 36, + "port": 36, + "row_terms": 1, + "word": [] + } + }, + { + "block": 0, + "port": 46, + "witness": { + "block": 0, + "coefficient": "-1", + "input_array": 46, + "port": 46, + "row_terms": 1, + "word": [] + } + }, + { + "block": 0, + "port": 57, + "witness": { + "block": 0, + "coefficient": "-1", + "input_array": 57, + "port": 57, + "row_terms": 1, + "word": [] + } + }, + { + "block": 0, + "port": 111, + "witness": { + "block": 0, + "coefficient": "-1", + "input_array": 111, + "port": 111, + "row_terms": 1, + "word": [] + } + }, + { + "block": 1, + "port": 21, + "witness": { + "block": 0, + "coefficient": "1/2", + "input_array": 21, + "port": 2, + "row_terms": 1, + "word": [ + -3, + 22 + ] + } + }, + { + "block": 1, + "port": 37, + "witness": { + "block": 0, + "coefficient": "-1/2", + "input_array": 37, + "port": 1, + "row_terms": 1, + "word": [ + -2, + 38 + ] + } + }, + { + "block": 1, + "port": 47, + "witness": { + "block": 0, + "coefficient": "-1/2", + "input_array": 47, + "port": 1, + "row_terms": 1, + "word": [ + -2, + 48 + ] + } + }, + { + "block": 1, + "port": 76, + "witness": { + "block": 0, + "coefficient": "1/2", + "input_array": 76, + "port": 1, + "row_terms": 1, + "word": [ + -2, + 77 + ] + } + }, + { + "block": 1, + "port": 81, + "witness": { + "block": 0, + "coefficient": "-1/2", + "input_array": 81, + "port": 1, + "row_terms": 1, + "word": [ + -2, + 82 + ] + } + }, + { + "block": 1, + "port": 87, + "witness": { + "block": 0, + "coefficient": "1/2", + "input_array": 87, + "port": 2, + "row_terms": 1, + "word": [ + -3, + 88 + ] + } + }, + { + "block": 1, + "port": 92, + "witness": { + "block": 0, + "coefficient": "-1/2", + "input_array": 92, + "port": 8, + "row_terms": 1, + "word": [ + -9, + 93 + ] + } + }, + { + "block": 1, + "port": 110, + "witness": { + "block": 0, + "coefficient": "-1/2", + "input_array": 110, + "port": 3, + "row_terms": 1, + "word": [ + -4, + 111 + ] + } + }, + { + "block": 2, + "port": 21, + "witness": { + "block": 1, + "coefficient": "1/2", + "input_array": 133, + "port": 20, + "row_terms": 1, + "word": [ + -133, + 134 + ] + } + }, + { + "block": 2, + "port": 37, + "witness": { + "block": 1, + "coefficient": "1/2", + "input_array": 149, + "port": 20, + "row_terms": 1, + "word": [ + -133, + 150 + ] + } + }, + { + "block": 2, + "port": 47, + "witness": { + "block": 1, + "coefficient": "-1/2", + "input_array": 159, + "port": 20, + "row_terms": 1, + "word": [ + -133, + 160 + ] + } + }, + { + "block": 2, + "port": 76, + "witness": { + "block": 1, + "coefficient": "1/2", + "input_array": 188, + "port": 0, + "row_terms": 1, + "word": [ + -113, + 189 + ] + } + }, + { + "block": 2, + "port": 81, + "witness": { + "block": 1, + "coefficient": "-1/2", + "input_array": 193, + "port": 0, + "row_terms": 1, + "word": [ + -113, + 194 + ] + } + }, + { + "block": 2, + "port": 87, + "witness": { + "block": 1, + "coefficient": "1/2", + "input_array": 199, + "port": 0, + "row_terms": 1, + "word": [ + -113, + 200 + ] + } + }, + { + "block": 2, + "port": 92, + "witness": { + "block": 1, + "coefficient": "1/2", + "input_array": 204, + "port": 0, + "row_terms": 1, + "word": [ + -113, + 205 + ] + } + }, + { + "block": 2, + "port": 110, + "witness": { + "block": 1, + "coefficient": "1/2", + "input_array": 222, + "port": 20, + "row_terms": 1, + "word": [ + -133, + 223 + ] + } + } + ], + "scope": "Information lemma at immediate post-B1; native reads, cost, cleanup and later cuts not admitted", + "semantic_faults": { + "discard_live_Y2_A": { + "block": 1, + "coefficient": "-1", + "input_array": 112, + "port": 0, + "row_terms": 53, + "word": [] + }, + "discard_live_Y2_U": { + "block": 0, + "coefficient": "1/2", + "input_array": 37, + "port": 1, + "row_terms": 5, + "word": [ + -2, + 38 + ] + }, + "future_chart_is_current_chart": { + "block": 1, + "coefficient": "1/2", + "input_array": 113, + "port": 0, + "row_terms": 104, + "word": [ + -113, + 114 + ] + }, + "omit_current_driver": { + "block": 0, + "coefficient": "-1/2", + "input_array": 37, + "port": 1, + "row_terms": 4, + "word": [ + -2, + 38 + ] + }, + "omit_future_T": { + "block": 1, + "coefficient": "1/2", + "input_array": 188, + "port": 0, + "row_terms": 4, + "word": [ + -113, + 189 + ] + }, + "use_pre_B1_Y_U": { + "block": 0, + "coefficient": "1/2", + "input_array": 37, + "port": 1, + "row_terms": 4, + "word": [ + -2, + 38 + ] + }, + "wrong_current_sign": { + "block": 0, + "coefficient": "-1", + "input_array": 37, + "port": 1, + "row_terms": 4, + "word": [ + -2, + 38 + ] + }, + "wrong_logger_sign": { + "block": 1, + "coefficient": "1", + "input_array": 113, + "port": 0, + "row_terms": 52, + "word": [ + -113, + 114 + ] + } + }, + "source_sha256": { + "research/community-frontier1042-audit/selected-replay.tar.gz": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "research/joint-query/certificate.json.gz": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7", + "research/joint-query/evidence/CONSERVED-QQ16.md": "60f0de3a7205ba5046b5ae7ffa8bf2b1ea42ea46b498face0a77966b59e7f3fb", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75", + "research/joint-query/evidence/QQ16-COVER-ACTION-ADDENDUM.md": "4bb4a68d8b4811b6d8364150612056bc124d38f1974d6f603dae68a99c4682fb" + }, + "status": "PASS_QQ16_L2_MINIMAL_RETENTION", + "template_member": { + "t16/global/base/split-centres/GLOBAL-TEMPLATE.json.gz": "a179dad87651aba340a5a8ddbcd86a8e757cad87b8a1f8bad48106fbecd38518" + } +} diff --git a/research/qq16-l2-minimal-retention/REVIEW.md b/research/qq16-l2-minimal-retention/REVIEW.md new file mode 100644 index 0000000000..15a034d904 --- /dev/null +++ b/research/qq16-l2-minimal-retention/REVIEW.md @@ -0,0 +1,355 @@ +# Independent mathematical review of the 24-array claim + +**Finding:** exactly 24 retained complete arrays are necessary and sufficient +under the stated rational-linear information contract. No mathematical defect +was found in the proposed recovery. This is an all-finite-dimension written +proof, supplemented below by an independent exact finite operator check. It is +not a formal-kernel proof or a native implementation/cost result. + +This review was prepared independently by the recursive-interfaces specialist +for this run, with substantial OpenAI Codex assistance. Only this review file +is owned by that specialist. The new package's implementation was not imported +or read to obtain the derivation or finite check below. The predecessor +definitions and displayed/source formulas were inspected. + +## Sources and precise contract + +The inspected predecessor heads are: + +- starship-s, [PR2443](https://github.com/CrocSwap/integer-mult-bounds/pull/2443), + `545c05e17243c962b112b91e7f84b4c1a41de7b8`: ordered F0 inverse and + the original two-cut decoder. +- thakrarsagar, [PR2470](https://github.com/CrocSwap/integer-mult-bounds/pull/2470), + `1b2eee3bf1ec67e68c0b0fa7f47c7b2a66febe56`: d1 L2 identity and its + sufficient 32-retained-array variant. +- ywz65, [PR2456](https://github.com/CrocSwap/integer-mult-bounds/pull/2456), + `665ba8d7bffab92a434413096e9d5c0df7db40bd`: exact operator audit of + PR2443 and the logical-D/physical-A chart distinction. + +These predecessor claims retain their own premises. In particular, PR2456's +operator result for its original observation contract does not automatically +certify this changed contract. + +Let a complete array belong to one common vector space `W = Q^n`, where +`1 <= n < infinity`. Coordinates include every owner and payload coordinate +of that array. All 224 input arrays `(x,y)` in `W^112 x W^112` are arbitrary +and independent. Let `A,T,U` be the pinned disjoint port sets of sizes +`8,8,96`. The consecutive events are exactly + +```text +(x1,y1) = F0(x,y), +(X2,Y2) = B_1_2(x1,y1). +``` + +At d1, immediately after the second event, the decoder is granted exactly +`C=X2_U`, `V=Y2_U`, and `Z=Y2_A`: 200 complete arrays. Additional information +consists of `r` retained arrays in `W`, each a rational-linear function of the +arbitrary inputs. No other reads, prior promises on the inputs, auxiliary +input-dependent records, or nonlinear encodings are admitted. Reading is +assumed to return the stated exact arrays; its implementation and restoration +are outside this contract. The decoder itself need not be linear for the +lower bound to apply. + +Other bank pairs do not enter these two local events. They may be arbitrary; +they are not recovered here. Allowing retained records to depend on them +does not defeat the bound: fixing those other inputs still leaves all +`224n` pair-zero input coordinates independent. + +## Ordered maps + +For chart `s`, let `D_(s,p)` be the admitted invertible logical map on `W` at +port `p`, and let `D_(s,L)` be their block diagonal direct sum. Write scalar +matrix actions with the identity on `W` understood: + +```text +ell_(s,L) = R_L D_(s,L), L=A,T, +B_s = R_U D_(s,U), +P_(s,L) = D_(s,L)^(-1) R_L^(-1), L=A,T, +K_(s,U) = D_(s,U)^(-1) R_U^T / 4. +``` + +The selected Grams `R_A R_A^T = R_T R_T^T = 4I` give two-sided inverses +`R_L^(-1)=R_L^T/4`; hence `ell_(s,L) P_(s,L)=I` and +`P_(s,L) ell_(s,L)=I`. Each section first applies the scalar inverse and +then each port's inverse cover map. No step below commutes a port-dependent +map through a scalar mixing matrix. Products act rightmost first. + +The relevant B1 equations are exactly: + +```text +a = ell_(1,T) x1_T, +C = x1_U - y1_U, +V = y1_U + K_(1,U) a, +Z = y1_A + P_(2,A) (B_2 y1_U + ell_(2,T) y1_T). +``` + +The last equation uses the future logger at chart 2, which changes only A, +and the fact that the B1 source A output is that logger's output. Replacing +chart 2 by chart 1, or replacing its logical maps by physical native +alignments without the required conjugation, is not justified. + +## Recovery with 24 retained arrays + +Retain `x1_A`, `x1_T`, and `y1_T`. Compute in this order: + +```text +a = ell_(1,T) x1_T, +y1_U = V - K_(1,U) a, +x1_U = C + y1_U, +y1_A = Z - P_(2,A) (B_2 y1_U + ell_(2,T) y1_T). +``` + +This reconstructs every post-F0 array. In the last line, form the two +chart-2 queries, add their eight output arrays, apply `R_A^(-1)`, then +apply the separate `D_(2,p)^(-1)`. The old-A baseline is the unknown being +recovered; it is not an extra retained input. No unread ordinary minor or +88-array record is needed. + +For completeness, the inherited F0 inverse is: + +```text +f = ell_(0,T) x1_T, +t = P_(0,T) ell_(0,A) x1_A, +x_U = x1_U + K_(0,U) f, +x_T = t, +x_A = P_(0,A) (f - B_0 x_U - ell_(0,T) t), +y_U = -C, +y_L = x1_L + y1_L - x_L, L=A,T. +``` + +Indeed F0 sends `x1_T=P_(0,T) R_0 x`, +`x1_A=P_(0,A) ell_(0,T)x_T`, and +`x1_U=x_U-K_(0,U)R_0x`; its ordinary Y equation is +`y1_U=y_U+x1_U`, and it preserves the selected pair sums. The displayed +inverse follows from the two-sided selected inverse identities. Conversely, +for arbitrary `x1,y1`, it produces an input whose F0 image is exactly that +state: its centre query is `f`, its two selected X outputs are the prescribed +ones, and the Y formulas invert the ordinary addition and selected sums. +Thus F0 is an isomorphism under this contract, without needing a separate +assumption about all of B1's unobserved outputs. + +All equations are exact over `Q`. No zero initial Y assumption, owner-constant +restriction, payload-constant restriction, commutativity of cover maps, or +bounded precision assumption enters this argument. + +## Lower bound and exact kernel + +Let `H:W^224 -> W^200` be the granted-observation map from original inputs, +and let `L:W^224 -> W^r` be any permitted retained record. Successful recovery +of every input requires `(H,L)` to be injective, irrespective of the +decoder's subsequent operations. Its target has dimension `(200+r)n`, +whereas its source has dimension `224n`. Therefore + +```text +224n <= (200+r)n, so r >= 24. +``` + +There is also an explicit exact description of the information lost by `H`. +Work in post-F0 coordinates, which is legitimate because F0 is invertible. +Choose arbitrary blocks `r_A,t_T,h_T` in `W^8`, and set + +```text +x1_A = r_A, +x1_T = t_T, +y1_T = h_T, +a = ell_(1,T) t_T, +y1_U = -K_(1,U) a, +x1_U = y1_U, +y1_A = -P_(2,A) (B_2 y1_U + ell_(2,T) h_T). +``` + +Then `C=V=Z=0`. Conversely, those three zero-observation equations force +exactly this form, leaving precisely the three displayed selected blocks +free. Consequently `ker H` is isomorphic to `W^24`, and `rank H=200n`. +The proposed record is a coordinate system on this kernel. This establishes +the exact floor rather than only an upper bound from counting observations. + +For a concrete dropped-block obstruction, set two of `r_A,t_T,h_T` to zero +and take the third nonzero in the preceding construction. The observations +remain zero and the other two retained blocks remain zero, but the input +is nonzero by F0 invertibility. Thus simply discarding any of the three +eight-array retained blocks fails. The dimension proof additionally excludes +every other rational-linear record with fewer than 24 complete arrays. + +The restriction to a common, positive, finite dimension matters. The count +does not establish a claim for infinite-dimensional array spaces, variable +record capacities, nonlinear encodings, extra reads, or a decoder asked to +recover only a quotient of the inputs. + +## Independent finite operator check + +An independent standard-library Python calculation was first run in memory, +then preserved as [independent_check.py](independent_check.py). Reproduce it +from the repository root with: + +```sh +python3 -I -B research/qq16-l2-minimal-retention/independent_check.py +python3 -O -I -B research/qq16-l2-minimal-retention/independent_check.py +``` + +It reads only the packet to obtain R and the partition; it imports no +predecessor executable or new-package implementation. The +packet SHA-256 was checked as +`a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7`. +The selected Grams were recomputed exactly. + +The fixture used `W=Q^2`, stage-0 identity maps, and these invertible, +port-dependent maps for `s=1,2`: + +```text +t = 1 + ((p + 2s) mod 3), u = (-1)^(p+s), +D_(s,p) = [[1,t],[u,1+ut]], +D_(s,p)^(-1) = [[1+ut,-t],[-u,1]]. +``` + +Each output coordinate was stored as a sparse exact `Fraction` linear form +in all 448 independent input coordinates. The F0 formulas and four B1 +observation equations above were implemented separately from the recovery +formulas. Complete coefficient comparison proved both compositions were +the identity: original inputs to observations/retention to original inputs, +and independently arbitrary observations/retention through the reverse +composition. Hence this finite check covers every rational input in this +two-coordinate fixture, rather than a finite sample of input values. + +Five incorrect decoders were rejected. Witnesses below encode +`(output side, output port, output coordinate; input scalar index; residual)`; +side 0 is X, side 1 is Y, and input scalar index is +`2*(112*side+port)+coordinate`. Set that one input scalar to 1 and every +other input scalar to 0 to obtain the stated residual. + +| Fault | Exact nonzero residual witness | +| --- | --- | +| Omit the `K_(1,U)a` correction | `(0,0,0; 0; -10)` | +| Reverse C's sign when recovering `x1_U` | `(0,0,0; 226; -1)` | +| Omit the future-T logger term | `(1,0,0; 0; -3)` | +| Add the logger instead of subtracting it | `(1,0,0; 0; -76)` | +| Apply port inverses before the scalar A inverse | `(1,0,0; 0; -32)` | + +The last mutation replaced `D_(2,A)^(-1)R_A^(-1)` by +`R_A^(-1)D_(2,A)^(-1)` in recovering `y1_A`. The tested order matters even +though all individual scalar coefficients commute with maps on `W`: +different ports carry different maps. + +The calculation returned `PASS_INDEPENDENT_TWO_COORDINATE_REVIEW`, with +448 formal input coordinates, 448 formal observation/retention coordinates, +two inverse identities, and all five faults detected, in both normal and +optimized Python modes. Explicit failure checks remain active under `-O`. +The fixture maps are +synthetic rational operators, not the actual 73-dimensional owner routes. +It is an algebraic stress check, not a second source-specific route-binding +audit. Its finite result supplements, and does not replace, the written +all-finite-dimension proof above. + +## Relation to predecessors and remaining obligations + +PR2470's L2 variant supplies `x1_U` using the same 200 granted live arrays +and 32 retained selected arrays. Once `y1_U` is reconstructed, the future-A +logger also reconstructs `y1_A`; those eight retained arrays are redundant. +Thus the change is from sufficient retention 32 to optimal retention 24 for +that enlarged d1 read set. PR2470 did not claim 32 was minimal. Its 120-array +floor for PR2443's smaller 104-live-array read set is a different, unchanged +statement. + +PR2443 supplies the F0 inverse and the logger relation. PR2456 supplies an +important source-specific caution: logical D and physical A have different +payload semantics. The present written proof permits arbitrary invertible +logical D but does not certify a physical routine that inserts native A in +only some of those positions. The run's primary checker owns its packet +registration and complete-coefficient checks. It was subsequently inspected +and replayed as recorded below; that inspection did not enter the independent +derivation or the independently written matrix checker. + +No legal native read of `Y2_U` or `Y2_A`, retention method, restored scratch, +copy cost, chart-map cost, source access, precision growth, final endpoint +availability, post-d1 schedule behavior, four-bank recovery, or complete +supplier invoice is supplied by this information theorem. In particular, +the eight-array reduction cannot be converted into a new kappa or physical +cost saving without those obligations. The result is conditional on the +logical local contract, with no selected-frontier change. + +## Open next questions + +1. Can the 200 granted arrays be read at d1 by a permitted native interface + while restoring all source and private scratch? A first step is to bind + each `Y2_U` and `Y2_A` read to its actual endpoint frame and price its + literal inverse. This is a recursive/native-interface obligation. +2. What is the fully charged cost of retaining the 24 arrays and applying + the ordered decoder? The independent information floor does not price + controller work or permit borrowing caller-owned arrays. Supplier and + asymptotic specialists own the subsequent complete cost transfer. + +New review text is Apache-2.0. Predecessor attribution and licenses are +retained in the surrounding package's source manifest. + +## Final package-claim audit and direct replays + +After completing the independent derivation and matrix checker, the reviewer +inspected the completed README and primary verifier. No mathematical or scope +defect was found. The examined files had these SHA-256 values: + +| File | SHA-256 | +| --- | --- | +| `README.md` | `b9de74e9e888496c2dff77326b5c078aec348b76529ece1c1072a41a4e832b3b` | +| `verify.py` | `639bebcde1003e9cc8d923f455a67c917f32cf506eb05c5081bc9850b99fc8ea` | +| `RESULT.json` | `d334ebd141e27f46e5a71be85d8efefacffe37a727cac4c11ebd0cb9a6e171c6` | +| `independent_check.py` | `5b20175e4d5e604fd7c08b7f9f2495d73bad99e0d8df0b798dfa017111861303` | + +The finite-dimensional information lower bound is stated at its actual scope: +fixed rational-linear records of equal capacity, all arbitrary pair-zero +inputs, and precisely the 200 specified live arrays. The code implements the +same ordered inverse. In particular, its F0 inverse subtracts +`c=ell_(0,A)x1_A`, equal to `ell_(0,T)t` in the displayed proof. + +The primary checker works in a rational free-group ring with separate +invertible symbols for each positive-stage port/chart map. Its zero formal +residuals specialize to zero for every admitted invertible realization, +including the pinned logical owner maps. This gives stronger algebraic +coverage than a test of one chosen representation. Conversely, a nonzero +free-group residual need not remain nonzero at every concrete specialization. +The README correctly identifies the 32 faults as formal controls rather than +actual native input counterexamples. + +The source checks bind the authenticated packet's exact `F_contract` and +`B_contract` strings, R/K, selected Grams, first two events, and map +registrations with both inverse orders. They do not +independently reconstruct chart phase geometry or derive the logical F/B +semantics from native programs. The README states these inherited-contract +limits explicitly. The review does not promote these checks into a physical +read, restoration, finite-precision, full-schedule, or supplier-cost result. + +Direct replay outcomes from the repository root: + +- With Python **3.14.6**, + `python3 -I -B research/qq16-l2-minimal-retention/verify.py` returned + `PASS_QQ16_L2_MINIMAL_RETENTION retained=24 live=200 inputs=224 identities=6 faults=32 no_new_kappa`. + This direct replay used the preceding verifier version + `4e379b4f72ab7e90e3ace313b377d0db631cf97bbd199634ca7d5b70d5647780`; + the narrowly reviewed update below adds only source guards. +- With Python **3.12.12**, + `python3.12 -I -B research/qq16-l2-minimal-retention/independent_check.py` + returned `PASS_INDEPENDENT_TWO_COORDINATE_REVIEW`, with the same two + 448-coordinate inverse checks and the five residuals listed above. +- The independent checker also passed normal and `-O` execution with + Python **3.14.6**. + +The subsequent verifier update adds exact equality checks for the pinned +forward/backward contract strings. The reviewer parsed those two guards, +checked their constants against the authenticated packet, and removed just +those two syntax nodes in memory: the remaining bytes hash to the previously +reviewed verifier above. Thus the current reviewed hash in the table differs +only by these two explicit source checks. This audit returned +`PASS_EXACT_TWO_GUARD_DELTA_AND_PACKET_TEXT`; the unchanged mathematical +replay was not repeated by this reviewer. The guards bind contract metadata +and do not derive native semantics or the definition of the future logger. + +The final README update distinguishes the run owner's registered replay from +this specialist's direct replays. Its adjacent-work statement was checked +against ywz65's linked PR2470 comment, created at `2026-10-15T12:12:54Z`: +that claim targets native L2 reconstruction with restored borrowed sources +and 96 owned outputs, and expressly excludes minimizing the retained record +or claiming the complete ordered decoder. The README correctly treats it as +a complementary lead without verified native evidence for this package. + +This reviewer ran the direct checks above. The generic registered replay, +behavioral test suite, preservation, publication, and hosted CI are separate +run-owner gates. No formal proof assistant was used. diff --git a/research/qq16-l2-minimal-retention/SOURCES.json b/research/qq16-l2-minimal-retention/SOURCES.json new file mode 100644 index 0000000000..69b9533b9d --- /dev/null +++ b/research/qq16-l2-minimal-retention/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754" + }, + { + "path": "research/joint-query/certificate.json.gz", + "usage": "input", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + }, + { + "path": "research/joint-query/evidence/CONSERVED-QQ16.md", + "usage": "input", + "git_blob": "4639583c1be02c2fb60ed8a8072c9969ef1569ce", + "sha256": "60f0de3a7205ba5046b5ae7ffa8bf2b1ea42ea46b498face0a77966b59e7f3fb" + }, + { + "path": "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "usage": "input", + "git_blob": "a6805c58f23132f9420efebf90f5b7e863c2e179", + "sha256": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75" + }, + { + "path": "research/joint-query/evidence/QQ16-COVER-ACTION-ADDENDUM.md", + "usage": "input", + "git_blob": "3dd1a990d7b9d57cfb20cf8e8dd45548f043a944", + "sha256": "4bb4a68d8b4811b6d8364150612056bc124d38f1974d6f603dae68a99c4682fb" + } + ] +} diff --git a/research/qq16-l2-minimal-retention/TASK.json b/research/qq16-l2-minimal-retention/TASK.json new file mode 100644 index 0000000000..15bd52498f --- /dev/null +++ b/research/qq16-l2-minimal-retention/TASK.json @@ -0,0 +1,154 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "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" + ], + "methods": [ + "Reconstruct the rank ledger from original operations rather than trusting its aggregate.", + "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": "Record the selected certificate and complex_profile rather than taking a PR headline as input.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "List the existing independent checks for the exact selected or candidate sources. Pick a new changed input, missing binding or distinct failure mode; stop with a handoff if the proposed arithmetic check is already covered.", + "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." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure" + ] + }, + "scope_status": "changed", + "actual_scope": "Determine the minimum retained rational-linear complete arrays for arbitrary QQ16 pair-0 recovery from fixed live post-B1 X2_U,Y2_U,Y2_A, extending PR2470 L2.", + "scope_change_reason": "The assigned independent-verification track is refined to a fresh missing retention implication instead of another existing moment/ledger check. The 32-array L2 handoff is audited and reduced with an explicit ordered inverse and matching dimension bound.", + "bottleneck_link": "Storage and cut availability are open QQ16 controller costs. This exact information minimum removes eight redundant retained arrays but supplies no physical tariff or supplier.", + "budget_minutes": 60, + "stop_rule": "One bounded question: stop on a failed ordered identity, source/overlap contradiction, or inability to independently verify by the final quarter. No new research round.", + "outcome": "completed", + "evidence": "README.md written proof; RESULT.json six free-operator inverse identities, 32 semantic faults; REVIEW.md and independent_check.py separate proof and 448-coordinate check.", + "author": "Ross Richardson with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for derivation, code, tests and prose; separate math-recursive-interfaces specialist derived and checked the proof with an independent concrete matrix representation. No human or formal-kernel review.", + "open_questions": [ + { + "question": "Can the 24 retained and 200 live arrays be legally accessed and retired at d1?", + "why_it_matters": "An information minimum is not an executable low-cost controller.", + "first_step": "Trace the post-F0/B1 native endpoint types, especially Y2_U, and price the ordered driver/logger reconstruction with storage and literal cleanup.", + "blocked_by": "Native access permissions, output ownership, retention and restoration costs." + }, + { + "question": "Can the d1 record serve the complete 19-event controller?", + "why_it_matters": "The immediate cut may not be a usable global delivery point.", + "first_step": "Propagate its required computations and records through the next bridge and F2.", + "blocked_by": "The remaining 17 schedule events and complete invoice are not checked here." + } + ], + "selection_nonce": "88c21fc75072ed670f22e8435884005d", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2424#discussioncomment-18948536", + "upstream_freshness": { + "checked_at_utc": "2026-10-15T12:02:24.879605+00:00", + "canonical_url": "https://github.com/CrocSwap/integer-mult-bounds.git", + "repository": "/Users/ross/git/math/integer-mult-bounds", + "upstream_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "primary_head": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "guidance_sha256": { + "AGENTS.md": "5378ffbf3a119fcd0c23bcce20f34e5dd2fa792a00a0033e47667aeba72bbc37", + "autoresearch.md": "79d0c8be61d90dd6c46b6e7250e0c88713d29854128d8d1361b6343682dad1d8", + "CONTRIBUTING.md": "df5b5646602f42cb5da5844f04ac925182ddcd0f627b9de1c96a5095bb7a277a", + "docs/research/agent-task-catalog.json": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "certificates/selected-result.json": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + } + }, + "overlap": { + "status": "POSSIBLE_OVERLAP_NOT_A_NOVELTY_CERTIFICATE", + "searched_at": "2026-10-15T12:03:47.702086+00:00", + "terms": [ + "L2 variant", + "32 retained", + "compressed contract", + "qq16-cut-retention", + "d1 read" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-15T11:55:52.575694+00:00", + "complete_pagination": true, + "records": 673 + }, + "discussions": { + "fetched_at": "2026-10-15T11:58:48.481090+00:00", + "complete_pagination": true, + "records": 1192 + } + }, + "local_records": 1536, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "matches_total": 2 + }, + "submission_overlap": { + "status": "POSSIBLE_OVERLAP_NOT_A_NOVELTY_CERTIFICATE", + "searched_at": "2026-10-15T12:21:39.328775+00:00", + "terms": [ + "qq16", + "retention", + "L2 variant" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-15T12:18:35.372205+00:00", + "complete_pagination": true, + "records": 678 + }, + "discussions": { + "fetched_at": "2026-10-15T12:21:39.227968+00:00", + "complete_pagination": true, + "records": 1194 + } + }, + "local_records": 1536, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "matches_total": 136, + "scope_review": "Read exact PR2443/2456/2470 heads unchanged at submission. Adjacent ywz65 native-L2 claim (PR2470 issuecomment6191762591) explicitly excludes this 24-array information minimum. Prior symbolic PR2456 audits a different observation contract. No novelty certificate or all-diff coverage claimed." + }, + "submission_upstream_freshness": { + "checked_at_utc": "2026-10-15T12:18:25.191043+00:00", + "canonical_url": "https://github.com/CrocSwap/integer-mult-bounds.git", + "repository": "/Users/ross/git/math/integer-mult-bounds", + "upstream_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "primary_head": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "guidance_sha256": { + "AGENTS.md": "5378ffbf3a119fcd0c23bcce20f34e5dd2fa792a00a0033e47667aeba72bbc37", + "autoresearch.md": "79d0c8be61d90dd6c46b6e7250e0c88713d29854128d8d1361b6343682dad1d8", + "CONTRIBUTING.md": "df5b5646602f42cb5da5844f04ac925182ddcd0f627b9de1c96a5095bb7a277a", + "docs/research/agent-task-catalog.json": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "certificates/selected-result.json": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + } + }, + "concurrent_work": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2470#issuecomment-6191762591", + "scope": "Native L2 x1_U reconstruction with owned outputs and restored sources; claim only, complementary and unverified here." + } +} diff --git a/research/qq16-l2-minimal-retention/VERIFY.json b/research/qq16-l2-minimal-retention/VERIFY.json new file mode 100644 index 0000000000..dcea5705cd --- /dev/null +++ b/research/qq16-l2-minimal-retention/VERIFY.json @@ -0,0 +1,56 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1042-audit/selected-replay.tar.gz", + "research/joint-query/certificate.json.gz", + "research/joint-query/evidence/CONSERVED-QQ16.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "research/joint-query/evidence/QQ16-COVER-ACTION-ADDENDUM.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Six complete ordered inverse identities, 24 retained omissions, eight semantic faults and complete fixed receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same fixed receipt with optimization; proof checks do not use assert." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent_check.py" + ], + "timeout_seconds": 120, + "checks": "Independent synthetic noncommuting Q^2 maps, all 448 input and observation coordinates, five faults." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Five behavior groups including input/receipt integrity, ineffective control and noncommutative algebra." + } + ] +} diff --git a/research/qq16-l2-minimal-retention/independent_check.py b/research/qq16-l2-minimal-retention/independent_check.py new file mode 100644 index 0000000000..a5e967b10e --- /dev/null +++ b/research/qq16-l2-minimal-retention/independent_check.py @@ -0,0 +1,197 @@ +#!/usr/bin/env python3 +"""Independent exact Q^2 audit of the 24-array information contract. + +Only the pinned scalar packet is read. No production or predecessor checker +is imported. Chart maps here are synthetic noncommuting rational operators; +this is not an audit of the actual owner/payload route binding. + +Prepared by the run's recursive-interfaces specialist with substantial +OpenAI Codex assistance. Apache-2.0. +""" + +from fractions import Fraction as Q +import gzip +import hashlib +import json +from pathlib import Path + + +ROOT = Path(__file__).resolve().parents[2] +PACKET = ROOT / "research/joint-query/certificate.json.gz" +PACKET_SHA256 = "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +raw = PACKET.read_bytes() +need(hashlib.sha256(raw).hexdigest() == PACKET_SHA256, "packet digest") +packet = json.loads(gzip.decompress(raw)) +R = [[Q(row.get(str(p), 0)) for p in range(112)] for row in packet["R_rows"]] +A = tuple(packet["A_ports"]) +T = tuple(packet["T_ports"]) +U = tuple(packet["U_ports"]) +SELECTED = A + T +need(A == (0, 7, 20, 27, 36, 46, 57, 111), "A partition") +need(T == (21, 37, 47, 76, 81, 87, 92, 110), "T partition") +need(U == tuple(p for p in range(112) if p not in SELECTED), "U partition") +need(len(R) == 8, "eight scalar query coordinates") +need(all(sum(R[i][p] * R[j][p] for p in ports) == 4 * (i == j) + for ports in (A, T) for i in range(8) for j in range(8)), + "selected Grams") + + +def linear(*terms): + """Exact sparse scalar linear forms in independent input coordinates.""" + result = {} + for coefficient, value in terms: + for variable, weight in value.items(): + result[variable] = result.get(variable, Q(0)) + coefficient * weight + return {k: v for k, v in result.items() if v} + + +def array(*terms): + return tuple(linear(*[(c, v[i]) for c, v in terms]) for i in range(2)) + + +def matrix(stage, port): + if stage == 0: + return ((1, 0), (0, 1)) + t = 1 + (port + 2 * stage) % 3 + u = (-1) ** (port + stage) + return ((1, t), (u, 1 + u * t)) + + +def route(stage, port, value, inverse=False): + m = matrix(stage, port) + if inverse: + m = ((m[1][1], -m[0][1]), (-m[1][0], m[0][0])) + return tuple(linear(*[(m[i][j], value[j]) for j in range(2)]) + for i in range(2)) + + +def query(bank, stage, ports): + moved = {p: route(stage, p, bank[p]) for p in ports} + return tuple(array(*[(R[i][p], moved[p]) for p in ports if R[i][p]]) + for i in range(8)) + + +def section(values, stage, ports, wrong_order=False): + if wrong_order: + need(len(ports) == 8, "wrong-order control has eight selected ports") + moved = [route(stage, ports[i], values[i], True) for i in range(8)] + return {p: array(*[(R[i][p] / 4, moved[i]) + for i in range(8) if R[i][p]]) for p in ports} + return {p: route(stage, p, + array(*[(R[i][p] / 4, values[i]) + for i in range(8) if R[i][p]]), True) + for p in ports} + + +def forward(x, y): + f = query(x, 0, range(112)) + correction = section(f, 0, U) + xx = {p: array((1, x[p]), (-1, correction[p])) for p in U} + xx.update(section(query(x, 0, T), 0, A)) + xx.update(section(f, 0, T)) + yy = {p: array((1, y[p]), (1, xx[p])) for p in U} + yy.update({p: array((1, x[p]), (1, y[p]), (-1, xx[p])) for p in SELECTED}) + return xx, yy + + +def observe(x, y): + """Original inputs to the 200 observations and 24 retained arrays.""" + xx, yy = forward(x, y) + correction = section(query(xx, 1, T), 1, U) + logger = section(query(yy, 2, U + T), 2, A) + return ({p: array((1, xx[p]), (-1, yy[p])) for p in U}, + {p: array((1, yy[p]), (1, correction[p])) for p in U}, + {p: array((1, yy[p]), (1, logger[p])) for p in A}, + {p: xx[p] for p in SELECTED}, + {p: yy[p] for p in T}) + + +def recover(observations, fault=None): + C, Y, YA, sx, yt = observations + correction = section(query(sx, 1, T), 1, U) + yu = {p: array((1, Y[p]), (0 if fault == "omit_K" else -1, correction[p])) + for p in U} + xu = {p: array((-1 if fault == "C_sign" else 1, C[p]), (1, yu[p])) for p in U} + logger = query(yu, 2, U) + if fault != "omit_future_T": + logger = tuple(array((1, a), (1, b)) for a, b in zip(logger, query(yt, 2, T))) + logger = section(logger, 2, A, fault == "reverse_section_order") + ya = {p: array((1, YA[p]), (1 if fault == "logger_sign" else -1, logger[p])) + for p in A} + sy = {**ya, **yt} + f = query(sx, 0, T) + old_t = section(query(sx, 0, A), 0, T) + correction = section(f, 0, U) + x = {p: array((1, xu[p]), (1, correction[p])) for p in U} + x.update(old_t) + center = tuple(array((1, a), (-1, b), (-1, c)) + for a, b, c in zip(f, query(x, 0, U), query(old_t, 0, T))) + x.update(section(center, 0, A)) + y = {p: array((-1, C[p])) for p in U} + y.update({p: array((1, sx[p]), (1, sy[p]), (-1, x[p])) for p in SELECTED}) + return x, y + + +def variable(index): + return ({2 * index: Q(1)}, {2 * index + 1: Q(1)}) + + +def first_residual(actual, expected): + for side in range(2): + for port in range(112): + for coordinate in range(2): + residual = linear((1, actual[side][port][coordinate]), + (-1, expected[side][port][coordinate])) + if residual: + k = min(residual) + return [side, port, coordinate, k, str(residual[k])] + return None + + +def main(): + for stage in (0, 1, 2): + for port in range(112): + v = variable(0) + need(route(stage, port, route(stage, port, v), True) == v, + "two-coordinate route inverse") + need(route(stage, port, route(stage, port, v, True)) == v, + "two-coordinate inverse route") + x = {p: variable(p) for p in range(112)} + y = {p: variable(112 + p) for p in range(112)} + observations = observe(x, y) + need(recover(observations) == (x, y), "all 448 input coefficients recovered") + independent = [] + index = 0 + for ports in (U, U, A, SELECTED, T): + block = {} + for p in ports: + block[p] = variable(index) + index += 1 + independent.append(block) + need(index == 224, "224 independent observation and retention arrays") + need(observe(*recover(independent)) == tuple(independent), + "all 448 observation and retention coefficients recovered") + controls = {} + for fault in ("omit_K", "C_sign", "omit_future_T", "logger_sign", + "reverse_section_order"): + controls[fault] = first_residual(recover(observations, fault), (x, y)) + need(controls[fault] is not None, "undetected control: " + fault) + print(json.dumps({ + "status": "PASS_INDEPENDENT_TWO_COORDINATE_REVIEW", + "formal_input_coordinates": 448, + "formal_observation_coordinates": 448, + "identity_orders": 2, + "logical_maps": "synthetic port-dependent determinant-one rational maps; actual pinned R", + "negative_control_witnesses": controls, + }, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main() diff --git a/research/qq16-l2-minimal-retention/test_verify.py b/research/qq16-l2-minimal-retention/test_verify.py new file mode 100644 index 0000000000..7c5e07f812 --- /dev/null +++ b/research/qq16-l2-minimal-retention/test_verify.py @@ -0,0 +1,92 @@ +#!/usr/bin/env python3 +"""Failure-sensitive package behavior; mathematical controls live in verify.py.""" +import contextlib +import importlib.util +import io +import json +from pathlib import Path +import tempfile +import unittest +from unittest import mock + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location('retention_verify', HERE / 'verify.py') +v = importlib.util.module_from_spec(spec) +spec.loader.exec_module(v) + + +class Behavior(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.result = v.run() + cls.encoded = json.dumps(cls.result, sort_keys=True, indent=2) + '\n' + + def test_committed_full_receipt(self): + self.assertEqual((HERE / 'RESULT.json').read_text(), self.encoded) + self.assertEqual(len(self.result['semantic_faults']), 8) + self.assertEqual(len(self.result['retained_coordinate_omissions']), 24) + + def test_missing_changed_receipts_and_explicit_generation(self): + with tempfile.TemporaryDirectory(prefix='qq16-retention-') as temp: + target = Path(temp) / 'RESULT.json' + with mock.patch.object(v, 'HERE', Path(temp)), mock.patch.object(v, 'run', return_value=self.result), \ + contextlib.redirect_stdout(io.StringIO()): + with mock.patch('sys.argv', ['verify.py']): + with self.assertRaises(FileNotFoundError): + v.main() + self.assertFalse(target.exists()) + target.write_text(self.encoded.replace('"retained_arrays": 24', '"retained_arrays": 23')) + with self.assertRaisesRegex(ValueError, 'mismatching committed result'): + v.main() + target.write_text(self.encoded) + v.main() + self.assertEqual(target.read_text(), self.encoded) + with mock.patch('sys.argv', ['verify.py', '--write-result']): + with self.assertRaises(FileExistsError): + v.main() + target.unlink() + v.main() + self.assertEqual(target.read_text(), self.encoded) + + def test_each_input_hash_rejects_changed_bytes(self): + pins = json.loads((HERE / 'SOURCES.json').read_text())['files'] + original = Path.read_bytes + for pin in pins: + if pin['usage'] != 'input': + continue + path = v.ROOT / pin['path'] + def corrupted(p, selected=path): + raw = original(p) + return bytes([raw[0] ^ 1]) + raw[1:] if p == selected else raw + with self.subTest(path=pin['path']), mock.patch.object(Path, 'read_bytes', corrupted): + with self.assertRaisesRegex(ValueError, 'source hash:'): + v.source_bytes() + + def test_ineffective_mutation_is_a_failure(self): + inputs = v.pair() + with self.assertRaisesRegex(ValueError, 'ineffective semantic control'): + v.rejected(inputs, inputs, 'identity mutant') + changed = ({**inputs[0], 1: {}}, inputs[1]) + self.assertIsNotNone(v.rejected(inputs, changed, 'actual omission')) + + def test_ordered_word_algebra_on_noncommuting_maps(self): + def multiply(a, b): + return tuple(tuple(sum(a[i][k] * b[k][j] for k in range(2)) + for j in range(2)) for i in range(2)) + eye = ((1, 0), (0, 1)) + matrices = {1: ((1, 1), (0, 1)), -1: ((1, -1), (0, 1)), + 2: ((1, 0), (1, 1)), -2: ((1, 0), (-1, 1))} + def evaluate(word): + result = eye + for letter in word: + result = multiply(result, matrices[letter]) + return result + for word in ((1, 2, -2, -1), (1, 2, -1, -2), (2, -1, 1, 2, -2)): + self.assertEqual(evaluate(word), evaluate(v.word_reduce(word))) + self.assertNotEqual(evaluate((1, 2)), evaluate((2, 1))) + self.assertNotEqual(v.move(1, v.move(2, v.variable(0))), + v.move(2, v.move(1, v.variable(0)))) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/qq16-l2-minimal-retention/verify.py b/research/qq16-l2-minimal-retention/verify.py new file mode 100644 index 0000000000..fbc87626cb --- /dev/null +++ b/research/qq16-l2-minimal-retention/verify.py @@ -0,0 +1,313 @@ +#!/usr/bin/env python3 +"""Exact ordered QQ16 L2 retention identities. Apache-2.0. + +Ross Richardson with substantial OpenAI Codex assistance. +No predecessor executable is imported. The algebra is a rational free-group +ring: distinct port/chart maps need not commute or satisfy any extra relation. +Native reads, retention implementation and full supplier costs are not checked. +""" +import argparse +from fractions import Fraction as Q +import gzip +import hashlib +import io +import json +from pathlib import Path +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +A = (0, 7, 20, 27, 36, 46, 57, 111) +T = (21, 37, 47, 76, 81, 87, 92, 110) +U = tuple(p for p in range(112) if p not in A + T) +MEMBER = 't16/global/base/split-centres/GLOBAL-TEMPLATE.json.gz' +MEMBER_SHA = 'a179dad87651aba340a5a8ddbcd86a8e757cad87b8a1f8bad48106fbecd38518' +PACKET = 'research/joint-query/certificate.json.gz' +ARCHIVE = 'research/community-frontier1042-audit/selected-replay.tar.gz' + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def source_bytes(root=ROOT): + pins = json.loads((HERE / 'SOURCES.json').read_text()) + data = {} + for item in pins['files']: + if item['usage'] == 'input': + raw = (root / item['path']).read_bytes() + need(sha(raw) == item['sha256'], 'source hash: ' + item['path']) + data[item['path']] = raw + return data + + +def xor_apply(columns, vector): + result = 0 + while vector: + bit = vector & -vector + result ^= columns[bit.bit_length() - 1] + vector ^= bit + return result + + +def sources(data): + packet = json.loads(gzip.decompress(data[PACKET])) + need(packet['F_contract'] == 'f=R_s x. X_U=x_U-K_s,U f; X_A=P_s,A ell_s,T x; X_T=P_s,T f. Y_U=y_U+X_U; Y_A+X_A=y_A+x_A; Y_T+X_T=y_T+x_T.', + 'pinned conserved forward contract') + need(packet['B_contract'] == 'u=E_t y; a=ell_s,T x; b=R_s u. Y_A=u_A; Y_U=y_U+K_s,U a; Y_T=u_T-P_s,T(b+11a). X_U=x_U-y_U; X_A=x_A+y_A-u_A; X_T=P_s,T(b+12a).', + 'pinned conserved backward contract') + need(tuple(packet['A_ports']) == A and tuple(packet['T_ports']) == T + and tuple(packet['U_ports']) == U, 'actual port partition') + r = [[Q(row.get(str(p), 0)) for p in range(112)] for row in packet['R_rows']] + need(len(r) == 8, 'eight query coordinates') + need(all(Q(packet['K_rows'][p].get(str(i), 0)) == r[i][p] / 4 + for p in range(112) for i in range(8)), 'K=R transpose/4') + for ports, gram in ((A, 4), (T, 4), (U, 48)): + need(all(sum(r[i][p] * r[j][p] for p in ports) == (gram if i == j else 0) + for i in range(8) for j in range(8)), 'selected/ordinary Gram') + with tarfile.open(fileobj=io.BytesIO(data[ARCHIVE]), mode='r:gz') as ar: + members = [m for m in ar.getmembers() if m.name == MEMBER] + need(len(members) == 1 and members[0].isfile(), 'unique template member') + raw = ar.extractfile(members[0]).read() + need(sha(raw) == MEMBER_SHA, 'template hash') + template = json.loads(gzip.decompress(raw)) + need(template['recipe'][:2] == [ + {'kind': 'local', 'pair': 0, 'reverse': False, 'stage': 0}, + {'kind': 'local', 'pair': 0, 'reverse': True, 'stage': 1}], 'immediate F0/B1 cut') + # Bind 224 positive-stage logical symbols to the actual port-specific + # owner maps. Logical D uses the owner component, not native translation. + bindings = [] + unit = tuple(1 << i for i in range(73)) + program = packet['programs']['B_1_2'] + for p in range(112): + maps = [e[2] for e in program if e[0] == 'cover_map' and e[1] == ['L', 112 + p]] + need(len(maps) == 4, 'four Y alignments per port') + for stage, offset in ((2, 0), (1, 2)): + entry, back = [packet['map_registry'][maps[offset + i]] for i in (0, 1)] + g, h = [tuple(v['owner_right_matrix_columns']) for v in (entry, back)] + need(len(g) == len(h) == 73 and all(0 <= c < 2**73 for c in g + h), 'owner dimensions') + need(tuple(xor_apply(g, c) for c in h) == unit + and tuple(xor_apply(h, c) for c in g) == unit, 'both owner inverse orders') + a, b = [v['payload_translation_at_identity_owner'] for v in (entry, back)] + need(a ^ xor_apply(g, b) == 0 and b ^ xor_apply(h, a) == 0, 'native inverse translations') + bindings.append([stage, p, maps[offset], maps[offset + 1]]) + return r, bindings + + +def word_reduce(word): + stack = [] + for letter in word: + if stack and stack[-1] == -letter: + stack.pop() + else: + stack.append(letter) + return tuple(stack) + + +def add(*terms): + """A row maps (independent array id, ordered map word) to a rational.""" + out = {} + for factor, row in terms: + if factor: + for key, value in row.items(): + out[key] = out.get(key, Q(0)) + factor * value + return {k: v for k, v in out.items() if v} + + +def move(letter, row): + if letter == 0: + return dict(row) + out = {} + for (var, word), value in row.items(): + key = (var, word_reduce((letter,) + word)) + out[key] = out.get(key, Q(0)) + value + return {k: v for k, v in out.items() if v} + + +def variable(i): + return {(i, ()): Q(1)} + + +def pair(): + return ({p: variable(p) for p in range(112)}, + {p: variable(112 + p) for p in range(112)}) + + +def route(stage, port): + return 0 if stage == 0 else 1 + (stage - 1) * 112 + port + + +class Algebra: + def __init__(self, r): + self.r = r + + def query(self, rows, ports, stage=0): + routed = {p: move(route(stage, p), rows[p]) for p in ports} + return [add(*[(self.r[i][p], routed[p]) for p in ports]) for i in range(8)] + + def inject(self, q, ports, stage=0): + return {p: move(-route(stage, p), add(*[(self.r[i][p] / 4, q[i]) for i in range(8)])) + for p in ports} + + def forward(self, x, y): + f = self.query(x, range(112)) + kf = self.inject(f, U + T) + a = self.inject(self.query(x, T), A) + xx = {p: add((1, x[p]), (-1, kf[p])) for p in U} | a | {p: kf[p] for p in T} + yy = {p: add((1, y[p]), (1, xx[p])) for p in U} + yy |= {p: add((1, x[p]), (1, y[p]), (-1, xx[p])) for p in A + T} + return xx, yy + + def forward_inverse(self, xx, yy): + f = self.query(xx, T) + c = self.query(xx, A) + kf = self.inject(f, U) + x = {p: add((1, xx[p]), (1, kf[p])) for p in U} | self.inject(c, T) + b = self.query(x, U) + x |= self.inject([add((1, f[i]), (-1, b[i]), (-1, c[i])) for i in range(8)], A) + y = {p: add((1, yy[p]), (-1, xx[p])) for p in U} + y |= {p: add((1, xx[p]), (1, yy[p]), (-1, x[p])) for p in A + T} + return x, y + + def observe(self, x, y): + """Input is post-F0. Blocks: retained x_A,x_T,y_T; live C,V,Z.""" + k = self.inject(self.query(x, T, 1), U, 1) + e = self.inject(self.query(y, U + T, 2), A, 2) + return ({p: x[p] for p in A}, {p: x[p] for p in T}, {p: y[p] for p in T}, + {p: add((1, x[p]), (-1, y[p])) for p in U}, + {p: add((1, y[p]), (1, k[p])) for p in U}, + {p: add((1, y[p]), (1, e[p])) for p in A}) + + def decode(self, obs, fault=None): + xa, xt, yt, c, v, z = obs + k = self.inject(self.query(xt, T, 1), U, 1) + y = {p: add((1, v[p]), (0 if fault == 'omit_current_driver' else + 1 if fault == 'wrong_current_sign' else -1, k[p])) for p in U} + x = dict(xa) | dict(xt) | {p: add((1, c[p]), (1, y[p])) for p in U} + y |= dict(yt) + stage = 1 if fault == 'future_chart_is_current_chart' else 2 + q = self.query(y, U if fault == 'omit_future_T' else U + T, stage) + e = self.inject(q, A, stage) + y |= {p: add((1, z[p]), (1 if fault == 'wrong_logger_sign' else -1, e[p])) for p in A} + return x, y + + +def free_observations(): + blocks, count = [], 0 + for ports in (A, T, T, U, U, A): + blocks.append({p: variable(count + i) for i, p in enumerate(ports)}) + count += len(ports) + need(count == 224, '224 independent observations') + return tuple(blocks) + + +def residual(want, got): + for block, (a, b) in enumerate(zip(want, got)): + for p in sorted(a): + row = add((1, b[p]), (-1, a[p])) + if row: + (var, word), value = sorted(row.items())[0] + return {'block': block, 'port': p, 'input_array': var, + 'word': list(word), 'coefficient': str(value), 'row_terms': len(row)} + return None + + +def require_equal(want, got, label): + need(want == got, label + ': ' + str(residual(want, got))) + + +def rejected(want, got, label): + witness = residual(want, got) + need(witness is not None, 'ineffective semantic control: ' + label) + return witness + + +def scalar_projection(row): + """Positive specialization D=I; this alone would lose ordered coverage.""" + return add(*[(q, variable(i)) for (i, _), q in row.items()]) + + +def run(): + data = source_bytes() + r, bindings = sources(data) + model = Algebra(r) + inputs = pair() + after = model.forward(*inputs) + require_equal(inputs, model.forward_inverse(*after), 'F0 left inverse') + require_equal(inputs, model.forward(*model.forward_inverse(*inputs)), 'F0 right inverse') + observed = model.observe(*inputs) + require_equal(inputs, model.decode(observed), 'post-F0 left inverse') + free = free_observations() + require_equal(free, model.observe(*model.decode(free)), 'post-F0 right inverse') + complete = model.observe(*after) + require_equal(inputs, model.forward_inverse(*model.decode(complete)), 'complete input recovery') + require_equal(free, model.observe(*model.forward(*model.forward_inverse(*model.decode(free)))), + 'complete observation recovery') + controls = {} + for fault in ('omit_current_driver', 'wrong_current_sign', 'omit_future_T', + 'wrong_logger_sign', 'future_chart_is_current_chart'): + wrong = model.decode(observed, fault) + controls[fault] = rejected(inputs, wrong, fault) + if fault == 'future_chart_is_current_chart': + need(all(scalar_projection(wrong[b][p]) == inputs[b][p] + for b in range(2) for p in range(112)), 'chart fault hidden by D=I') + drops = [] + for b in range(3): + for p in observed[b]: + bad = [dict(block) for block in observed] + bad[b][p] = {} + drops.append({'block': b, 'port': p, + 'witness': rejected(inputs, model.decode(tuple(bad)), 'retained coordinate omission')}) + bad = [dict(block) for block in observed] + bad[4] = {p: {} for p in U} + controls['discard_live_Y2_U'] = rejected(inputs, model.decode(tuple(bad)), 'missing new live read') + bad[4] = dict(inputs[1]) + controls['use_pre_B1_Y_U'] = rejected(inputs, model.decode(tuple(bad)), 'incorrect live cut') + bad = [dict(block) for block in observed] + bad[5] = {p: {} for p in A} + controls['discard_live_Y2_A'] = rejected(inputs, model.decode(tuple(bad)), 'missing live logger') + reversed_rows = tuple({p: dict(reversed(list(row.items()))) for p, row in reversed(list(block.items()))} + for block in observed) + require_equal(inputs, model.decode(reversed_rows), 'term and port reorder') + split_rows = tuple({p: add((Q(1, 3), row), (Q(2, 3), row)) for p, row in block.items()} + for block in observed) + require_equal(inputs, model.decode(split_rows), 'equivalent rational splitting') + return {'status': 'PASS_QQ16_L2_MINIMAL_RETENTION', 'no_new_kappa': True, + 'source_sha256': {k: sha(v) for k, v in sorted(data.items())}, + 'template_member': {MEMBER: MEMBER_SHA}, 'registered_route_pairs': bindings, + 'input_arrays': 224, 'live_arrays': 200, 'retained_arrays': 24, + 'predecessor_L2_retained_arrays': 32, 'retained_blocks': ['x1_A', 'x1_T', 'y1_T'], + 'live_blocks': ['X2_U', 'Y2_U', 'Y2_A'], + 'algebra': 'Q free-group ring on 224 invertible chart/port symbols; D0=I', + 'identities': ['F0^-1 F0=I', 'F0 F0^-1=I', 'decode observe=I', + 'observe decode=I', 'full decoder full observation=I', + 'full observation full decoder=I'], + 'lower_bound': 'For finite array dimension n>0, (200+q)n>=224n; hence q>=24', + 'semantic_faults': controls, 'retained_coordinate_omissions': drops, + 'positive_controls': ['reordered terms/ports', 'rational splitting'], + 'chart_fault_invisible_at_identity_specialization': True, + 'scope': 'Information lemma at immediate post-B1; native reads, cost, cleanup and later cuts not admitted'} + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument('--write-result', action='store_true') + args = ap.parse_args() + result = run() + encoded = json.dumps(result, sort_keys=True, indent=2) + '\n' + path = HERE / 'RESULT.json' + if args.write_result: + with path.open('x') as f: + f.write(encoded) + else: + need(path.read_text() == encoded, 'missing or mismatching committed result') + print(result['status'], 'retained=24 live=200 inputs=224 identities=6 faults=32 no_new_kappa') + + +if __name__ == '__main__': + main()