From 6b2717ce2bbb13c2152e64efea48867b78840bbb Mon Sep 17 00:00:00 2001 From: commdata2338 <199849969+commdata2338@users.noreply.github.com> Date: Thu, 15 Oct 2026 00:28:30 -0500 Subject: [PATCH] Research: the QQ16 shear prefix needs exactly sixteen native lines Prices the initial-prefix part of PR #2252's typed-fusion handoff. After factoring the common completed frame, PR #2216's paired A-to-T shear followed by B1's eight initial X_T inverse-line normalizations has, for each selected pair, the endpoint a' = a, t' = C_q^-1 (t + a), v' = v - C_q^-1 a. At payload characters 0 and 256 every actual q_T has bit 8 set, so each inverse line changes from 1 to -i; the difference of the two transfer matrices contains a 16-by-16 minor of determinant (-1-i)^16 = 256. Free payload-independent scalar gates have zero character difference and each single-field native line has difference rank at most one, so rank telescoping gives at least sixteen lines for any circuit in the model, even with scratch, copies and clears. A typed one-C0 prefix attains sixteen (eight more than inherited), restoring every borrowed helper and clearing C0. Fusion with later B1 operations or cover maps is outside the model; no supplier or kappa change. Adds research/qq16-shear-prefix-cost/ only. Submitted by @commdata2338 with substantial AI assistance (OpenAI Codex research and implementation; packaged with Claude Code). Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01X86sCSXdoDd61SDFfC1PKG --- research/qq16-shear-prefix-cost/PREFIX.json | 802 ++++++++++++++++++ research/qq16-shear-prefix-cost/README.md | 285 +++++++ research/qq16-shear-prefix-cost/RESULT.json | 155 ++++ research/qq16-shear-prefix-cost/SOURCES.json | 48 ++ research/qq16-shear-prefix-cost/TASK.json | 148 ++++ research/qq16-shear-prefix-cost/VERIFY.json | 35 + .../qq16-shear-prefix-cost/test_artifacts.py | 87 ++ research/qq16-shear-prefix-cost/verify.py | 441 ++++++++++ 8 files changed, 2001 insertions(+) create mode 100644 research/qq16-shear-prefix-cost/PREFIX.json create mode 100644 research/qq16-shear-prefix-cost/README.md create mode 100644 research/qq16-shear-prefix-cost/RESULT.json create mode 100644 research/qq16-shear-prefix-cost/SOURCES.json create mode 100644 research/qq16-shear-prefix-cost/TASK.json create mode 100644 research/qq16-shear-prefix-cost/VERIFY.json create mode 100644 research/qq16-shear-prefix-cost/test_artifacts.py create mode 100644 research/qq16-shear-prefix-cost/verify.py diff --git a/research/qq16-shear-prefix-cost/PREFIX.json b/research/qq16-shear-prefix-cost/PREFIX.json new file mode 100644 index 0000000000..750f3d26d8 --- /dev/null +++ b/research/qq16-shear-prefix-cost/PREFIX.json @@ -0,0 +1,802 @@ +[ + [ + "private_sweep", + "shear_prefix_21", + [ + [ + "scalar", + [ + "clear", + [ + "C", + 0 + ] + ], + "f1" + ], + [ + "scalar", + [ + "add", + [ + "C", + 0 + ], + [ + "L", + 0 + ], + 1, + 1 + ], + "f1" + ], + [ + "scalar", + [ + "add", + [ + "L", + 21 + ], + [ + "C", + 0 + ], + 1, + 1 + ], + "f1" + ], + [ + "native_line", + [ + "C", + 0 + ], + "inverse_21", + "f1", + "f23" + ], + [ + "scalar", + [ + "add", + [ + "L", + 133 + ], + [ + "C", + 0 + ], + -1, + 1 + ], + "f23" + ], + [ + "scalar", + [ + "clear", + [ + "C", + 0 + ] + ], + "f0" + ] + ], + "For each cover owner, execute the whole body before the next owner. One ownedC0 is reused." + ], + [ + "native_line", + [ + "L", + 21 + ], + "inverse_21", + "f1", + "f23" + ], + [ + "private_sweep", + "shear_prefix_37", + [ + [ + "scalar", + [ + "clear", + [ + "C", + 0 + ] + ], + "f1" + ], + [ + "scalar", + [ + "add", + [ + "C", + 0 + ], + [ + "L", + 7 + ], + 1, + 1 + ], + "f1" + ], + [ + "scalar", + [ + "add", + [ + "L", + 37 + ], + [ + "C", + 0 + ], + 1, + 1 + ], + "f1" + ], + [ + "native_line", + [ + "C", + 0 + ], + "inverse_37", + "f1", + "f39" + ], + [ + "scalar", + [ + "add", + [ + "L", + 149 + ], + [ + "C", + 0 + ], + -1, + 1 + ], + "f39" + ], + [ + "scalar", + [ + "clear", + [ + "C", + 0 + ] + ], + "f0" + ] + ], + "For each cover owner, execute the whole body before the next owner. One ownedC0 is reused." + ], + [ + "native_line", + [ + "L", + 37 + ], + "inverse_37", + "f1", + "f39" + ], + [ + "private_sweep", + "shear_prefix_47", + [ + [ + "scalar", + [ + "clear", + [ + "C", + 0 + ] + ], + "f1" + ], + [ + "scalar", + [ + "add", + [ + "C", + 0 + ], + [ + "L", + 20 + ], + 1, + 1 + ], + "f1" + ], + [ + "scalar", + [ + "add", + [ + "L", + 47 + ], + [ + "C", + 0 + ], + 1, + 1 + ], + "f1" + ], + [ + "native_line", + [ + "C", + 0 + ], + "inverse_47", + "f1", + "f49" + ], + [ + "scalar", + [ + "add", + [ + "L", + 159 + ], + [ + "C", + 0 + ], + -1, + 1 + ], + "f49" + ], + [ + "scalar", + [ + "clear", + [ + "C", + 0 + ] + ], + "f0" + ] + ], + "For each cover owner, execute the whole body before the next owner. One ownedC0 is reused." + ], + [ + "native_line", + [ + "L", + 47 + ], + "inverse_47", + "f1", + "f49" + ], + [ + "private_sweep", + "shear_prefix_76", + [ + [ + "scalar", + [ + "clear", + [ + "C", + 0 + ] + ], + "f1" + ], + [ + "scalar", + [ + "add", + [ + "C", + 0 + ], + [ + "L", + 27 + ], + 1, + 1 + ], + "f1" + ], + [ + "scalar", + [ + "add", + [ + "L", + 76 + ], + [ + "C", + 0 + ], + 1, + 1 + ], + "f1" + ], + [ + "native_line", + [ + "C", + 0 + ], + "inverse_76", + "f1", + "f78" + ], + [ + "scalar", + [ + "add", + [ + "L", + 188 + ], + [ + "C", + 0 + ], + -1, + 1 + ], + "f78" + ], + [ + "scalar", + [ + "clear", + [ + "C", + 0 + ] + ], + "f0" + ] + ], + "For each cover owner, execute the whole body before the next owner. One ownedC0 is reused." + ], + [ + "native_line", + [ + "L", + 76 + ], + "inverse_76", + "f1", + "f78" + ], + [ + "private_sweep", + "shear_prefix_81", + [ + [ + "scalar", + [ + "clear", + [ + "C", + 0 + ] + ], + "f1" + ], + [ + "scalar", + [ + "add", + [ + "C", + 0 + ], + [ + "L", + 36 + ], + 1, + 1 + ], + "f1" + ], + [ + "scalar", + [ + "add", + [ + "L", + 81 + ], + [ + "C", + 0 + ], + 1, + 1 + ], + "f1" + ], + [ + "native_line", + [ + "C", + 0 + ], + "inverse_81", + "f1", + "f83" + ], + [ + "scalar", + [ + "add", + [ + "L", + 193 + ], + [ + "C", + 0 + ], + -1, + 1 + ], + "f83" + ], + [ + "scalar", + [ + "clear", + [ + "C", + 0 + ] + ], + "f0" + ] + ], + "For each cover owner, execute the whole body before the next owner. One ownedC0 is reused." + ], + [ + "native_line", + [ + "L", + 81 + ], + "inverse_81", + "f1", + "f83" + ], + [ + "private_sweep", + "shear_prefix_87", + [ + [ + "scalar", + [ + "clear", + [ + "C", + 0 + ] + ], + "f1" + ], + [ + "scalar", + [ + "add", + [ + "C", + 0 + ], + [ + "L", + 46 + ], + 1, + 1 + ], + "f1" + ], + [ + "scalar", + [ + "add", + [ + "L", + 87 + ], + [ + "C", + 0 + ], + 1, + 1 + ], + "f1" + ], + [ + "native_line", + [ + "C", + 0 + ], + "inverse_87", + "f1", + "f89" + ], + [ + "scalar", + [ + "add", + [ + "L", + 199 + ], + [ + "C", + 0 + ], + -1, + 1 + ], + "f89" + ], + [ + "scalar", + [ + "clear", + [ + "C", + 0 + ] + ], + "f0" + ] + ], + "For each cover owner, execute the whole body before the next owner. One ownedC0 is reused." + ], + [ + "native_line", + [ + "L", + 87 + ], + "inverse_87", + "f1", + "f89" + ], + [ + "private_sweep", + "shear_prefix_92", + [ + [ + "scalar", + [ + "clear", + [ + "C", + 0 + ] + ], + "f1" + ], + [ + "scalar", + [ + "add", + [ + "C", + 0 + ], + [ + "L", + 57 + ], + 1, + 1 + ], + "f1" + ], + [ + "scalar", + [ + "add", + [ + "L", + 92 + ], + [ + "C", + 0 + ], + 1, + 1 + ], + "f1" + ], + [ + "native_line", + [ + "C", + 0 + ], + "inverse_92", + "f1", + "f94" + ], + [ + "scalar", + [ + "add", + [ + "L", + 204 + ], + [ + "C", + 0 + ], + -1, + 1 + ], + "f94" + ], + [ + "scalar", + [ + "clear", + [ + "C", + 0 + ] + ], + "f0" + ] + ], + "For each cover owner, execute the whole body before the next owner. One ownedC0 is reused." + ], + [ + "native_line", + [ + "L", + 92 + ], + "inverse_92", + "f1", + "f94" + ], + [ + "private_sweep", + "shear_prefix_110", + [ + [ + "scalar", + [ + "clear", + [ + "C", + 0 + ] + ], + "f1" + ], + [ + "scalar", + [ + "add", + [ + "C", + 0 + ], + [ + "L", + 111 + ], + 1, + 1 + ], + "f1" + ], + [ + "scalar", + [ + "add", + [ + "L", + 110 + ], + [ + "C", + 0 + ], + 1, + 1 + ], + "f1" + ], + [ + "native_line", + [ + "C", + 0 + ], + "inverse_110", + "f1", + "f112" + ], + [ + "scalar", + [ + "add", + [ + "L", + 222 + ], + [ + "C", + 0 + ], + -1, + 1 + ], + "f112" + ], + [ + "scalar", + [ + "clear", + [ + "C", + 0 + ] + ], + "f0" + ] + ], + "For each cover owner, execute the whole body before the next owner. One ownedC0 is reused." + ], + [ + "native_line", + [ + "L", + 110 + ], + "inverse_110", + "f1", + "f112" + ] +] diff --git a/research/qq16-shear-prefix-cost/README.md b/research/qq16-shear-prefix-cost/README.md new file mode 100644 index 0000000000..0b3b0922bc --- /dev/null +++ b/research/qq16-shear-prefix-cost/README.md @@ -0,0 +1,285 @@ +# QQ16 shear and initial normalization: exactly sixteen native lines + +The paired A-to-T shear from [PR2216](https://github.com/CrocSwap/integer-mult-bounds/pull/2216), +followed by B1's initial eight X_T normalizations, needs **exactly sixteen +single-field native line calls** in the model below. The inherited prefix +uses eight calls, so this boundary-preserving implementation adds eight. +Arbitrary payload-independent scalar resynthesis, extra scalar registers, +copying and clearing do not lower that minimum. + +This answers the **initial-prefix** part of +[PR2252's typed-fusion handoff](https://github.com/CrocSwap/integer-mult-bounds/pull/2252). +PR2252 already showed that the eight bare Y subtractions have incompatible +frames. It explicitly supplied no line-count lower bound. The result here +does not exclude fusion with later B1 operations or owner/cover maps. +It gives no full controller, admitted supplier or new κ. + +Evidence status: author-checked scoped proof and exact finite certificate; +no independent human review or formal-kernel proof. The selected result is +unchanged. The claim is in [discussion #2205](https://github.com/CrocSwap/integer-mult-bounds/discussions/2205#discussioncomment-18941102). + +## Fixed boundary and cost model + +The actual selected pairs are + +```text +A = [ 0, 7, 20, 27, 36, 46, 57, 111] +T = [21, 37, 47, 76, 81, 87, 92, 110] +q_T = [289, 274, 268, 448, 478, 493, 499, 319]. +``` + +Let `F = completed(0)` and + +```text +C_q = ((1+i) I + (1-i) T_q)/2, (T_q x)(z) = x(z XOR q). +``` + +The retained F0 output has physical `X_p = F x_p` and +`Y_p = F C_q^-1 y_p`. This is the inherited core boundary in +[CONSERVED-QQ16](../joint-query/evidence/CONSERVED-QQ16.md#cover-action-and-native-phases). +The certificate's first eight `B_1_2` events apply `C_q^-1` to X_T; +the audit binds those exact events and checks that F0's wrappers never +write Y_T. It does not independently re-prove the retained core boundary. + +Fix one owner. Factor the common invertible F from **physical** input and +output coordinates; it commutes with every translation line. For pair j, +write `a=F^-1 X_A[j]`, `t=F^-1 X_T[j]`, and `v=F^-1 Y_T[j]`. +Here v is a physical coordinate, equal to `C_q^-1` times logical Y_T. +The required complete prefix is + +```text +a' = a +t' = C_q^-1 (t+a) +v' = v - C_q^-1 a. (1) +``` + +All other data and borrowed helpers are unchanged. One existing **owned** +field C0 may have arbitrary initial contents, which are discarded; it +returns zero/I after each row. No data or borrowed helper is cleared. + +The lower-bound model grants any finite number of scalar registers and +arbitrary linear scalar operations for free, including mixing, copying, +clearing and projections. Their coefficients must be independent of the +payload address/frequency. They act at the same owner and address. Each +atomic `C_q` or `C_q^-1` on one field costs one, for any binary label q; +all intermediate and restoring calls count. This relaxation even permits +scalar operations between incompatible frame types, so its lower bound +applies in particular to the legal typed subclass. + +There are **no explicit owner/cover maps, payload-address permutations or +translations outside the atomic line recipes, frequency-dependent free +coefficients, multi-field native primitives, or fusion past the initial +normalization block**. Splitting native recipes to share their internal +wrappers is also outside the atomic-line model. Their two wrapper maps +are counted separately in the attaining invoice. This is a native-line +count, not a universal lower bound on recursive rank tariffs. + +## Lower bound, including arbitrary scalar scratch + +For binary frequency w, let `chi_w(z)=(-1)^(w dot z)`. Every permitted +operation preserves this character subspace. On it, + +```text +C_q^epsilon = i^(epsilon * (q dot w)), epsilon in {+1,-1}. +``` + +Compare `w=0` with `w=256` (coordinate 8). Every actual q_T above has +bit 8 set, so the eight inverse lines have eigenvalue `c=-i` at 256 and +eigenvalue 1 at zero. In the input order `(a,t,v)`, (1) has matrix + +```text +M(c) = [ 1 0 0 ] + [ c c 0 ] + [-c 0 1 ]. +``` + +Select output rows `(t',v')` and input columns `(a,t)` in +`M(-i)-M(1)`. The resulting two-by-two block is + +```text +d * [ 1 1 ], d=-1-i, + [-1 0 ] +``` + +and has determinant d². The eight disjoint blocks give a 16-by-16 minor +of determinant `d^16 = 256`. Therefore the difference between the two +required transfer matrices has rank at least 16. In fact it has rank 16, +since no other output rows differ. The verifier checks the actual row and +column indices and computes the determinant independently over Q(i). + +For completeness, let `P(w)=G_n(w)...G_1(w)` be any candidate circuit on +a fixed enlarged register set. For its two evaluations, telescoping gives + +```text +P(w)-P(0) = sum_k G_n(w)...G_(k+1)(w) + (G_k(w)-G_k(0)) G_(k-1)(0)...G_1(0). (2) +``` + +A free scalar gate has zero difference. A single-field native line has +difference rank at most one. Multiplication and restriction to the +required input/output coordinates cannot increase rank; subadditivity +in (2) thus gives `rank(P(w)-P(0)) <= number of native lines`. +Nothing uses invertibility of a free gate. Clear, copy and discarded +owned inputs are covered, as are zero-initialized extra fields (restrict +to the original input columns). Padding with unused registers makes any +finite allocation schedule a fixed-size circuit. + +The nonzero minor forces at least sixteen lines. This is a proof for all +finite circuits in the stated model, not a search to a bounded depth. +The zero-character restriction alone sees no line cost; that is precisely +why a payload-constant witness cannot certify the proposed native bill. + +For positive tensor length, take frequency 256 on one payload layer and +zero on the others. For owner d use the dual frequency that pairs with +dq as 256 pairs with q. With no owner mixing the same proof applies to +each fiber. The upper identity below is linear and holds for the inherited +tensor line operators as well. The finite replay checks the nine active +coordinates at identity owner; the extensions use this written argument. + +## Attaining typed prefix and its invoice + +For each pair `(a,t)=(A_j,T_j)`, use one owner-serial private sweep: + +```text +C0 <- 0 in F +C0 += X_a in F +X_t += C0 in F +C0 <- C_q^-1 C0 F -> F C_q^-1 +Y_t -= C0 in F C_q^-1 +C0 <- 0 return to I +``` + +Complete that sweep over all owners, then execute the original +`X_t <- C_q^-1 X_t` normalization. Repeat for the eight disjoint pairs. +Every ADD has exactly equal source/target phase polynomials. The existing +owned C0 is reused, and its row body finishes before the next owner. +No full-cover scratch bank or new field is allocated. All X_A values and +all other fields remain untouched. Direct substitution proves (1). + +[PREFIX.json](PREFIX.json) is the complete literal prefix in the retained +event grammar. [RESULT.json](RESULT.json) records the exact local invoice: + +| Quantity | Attaining prefix | Inherited normalization prefix | +|---|---:|---:| +| Rank-one native line calls | 16 | 8 | +| Native recipe wrapper maps | 32 | 16 | +| Explicit cover maps | 0 | 0 | +| Complex scalar ADDs | 24 | 0 | +| Owned CLEARs | 16 | 0 | +| Private row sweeps | 8 | 0 | +| Scalar real-primitive bound | 224 | 0 | + +The scalar bound uses the pinned QQ16 convention: 8 per unit complex ADD +and 2 per CLEAR. Native children and their wrapper maps are separate +charges, not included in 224. All restoration within this prefix is +included. Replacing the initial eight B1 normalizations by this prefix +preserves the exact frame boundary at which the unchanged suffix starts. +Composition therefore realizes B1 after the logical shear under the +inherited B1 contract; no full B1 replay or global supplier admission is +claimed here. + +The initial target was zero additional native children at this boundary. +The sharp extra-eight requirement rules it out in this model, so no +controller synthesis or moment-improvement claim follows. The result +does not price physical stream/address execution, new child hosting, +complete precision growth, or all-size admission. In particular the old +precision guard must not simply be reused for a changed word. + +## Exact checks and reproduction + +From the repository root, with Python 3.12 and its standard library: + +```sh +python3 -I -B scripts/research_package.py --package research/qq16-shear-prefix-cost +``` + +The main checker prints: + +```text +PASS_QQ16_SHEAR_PREFIX_COST minimum_lines=16 inherited=8 additional=8 characters=512 inputs=712 controls=14 +``` + +The registered replay also runs artifact-integrity controls. Direct replay: + +```sh +python3 -I -O -B research/qq16-shear-prefix-cost/verify.py +``` + +Checks comprise: + +- all 712 formal input/output fields at every one of the 512 characters + (364,544 sparse output rows), including arbitrary initial C0 and every + borrowed helper; +- exact native frame equality, sweep barriers, C0 lifetime and the complete + event invoice; +- 4,096 computational-basis columns of the eight actual inverse-line + recipes, checking their monomial wrappers against the translation kernel; +- a separate address-convolution interpreter for the 25 affected input + fields at address zero, whose translation-equivariant identity covers + their 12,800 shifted basis inputs; untouched fields are literal identity; +- the Gaussian minor, whose determinant is 256; the difference-rank + histogram over all characters is `{0:32, 8:448, 16:32}`; +- fourteen controls, including wrong native sign/phase, equal-frame wrong + source, omitted conversion, uncleared scratch, missing endpoint/lifetime + obligations and the constant-payload blind spot. Thirteen reject a + malformed claim; the blind-spot control deliberately passes only on the + constant subspace. + +The verifier imports no predecessor executable and does not regenerate +sources. `--write-results` explicitly regenerates only this package's +PREFIX/RESULT artifacts. Source and receipt corruption checks, typed JSON +changes and a Git-free read-only optimized replay are in +[test_artifacts.py](test_artifacts.py). + +## Provenance and scope selection + +Scientific base: `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. +[SOURCES.json](SOURCES.json) pins every consumed main file by Git blob and +SHA-256. [TASK.json](TASK.json) records priority revision 4 and the scope +change from the suggested centre-path-sharing card to this concrete +native overhead in a centre-free replacement interface. This is a +necessary-interface side result, not completion of that card's supplier +acceptance gate. The original nonce was +`65caf5d8d22a40513a218a490c257348`; no new randomized selection was used. + +Predecessors, with exact inspected heads: + +- Ali Romman's retained [PR1969](https://github.com/CrocSwap/integer-mult-bounds/pull/1969), + `a6e6ad3936f67b8f63b5b68c5e75d540610a65e7`: QQ16 maps, native grammar, + line recipes, owned scratch and inherited core/Clifford/owner lineage. +- Cinna Davis's [PR2216](https://github.com/CrocSwap/integer-mult-bounds/pull/2216), + `b80e9ba43367fb8b20877a97da1cb677c34f9264`: the logical shear and its + separately scoped payload-constant witness. That rank result is not + re-certified or refuted here. +- Charles Bethin's [PR2252](https://github.com/CrocSwap/integer-mult-bounds/pull/2252), + `6dd49c2b186e08ef1f3efd08f62e1add97ff04a3`: the native-frame correction + and explicit typed-fusion handoff. Its counterexample is credited; + the new result is a sharp prefix cost and a legal attaining word. +- Cinna Davis's nearby [PR2268](https://github.com/CrocSwap/integer-mult-bounds/pull/2268), + `daf44bfc752a5e89127defa1cb296210708cf7e6`: a further ordinary-source + tap. Its observation kernel and full-tail behavior are outside this + package; no tap search was performed. + +Pending PRs supply context, not executable dependencies or supplier +admission. The native semantic and monomial checks follow the credited +retained methods in a separate implementation. All source packages and +their licenses/notices remain unchanged. New material is Apache-2.0. + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. + +## Open next questions + +1. Can fusion **past** the first eight normalizations use later B1 native + operations to realize the shear with no additional calls? It matters + because those operations are excluded from the fixed endpoint here. + First choose one later cut and derive its complete physical transfer, + including arbitrary helper outputs, before searching. The blocker is + that its later cover maps invalidate the two-character local invariant. +2. Can a different useful controller change avoid this prefix endpoint + altogether? First demand full selected-input recovery on arbitrary data + and an explicitly typed boundary; then count children, maps, storage, + restoration, precision and hosting. Witness separation alone does not + establish that recovery, and this package supplies neither a controller + nor its completed budget. + +The structured versions and stopping tests are in TASK.json. diff --git a/research/qq16-shear-prefix-cost/RESULT.json b/research/qq16-shear-prefix-cost/RESULT.json new file mode 100644 index 0000000000..aa8d7cc199 --- /dev/null +++ b/research/qq16-shear-prefix-cost/RESULT.json @@ -0,0 +1,155 @@ +{ + "additional_lines": 8, + "controls": [ + "omitted_scratch_inverse_types", + "omitted_scratch_inverse_semantics", + "constant_payload_blind_spot_reproduced", + "wrong_native_sign", + "equal_frame_wrong_source", + "uncleared_arbitrary_scratch", + "scratch_not_zero_at_row_boundary", + "missing_inherited_X_normalization", + "wrong_Y_subtraction_sign", + "private_lifetime_barrier", + "native_wrapper_global_phase", + "prefix_boundary_binding", + "missing_Y_obligation_destroys_minor", + "constant_character_cannot_certify_bound" + ], + "coverage": { + "affected_physical_basis_columns_by_translation": 12800, + "borrowed_helpers_restored": 480, + "characters": 512, + "field_character_rows": 364544, + "identity_fields_outside_footprint": 687, + "input_fields": 712, + "native_recipe_basis_columns": 4096, + "output_fields": 712, + "owned_scratch_fields": 1, + "participating_fields": 25, + "untouched_fields": 695 + }, + "inherited_prefix_lines": 8, + "invoice": { + "adds": 24, + "clears": 16, + "explicit_cover_maps": 0, + "native_lines": 16, + "native_wrapper_maps": 32, + "private_sweeps": 8, + "scalar_real_primitive_bound": 224 + }, + "lower_bound": { + "characters": [ + 0, + 256 + ], + "determinant_gaussian": [ + 256, + 0 + ], + "difference_rank_histogram": { + "0": 32, + "16": 32, + "8": 448 + }, + "minor_columns": [ + 0, + 21, + 7, + 37, + 20, + 47, + 27, + 76, + 36, + 81, + 46, + 87, + 57, + 92, + 111, + 110 + ], + "minor_rows": [ + 21, + 133, + 37, + 149, + 47, + 159, + 76, + 188, + 81, + 193, + 87, + 199, + 92, + 204, + 110, + 222 + ], + "rank": 16 + }, + "native_line_minimum": 16, + "scope": "Fixed shear-plus-initial-normalization endpoint; atomic single-field native lines; no cover maps or later B1 fusion. No supplier, full controller, precision admission or kappa claim.", + "status": "PASS_QQ16_SHEAR_PREFIX_COST", + "targets": [ + { + "A_port": 0, + "T_port": 21, + "X_frame": "f1", + "Y_frame": "f23", + "q": 289 + }, + { + "A_port": 7, + "T_port": 37, + "X_frame": "f1", + "Y_frame": "f39", + "q": 274 + }, + { + "A_port": 20, + "T_port": 47, + "X_frame": "f1", + "Y_frame": "f49", + "q": 268 + }, + { + "A_port": 27, + "T_port": 76, + "X_frame": "f1", + "Y_frame": "f78", + "q": 448 + }, + { + "A_port": 36, + "T_port": 81, + "X_frame": "f1", + "Y_frame": "f83", + "q": 478 + }, + { + "A_port": 46, + "T_port": 87, + "X_frame": "f1", + "Y_frame": "f89", + "q": 493 + }, + { + "A_port": 57, + "T_port": 92, + "X_frame": "f1", + "Y_frame": "f94", + "q": 499 + }, + { + "A_port": 111, + "T_port": 110, + "X_frame": "f1", + "Y_frame": "f112", + "q": 319 + } + ] +} diff --git a/research/qq16-shear-prefix-cost/SOURCES.json b/research/qq16-shear-prefix-cost/SOURCES.json new file mode 100644 index 0000000000..94bb7ed778 --- /dev/null +++ b/research/qq16-shear-prefix-cost/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/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/NATIVE-REVIEW.md", + "usage": "input", + "git_blob": "525b38dbdefed0e8192a9c5165e802136cc05034", + "sha256": "2247e3cbe73f3f0da55c647ffae15f98dd9445b2366ba9e255b9bebc9f742b70" + }, + { + "path": "research/joint-query/verify_native.py", + "usage": "input", + "git_blob": "ede9e7e42744dd0c96790516a9acdfe07d180018", + "sha256": "1c58e7b6e8e1cde4df455c2129601c145ed763fc63a3ab427eb1058d1fc08bd2" + }, + { + "path": "research/joint-query/verify_scalar.py", + "usage": "input", + "git_blob": "7a7051fa8a70f48589fa1fccd5c38fccb5eacbf7", + "sha256": "33bdbad17a0531fe527aff306eb235d9c38c1629db4fd167b989725930b0327a" + } + ] +} diff --git a/research/qq16-shear-prefix-cost/TASK.json b/research/qq16-shear-prefix-cost/TASK.json new file mode 100644 index 0000000000..c780af1bcb --- /dev/null +++ b/research/qq16-shear-prefix-cost/TASK.json @@ -0,0 +1,148 @@ +{ + "schema_version": 1, + "task_id": "centre-path-sharing", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "centre-path-sharing", + "question": "Can the 64-per-call centre path (eight rank-8 COPY/ERASE totals through the private temporary) be shared across calls or shrunk?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt", + "certificates/selected-result.json" + ], + "methods": [ + "Derive a fully charged favorable relaxation for sharing one centre path across k calls, including restoration, hosting and precision.", + "Prove a lower bound on copied information per call for the selected decoder contract." + ], + "acceptance_gate": "Show the changed centre charge and copy profile per call with every added restoration or hosting cost charged, and its ceiling via ceiling.ceiling(centre=...).", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write the per-call centre charge and copy children for sharing across k = 2 calls, charge the sharing overhead, and screen it; stop this route if even the ideal sharing gains under 10%. Ideal budgets: free 2.80x, shared by two 1.90x (levers.py).", + "bottleneck_link": "The centre path consumes 64 of about 99.6 unpaid coordinates per call, i.e. about 64% of the raw deficit.", + "allowed_variations": [ + "One sharing pattern across a fixed number of calls.", + "One reduced copied-total contract for the existing decoder.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Removing copies without a replacement contract for the decoder's copied totals." + ], + "overlap_terms": [ + "centre path", + "copied totals", + "private temporary", + "shared centre", + "batching" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact native-line cost of the QQ16 A-to-T shear followed by B1's initial eight X_T inverse-line normalizations, with its complete data/borrowed-helper endpoint fixed and one clearable owned C0.", + "scope_change_reason": "Take PR2252's concrete typed-fusion handoff as a native-overhead side result for the centre-free QQ16 replacement. This is neither the incumbent centre source-rank problem nor a complete controller/supplier acceptance claim. Restrict fusion to the initial normalization prefix; allow arbitrary payload-independent scalar resynthesis in the lower-bound relaxation.", + "bottleneck_link": "A centre-free local interface helps only after all typed observation/restoration work is paid. The proposed shear's eight missing Y conversions cannot be absorbed into the inherited eight-line prefix: its sharp cost is sixteen. This necessary-interface cost closes one zero-additional-child route; it supplies no new moment or kappa.", + "budget_minutes": 60, + "stop_rule": "Stop the prefix-only zero-added-child route when a source-bound lower bound exceeds the inherited eight lines. Match the bound with a typed prefix if possible, then hand off larger-cut fusion without beginning a controller search.", + "outcome": "completed", + "evidence": "README.md proves the arbitrary-circuit two-character rank bound; PREFIX.json supplies a legal attaining word; RESULT.json records minimum 16, extra 8, exact determinant 256, 512 characters x 712 output forms,4096 actual recipe columns and fourteen controls. A separate physical convolution check covers 12800 affected basis columns by translation. test_artifacts.py rejects source/typed artifact corruption and replays a read-only Git-free export under -O.", + "author": "commdata2338", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematical derivation, code, verification and writing. Author-checked only; no independent human review or formal proof.", + "open_questions": [ + { + "question": "Can fusion past the first eight normalizations use later B1 native operations without additional calls?", + "why_it_matters": "This could escape the proved fixed-prefix endpoint and its eight extra lines.", + "first_step": "Choose one later B1 cut, derive every physical data/helper output and test a complete typed candidate; stop if its favorable charged bill already loses.", + "blocked_by": "Later cover maps mix the owner/frequency sectors used by the local lower bound; their full endpoint and invoice must be analyzed afresh." + }, + { + "question": "Can another useful controller change avoid this fixed shear-prefix endpoint?", + "why_it_matters": "Witness separation alone need not supply arbitrary selected-input recovery or a favorable centre-free replacement.", + "first_step": "Specify complete observations and typed endpoint, test arbitrary-input recovery, then charge every native call, map, storage, restoration and precision cost.", + "blocked_by": "No full controller or admitted global implementation is supplied here." + } + ], + "assignment_nonce": "65caf5d8d22a40513a218a490c257348", + "track": "recursive-interfaces", + "scope_key": "a55534776f5479f1686c", + "refined_scope_key": "QQ16/F0-B12/shear-plus-initial-normalization/no-cover-map/native-line-minimum", + "result_kind": "scoped-proof-with-finite-certificate", + "original_suggestions": [ + { + "task_id": "coverage-law-change", + "scope_key": "f383d8fc405ee6982cdd" + }, + { + "task_id": "centre-path-sharing", + "scope_key": "a55534776f5479f1686c" + }, + { + "task_id": "joint-query-controller", + "scope_key": "0e34adbc1dd119161c3a" + } + ], + "predecessors": [ + { + "pr": 1969, + "head": "a6e6ad3936f67b8f63b5b68c5e75d540610a65e7", + "author": "Ali Romman", + "role": "Retained main QQ16/native contract; scientific files pinned in SOURCES.json." + }, + { + "pr": 2216, + "head": "b80e9ba43367fb8b20877a97da1cb677c34f9264", + "author": "Cinna Davis", + "role": "Logical shear; contextual, no executable dependency." + }, + { + "pr": 2252, + "head": "6dd49c2b186e08ef1f3efd08f62e1add97ff04a3", + "author": "Charles Bethin", + "role": "Native-frame correction and typed-fusion handoff; contextual, no executable dependency." + }, + { + "pr": 2268, + "head": "daf44bfc752a5e89127defa1cb296210708cf7e6", + "author": "Cinna Davis", + "role": "Adjacent ordinary-source tap; no tap/kernel result claimed or code used." + } + ], + "local_task_card": { + "object_and_question": "Can the paired logical shear plus the inherited initial B1 normalization block be realized using only eight native lines? What is the exact minimum in a payload-independent, owner-local scalar circuit?", + "restriction_changed": "Permit legal native adaptation and arbitrary scalar resynthesis in place of the already refuted bare-scalar shear, preserving the named prefix data/helper endpoint.", + "method_and_domain": "Two Fourier characters, exact Gaussian minor and general rank telescoping; any finite scalar scratch/copy/clear schedule, atomic C_q or inverse on one field, no cover maps or later B1 operations. Actual eight A/T pairs and all 512 active characters; complete 712-field transfer.", + "nearest_overlap_and_delta": "PR2252 provides native mismatch witnesses without a line-count bound. PR2216 provides one constant-payload witness separation, not typed fusion. The new result is a sharp 16-line prefix bound and an attaining typed word; full controller kernels remain separate.", + "optimistic_budget": "Target eight lines total, zero additional calls beyond the inherited prefix. Actual minimum 16; attaining invoice 24 complex ADDs, 16 CLEARs, 32 internal wrapper maps, zero explicit cover maps, one existing owned C0. No complete supplier budget inferred.", + "success_and_falsification": "Nonzero actual 16-by-16 minor plus matching legal word. Wrong native sign, phase, source, scratch restoration, boundary, character or observation must reject. Stop outside this finite prefix boundary.", + "artifact_and_command": "python3 -I -B scripts/research_package.py --package research/qq16-shear-prefix-cost" + }, + "limitations": [ + "Retained F0/core output contract and native primitive admission inherited, not independently cold-replayed.", + "No owner/cover maps, free payload-address operations, native-wrapper sharing or fusion past the initial eight normalizations in the lower-bound model.", + "No full controller injectivity, ordinary-source tap search, full B1 replay, child hosting, physical address cost, complete precision or all-size admission.", + "No selected-supplier/profile update or new kappa." + ], + "freshness_checkpoint": { + "utc": "2026-10-15T05:16:25Z", + "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "changes_since_base": "None; AGENTS.md, autoresearch.md, catalogue, selected record and scientific inputs unchanged. Continue on the frozen base.", + "open_pr_snapshot": "2026-10-15T05:15:02.657475+00:00", + "discussion_snapshot": "2026-10-15T05:18:03.093031+00:00", + "overlap_limitation": "Complete cached pagination; read-only snapshot may miss newer changes. No matching prefix-cost result found.", + "final_overlap_utc": "2026-10-15T05:19:13Z" + }, + "verification_environment": { + "implementation": "CPython", + "python": "3.12.3", + "dependencies": "standard library only", + "parallel_workers": 1 + }, + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2205#discussioncomment-18941102" +} diff --git a/research/qq16-shear-prefix-cost/VERIFY.json b/research/qq16-shear-prefix-cost/VERIFY.json new file mode 100644 index 0000000000..bcc5aeea79 --- /dev/null +++ b/research/qq16-shear-prefix-cost/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/joint-query/certificate.json.gz", + "research/joint-query/evidence/CONSERVED-QQ16.md", + "research/joint-query/evidence/NATIVE-REVIEW.md", + "research/joint-query/verify_native.py", + "research/joint-query/verify_scalar.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Actual boundary/source binding; complete character transfer; independent physical recipe and convolution checks; exact native-line minimum and local invoice; fourteen semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_artifacts.py" + ], + "timeout_seconds": 120, + "checks": "Git-free read-only optimized source export and rejection of corrupted source, typed receipt and typed prefix artifacts." + } + ] +} diff --git a/research/qq16-shear-prefix-cost/test_artifacts.py b/research/qq16-shear-prefix-cost/test_artifacts.py new file mode 100644 index 0000000000..10fa3d6f88 --- /dev/null +++ b/research/qq16-shear-prefix-cost/test_artifacts.py @@ -0,0 +1,87 @@ +#!/usr/bin/env python3 +"""Portable artifact-integrity controls for the QQ16 prefix certificate.""" + +import gzip +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def run(package, wanted): + result = subprocess.run([sys.executable, "-I", "-O", "-B", str(package / "verify.py")], + cwd=package.parents[1], text=True, capture_output=True, timeout=60) + text = result.stdout + result.stderr + need((result.returncode == 0) == (wanted == "PASS_QQ16_SHEAR_PREFIX_COST"), text) + need(wanted in text, "missing expected result: " + wanted + "\n" + text) + + +def main(): + with tempfile.TemporaryDirectory(prefix="qq16-prefix-artifacts-") as temporary: + export = Path(temporary) + package = export / "research" / HERE.name + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns("__pycache__")) + manifest = json.loads((HERE / "SOURCES.json").read_text()) + for entry in manifest["files"]: + if entry["usage"] == "input": + target = export / entry["path"] + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copy2(ROOT / entry["path"], target) + files = sorted(p for p in export.rglob("*") if p.is_file()) + before = {str(p.relative_to(export)): hashlib.sha256(p.read_bytes()).hexdigest() for p in files} + directories = sorted([export] + [p for p in export.rglob("*") if p.is_dir()], + key=lambda p: len(p.parts), reverse=True) + try: + for p in files: + p.chmod(0o444) + for p in directories: + p.chmod(0o555) + run(package, "PASS_QQ16_SHEAR_PREFIX_COST") + after = {str(p.relative_to(export)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in export.rglob("*") if p.is_file()} + need(before == after, "read-only export changed or created files") + finally: + for p in directories: + p.chmod(0o755) + for p in files: + p.chmod(0o644) + + source = export / "research/joint-query/certificate.json.gz" + original = source.read_bytes() + packet = json.loads(gzip.decompress(original)) + packet["native_line_recipes"]["inverse_21"]["label"] ^= 1 + source.write_bytes(gzip.compress(json.dumps(packet).encode(), mtime=0)) + run(package, "source pin:") + source.write_bytes(original) + + receipt = package / "RESULT.json" + original = receipt.read_bytes() + data = json.loads(original) + data["coverage"]["owned_scratch_fields"] = True # Python True == 1 must not pass. + receipt.write_text(json.dumps(data)) + run(package, "complete frozen receipt") + receipt.write_bytes(original) + + prefix = package / "PREFIX.json" + original = prefix.read_bytes() + data = json.loads(original) + data[0][2][1][1][3] = True # Same arithmetic value, different artifact type. + prefix.write_text(json.dumps(data)) + run(package, "complete frozen prefix instructions") + prefix.write_bytes(original) + print("PASS_QQ16_PREFIX_ARTIFACTS relocated_readonly_optimized=1 source_and_typed_artifact_rejections=3") + + +if __name__ == "__main__": + main() diff --git a/research/qq16-shear-prefix-cost/verify.py b/research/qq16-shear-prefix-cost/verify.py new file mode 100644 index 0000000000..e959d2d061 --- /dev/null +++ b/research/qq16-shear-prefix-cost/verify.py @@ -0,0 +1,441 @@ +#!/usr/bin/env python3 +"""Exact QQ16 shear-plus-normalization prefix certificate. Apache-2.0. + +Prepared for commdata2338 with substantial OpenAI Codex assistance. +Ali Romman supplies the retained QQ16 interface and native recipes; Cinna +Davis supplies the logical shear; Charles Bethin identifies its frame gap. +No predecessor executable is imported. See README.md for the cost model. +""" + +import argparse +from collections import Counter +from copy import deepcopy +from fractions import Fraction as Q +import gzip +import hashlib +import json +from pathlib import Path + +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] +SIZE, SCRATCH = 712, 704 +ZERO, ONE = (0, 0), (1, 0) +UNITS = (ONE, (0, 1), (-1, 0), (0, -1)) +BARRIER = ("For each cover owner, execute the whole body before the next owner. " + "One ownedC0 is reused.") +MARKER = "PASS_QQ16_SHEAR_PREFIX_COST" + + +def exact_json(value): + """Preserve JSON scalar types when comparing proof-relevant artifacts.""" + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def add(x, y): + return x[0] + y[0], x[1] + y[1] + + +def mul(x, y): + return x[0]*y[0] - x[1]*y[1], x[0]*y[1] + x[1]*y[0] + + +def neg(x): + return -x[0], -x[1] + + +def divide(x, y): + d = y[0]*y[0] + y[1]*y[1] + need(d != 0, "nonzero Gaussian pivot") + return Q(x[0]*y[0] + x[1]*y[1], d), Q(x[1]*y[0] - x[0]*y[1], d) + + +def determinant(matrix): + """Exact elimination over Q(i), independently of the block formula.""" + rows, result = deepcopy(matrix), ONE + for col in range(len(rows)): + pivot = next((i for i in range(col, len(rows)) if rows[i][col] != ZERO), None) + if pivot is None: + return ZERO + if pivot != col: + rows[col], rows[pivot] = rows[pivot], rows[col] + result = neg(result) + entry = rows[col][col] + result = mul(result, entry) + for i in range(col + 1, len(rows)): + if rows[i][col] != ZERO: + factor = divide(rows[i][col], entry) + rows[i] = [add(x, neg(mul(factor, y))) + for x, y in zip(rows[i], rows[col], strict=True)] + return result + + +def row_add(left, right, coefficient=ONE): + result = dict(left) + for column, value in right.items(): + result[column] = add(result.get(column, ZERO), mul(coefficient, value)) + if result[column] == ZERO: + del result[column] + return result + + +def field(token): + need(isinstance(token, list) and len(token) == 2, "field token") + name, index = token + need(type(index) is int and name in ("L", "C"), "field name/index") + need(0 <= index < (704 if name == "L" else 8), "field range") + return index + (704 if name == "C" else 0) + + +def phase(frame, w): + exponent = sum(c for i, c in enumerate(frame["linear_Z4"]) if (w >> i) & 1) + exponent += 2 * sum((row & w).bit_count() for i, row in enumerate(frame["quadratic_rows"]) + if (w >> i) & 1) + return exponent % 4 + + +def line_phase(item, w): + return (item["sign"] * ((item["label"] & w).bit_count() % 2)) % 4 + + +def flatten(program): + for event in program: + if event[0] in ("private_sweep", "cover_sweep"): + yield from flatten(event[2]) + else: + yield event + + +def load_packet(root): + for entry in json.loads((HERE / "SOURCES.json").read_text())["files"]: + if entry["usage"] == "input": + need(hashlib.sha256((root / entry["path"]).read_bytes()).hexdigest() == entry["sha256"], + "source pin: " + entry["path"]) + return json.loads(gzip.decompress((root / "research/joint-query/certificate.json.gz").read_bytes())) + + +def bind(packet): + need(packet["A_ports"] == A and packet["T_ports"] == T, "selected A/T partition") + need(packet["field_namespace"]["formal_input_columns"] == SIZE, "all 712 inputs") + prefix, frames = packet["programs"]["B_1_2"][:8], packet["native_frame_registry"] + full = prefix[0][3] + need(frames[full]["line_terms_Z4"] == [[1 << j, 1] for j in range(9)], "completed(0) frame") + zero = next(k for k, v in frames.items() if v["line_terms_Z4"] == []) + targets = [] + for a, t, event in zip(A, T, prefix, strict=True): + need(event[:3] == ["native_line", ["L", t], "inverse_" + str(t)], "B1 prefix order") + item = packet["native_line_recipes"][event[2]] + need(item["sign"] == -1 and item["port"] == t, "inverse port recipe") + need(item["rank"] == item["recipe"]["rank"] == 1, "one child per line") + need(0 < item["label"] < 512 and item["label"] & 256, "common odd character") + need(event[3] == full, "initial X_T frame") + need(all(axis < 512 for axis, _ in frames[event[4]]["line_terms_Z4"]), "no spectator phase") + for w in range(512): + direct = sum(c*((axis & w).bit_count() % 2) for axis, c in frames[event[4]]["line_terms_Z4"]) % 4 + need(direct == phase(frames[event[4]], w), "stored frame polynomial") + need((direct - phase(frames[full], w)) % 4 == line_phase(item, w), "Y_T inverse-line type") + targets.append({"A_port": a, "T_port": t, "q": item["label"], + "X_frame": full, "Y_frame": event[4]}) + need(packet["programs"]["F_0"][0][:3] == ["retained_core", "forward", 0], "F0 core first") + # Inherited core output contract; this checks only the retained F0 wrappers. + for event in flatten(packet["programs"]["F_0"][1:]): + token = event[1][1] if event[0] == "scalar" else event[1] + need(field(token) not in [112 + p for p in T], "F0 wrappers leave Y_T unchanged") + return full, zero, targets + + +def construct(packet, full, zero): + program = [] + for a, t, normalization in zip(A, T, packet["programs"]["B_1_2"][:8], strict=True): + yframe = normalization[4] + 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]], zero], + ] + program += [["private_sweep", "shear_prefix_" + str(t), body, BARRIER], deepcopy(normalization)] + return program + + +def typed_check(packet, program, full, zero): + """Exact phase types, owned lifetime and every spectator boundary.""" + frames = {key: tuple(phase(value, w) for w in range(512)) + for key, value in packet["native_frame_registry"].items() + if key in {full, zero} | {e[4] for e in packet["programs"]["B_1_2"][:8]}} + state = [("opaque", i) for i in range(SIZE)] + state[:112] = [frames[full]] * 112 + for t, event in zip(T, packet["programs"]["B_1_2"][:8], strict=True): + state[112+t] = frames[event[4]] + state[SCRATCH] = frames[zero] + expected = list(state) + for t in T: + expected[t] = state[112+t] + counts = Counter() + + def consume(event, private): + if event[0] == "native_line": + _, token, name, old, new = event + i = field(token) + need(i in T or i == SCRATCH and private, "line field/lifetime") + need(state[i] == frames[old], "line input type") + item = packet["native_line_recipes"][name] + state[i] = tuple((p + line_phase(item, w)) % 4 for w, p in enumerate(state[i])) + need(state[i] == frames[new], "line output type") + counts["native_lines"] += 1 + return + need(event[0] == "scalar", "no maps, core or hidden primitive") + _, gate, name = event + i = field(gate[1]) + if gate[0] == "clear": + need(i == SCRATCH and private, "only owned C0 may be cleared") + state[i] = frames[name] # Zero admits the declared frame. + counts["clears"] += 1 + else: + need(gate[0] == "add" and gate[3] in (-1, 1) and gate[4] == 1, "unit scalar ADD") + j = field(gate[2]) + need(i != j and i in T + [112+t for t in T] + [SCRATCH], "ADD destination") + need(j in A + [SCRATCH], "unchanged source or owned C0") + need((i != SCRATCH and j != SCRATCH) or private, "scratch lifetime") + need(state[i] == state[j] == frames[name], "equal full native ADD frames") + counts["adds"] += 1 + + for event in program: + if event[0] != "private_sweep": + consume(event, False) + continue + need(event[3] == BARRIER, "whole row before next owner") + body = event[2] + need(body[0][:2] == body[-1][:2] == ["scalar", ["clear", ["C", 0]]], "owned lifetime clears") + for op in body: + consume(op, True) + need(state[SCRATCH] == expected[SCRATCH], "scratch zero/I each row") + counts["private_sweeps"] += 1 + need(state == expected, "all 712 endpoint types") + counts["native_wrapper_maps"] = 2 * counts["native_lines"] + counts["explicit_cover_maps"] = 0 + # Pinned verify_scalar.py: unit complex ADD costs 8 real primitives; CLEAR 2. + counts["scalar_real_primitive_bound"] = 8*counts["adds"] + 2*counts["clears"] + return dict(sorted(counts.items())) + + +def transfer(packet, program, w): + rows = [{i: ONE} for i in range(SIZE)] + for event in flatten(program): + if event[0] == "native_line": + i = field(event[1]) + value = UNITS[line_phase(packet["native_line_recipes"][event[2]], w)] + rows[i] = {j: mul(c, value) for j, c in rows[i].items()} + else: + need(event[0] == "scalar", "local character replay") + gate, i = event[1], field(event[1][1]) + rows[i] = {} if gate[0] == "clear" else row_add(rows[i], rows[field(gate[2])], (gate[3], 0)) + return rows + + +def desired(packet, w): + rows = [{i: ONE} for i in range(SIZE)] + for a, t in zip(A, T, strict=True): + q = packet["native_line_recipes"]["inverse_" + str(t)]["label"] + c = (0, -1) if (q & w).bit_count() % 2 else ONE + rows[t] = {t: c, a: c} + rows[112+t] = {112+t: ONE, a: neg(c)} + rows[SCRATCH] = {} + return rows + + +def minor_difference(first, second): + columns = [i for pair in zip(A, T, strict=True) for i in pair] + rows = [i for t in T for i in (t, 112+t)] + return [[add(first[i].get(j, ZERO), neg(second[i].get(j, ZERO))) for j in columns] for i in rows] + + +def mono(recipe, address): + """Stored monomial action on a computational basis ket.""" + exponent, output = recipe["phase"], recipe["offset"] + for j in range(9): + if address & (1 << j): + exponent += recipe["linear_Z4"][j] + 2*(recipe["quadratic_rows"][j] & address).bit_count() + for j, row in enumerate(recipe["matrix_rows"]): + output ^= ((row & address).bit_count() % 2) << j + return output, UNITS[exponent % 4] + + +def recipe_column(recipe, address): + """Twice a physical column: right monomial, C_e0, left monomial.""" + middle, right = mono(recipe["right"], address) + out = {} + for target, coefficient in ((middle, (1, 1)), (middle ^ 1, (1, -1))): + destination, left = mono(recipe["left"], target) + out[destination] = add(out.get(destination, ZERO), mul(mul(right, coefficient), left)) + return {i: c for i, c in out.items() if c != ZERO} + + +def physical_check(packet): + count = 0 + for t in T: + item = packet["native_line_recipes"]["inverse_" + str(t)] + for z in range(512): + need(recipe_column(item["recipe"], z) == {z: (1, -1), z ^ item["label"]: (1, 1)}, + "actual recipe equals inverse line on every basis input") + count += 1 + return count + + +def physical_prefix_check(packet, program): + """Separate address-convolution engine; no character phases are used. + + Check 25 input fields at address zero. Translation equivariance proves + the 512 shifts of each check; all unaffected fields are literal identity. + """ + affected = A + T + [112+t for t in T] + [SCRATCH] + for column in affected: + fields = {i: ({0: ONE} if i == column else {}) for i in affected} + for op in flatten(program): + if op[0] == "native_line": + i, item = field(op[1]), packet["native_line_recipes"][op[2]] + row = {} + for z, value in fields[i].items(): + row[z] = add(row.get(z, ZERO), mul(value, (Q(1, 2), Q(item["sign"], 2)))) + other = z ^ item["label"] + row[other] = add(row.get(other, ZERO), mul(value, (Q(1, 2), Q(-item["sign"], 2)))) + fields[i] = {z: v for z, v in row.items() if v != ZERO} + else: + gate, i = op[1], field(op[1][1]) + fields[i] = {} if gate[0] == "clear" else row_add(fields[i], fields[field(gate[2])], (gate[3], 0)) + expected = {i: ({0: ONE} if i == column else {}) for i in affected} + expected[SCRATCH] = {} + for a, t in zip(A, T, strict=True): + q = packet["native_line_recipes"]["inverse_" + str(t)]["label"] + inverse = {0: (Q(1, 2), Q(-1, 2)), q: (Q(1, 2), Q(1, 2))} + if column in (a, t): + expected[t] = inverse + if column == a: + expected[112+t] = {z: neg(c) for z, c in inverse.items()} + need(fields == expected, "independent physical prefix identity") + return len(affected) * 512 + + +def failure_controls(packet, program, full, zero): + controls = [] + + def rejected(name, action): + try: + action() + except ValueError: + controls.append(name) + else: + raise ValueError("control not rejected: " + name) + + def semantic(candidate, w=256): + need(transfer(packet, candidate, w) == desired(packet, w), "complete dirty endpoint") + + bad = deepcopy(program) + del bad[0][2][3] + rejected("omitted_scratch_inverse_types", lambda: typed_check(packet, bad, full, zero)) + rejected("omitted_scratch_inverse_semantics", lambda: semantic(bad)) + semantic(bad, 0) + controls.append("constant_payload_blind_spot_reproduced") + bad = deepcopy(program) + bad[0][2][3][2] = next(k for k, v in packet["native_line_recipes"].items() + if v["port"] == T[0] and v["sign"] == 1) + rejected("wrong_native_sign", lambda: semantic(bad)) + bad = deepcopy(program) + bad[0][2][1][1][2] = ["L", A[1]] + typed_check(packet, bad, full, zero) # Preserves every frame type. + rejected("equal_frame_wrong_source", lambda: semantic(bad)) + bad = deepcopy(program) + del bad[0][2][0] + rejected("uncleared_arbitrary_scratch", lambda: semantic(bad)) + bad = deepcopy(program) + del bad[0][2][-1] + # The next clear could hide the defect; test the first completed row itself. + rejected("scratch_not_zero_at_row_boundary", lambda: typed_check(packet, bad, full, zero)) + bad = deepcopy(program) + del bad[1] + rejected("missing_inherited_X_normalization", lambda: semantic(bad)) + bad = deepcopy(program) + bad[0][2][4][1][3] = 1 + rejected("wrong_Y_subtraction_sign", lambda: semantic(bad)) + bad = deepcopy(program) + bad[0][3] = "interleave owners before clearing scratch" + rejected("private_lifetime_barrier", lambda: typed_check(packet, bad, full, zero)) + bad = deepcopy(packet) + bad["native_line_recipes"]["inverse_21"]["recipe"]["left"]["phase"] += 1 + rejected("native_wrapper_global_phase", lambda: physical_check(bad)) + bad = deepcopy(packet) + bad["programs"]["B_1_2"][0][1] = ["L", T[1]] + rejected("prefix_boundary_binding", lambda: bind(bad)) + minor = minor_difference(desired(packet, 256), desired(packet, 0)) + minor[1] = [ZERO] * 16 + rejected("missing_Y_obligation_destroys_minor", lambda: need(determinant(minor) != ZERO, "minor")) + rejected("constant_character_cannot_certify_bound", lambda: need( + determinant(minor_difference(desired(packet, 0), desired(packet, 0))) != ZERO, "minor")) + return controls + + +def calculate(root, program=None): + packet = load_packet(root) + full, zero, targets = bind(packet) + expected_program = construct(packet, full, zero) + if program is None: + program = expected_program + need(exact_json(program) == exact_json(expected_program), "complete frozen prefix instructions") + invoice = typed_check(packet, program, full, zero) + need((invoice["native_lines"], invoice["adds"], invoice["clears"]) == (16, 24, 16), "attaining invoice") + histogram = Counter() + for w in range(512): + need(transfer(packet, program, w) == desired(packet, w), "all 712 rows at character " + str(w)) + histogram[2*sum((e["q"] & w).bit_count() % 2 for e in targets)] += 1 + low = minor_difference(desired(packet, 256), desired(packet, 0)) + need(determinant(low) == (256, 0), "rank-16 exact Gaussian determinant") + need(minor_difference(transfer(packet, program, 256), transfer(packet, program, 0)) == low, + "minor agrees with literal program") + recipe_columns, physical_columns = physical_check(packet), physical_prefix_check(packet, program) + controls = failure_controls(packet, program, full, zero) + receipt = { + "status": MARKER, "native_line_minimum": 16, "inherited_prefix_lines": 8, "additional_lines": 8, + "lower_bound": {"characters": [0, 256], "minor_rows": [i for t in T for i in (t, 112+t)], + "minor_columns": [i for pair in zip(A, T, strict=True) for i in pair], + "determinant_gaussian": [256, 0], "rank": 16, + "difference_rank_histogram": {str(k): v for k, v in sorted(histogram.items())}}, + "targets": targets, "invoice": invoice, + "coverage": {"characters": 512, "input_fields": SIZE, "output_fields": SIZE, + "field_character_rows": SIZE*512, "native_recipe_basis_columns": recipe_columns, + "affected_physical_basis_columns_by_translation": physical_columns, + "participating_fields": 25, "untouched_fields": SIZE-17, + "identity_fields_outside_footprint": SIZE-25, + "borrowed_helpers_restored": 480, "owned_scratch_fields": 1}, + "controls": controls, + "scope": "Fixed shear-plus-initial-normalization endpoint; atomic single-field native lines; no cover maps or later B1 fusion. No supplier, full controller, precision admission or kappa claim." + } + return program, receipt + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--root", type=Path, default=ROOT) + parser.add_argument("--write-results", action="store_true") + args = parser.parse_args() + if args.write_results: + program, receipt = calculate(args.root) + for name, data in (("PREFIX.json", program), ("RESULT.json", receipt)): + (HERE / name).write_text(json.dumps(data, indent=2, sort_keys=True) + "\n") + else: + _, receipt = calculate(args.root, json.loads((HERE / "PREFIX.json").read_text())) + need(exact_json(json.loads((HERE / "RESULT.json").read_text())) == exact_json(receipt), + "complete frozen receipt") + print(MARKER + " minimum_lines=16 inherited=8 additional=8 characters=512 inputs=712 controls=" + + str(len(receipt["controls"]))) + + +if __name__ == "__main__": + main()