diff --git a/research/qq16-even-map-native-cut/PROOF.md b/research/qq16-even-map-native-cut/PROOF.md new file mode 100644 index 0000000000..4ca1d6acf3 --- /dev/null +++ b/research/qq16-even-map-native-cut/PROOF.md @@ -0,0 +1,225 @@ +# Sharp native cost through the QQ16 A-copy cut + +This is a successor to PR2328, not a new controller or a recursive-rank +lower bound. Fix the literal `B_1_2[:80]` boundary in the main QQ16 packet. +It includes the first eight inverse X_T lines and all eight A-copy private +sweeps, including their 64 source cover maps. Event 80, the first future-Y +alignment, is excluded. Require the physical A/T shear from PR2216 before +this prefix. The typed shear correction and its initial-normalization +implementation are credited to PR2252 and PR2328, respectively. + +The resulting endpoint requires exactly **24 atomic single-field native +line calls**, compared with 16 in the inherited prefix. This remains true +when arbitrary scalar-linear resynthesis and arbitrary orthogonal cover +maps with even translations are free. In particular these later A-copy +operations cannot absorb the shear's eight extra native lines in this +model. The free scalar coefficients are uniform over owners and independent +of payload addresses and frequencies; they act at the same owner/address. +Cover maps outside that even-translation class, later cuts, +multi-field native primitives and splitting the internal wrappers of a +native recipe are outside the theorem. + +## The exact operator boundary + +Write `A=[0,7,20,27,36,46,57,111]` and +`T=[21,37,47,76,81,87,92,110]`. At an owner d the inherited common X frame +is F, and port p's Y frame is `F C_(dq_p)^-1`. The common invertible F +commutes with the translation lines, so the logical shear takes the +physical form below. No conjugation of the cover maps by F is used. +Use a, t and v for the eight actual physical input X_A, X_T and +Y_T coordinates, and y for physical Y_A. No logical-zero assumption is +made about any of these coordinates or about the 480 ordinary helpers. + +The shear in physical coordinates is + + X_T <- t+a, Y_T <- v-C_T^-1 a, X_A <- a. + +The diagonal C_T has the eight selected q_T labels; the inverse acts on +the source's payload before its contribution reaches Y_T. A bare physical +`Y_T -= X_A` has the wrong operator and incompatible native frames. + +For A port p let V_(p,t) be the literal completed source path for target +t, and let D_(p,t) be the signed half coefficient in that private sweep. +Every row has four nonzero D coefficients, all in T. The exact prefix +endpoint after the shear is + + X_T' = C_T^-1(t+a), + Y_T' = v-C_T^-1 a, + X_A'[p] = a[p] + C_(dq_p) (y[p] + + sum_t D_(p,t) V_(p,t) C_(dq_t)^-1(t[t]+a[t])). + +Here `a[t]` denotes the A input paired with T port t, not an A port with +the same numeric index. All other persistent fields are unchanged. +Each source path is undone after its row. C0 is an existing owned +private register: its arbitrary input is discarded and its output is +zero in I after each private sweep. C1 through C7 remain arbitrary and +unchanged at this cut; they are cleared only by the later retained core. + +At **one payload tensor layer (`lambda=1`)**, the checker uses exact +Gaussian rational coefficients and the ordered affine group algebra, with + + M(g,delta) f(d,z) = f(dg,z XOR d delta), + M(g,a) M(h,b) = M(gh,a XOR g b). + +At that tensor length it compares all 712 output rows of the constructed upper word against +the literal inherited prefix composed with the physical shear. This is +an equality of complete ordered affine-operator expressions, before any +character restriction; it suffices for all owners and arbitrary input +arrays at `lambda=1`. Equality is not inferred merely from the two +characters below. The finite nine-axis native recipe binding is checked +separately. This affine replay does not expand a native tensor power at +larger lambda: `C_q tensor C_q` has eigenvalue `i*i=-1` on an odd/odd +character, whereas a two-term simultaneous-translation surrogate has +eigenvalue 1 there. An explicit exact negative control rejects that +incorrect substitution. + +The all-layer upper bound instead uses a formal linear-operator identity. +For any linear operator `N_t`, the per-pair constructed prefix executes + + C0 <- 0; C0 <- a; t <- t+a; C0 <- N_t a; + v <- v-N_t a; C0 <- 0; t <- N_t(t+a). + +Its data and persistent-field endpoint is exactly the physical shear +`t <- t+a, v <- v-N_t a` followed by the inherited normalization `N_t` +on t, with a unchanged. The constructed prefix returns C0 zero; the +physical-shear-plus-normalization reference still has arbitrary initial +C0 at this intermediate boundary. Literal suffix events 8 through 11 +only map X_T, and event 12 clears C0 before its first read. That clear +annihilates the sole intermediate scratch difference, giving equality +on all 712 fields at the selected final cut. This identity uses only linearity; +it holds in particular for the actual `N_t=(C_(dq_t)^-1) tensor lambda` +at every positive integer lambda. The subsequent literal events 8 +through 79 are identical in both compositions, so their complete ordered +operators, helper outputs and scratch outputs remain equal for all such +lambda. A second checker independently replays all 712 endpoint rows as +rational word polynomials in arbitrary noncommuting native and map +operator symbols. It uses one symbol for each literal signed recipe or +cover-map label, without expanding C_q or using any inverse relation. +The constructed word and the inherited word after the physical shear +have identical word-polynomial rows. A changed conversion/subtraction +order is rejected. Interpreting these symbols as the actual tensor +operators proves the all-layer endpoint identity. This fresh formal +operator equality and its tensor interpretation are separate from the +one-layer affine replay. The affine composition law for the unchanged +source maps, and equality of their per-layer frame polynomials, apply +to every layer and supply the same path restoration and typed access. + +## A character preserved by the later source maps + +Let `Omega=(1<<73)-1`, the characteristic vector for the standard binary +bilinear form. Every orthogonal binary matrix g fixes Omega. Indeed + + Omega dot g v = (g v) dot (g v) = v dot v = Omega dot v + +for all v; hence `g^T Omega=Omega`, and invertibility also gives +`g Omega=Omega`. Consider two owner-covariant payload functions with +constant amplitude over owners: + + f_0(d,z)=1, + f_Omega(d,z)=(-1)^(Omega dot d^-1 z). + +The owner matrices d and g are orthogonal. Apply the actual cover action: + + M(g,delta) f_Omega(d,z) + = (-1)^(Omega dot (g^-1 d^-1 z XOR g^-1 delta)) + = f_Omega(d,z) (-1)^(Omega dot delta). + +Thus an even translation delta makes every such map the identity on +both functions. This explicitly includes the owner action; a fixed-owner +payload Fourier mode alone would not justify erasing owner maps. +The source checker verifies orthogonality and even translation for all +64 map events in the selected cut. Arbitrary repetitions, inverses and +products of this class remain in the class. The lower-bound relaxation +may therefore grant any such maps for free, not just their selected order. + +A native line `C_(dq)^epsilon` has eigenvalue 1 on f_0 and +`i^(epsilon*(Omega dot q))` on f_Omega. The 16 native labels used by the +inherited cut are odd. Thus inverse T lines have value c=-i, and positive +A lines value b=i. Any arbitrary native label allowed in the relaxation +still changes at most one field coordinate between the two evaluations. + +For multiple positive tensor layers choose f_Omega on one layer and +f_0 on the others. The simultaneous owner-relative translations on all +layers then give exactly the same invariant and native eigenvalues. +The lower bound requires at least one payload layer; it makes no claim +for the degenerate zero-layer specialization. The input/output frames +are invertible coordinate changes on independent arbitrary physical +arrays, so they impose no relation that could remove the minor's inputs. + +## The 24-dimensional minor + +At the two invariant characters every source path is identity. At f_0 +both b and c are 1; at f_Omega they are i and -i, so bc=1 in both cases. +Consequently, with D the scalar signed-half matrix, the evaluated map is + + X_T' = c(t+a), + Y_T' = v-ca, + X_A' = a+b y+D(t+a). + +Only the X_T, Y_T and X_A output rows differ. Set `d=-1-i`. Order the +first 16 rows in paired `(X_T,Y_T)` order and their input columns in +paired `(X_A,X_T)` order; append the eight X_A output rows and Y_A input +columns. The difference minor is block diagonal: eight blocks + + d [ 1 1 ] + [-1 0 ] + +and an eight-dimensional diagonal `(i-1) I`. Its determinant is + + d^16 (i-1)^8 = 256 * 16 = 4096. + +It therefore has rank 24, exactly, since only 24 output rows differ. +The checker computes this Gaussian rational determinant from the full +literal operator and records the exact field indices. Without the shear +the only differing output rows are X_T and X_A; the corresponding +16-dimensional minor is nonsingular and the inherited difference rank +is exactly 16. + +Now take any finite circuit in the stated relaxation, with arbitrary +additional scalar registers. Pad its register set to fixed size. Evaluate +the circuit on f_0 and f_Omega and telescope the difference of the two +matrix products. A free scalar gate has zero difference. A free +orthogonal/even-translation map has zero difference. Each atomic +single-field native line has difference rank at most one. Product rank +and subadditivity therefore bound the endpoint difference rank by the +number of paid lines. Restricting to original inputs and required outputs +cannot increase rank. This argument allows noninvertible free scalar +operations, copying, projections, owned clears, finite zero-initialized +scratch and discarded private input columns. The rank-24 minor proves +that at least 24 lines are necessary. + +## Typed attainment and the complete local invoice + +Use PR2328's typed 16-line shear-plus-initial-normalization prefix: for +each pair, clear C0 in F, add X_A to C0 and X_T, apply the inverse T line +to C0, subtract C0 from Y_T, clear C0 to I, and execute the original +inverse X_T line. Append the unchanged literal events 8 through 79. +Every scalar ADD has equal exact phase polynomials, every source path +is restored, and every private body has the whole-owner barrier and +initial/final owned clears. This yields the desired complete endpoint +with 24 lines and no new field. + +| Charge | Inherited cut | Attaining sheared cut | Difference | +|---|---:|---:|---:| +| Atomic rank-one native lines | 16 | 24 | +8 | +| Native recipe wrapper maps | 32 | 48 | +16 | +| Explicit cover maps | 64 | 64 | 0 | +| Complex scalar ADDs | 48 | 72 | +24 | +| Owned CLEARs | 16 | 32 | +16 | +| Private row sweeps | 8 | 16 | +8 | +| Scalar real-primitive allowance | 480 | 704 | +224 | + +The scalar allowance charges 8 per unit complex ADD, 10 per half ADD, +and 2 per CLEAR. Native children and all map costs remain separate. +The lower bound is sharp for native-line count, not necessarily for the +scalar/map invoice. No physical stream/address cost, precision envelope, +child hosting, controller closure, supplier admission or new kappa follows. + +The retained QQ16 maps, source paths, native recipes and arbitrary-helper +contract are credited to Ali Romman's PR1969 and its conserved-QQ16 +source contributors. Cinna Davis's PR2216 supplies the shear, Charles +Bethin's PR2252 its native-frame warning, and PR2328 supplies the sharp +initial-prefix obstruction and typed upper construction. The new step +here is the owner-covariant characteristic-vector invariant for the +actual even source routes, its exact later cut and sharp 24-line boundary. +Substantial OpenAI Codex assistance was used. New material is Apache-2.0. diff --git a/research/qq16-even-map-native-cut/README.md b/research/qq16-even-map-native-cut/README.md new file mode 100644 index 0000000000..bffec2e2e1 --- /dev/null +++ b/research/qq16-even-map-native-cut/README.md @@ -0,0 +1,147 @@ +# QQ16: the eight extra native lines survive the A-copy cut + +At the retained `B_1_2` boundary after top-level events `[:80]`, the +logical paired A-to-T shear followed by the inherited word needs exactly +**24 atomic single-field native lines**, versus **16** in the inherited +word. The eight A-copy sweeps and their 64 actual cover maps do not absorb +the earlier eight-line overhead. This answers one later-cut handoff from +[commdata2338's PR #2328](https://github.com/CrocSwap/integer-mult-bounds/pull/2328), +head `6b2717ce2bbb13c2152e64efea48867b78840bbb`. + +The lower bound grants arbitrary finite, frequency-independent scalar +resynthesis with scratch, and any number of free cover maps +`M(g,delta)` with **orthogonal owner matrix g and even translation delta**. +The model uses uniform scalar coefficients over owners and payload +addresses. It excludes odd translations, nonorthogonal owner changes, +other payload-address operations and multi-field native atoms. It applies +with at least one payload layer. See [PROOF.md](PROOF.md) for the exact +domain and the telescoping rank argument. There is no claim about a later +cut, unrestricted cover maps, full controller recovery, supplier admission +or a new kappa. The selected frontier is unchanged. + +## Endpoint and evidence + +The cut is just before event 80, `cover_map L112 m89`, the first future-Y +alignment. It includes eight initial X_T inverse lines, all eight A-copy +sweeps, and all source-path restoration maps. The target is the actual +cut composed with the physical version of the logical shear: +`X_T += X_A; Y_T -= C_qT^-1 X_A`. Bare physical `Y_T -= X_A` is invalid +on general payloads, as Charles Bethin's PR #2252 identified. + +The owner-covariant character +`chi_Omega(d,z)=(-1)^(Omega dot d^-1 z)`, `Omega=2^73-1`, and the constant +character are both fixed by every allowed free cover map. The exact +character-difference matrix has rank 24, certified by the recorded +24-by-24 minor of determinant **4096**. Every single-field native atom +contributes difference rank at most one. The inherited endpoint has +difference rank 16. + +The checker separately compares all 712 field rows in a free +noncommuting-operator algebra, treating each complete native line and +cover map as an atom. This proves equality at the selected cut after +the identical suffix for any tensor length. A second, complete ordered +affine-group-algebra replay specializes to **one payload layer** and +checks source-path restoration, all 480 arbitrary dirty helpers, cleared +C0 and arbitrary unchanged C1..C7. The written proof interprets the free +atoms as the actual tensor operators for every positive number of +layers. Two characters alone are insufficient to establish the upper +construction, and the one-layer two-term native kernel is not silently +used as a multiple-layer operator. + +Ordered native frames, ADD compatibility and private sweep barriers are +checked separately. A fresh literal physical recipe check covers the 16 +used signed native recipes on 512 basis columns each. A two-layer control +distinguishes the tensor native line from a simultaneous two-term shift. +No pending predecessor verifier is imported or executed. + +The attaining construction uses PR #2328's credited 16-line owned-C0 +prefix followed by the unchanged eight A-copy sweeps. Counts include the +native wrappers separately from explicit cover maps: + +| Local quantity | Inherited cut | Attaining sheared cut | Difference | +|---|---:|---:|---:| +| Atomic native lines | 16 | 24 | +8 | +| Native wrapper maps | 32 | 48 | +16 | +| Explicit cover maps | 64 | 64 | 0 | +| Complex ADDs | 48 | 72 | +24 | +| CLEARs | 16 | 32 | +16 | +| Private whole-owner sweeps | 8 | 16 | +8 | +| Scalar real primitive upper bound | 480 | 704 | +224 | + +The scalar bound charges unit complex ADD at 8, half ADD at 10 and CLEAR +at 2; both cuts contain 32 half ADDs. This is a complete **local abstract +invoice**, not a global physical hosting or recursion bill. Cover maps are +free only in the lower-bound relaxation; their actual counts remain in +the invoice. C0 already exists and is cleared before and after each sweep; +no dirty helper is borrowed. The added native lines carry the same labels +and native rank-one contract as the inherited word. No new all-size or +coefficient-precision admission is inferred. + +## Reproduce + +From the repository root with CPython 3.12, standard library only: + +```sh +python3.12 -I -B scripts/research_package.py --package research/qq16-even-map-native-cut +``` + +`VERIFY.json` runs normal and optimized exact checks plus independent +integration tests. The main marker is +`PASS_QQ16_EVEN_MAP_NATIVE_CUT rank=24 baseline_lines=16 attaining_lines=24`. +`RESULT.json` is compared in full with type-exact JSON equality. Default +verification does not rewrite it. To generate a separate receipt, pass +`--write-result /absolute/fresh/path.json` to `verify.py`; the output must +be new and outside the repository. `SOURCES.json` pins the only live +mathematical input and the originating catalogue; generic replay verifies +their Git objects at the base commit as well as live input bytes. + +The session's broad baseline command was attempted but did not pass: +the isolated sparse checkout lacks the selected supplier's full source +inventory (`research/complex-sw4-frame8`). This package's source closure +is present and checked separately. `make frontier1094-verify`, full QQ16 +supplier replay, global hosting, precision, recursive compiler admission +and proof-assistant checking were not run. Agent reviews are recorded as +agent reviews; no independent human review is claimed. + +## Assignment and predecessor credit + +Base main: `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority revision 4. +One OS-seeded chooser draw: `f7a0c6caa6b3f1906aa449affcb084ab`, track +`recursive-interfaces`, task `joint-query-controller`, scope key +`22e535909f1d243e7553`. The full standard chooser replay used the same +nonce. [TASK.json](TASK.json) records a **changed** scope: a precise +physical-cost handoff replaces the already-covered generic extra-read +experiment. This completes the stated side result, not the card's full +controller gate. Coordination is in +[Discussion #2205](https://github.com/CrocSwap/integer-mult-bounds/discussions/2205#discussioncomment-18944331). +The entry scan paginated 614 open PR bodies including drafts. The +canonical QQ16 thread and targeted board/handoff pages were read; broad +Discussion history, closed work, all diffs and unpublished work were not +exhaustively searched. No novelty certification is claimed. + +Credit **commdata2338** (PR #2328) for the character-difference method, +earlier 16-line minimum, owned-scratch prefix and later-cut handoff; +**Charles Bethin / cbethin** (PR #2252, +`6dd49c2b186e08ef1f3efd08f62e1add97ff04a3`) for the native-frame correction; +**Cinna Davis / 1337isnot1337** (PR #2216, +`b80e9ba43367fb8b20877a97da1cb677c34f9264`) for the logical paired shear; +and **Ali Romman / aliromman** (PR #1969, +`a6e6ad3936f67b8f63b5b68c5e75d540610a65e7`) and the retained joint-query +lineage for the packet, native recipes, maps, words and notices. +The covariant-character extension to the stated cover-map subgroup, +later rank-24 endpoint, exact full-operator check and local invoice are +this package's additions. New material by ToikY with substantial OpenAI +Codex assistance, including separate implementation and test/review +agents, under Apache-2.0. All existing source notices and licenses remain +in place; see [joint-query/NOTICE.md](../joint-query/NOTICE.md). + +## Open next questions + +1. At a specified later cut or with an expanded map alphabet, can a + fully typed construction absorb this overhead? Start by stating the + endpoint and allowed operations; an odd translation already defeats + this particular character invariant. +2. Which sufficient retained record survives the complete ordered QQ16 + tail and has a favorable full physical invoice? Screen its kernel + against PR #2368/#2381 before native costing. Retention, global hosting, + precision, all-size compilation and supplier admission remain open. diff --git a/research/qq16-even-map-native-cut/RESULT.json b/research/qq16-even-map-native-cut/RESULT.json new file mode 100644 index 0000000000..5083d17a26 --- /dev/null +++ b/research/qq16-even-map-native-cut/RESULT.json @@ -0,0 +1,210 @@ +{ + "controls": [ + { + "name": "two_layer_simultaneous_translation_substitution", + "outcome": "REJECT" + }, + { + "name": "free_operator_late_source_conversion", + "outcome": "REJECT" + }, + { + "name": "wrong_native_sign", + "outcome": "REJECT" + }, + { + "name": "native_wrapper_global_phase", + "outcome": "REJECT" + }, + { + "name": "arbitrary_C0_without_initial_clear", + "outcome": "REJECT" + }, + { + "name": "missing_row_boundary_clear", + "outcome": "REJECT" + }, + { + "name": "omitted_X_T_normalization", + "outcome": "REJECT" + }, + { + "name": "borrowed_helper_clear", + "outcome": "REJECT" + }, + { + "name": "private_owner_barrier", + "outcome": "REJECT" + }, + { + "name": "odd_translation_breaks_invariant", + "outcome": "REJECT" + }, + { + "name": "wrong_translation_full_endpoint", + "outcome": "REJECT" + }, + { + "name": "payload_only_owner_route", + "outcome": "REJECT" + }, + { + "name": "bare_Y_subtraction", + "outcome": "REJECT" + } + ], + "cut": { + "case": "B_1_2", + "end_exclusive": 80, + "next_event": [ + "cover_map", + [ + "L", + 112 + ], + "m89" + ] + }, + "exact": { + "baseline_difference_rank": 16, + "dirty_helpers_restored": 480, + "free_operator_rows": 712, + "free_operator_rows_scope": "arbitrary noncommuting linear native/map operators, no tensor expansion", + "full_operator_rows": 712, + "full_operator_rows_scope": "one payload tensor layer (lambda=1)", + "minor_columns": [ + 0, + 21, + 7, + 37, + 20, + 47, + 27, + 76, + 36, + 81, + 46, + 87, + 57, + 92, + 111, + 110, + 112, + 119, + 132, + 139, + 148, + 158, + 169, + 223 + ], + "minor_det": [ + 4096, + 0 + ], + "minor_rows": [ + 21, + 133, + 37, + 149, + 47, + 159, + 76, + 188, + 81, + 193, + 87, + 199, + 92, + 204, + 110, + 222, + 0, + 7, + 20, + 27, + 36, + 46, + 57, + 111 + ], + "native_recipe_basis_columns": 8192, + "private_outputs": "C0 zero; C1..C7 arbitrary unchanged", + "rank": 24 + }, + "invariant": { + "characters": [ + 0, + 9444732965739290427391 + ], + "maps": 64, + "native_labels": [ + 289, + 274, + 268, + 448, + 478, + 493, + 499, + 319, + 11, + 21, + 161, + 38, + 146, + 140, + 56, + 191 + ], + "odd_lines": 16 + }, + "invoice": { + "attaining": { + "adds": 72, + "clears": 32, + "explicit_cover_maps": 64, + "native_lines": 24, + "native_wrapper_maps": 48, + "private_sweeps": 16, + "scalar_real_primitive_bound": 704 + }, + "baseline": { + "adds": 48, + "clears": 16, + "explicit_cover_maps": 64, + "native_lines": 16, + "native_wrapper_maps": 32, + "private_sweeps": 8, + "scalar_real_primitive_bound": 480 + }, + "delta": { + "adds": 24, + "clears": 16, + "explicit_cover_maps": 0, + "native_lines": 8, + "native_wrapper_maps": 16, + "private_sweeps": 8, + "scalar_real_primitive_bound": 224 + } + }, + "source_boundary": { + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "packet_sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + }, + "status": "PASS_QQ16_EVEN_MAP_NATIVE_CUT", + "tensor_scope": { + "exact_affine_replay_layers": 1, + "lower_bound": "all integer lambda>=1 by one Omega character layer and constant other layers", + "two_layer_odd_odd_counterexample": { + "native_tensor_eigenvalue": [ + -1, + 0 + ], + "simultaneous_two_term_eigenvalue": [ + 1, + 0 + ] + }, + "upper_bound": "all integer lambda>=1 by fresh free-operator endpoint equality and the written tensor interpretation" + } +} diff --git a/research/qq16-even-map-native-cut/SOURCES.json b/research/qq16-even-map-native-cut/SOURCES.json new file mode 100644 index 0000000000..a41017b597 --- /dev/null +++ b/research/qq16-even-map-native-cut/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "research/joint-query/certificate.json.gz", + "usage": "input", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050" + } + ] +} diff --git a/research/qq16-even-map-native-cut/TASK.json b/research/qq16-even-map-native-cut/TASK.json new file mode 100644 index 0000000000..2e2ffe94d9 --- /dev/null +++ b/research/qq16-even-map-native-cut/TASK.json @@ -0,0 +1,119 @@ +{ + "schema_version": 1, + "seed": "f7a0c6caa6b3f1906aa449affcb084ab", + "track": "recursive-interfaces", + "task_id": "joint-query-controller", + "scope_key": "22e535909f1d243e7553", + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "catalog_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "original_card": { + "id": "joint-query-controller", + "question": "Can one explicitly changed QQ16 interface recover the missing chart query and close a two-call controller within a favorable full budget?", + "starting_points": [ + "research/joint-query/README.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Add one explicitly priced ordinary-to-selected observation and derive the ordered two-call map and inverse.", + "Change the first local pair or retained state, then test the existing lost-observation witness and price all new operations." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the fixed-first-pair QQ16 witness before designing a controller. The checked #1969 local words do not evade that witness or supply global placement.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Apply the existing witness to one proposed extra observation or changed first pair. If it still loses the required record, stop. Otherwise derive one ordered two-call identity and charge the added read, chart maps and restoration before extending to more stages.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969" + ] + }, + "scope_status": "changed", + "scope_change_reason": "Follow the explicit released later-B1-cut handoff from PR2328 instead of repeating the densely covered ordinary-observation/kernel work. This closes one physical native-cost question, not the original full-controller acceptance gate.", + "actual_scope": "At actual B_1_2 events[:80], determine the exact atomic single-field native-line minimum for the physical A-to-T paired shear followed by the inherited cut, for every positive tensor length, allowing arbitrary finite scalar resynthesis with uniform coefficients and free orthogonal-owner/even-translation cover maps.", + "bottleneck_link": "Tests whether the next eight native A-copy lines and their 64 cover maps can absorb the eight extra native lines proved necessary at the earlier normalization cut; a complete physical invoice is required before any controller budget can close.", + "stop_rule": "Stop at this one exact later cut and model, with matching lower/upper native counts and full typed endpoint; no later cuts, arbitrary cover-map alphabet, recursive supplier or frontier change. Construction cutoff 2026-10-15T08:42:28Z, session budget ends 08:57:28Z.", + "outcome": "completed", + "evidence": "All 712-row endpoint equality in a free noncommutative operator algebra for any positive tensor length; separate one-layer Gaussian rational affine-group replay and restoration; rank-24 minor with determinant 4096; source-bound typing and native recipe checks; complete local invoice; 13 semantic controls and nine integration tests in normal and optimized Python. The written character proof applies to every positive tensor length. Separate agent reviews, no human or proof-assistant review.", + "author": "ToikY", + "ai_assistance": "Substantial OpenAI Codex assistance; separate implementation and test/review agents. Agent review is not independent human review.", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2205#discussioncomment-18944331", + "predecessors": [ + { + "pr": 2328, + "author": "commdata2338", + "head": "6b2717ce2bbb13c2152e64efea48867b78840bbb", + "contribution": "Character-difference native-line method, earlier 16-line theorem, legal owned-C0 prefix and explicit later-cut handoff." + }, + { + "pr": 2252, + "author": "Charles Bethin (cbethin)", + "head": "6dd49c2b186e08ef1f3efd08f62e1add97ff04a3", + "contribution": "Native-frame correction and fusion question." + }, + { + "pr": 2216, + "author": "Cinna Davis (1337isnot1337)", + "head": "b80e9ba43367fb8b20877a97da1cb677c34f9264", + "contribution": "Logical paired A-to-T shear on the earlier witness." + }, + { + "pr": 1969, + "author": "Ali Romman (aliromman)", + "head": "a6e6ad3936f67b8f63b5b68c5e75d540610a65e7", + "contribution": "Retained source packet, maps, native lines, ordered words and inherited attribution." + } + ], + "open_questions": [ + { + "question": "Can a specified later B1 cut or an expanded cover-map alphabet absorb the extra native-line charge?", + "why_it_matters": "This result ends before the future Y alignment and uses a stated character-preserving map subgroup.", + "first_step": "State one new fixed endpoint and full native/map alphabet; test a valid invariant or an explicit typed counterword.", + "blocked_by": "No such endpoint or circuit is verified here." + }, + { + "question": "Can a sufficient retained record recover the full selected input with a favorable physical invoice?", + "why_it_matters": "The paired shear alone does not settle the controller kernel or supplier admission.", + "first_step": "Use the existing dense-record/kernel results (PR2368/2381) to screen a fully specified record before pricing it.", + "blocked_by": "Full recovery, retention, helper placement, precision and all-size/native compiler obligations remain open." + } + ], + "orientation": { + "first_step_command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "outcome": "ATTEMPTED_NOT_PASS", + "reason": "Sparse source closure lacks research/complex-sw4-frame8; baseline command raises Invalid package root. Exact selected record/review and named QQ16 witness were read; no selected-frontier reproduction claimed." + }, + "overlap": { + "open_pr_bodies": 614, + "complete_pr_pagination": true, + "discussions": "Discussion #2205: all 14 top-level comments and six replies were read before the claim; the new 15th comment was verified after posting. Targeted #1163/#1166 and the active board were checked. Discussion-wide pagination was unavailable.", + "local_scope": "Sparse current-main starting points and local PR ledger, not complete local research inventory.", + "novelty": "No novelty certification or first-closure claim." + } +} diff --git a/research/qq16-even-map-native-cut/VERIFY.json b/research/qq16-even-map-native-cut/VERIFY.json new file mode 100644 index 0000000000..571eb8ec2c --- /dev/null +++ b/research/qq16-even-map-native-cut/VERIFY.json @@ -0,0 +1,53 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/joint-query/certificate.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "checks": "Source pins, all-layer free-operator endpoint, one-layer affine-group endpoint/restoration, native recipe/frame bindings, owned scratch, character invariant/minor, invoice and semantic controls.", + "timeout_seconds": 180 + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "checks": "Same frozen receipt and semantic controls with Python assertions disabled.", + "timeout_seconds": 180 + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "checks": "Independent arithmetic and receipt/CLI integrity regression tests.", + "timeout_seconds": 180 + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_verify.py" + ], + "checks": "Independent tests in optimized mode.", + "timeout_seconds": 180 + } + ] +} diff --git a/research/qq16-even-map-native-cut/test_verify.py b/research/qq16-even-map-native-cut/test_verify.py new file mode 100644 index 0000000000..bc3d174e90 --- /dev/null +++ b/research/qq16-even-map-native-cut/test_verify.py @@ -0,0 +1,227 @@ +#!/usr/bin/env python3 +"""Boundary, arithmetic and exported-receipt controls; standard library only.""" +from copy import deepcopy +from fractions import Fraction as Q +import importlib.util +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("qq16_cut", HERE / "verify.py") +v = importlib.util.module_from_spec(spec) +spec.loader.exec_module(v) + + +def character(rows, odd): + """Separate scalar evaluator, without the production evaluate helper.""" + result = [] + for row in rows: + out = {} + for (column, (_, shift)), (real, imag) in row.items(): + sign = -1 if odd and shift.bit_count() % 2 else 1 + old = out.get(column, (Q(0), Q(0))) + out[column] = (old[0] + sign*real, old[1] + sign*imag) + result.append({key: value for key, value in out.items() if value != (0, 0)}) + return result + + +def real_minor(rows, row_ids, column_ids): + lo, hi = character(rows, False), character(rows, True) + a, b = [], [] + for i in row_ids: + pairs = [(hi[i].get(j, (0, 0))[0] - lo[i].get(j, (0, 0))[0], + hi[i].get(j, (0, 0))[1] - lo[i].get(j, (0, 0))[1]) for j in column_ids] + a.append([Q(x) for x, _ in pairs]) + b.append([Q(y) for _, y in pairs]) + return [x + [-y for y in z] for x, z in zip(a, b)] + [z + x for x, z in zip(a, b)] + + +def rational_rank_det(matrix): + """Real rational elimination, independent of Gaussian determinant code.""" + a, rank, determinant = deepcopy(matrix), 0, Q(1) + for col in range(len(a[0])): + pivot = next((i for i in range(rank, len(a)) if a[i][col]), None) + if pivot is None: + continue + if pivot != rank: + a[pivot], a[rank] = a[rank], a[pivot] + determinant = -determinant + value = a[rank][col] + determinant *= value + for i in range(rank+1, len(a)): + scale = a[i][col] / value + if scale: + a[i] = [x-scale*y for x, y in zip(a[i], a[rank])] + rank += 1 + return rank, determinant if rank == len(a) else Q(0) + + +class CutTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.packet = v.load_packet() + cls.original = cls.packet["programs"]["B_1_2"][:80] + cls.upper = v.construct(cls.packet) + cls.target = v.replay(cls.packet, cls.original, v.physical_shear(cls.packet)) + cls.actual = v.replay(cls.packet, cls.upper) + + def test_independent_realified_rank_and_determinant(self): + rows = [x for t in v.T for x in (t, 112+t)] + v.A + cols = [x for a, t in zip(v.A, v.T) for x in (a, t)] + [112+a for a in v.A] + self.assertEqual(rational_rank_det(real_minor(self.target, rows, cols)), (48, Q(4096**2))) + baseline = v.replay(self.packet, self.original) + self.assertEqual(rational_rank_det(real_minor(baseline, v.T+v.A, v.T+[112+a for a in v.A]))[0], 32) + + def test_projection_is_insufficient_for_full_operator(self): + bad = deepcopy(self.upper) + event = deepcopy(self.original[8]) + event[1] = ["L", 224] + bad.append(event) + damaged = v.replay(self.packet, bad) + self.assertNotEqual(damaged[224], self.target[224]) + for odd in (False, True): + self.assertEqual(character(damaged, odd), character(self.target, odd)) + with self.assertRaises(ValueError): + v.typed(self.packet, bad) + + def test_all_fields_and_arbitrary_private_input(self): + self.assertEqual(self.actual, self.target) + unit = v.identity() + self.assertEqual(self.actual[224:704], unit[224:704]) + self.assertEqual(self.actual[704], {}) + self.assertEqual(self.actual[705:], unit[705:]) + bad = deepcopy(self.upper) + del bad[0][2][0] + damaged = v.replay(self.packet, bad) + self.assertNotEqual(damaged, self.target) + self.assertTrue(any(column == 704 for row in damaged[:224] for column, _ in row)) + bad = deepcopy(self.upper) + del bad[0][2][-1] + with self.assertRaises(ValueError): + v.typed(self.packet, bad) + + def test_map_class_and_actual_native_recipe(self): + name = self.original[8][2] + bad = deepcopy(self.packet) + bad["map_registry"][name]["payload_translation_at_identity_owner"] ^= 1 + with self.assertRaisesRegex(ValueError, "even payload"): + v.invariants(bad) + bad = deepcopy(self.packet) + bad["map_registry"][name]["action"] = "payload-only action" + with self.assertRaisesRegex(ValueError, "owner/payload"): + v.invariants(bad) + bad = deepcopy(self.packet) + bad["map_registry"][name]["owner_right_matrix_columns"] = list(v.AXES) + bad["map_registry"][name]["owner_right_matrix_columns"][0] ^= 2 + with self.assertRaisesRegex(ValueError, "orthogonal"): + v.invariants(bad) + self.assertEqual(v.physical_check(self.packet), 8192) + bad = deepcopy(self.packet) + bad["native_line_recipes"]["inverse_21"]["recipe"]["left"]["phase"] += 1 + with self.assertRaisesRegex(ValueError, "Gaussian column"): + v.physical_check(bad) + + def test_literal_invoice_and_illegal_fields(self): + def invoice(word): + flat = list(v.flatten(word)) + adds = [e for e in flat if e[0] == "scalar" and e[1][0] == "add"] + clears = sum(e[0] == "scalar" and e[1][0] == "clear" for e in flat) + unit = sum(e[1][4] == 1 for e in adds) + half = sum(e[1][4] == 2 for e in adds) + self.assertEqual(unit+half, len(adds)) + return (sum(e[0] == "native_line" for e in flat), sum(e[0] == "cover_map" for e in flat), + unit, half, clears, 8*unit+10*half+2*clears) + self.assertEqual(invoice(self.original), (16, 64, 16, 32, 16, 480)) + self.assertEqual(invoice(self.upper), (24, 64, 40, 32, 32, 704)) + for token in (["L", True], ["L", 704], ["C", 8], ["Q", 0]): + with self.subTest(token=token), self.assertRaises(ValueError): + v.register(token) + bad = deepcopy(self.upper) + bad[0][2][3][2] = "unknown_native" + with self.assertRaises(KeyError): + v.typed(self.packet, bad) + + def test_strict_json_types(self): + for raw in ('{"x":1,"x":2}', '{"x":NaN}', '{"x":Infinity}', '{"x":1.0}'): + with self.subTest(raw=raw), self.assertRaises(ValueError): + v.load_json(raw) + self.assertNotEqual(v.exact({"x": False}), v.exact({"x": 0})) + + def test_single_layer_replay_does_not_prove_tensor_replay(self): + # On two odd Fourier modes, C tensor C has eigenvalue i*i=-1. + # The simultaneous shift of both modes is +1, so alpha I+beta(T tensor T) + # instead has eigenvalue +1. The complete replay must retain its lambda=1 scope. + alpha, beta = (Q(1, 2), Q(1, 2)), (Q(1, 2), Q(-1, 2)) + odd = [1, -1, -1, 1] + c = [[alpha, beta], [beta, alpha]] + actual = [v.ZERO]*4 + for i in range(4): + for j in range(4): + coefficient = v.mul(c[i//2][j//2], c[i%2][j%2]) + actual[i] = v.add(actual[i], (odd[j]*coefficient[0], odd[j]*coefficient[1])) + simultaneous = [v.add((alpha[0]*odd[i], alpha[1]*odd[i]), + (beta[0]*odd[i ^ 3], beta[1]*odd[i ^ 3])) for i in range(4)] + self.assertEqual(actual, [(-x, Q(0)) for x in odd]) + self.assertEqual(simultaneous, [(x, Q(0)) for x in odd]) + self.assertNotEqual(actual, simultaneous) + + def test_free_noncommuting_endpoint_and_wrong_order(self): + target = v.free_replay(self.original, sheared=True) + self.assertEqual(v.free_replay(self.upper), target) + bad = deepcopy(self.upper) + bad[0][2][3], bad[0][2][4] = bad[0][2][4], bad[0][2][3] + damaged = v.free_replay(bad) + self.assertNotEqual(damaged, target) + # Subtracting before converting the source leaves the bare source word. + self.assertEqual(damaged[112+v.T[0]][(v.A[0], ())], Q(-1)) + self.assertNotIn((v.A[0], ()), target[112+v.T[0]]) + + def test_relocated_cli_and_corruption_controls(self): + with tempfile.TemporaryDirectory(prefix="qq16-cut-tests-") as temp: + root = Path(temp) / "repo" + package = root / "research" / "cut" + package.mkdir(parents=True) + for name in ("verify.py", "SOURCES.json", "RESULT.json"): + shutil.copy2(HERE / name, package / name) + packet_path = root / v.PACKET + packet_path.parent.mkdir(parents=True) + shutil.copy2(v.ROOT / v.PACKET, packet_path) + def run(*args, optimized=False): + command = [sys.executable, "-I", "-B"] + (["-O"] if optimized else []) + return subprocess.run(command + [str(package / "verify.py"), *map(str, args)], + capture_output=True, text=True, timeout=120) + self.assertEqual(run(optimized=True).returncode, 0) + receipt = (package / "RESULT.json").read_text() + result = json.loads(receipt) + result["exact"]["minor_det"][1] = False + (package / "RESULT.json").write_text(json.dumps(result)) + self.assertIn("type-exact frozen RESULT", run().stderr) + (package / "RESULT.json").write_text('{"status":"stale",' + receipt.lstrip()[1:]) + self.assertIn("duplicate JSON key", run().stderr) + (package / "RESULT.json").write_text(receipt) + source = (package / "SOURCES.json").read_text() + stale = json.loads(source); stale["base_commit"] = "0"*40 + (package / "SOURCES.json").write_text(json.dumps(stale)) + self.assertIn("source base", run().stderr) + (package / "SOURCES.json").write_text(source) + raw = packet_path.read_bytes() + packet_path.write_bytes(raw[:-1] + bytes([raw[-1] ^ 1])) + self.assertIn("source SHA", run().stderr) + packet_path.write_bytes(raw) + output = Path(temp) / "fresh.json" + self.assertEqual(run("--write-result", output).returncode, 0) + self.assertEqual(json.loads(output.read_text()), json.loads(receipt)) + before = output.read_bytes() + self.assertIn("fresh external output only", run("--write-result", output).stderr) + self.assertEqual(output.read_bytes(), before) + self.assertIn("fresh external output only", run("--write-result", package / "new.json").stderr) + self.assertFalse((package / "new.json").exists()) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/qq16-even-map-native-cut/verify.py b/research/qq16-even-map-native-cut/verify.py new file mode 100644 index 0000000000..64150b5430 --- /dev/null +++ b/research/qq16-even-map-native-cut/verify.py @@ -0,0 +1,525 @@ +#!/usr/bin/env python3 +"""Exact QQ16 cut audit; standard library only, no predecessor execution.""" +import argparse +from collections import Counter +from copy import deepcopy +from fractions import Fraction as Q +from functools import lru_cache +import gzip +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASE = "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2" +PACKET = "research/joint-query/certificate.json.gz" +PACKET_SHA = "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" +A = [0, 7, 20, 27, 36, 46, 57, 111] +T = [21, 37, 47, 76, 81, 87, 92, 110] +AXES = tuple(1 << i for i in range(73)) +UNIT = (AXES, 0) +OMEGA = (1 << 73) - 1 +ZERO, ONE = (Q(0), Q(0)), (Q(1), Q(0)) +MARKER = "PASS_QQ16_EVEN_MAP_NATIVE_CUT" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def exact(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False) + + +def load_json(raw): + def unique(pairs): + out = {} + for key, value in pairs: + need(key not in out, "duplicate JSON key") + out[key] = value + return out + + def no_float(value): + raise ValueError("JSON floats/nonfinite values are not permitted") + + return json.loads(raw, object_pairs_hook=unique, parse_float=no_float, parse_constant=no_float) + + +def add(a, b): + return a[0] + b[0], a[1] + b[1] + + +def neg(a): + return -a[0], -a[1] + + +def mul(a, b): + return a[0]*b[0] - a[1]*b[1], a[0]*b[1] + a[1]*b[0] + + +def div(a, b): + d = b[0]*b[0] + b[1]*b[1] + need(d != 0, "nonzero Gaussian divisor") + c = mul(a, (b[0], -b[1])) + return c[0]/d, c[1]/d + + +def bits(n): + while n: + b = n & -n + yield b.bit_length() - 1 + n ^= b + + +def act(columns, vector): + result = 0 + for i in bits(vector): + result ^= columns[i] + return result + + +@lru_cache(None) +def compose(left, right): + g, a = left + h, b = right + return tuple(act(g, c) for c in h), a ^ act(g, b) + + +def row_add(row, other, coefficient=ONE): + out = dict(row) + for key, value in other.items(): + out[key] = add(out.get(key, ZERO), mul(coefficient, value)) + if out[key] == ZERO: + del out[key] + return out + + +def operate(row, operator, coefficient=ONE): + out = {} + for (column, old), value in row.items(): + key = column, compose(operator, old) + out[key] = add(out.get(key, ZERO), mul(coefficient, value)) + if out[key] == ZERO: + del out[key] + return out + + +def identity(): + return [{(i, UNIT): ONE} for i in range(712)] + + +def register(token): + need(type(token) is list and len(token) == 2, "field token") + name, at = token + need(type(at) is int and name in ("L", "C"), "field type") + need(0 <= at < (704 if name == "L" else 8), "field range") + return at + (704 if name == "C" else 0) + + +def mapping(packet, label): + record = packet["map_registry"][label] + return tuple(record["owner_right_matrix_columns"]), record["payload_translation_at_identity_owner"] + + +def line(row, item): + """One payload layer only; this two-term formula is not a tensor power.""" + sign, q = item["sign"], item["label"] + return row_add(operate(row, UNIT, (Q(1, 2), Q(sign, 2))), + operate(row, (AXES, q), (Q(1, 2), Q(-sign, 2)))) + + +def flatten(program): + for event in program: + if event[0] == "private_sweep": + yield from event[2] + else: + yield event + + +def replay(packet, program, rows=None): + """Full ordered affine-operator replay at payload tensor length lambda=1.""" + rows = identity() if rows is None else [dict(r) for r in rows] + for e in flatten(program): + at = register(e[1][1] if e[0] == "scalar" else e[1]) + if e[0] == "cover_map": + rows[at] = operate(rows[at], mapping(packet, e[2])) + elif e[0] == "native_line": + rows[at] = line(rows[at], packet["native_line_recipes"][e[2]]) + else: + need(e[0] == "scalar", "known cut event") + gate = e[1] + if gate[0] == "clear": + rows[at] = {} + else: + need(gate[0] == "add", "cut has only ADD/CLEAR") + rows[at] = row_add(rows[at], rows[register(gate[2])], (Q(gate[3], gate[4]), Q(0))) + return rows + + +def physical_shear(packet): + rows = identity() + for a, t in zip(A, T, strict=True): + rows[t] = row_add(rows[t], rows[a]) + rows[112+t] = row_add(rows[112+t], line(rows[a], packet["native_line_recipes"]["inverse_" + str(t)]), neg(ONE)) + return rows + + +def free_replay(program, sheared=False): + """Rational word polynomials in arbitrary noncommuting native/map operators. + + No C_q expansion, tensor specialization, or inverse relation is used. + """ + rows = [{(i, ()): Q(1)} for i in range(712)] + + def merge(row, other, c=Q(1)): + out = dict(row) + for key, value in other.items(): + out[key] = out.get(key, Q(0)) + c*value + if not out[key]: + del out[key] + return out + + def apply(row, tag): + return {(col, (tag,) + word): value for (col, word), value in row.items()} + + if sheared: + for a, t in zip(A, T, strict=True): + rows[t] = merge(rows[t], rows[a]) + rows[112+t] = merge(rows[112+t], apply(rows[a], ("native_line", "inverse_" + str(t))), Q(-1)) + for e in flatten(program): + at = register(e[1][1] if e[0] == "scalar" else e[1]) + if e[0] in ("cover_map", "native_line"): + rows[at] = apply(rows[at], (e[0], e[2])) + else: + need(e[0] == "scalar", "free-operator primitive") + gate = e[1] + if gate[0] == "clear": + rows[at] = {} + else: + need(gate[0] == "add", "free-operator ADD/CLEAR") + rows[at] = merge(rows[at], rows[register(gate[2])], Q(gate[3], gate[4])) + return rows + + +def construct(packet): + original = packet["programs"]["B_1_2"] + out = [] + for a, t, normalization in zip(A, T, original[:8], strict=True): + full, yframe = normalization[3:] + body = [["scalar", ["clear", ["C", 0]], full], + ["scalar", ["add", ["C", 0], ["L", a], 1, 1], full], + ["scalar", ["add", ["L", t], ["C", 0], 1, 1], full], + ["native_line", ["C", 0], "inverse_" + str(t), full, yframe], + ["scalar", ["add", ["L", 112+t], ["C", 0], -1, 1], yframe], + ["scalar", ["clear", ["C", 0]], "f0"]] + out += [["private_sweep", "shear_" + str(t), body, original[12][3]], deepcopy(normalization)] + return out + deepcopy(original[8:80]) + + +def terms(entries): + out = Counter() + for axis, c in entries: + out[axis] = (out[axis] + c) % 4 + return tuple((a, c) for a, c in sorted(out.items()) if a and c) + + +@lru_cache(None) +def polynomial(entries): + linear, cross = [0]*73, [0]*73 + for axis, c in entries: + for i in bits(axis): + linear[i] = (linear[i] + c) % 4 + if c % 2: + for j in bits(axis): + if j > i: + cross[i] ^= 1 << j + return tuple(linear), tuple(cross) + + +def typed(packet, program): + registry = packet["native_frame_registry"] + frames = {k: terms(v["line_terms_Z4"]) for k, v in registry.items()} + for k, frame in frames.items(): + need(polynomial(frame) == (tuple(registry[k]["linear_Z4"]), tuple(registry[k]["quadratic_rows"])), "frame polynomial") + state = [("opaque", i) for i in range(712)] + full = frames["f1"] + for p in A + T: + state[p] = full + q = packet["native_line_recipes"]["inverse_" + str(p)]["label"] + state[112+p] = terms(full + ((q, -1),)) + initial = list(state) + count = Counter() + + def consume(e, private=False): + kind = e[0] + at = register(e[1][1] if kind == "scalar" else e[1]) + need(at < 224 or at == 704 and private, "data/owned C0 destination") + if kind == "cover_map": + need(not private and at in T, "source path outside private sweep") + need(polynomial(state[at]) == polynomial(frames[e[3]]), "map input frame") + g, shift = mapping(packet, e[2]) + state[at] = terms(tuple((act(g, axis), c) for axis, c in state[at]) + tuple((1 << j, 2) for j in bits(shift))) + need(polynomial(state[at]) == polynomial(frames[e[4]]), "map output frame") + count["explicit_cover_maps"] += 1 + elif kind == "native_line": + need(at in T or at == 704 and private, "native field/lifetime") + need(polynomial(state[at]) == polynomial(frames[e[3]]), "native input frame") + item = packet["native_line_recipes"][e[2]] + state[at] = terms(state[at] + ((item["label"], item["sign"]),)) + need(polynomial(state[at]) == polynomial(frames[e[4]]), "native output frame") + count["native_lines"] += 1 + else: + need(kind == "scalar", "typed primitive") + gate = e[1] + if gate[0] == "clear": + need(at == 704 and private, "only owned C0 is cleared") + state[at] = frames[e[2]] + count["clears"] += 1 + else: + need(gate[0] == "add" and gate[4] in (1, 2), "dyadic cut ADD") + source = register(gate[2]) + need(source < 224 or source == 704 and private, "data/owned source") + need(source != at and polynomial(state[source]) == polynomial(state[at]) == polynomial(frames[e[2]]), "equal ADD frames") + count["adds"] += 1 + + for e in program: + if e[0] != "private_sweep": + consume(e) + continue + need(e[3] == packet["programs"]["B_1_2"][12][3], "whole-owner private barrier") + need(e[2][0][:2] == e[2][-1][:2] == ["scalar", ["clear", ["C", 0]]], "private initial/final clears") + for child in e[2]: + consume(child, True) + need(state[704] == (), "C0 returns zero/I per private row") + count["private_sweeps"] += 1 + expected = list(initial) + for t in T: + expected[t] = initial[112+t] + expected[704] = () + need(all((polynomial(x) == polynomial(y) if isinstance(x, tuple) and (not x or isinstance(x[0], tuple)) else x == y) for x, y in zip(state, expected, strict=True)), "all 712 final frame boundaries") + count["native_wrapper_maps"] = 2*count["native_lines"] + # A half ADD has bound10, a unit ADD8, CLEAR2 (complex real-component ledger). + count["scalar_real_primitive_bound"] = sum(2 if e[1][0] == "clear" else (8 if e[1][4] == 1 else 10) for e in flatten(program) if e[0] == "scalar") + return dict(sorted(count.items())) + + +def invariants(packet): + original = packet["programs"]["B_1_2"] + need(packet["A_ports"] == A and packet["T_ports"] == T and packet["field_namespace"]["formal_input_columns"] == 712, "selected namespace") + need(len(original) == 557 and original[80][:3] == ["cover_map", ["L", 112], "m89"], "exact later cut") + maps, labels = [], [] + for e in flatten(original[:80]): + if e[0] == "cover_map": + need(packet["map_registry"][e[2]]["action"] == "out(d,z_1,...,z_lambda)=in(d*g,z_1 XOR d*delta,...,z_lambda XOR d*delta)", "actual full owner/payload action") + g, shift = mapping(packet, e[2]) + need(len(g) == 73 and all(type(x) is int and 0 < x < 1 << 73 for x in g), "map dimensions") + need(all((g[i] & g[j]).bit_count() % 2 == (i == j) for i in range(73) for j in range(73)), "orthogonal owner matrix") + need(act(g, OMEGA) == OMEGA and all(x.bit_count() % 2 == 1 for x in g), "characteristic vector fixed in both directions") + need(type(shift) is int and 0 <= shift < 1 << 73 and shift.bit_count() % 2 == 0, "even payload translation") + maps.append(e[2]) + elif e[0] == "native_line": + item = packet["native_line_recipes"][e[2]] + need(item["rank"] == item["recipe"]["rank"] == 1 and item["sign"] in (-1, 1), "atomic signed rank-one line") + need(item["label"].bit_count() % 2 == 1, "odd native label") + labels.append(item["label"]) + need(len(maps) == 64 and len(labels) == 16, "complete cut inventory") + return {"maps": 64, "odd_lines": 16, "native_labels": labels, "characters": [0, OMEGA]} + + +def physical_check(packet): + """Bind each used signed native line to all 512 actual recipe columns.""" + names = sorted({e[2] for e in flatten(packet["programs"]["B_1_2"][:80]) if e[0] == "native_line"}) + + def mono(recipe, address): + need(len(recipe["matrix_rows"]) == len(recipe["linear_Z4"]) == len(recipe["quadratic_rows"]) == 9, "nine-axis monomial dimensions") + exponent = recipe["phase"] + for j in bits(address): + exponent += recipe["linear_Z4"][j] + 2*(recipe["quadratic_rows"][j] & address).bit_count() + dest = recipe["offset"] + for j, row in enumerate(recipe["matrix_rows"]): + dest ^= ((row & address).bit_count() % 2) << j + need(0 <= dest < 512, "native monomial address") + return dest, ((1, 0), (0, 1), (-1, 0), (0, -1))[exponent % 4] + + for name in names: + item = packet["native_line_recipes"][name] + recipe, q, sign = item["recipe"], item["label"], item["sign"] + need(type(q) is int and 0 < q < 512 and type(sign) is int and sign in (-1, 1), "literal native label/sign") + for address in range(512): + mid, right = mono(recipe["right"], address) + out = {} + for at, coefficient in ((mid, (1, 1)), (mid ^ 1, (1, -1))): + dest, left = mono(recipe["left"], at) + out[dest] = add(out.get(dest, ZERO), mul(mul(right, coefficient), left)) + out = {k: v for k, v in out.items() if v != ZERO} + need(out == {address: (1, sign), address ^ q: (1, -sign)}, "actual native recipe Gaussian column") + return len(names)*512 + + +def evaluate(rows, odd): + out = [] + for row in rows: + r = {} + for (col, (g, shift)), value in row.items(): + need(act(g, OMEGA) == OMEGA, "evaluation preserves covariant character") + sign = -1 if odd and shift.bit_count() % 2 else 1 + r[col] = add(r.get(col, ZERO), mul((Q(sign), Q(0)), value)) + if r[col] == ZERO: + del r[col] + out.append(r) + return out + + +def determinant(matrix): + matrix = [list(row) for row in matrix] + d = ONE + for k in range(len(matrix)): + pivots = [i for i in range(k, len(matrix)) if matrix[i][k] != ZERO] + if not pivots: + return ZERO + p = pivots[0] + if p != k: + matrix[k], matrix[p] = matrix[p], matrix[k] + d = neg(d) + pivot = matrix[k][k] + d = mul(d, pivot) + for i in range(k+1, len(matrix)): + c = div(matrix[i][k], pivot) + for j in range(k+1, len(matrix)): + matrix[i][j] = add(matrix[i][j], neg(mul(c, matrix[k][j]))) + matrix[i][k] = ZERO + return d + + +def load_packet(): + source = load_json((HERE / "SOURCES.json").read_text()) + need(source["base_commit"] == BASE, "source base") + paths = [r["path"] for r in source["files"]] + need(len(paths) == len(set(paths)) and PACKET in paths, "unique source inventory") + for row in source["files"]: + need(row["usage"] in ("input", "provenance"), "source usage") + if row["usage"] == "input": + path = (ROOT / row["path"]).resolve() + need(path.is_relative_to(ROOT), "source path inside repository") + raw = path.read_bytes() + need(hashlib.sha256(raw).hexdigest() == row["sha256"], "source SHA: " + row["path"]) + need(hashlib.sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() == row["git_blob"], "source Git blob") + need(next(r for r in source["files"] if r["path"] == PACKET)["usage"] == "input", "packet is consumed input") + raw = (ROOT / PACKET).read_bytes() + need(hashlib.sha256(raw).hexdigest() == PACKET_SHA, "fixed packet pin") + return load_json(gzip.decompress(raw)) + + +def compute(): + packet = load_packet() + invariant = invariants(packet) + native_columns = physical_check(packet) + original, upper = packet["programs"]["B_1_2"][:80], construct(packet) + baseline_bill, upper_bill = typed(packet, original), typed(packet, upper) + baseline = replay(packet, original) + target = replay(packet, original, physical_shear(packet)) + actual = replay(packet, upper) + need(actual == target, "complete ordered group-affine endpoint, all 712 rows") + free_target = free_replay(original, sheared=True) + need(free_replay(upper) == free_target, "all 712 free noncommuting-operator endpoint rows") + for a, t in zip(A, T, strict=True): + item = packet["native_line_recipes"]["inverse_" + str(t)] + need(baseline[t] == line({(t, UNIT): ONE}, item), "every completed source path restores X_T") + need(actual[t] == line({(t, UNIT): ONE, (a, UNIT): ONE}, item), "complete X_T endpoint") + need(actual[112+t] == physical_shear(packet)[112+t], "complete Y_T endpoint") + changed = set(A + T + [112+t for t in T] + [704]) + need(all(actual[i] == {(i, UNIT): ONE} for i in range(712) if i not in changed), "all fields outside complete endpoint footprint unchanged") + need(all(actual[i] == {(i, UNIT): ONE} for i in range(224, 704)), "all 480 dirty helpers restored") + need(actual[704] == {} and all(actual[i] == {(i, UNIT): ONE} for i in range(705, 712)), "private endpoint C0 zero, C1..7 unchanged") + lo, hi = evaluate(target, False), evaluate(target, True) + rr = [i for t in T for i in (t, 112+t)] + A + cc = [i for a, t in zip(A, T, strict=True) for i in (a, t)] + [112+a for a in A] + minor = [[add(hi[i].get(j, ZERO), neg(lo[i].get(j, ZERO))) for j in cc] for i in rr] + need(determinant(minor) == (Q(4096), Q(0)), "exact rank-24 Gaussian minor") + need([i for i in range(712) if lo[i] != hi[i]] == sorted(rr), "difference has exactly 24 nonzero rows") + blo, bhi = evaluate(baseline, False), evaluate(baseline, True) + br, bc = T + A, T + [112+a for a in A] + need(determinant([[add(bhi[i].get(j, ZERO), neg(blo[i].get(j, ZERO))) for j in bc] for i in br]) != ZERO, "baseline rank-16 minor") + need(sum(x != y for x, y in zip(blo, bhi, strict=True)) == 16, "baseline difference rank exactly 16") + controls = [] + + def reject(name, action): + try: + action() + except (ValueError, KeyError): + controls.append({"name": name, "outcome": "REJECT"}) + else: + raise ValueError("control accepted: " + name) + + def semantic(program, source=packet): + need(replay(source, program) == target, "full endpoint mismatch") + + # At two odd character layers C_q tensor C_q has eigenvalue i*i=-1. + # A two-term simultaneous translation has eigenvalue alpha+beta=1. + simultaneous = add((Q(1, 2), Q(1, 2)), (Q(1, 2), Q(-1, 2))) + tensor = mul((Q(0), Q(1)), (Q(0), Q(1))) + reject("two_layer_simultaneous_translation_substitution", lambda: need( + simultaneous == tensor, "one-layer two-term model differs from native tensor power")) + bad = deepcopy(upper); bad[0][2][3], bad[0][2][4] = bad[0][2][4], bad[0][2][3] + reject("free_operator_late_source_conversion", lambda: need( + free_replay(bad) == free_target, "free-operator order differs before target subtraction")) + bad = deepcopy(upper); bad[0][2][3][2] = "positive_21" + reject("wrong_native_sign", lambda: semantic(bad)) + badp = deepcopy(packet); badp["native_line_recipes"]["inverse_21"]["recipe"]["left"]["phase"] += 1 + reject("native_wrapper_global_phase", lambda: physical_check(badp)) + bad = deepcopy(upper); del bad[0][2][0] + reject("arbitrary_C0_without_initial_clear", lambda: semantic(bad)) + bad = deepcopy(upper); del bad[0][2][-1] + reject("missing_row_boundary_clear", lambda: typed(packet, bad)) + bad = deepcopy(upper); del bad[1] + reject("omitted_X_T_normalization", lambda: semantic(bad)) + bad = deepcopy(upper); bad[0][2][0][1][1] = ["L", 224] + reject("borrowed_helper_clear", lambda: typed(packet, bad)) + bad = deepcopy(upper); bad[0][3] = "interleave owners" + reject("private_owner_barrier", lambda: typed(packet, bad)) + badp = deepcopy(packet); name = original[8][2] + badp["map_registry"][name]["payload_translation_at_identity_owner"] ^= 1 + reject("odd_translation_breaks_invariant", lambda: invariants(badp)) + reject("wrong_translation_full_endpoint", lambda: semantic(upper, badp)) + badp = deepcopy(packet) + for event in original: + if event[0] == "cover_map": + badp["map_registry"][event[2]]["owner_right_matrix_columns"] = list(AXES) + reject("payload_only_owner_route", lambda: semantic(upper, badp)) + bare = physical_shear(packet) + for a, t in zip(A, T, strict=True): + bare[112+t] = row_add({(112+t, UNIT): ONE}, {(a, UNIT): ONE}, neg(ONE)) + reject("bare_Y_subtraction", lambda: need(replay(packet, original, bare) == target, "bare Y shear differs")) + need((baseline_bill["native_lines"], upper_bill["native_lines"]) == (16, 24), "attaining native line invoice") + return {"status": MARKER, "source_boundary": {"base_commit": BASE, "packet_sha256": PACKET_SHA}, + "cut": {"case": "B_1_2", "end_exclusive": 80, "next_event": packet["programs"]["B_1_2"][80][:3]}, + "invoice": {"baseline": baseline_bill, "attaining": upper_bill, "delta": {k: upper_bill[k]-baseline_bill[k] for k in upper_bill}}, + "exact": {"full_operator_rows": 712, "full_operator_rows_scope": "one payload tensor layer (lambda=1)", "free_operator_rows": 712, "free_operator_rows_scope": "arbitrary noncommuting linear native/map operators, no tensor expansion", "native_recipe_basis_columns": native_columns, "dirty_helpers_restored": 480, "private_outputs": "C0 zero; C1..C7 arbitrary unchanged", "minor_rows": rr, "minor_columns": cc, "minor_det": [4096, 0], "rank": 24, "baseline_difference_rank": 16}, + "tensor_scope": {"exact_affine_replay_layers": 1, + "upper_bound": "all integer lambda>=1 by fresh free-operator endpoint equality and the written tensor interpretation", + "lower_bound": "all integer lambda>=1 by one Omega character layer and constant other layers", + "two_layer_odd_odd_counterexample": {"native_tensor_eigenvalue": [-1, 0], "simultaneous_two_term_eigenvalue": [1, 0]}}, + "invariant": invariant, "controls": controls} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-result", type=Path) + args = parser.parse_args() + if args.write_result: + output = args.write_result.resolve() + need(not output.is_relative_to(ROOT) and not output.exists(), "fresh external output only") + result = compute() + if args.write_result: + with output.open("x") as handle: + json.dump(result, handle, sort_keys=True, indent=2) + handle.write("\n") + else: + need(exact(load_json((HERE / "RESULT.json").read_text())) == exact(result), "complete type-exact frozen RESULT") + print(MARKER + " rank=24 baseline_lines=16 attaining_lines=24 controls=" + str(len(result["controls"]))) + + +if __name__ == "__main__": + main()