diff --git a/research/qq16-rounded-producer-envelope/README.md b/research/qq16-rounded-producer-envelope/README.md new file mode 100644 index 0000000000..2624a443e2 --- /dev/null +++ b/research/qq16-rounded-producer-envelope/README.md @@ -0,0 +1,357 @@ +# A rounded-operation envelope for the QQ16 producer pair + +**Conditional interface lemma and exact finite certificate; no new kappa.** +For the literal F0 followed by B_1_2 producer, the sufficient local relative +tolerance + +```text +u <= 2^(-beta-delta-102) +``` + +implies the two completed-stage data tolerances required by +[Nick Petalas's PR2965](../qq16-producer-defect-transfer/README.md), under the +completed-operation premises below. Original data have norm at most H>0; +the 480 dirty helper inputs have norm at most `2^delta H`, where integers +`beta, delta >= 0`. Scalar, native-child, adapter and cover-map defects are +all permitted. Owned private CLEARs are exact. Helper errors from F0 are +carried into B1's actual operand bounds. + +This establishes a sufficient error contract for the source trace, **not an +implementation satisfying that contract**. In particular, 102 is neither a +component width nor a minimum precision. Exact restoration of borrowed helper +bits, native interiors, finite grids, physical hosting and a paid F17 consumer +are not supplied. The selected result and predecessor sources are unchanged. + +## Delta and dependencies + +PR2965 supplies the completed-output inequality +`49 epsF + 1923 epsB + epsD`, but not producer-interior error bounds. +[PR2995](../qq16-producer-dirty-fault/README.md) and +[PR3017](../qq16-native-dirty-fault/README.md) show why a dirty-input bound is +necessary under a permissive relative-error contract. PR3036/3067 and +[the component-rounding reference](../qq16-native-rounded-components/README.md) +also provide concrete finite rounding failures. We do not rederive those +witnesses. + +[PR3181](https://github.com/CrocSwap/integer-mult-bounds/pull/3181), pinned at +`80fc72d14546088e9fce3c06dc12bc67270da0af`, studies signed scalar-projection +cancellation, grids and adjoints. [PR3189](../qq16-noise-lattice-audit/README.md) +shows that ideal input-grid checks do not establish exact scalar arithmetic +after arbitrary approximate child returns. Here scalar errors are charged, +and no signed cancellation between different native routes is used in the +interior error envelope. The new +quantities are positive **relative-defect derivatives** for the complete +native event streams, their verified all-cut maxima, and the noisy two-stage +composition. The old Horner magnitude values are reproduced and credited, +not claimed as new range improvements. + +Scientific base: `463113d675af7410ac91d53a4fed51ec6494eb9a`, priority revision 6. +The literal source is the retained joint-query commit +`a6e6ad3936f67b8f63b5b68c5e75d540610a65e7`; PR2965 is +`526f2c242202b31b15e09a7502dfb8ff757b2bad`. Ideal native, owner, sweep and +endpoint semantics are inherited from the pinned +[native review](../joint-query/evidence/NATIVE-REVIEW.md), +[bridge review](../joint-query/evidence/BRIDGE-REVIEW.md) and +[conserved word](../joint-query/evidence/CONSERVED-QQ16.md). +No predecessor executable is imported. [SOURCES.json](SOURCES.json) binds +the actual main bytes, exact heads and documentary comparisons. The claim is +in discussion [#2727](https://github.com/CrocSwap/integer-mult-bounds/discussions/2727#discussioncomment-19001931), +following PR2965's producer handoff. [TASK.json](TASK.json) records the scope. + +## Norm and completed-operation contract + +For each field use `max_owner ||payload(owner)||_2`, then maximize over any +stated field sector. This norm is preserved by the inherited native unitary +operators, their monomial adapters, and full-cover owner/payload maps, at +every positive common tensor depth. The owner action is retained: a cover map +is not identified with a payload permutation at a single owner. + +The bound is at **completed event boundaries**. In the literal order, allow +the following destination-local errors, measured using the actual operands: + +| Event | Maximum allowed defect | +| --- | --- | +| ADD `d += c s` | `u (||d|| + |c| ||s||)` | +| SCALE `d *= c` | `u |c| ||d||` | +| Completed native child/line, adapter or cover map on d | `u ||d||` | +| Owned private CLEAR | zero | + +The same u bounds all categories within one stage. Errors may be coherent, +state-dependent, nonlinear or correlated. Nothing requires independent noise. +No event may change another field. A child implementation must therefore +establish its complete destination and scratch/side-effect contract; a bound +on its central arithmetic alone is insufficient. Native internal rounding, +operand access, sweep barriers and actual finite storage remain implementation +obligations. Serialized phase events are control labels; mathematical phases +inside completed native recipes are covered by their unitary contracts. + +Initially L0..L703 have norm at most A. C0..C7 may contain arbitrary private +dirt. The checker rejects every read before its first CLEAR and checks their +exact final zeros. Uninitialized private contents are excluded from magnitude +claims; no bound on their initial norm is needed. There are no CLEARs of +persistent data or helpers. Exact helper endpoint semantics are inherited; +their needed norm consequence is that the ideal returned helper block has +norm at most its entry bound, including its prescribed unitary frames. + +The source's owner-local bodies are analyzed per owner, with sweep barriers +retained. In particular, each of the sixteen private bodies across the pair +contains only scalar operations and a native line, with first/last C0 CLEARs; +the checker verifies this. A cut-table row is the virtual aligned cut for +that body. The all-cut maximum bounds unprocessed, active and completed owners +during its physical sweep, and the endpoint bounds apply after the barrier. +This reasoning permits the stated reuse of one C0; it does not allocate a +full private bank or price a physical owner schedule. Core access/embedding +semantics remain inherited, and extra unlisted inexact movements are excluded +from the contract until separately charged. + +## Positive recurrence and proof + +Attach a polynomial `q_d(z)` with nonnegative rational coefficients to each +initialized field. Persistent entry fields have polynomial 1. At a CLEAR, +set the polynomial to zero. At an ADD set + +```text +q_d(z) <- z (q_d(z) + |c| q_s(z)); +``` + +at a SCALE use `z |c| q_d(z)`, and at a native child, adapter or map use +`z q_d(z)`. These are **norm inequalities**, not a replacement of native +operators by identities in a signed-state replay. The largest polynomial +degree is at most the number N of permitted defect sites in the whole stage. + +Let `P_d=q_d(1)` and `J_d=q'_d(1)`. Their exact recurrence is inexpensive: +apply the same positive row transfer to P and J, then add the updated P to J +at each inexact event. CLEAR resets both to zero. The verifier separately +accumulates the five derivative categories ADD, SCALE, child, adapter and map. +Their sum is J; [RESULT.json](RESULT.json) records the relevant exact rows. + +Induction using the local defect inequalities proves, at every cut, + +```text +ideal norm <= A P_d, +actual norm <= A q_d(1+u), +actual-versus-ideal error <= A (q_d(1+u)-q_d(1)). +``` + +For the third inequality, transfer the previous error by the positive row +map and add the new error bounded by u times the positive combination of +actual operand norms. This is precisely the difference between the q and P +recurrences. CLEAR resets the error. The argument holds for arbitrary native +isometries, including noncommuting ones, and for every allowed error pattern. + +For any degree-n nonnegative monomial, with `n<=N` and `u>=0`, + +```text +(1+u)^n - 1 <= n u (1+u)^(N-1). +``` + +Summing the monomials gives +`q_d(1+u)-q_d(1) <= u (1+u)^(N-1) J_d`. +If `N u <= 1/2`, then + +```text +(1+u)^N = sum_k binom(N,k) u^k + <= sum_(k>=0) (N u)^k = 1/(1-Nu) <= 2. +``` + +Thus the useful finite-trace bounds are + +```text +all-cut error <= 2 A u J_d, +all-cut actual norm <= 2 A P_d. (2) +``` + +These constants are sufficient majorants, not asserted attainable physical +norms. The feedback factor cannot simply be omitted: two scalar identity +steps with positive relative errors already give `(1+u)^2-1 > 2u`. +For category tolerances `u_c`, the same path argument gives +`error <= 2 A sum_c u_c J_(d,c)` when `N max_c u_c <= 1/2`. +Different category tolerances require maximizing that weighted sum over the +relevant cuts; the recorded global maxima here use a common u. + +## Exact finite ledger + +The source has 712 fields: 224 data, 480 persistent helpers and eight private +fields. Indices below are zero-based in the expanded, unfiltered stream. + +| Quantity | F0 | B_1_2 | +| --- | ---: | ---: | +| Events / changed-field cuts | 26099 / 26089 | 27019 / 27009 | +| Permitted defect sites N | 26057 | 26977 | +| Exact private CLEARs | 32 | 32 | +| Maximum polynomial degree | 184 | 854 | +| All-cut P maximum | 5413950274051752469/256 | 573411134169296526275133/64 | +| All-cut J maximum | 10632335516156845470267/4096 | 34778728470688788237067911/8 | +| First maximizing event / field for both P and J | 26052 / L132 | 26777 / L86 | + +In each stage the displayed J also bounds every completed data and helper +output, and is attained by the positive recurrence at a final data output. +The inequalities `J_F < 2^62`, `J_B < 2^82`, `P_F < 2^55` and `P_B < 2^73` +are exact rational comparisons. The receipt additionally supplies the helper +terminal maxima, category contributions and complete cut-table digests. + +## Composition with bounded dirty helpers + +Let original data be bounded by H>0 and initial helper norms by `2^delta H`, +where `beta,delta>=0` are integers. Both stages start with arbitrary private +dirt and execute the prescribed exact CLEARs. No additional inexact handoff +operation is silently inserted between stages. + +It suffices to choose separate tolerances + +```text +u_F <= 2^(-beta-delta-71), +u_B <= 2^(-beta-delta-102). (3) +``` + +Both satisfy `N u <= 1/2`. For F0 take `A_F=2^delta H`. By (2), even its +all-cut error is bounded by + +```text +2 A_F u_F J_F < H 2^(-beta-8) = eta_F. +``` + +The inherited ideal F0 data map has norm at most 58 independently of helper +values. The checker calibrates this bound from the actual R/K row sums, +the A/T section identities and the retained endpoint equations: X bounds on +A/T/U are 4/56/57, and Y bounds are 6/58/58. This is predecessor evidence, +checked here because the handoff uses it. The actual completed data therefore +have norm below `59H`. Ideal +helper endpoints preserve their entry norm, so the actual helpers are bounded +by `2^delta H + eta_F`, not by their original bound alone. Consequently all +persistent B1 entry fields are bounded by the conservative common value +`A_B=2^(delta+6) H`. This explicitly carries the F0 helper error into B1. +Prescribed unitary representation changes preserve these norm bounds; any +extra physical conversion must separately satisfy a charged error contract. + +Apply B1's estimate to the actual incoming data and helpers. Its ideal data +endpoint is independent of the arbitrary helper inputs. By (2) and (3), + +```text +2 A_B u_B J_B < H 2^(-beta-13) = eta_B. +``` + +These are exactly sufficient completed-stage defects for PR2965. If the +chosen decoder additionally supplies `epsD <= H 2^(-beta-1)`, that theorem gives + +```text +decoded data error <= (49/256 + 1923/8192 + 1/2) H 2^-beta + = (7587/8192) H 2^-beta < H 2^-beta. +``` + +For example, beta=64 and delta=0 permit completed-event tolerances `2^-135` +in F0 and `2^-166` in B1. The single common tolerance in the opening statement +satisfies both. These exponents concern the local norm contract, not floating +significands, fixed-point fractional positions or sufficient register widths. + +The noisy all-cut magnitude bounds include data, helpers and initialized +private fields: F0 is below `2^(delta+56) H`; B1 is below `2^(delta+80) H`. +They do not bound intermediates inside an atomic native event. +Relative to the corresponding ideal pair's returned helper block, helper +error is at most `eta_F+eta_B`, using the inherited isometric return map. +This is an approximate return bound; it does not establish exact borrowed-bit +restoration. The eight private fields do return exactly to zero. + +## Cost and expansion decision + +No word, tariff or selected frontier is changed. The literal producer counts +checked here are: + +| Completed operation | F0 | B1 | +| --- | ---: | ---: | +| ADD / SCALE / CLEAR | 20278 / 715 / 32 | 20654 / 715 / 32 | +| Native children, including wrapper lines | 3494 | 3510 | +| Core endpoint/residual adapter events | 1570 | 1570 | +| Full-cover map events | 0 | 528 | + +The predecessor's constructive local scalar allowances remain 211210 and +214986 real primitives, with native rank masses 5530 and 5546. Its eight and +24 additional line children also require 16 and 48 native wrapper maps. +These are predecessor abstract allowances, not prices certified for an +implementation of (3). The retained PR2707 decoder further lists 336 rank-one +children, 672 wrappers, 464 cover maps, scalar allowance 25840, 224 owned output +fields and up to sixteen private fields. None is free or implemented here. + +The new error implication and norm envelopes are proved under the stated +contracts. Ideal operator semantics and the completed decoder theorem are +inherited. Finite arithmetic realizing the local tolerances, component +representation/grid, child scratch restoration, exact borrowed-state return, +physical allocation/movement, tape/control and subsequent F17 consumption are +unknown. The centre-charge/coverage decision is also not settled by this +numerical lemma. No favorable complete recursive invoice is asserted. +Family decision: **narrow and stop** at this conditional interface; these +unknown costs do not justify another dependent implementation search. + +## Reproduce and verification limits + +From the repository root, standard-library Python 3.12: + +```sh +python3 -Werror -I -B scripts/research_package.py --package research/qq16-rounded-producer-envelope +``` + +The principal markers are + +```text +PASS_QQ16_ROUNDED_PRODUCER_ENVELOPE stages=2 cuts=53098 offset=102 conditional_completed_operations no_new_kappa +PASS_QQ16_PRODUCER_ENVELOPE_INDEPENDENT integer_cuts=53098 reverse_rows=6 categories=5 +``` + +[verify.py](verify.py) authenticates seven live inputs and calculates every +changed-field row using exact rationals, in normal and optimized Python. +[independent.py](independent.py) imports no primary/predecessor implementation: +it checks every P/J row with a separately written integer-grid interpreter, +then uses six reverse covectors to check the five relative-defect categories. +The verifier's oversized exact integer grid is an arithmetic cross-check; +it is not a proposed physical representation for QQ16. + +Ten behavioral groups in [test_verify.py](test_verify.py) include actual +noncommuting two-dimensional isometries with coherent state-dependent faults, +explicit positive polynomials, a feedback-factor counterexample, dirty input +and noisy-helper reuse, omitted child/map faults, erased private transients, +illegal CLEARs/uninitialized reads, scalar coefficient changes, exact tolerance +comparisons, endpoint-geometry mutations and pre-execution source corruption. Finite fixtures corroborate +the written arbitrary-dimension proof; they do not replay the complete physical +native operators. No independent human or formal-kernel review is claimed. + +Replay is read-only. `verify.py --write PATH` creates an absent receipt and +refuses to overwrite one. The direct three Python commands work in a source +export containing the declared inputs. The primary replay is bounded by two +28000-event words, 712 fields and five error categories; the certificate read +is capped at 16 MB. Python integers/collections allocate dynamically. No solver, +network, third-party package or native toolchain is required. The selected cold +replay and full native proof replay were not run because their source/claims +are unchanged and are explicitly inherited. + +## Open next questions + +1. Supply one actual native child's complete destination/scratch defect + contract at a finite grid and dirty range. Begin at a literal child followed + by a half-ADD, retaining the latter's nonzero rounding allowance. The absence + of a finite, priced child implementation blocks numerical realization of (3). +2. Decide the required helper return contract. If exact borrowed bits must be + restored, prove a restoration mechanism or an exact arithmetic invariant; + the `eta_F+eta_B` estimate is insufficient. Any correction must include its + error, storage and movement costs. +3. Bind a complete F17 consumer and owner/sweep schedule to the producer and + decoder. Start with the charged operation/lifetime ledger above, including + the centre/coverage convention. Unknown physical and recursive tariffs + currently prevent a favorable complete-cost decision. + +## Credit + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. +New derivation, checker, tests and prose are Apache-2.0. No independent human +review is claimed. Nick Petalas supplies PR2965's completed-output transfer and +PR2736's preceding decoder defect analysis. The positive-majorant method is +standard; its noise-aware application and two-stage dirty-helper composition +for these literal producer words are the contribution here. + +Credit Ali Romman and the retained QQ16 team for the words and operator/sweep +contracts; ywz65 for PR2707/2540; Arham Tahir for PR2681/2995/3036; Tekalign for +PR3017/3189; Ross Richardson for PR3067 and earlier rounded/restoration +contracts; Sricharan Vagvala for the native component-rounding reference; +dcharb78 for PR3181's separate scalar-projection study; and starship-s, Sagar +Thakrar, DLamdata, Douglas Colkitt and the source contributors retained in +[the original notice](../joint-query/NOTICE.md). Their frozen files and credit +are unchanged. diff --git a/research/qq16-rounded-producer-envelope/RESULT.json b/research/qq16-rounded-producer-envelope/RESULT.json new file mode 100644 index 0000000000..db80a6a402 --- /dev/null +++ b/research/qq16-rounded-producer-envelope/RESULT.json @@ -0,0 +1,201 @@ +{ + "cases": { + "B_1_2": { + "P_J_cut_table_sha256": "1cb5a68a78697147e57072d7ca95205cfc906febd39e43a9f4a307781cc8c760", + "all_cut": { + "J": { + "J": "34778728470688788237067911/8", + "J_by_category": { + "adapter": "573411134169296526275133/32", + "add": "528563836636664365942901081/128", + "child": "868124559712689196132629/16", + "map": "447350418393498392438827/8", + "scale": "11499571185681571897002699/128" + }, + "P": "573411134169296526275133/64", + "degree": 854, + "event": 26777, + "wire": 86 + }, + "P": { + "J": "34778728470688788237067911/8", + "J_by_category": { + "adapter": "573411134169296526275133/32", + "add": "528563836636664365942901081/128", + "child": "868124559712689196132629/16", + "map": "447350418393498392438827/8", + "scale": "11499571185681571897002699/128" + }, + "P": "573411134169296526275133/64", + "degree": 854, + "event": 26777, + "wire": 86 + } + }, + "changed_cuts": 27009, + "clear_sites": 32, + "cut_table_sha256": "9a88f4de7e48af700738d2b7151c6826646f0e19cd80138eee889e70fd82954d", + "defect_category_counts": { + "adapter": 1570, + "add": 20654, + "child": 3510, + "map": 528, + "scale": 715 + }, + "defect_sites": 26977, + "degree_max": 854, + "event_counts": { + "adapter": 1090, + "climb": 3486, + "cover_map": 528, + "native_line": 24, + "phase": 10, + "residual_adapter": 480, + "scalar": 21401 + }, + "event_sha256": "3de03cde4586411cf38af53c4b69a4d5bd58aa774a266c25c2cda943daa75664", + "events": 27019, + "terminal": { + "data": { + "J": "34778728470688788237067911/8", + "J_by_category": { + "adapter": "573411134169296526275133/32", + "add": "528563836636664365942901081/128", + "child": "868124559712689196132629/16", + "map": "447350418393498392438827/8", + "scale": "11499571185681571897002699/128" + }, + "P": "573411134169296526275133/64", + "degree": 854, + "event": 27018, + "wire": 86 + }, + "helpers": { + "J": "1340378160314112760812753/128", + "J_by_category": { + "adapter": "824409778576412307071/16", + "add": "1262719250976545336699813/128", + "child": "2447279125924334138203/16", + "map": "1285568796554817686775/8", + "scale": "7729074339171092390587/32" + }, + "P": "824409778576412307071/32", + "degree": 784, + "event": 27018, + "wire": 426 + } + } + }, + "F_0": { + "P_J_cut_table_sha256": "53b63316175717560fae8aa83e664acb8dd72e07927bd4d0ccdbbeae67d5b8be", + "all_cut": { + "J": { + "J": "10632335516156845470267/4096", + "J_by_category": { + "adapter": "5413950274051752469/128", + "add": "4426833844834375166319/2048", + "child": "75241476382820606935/512", + "map": "0", + "scale": "1003489606655874203141/4096" + }, + "P": "5413950274051752469/256", + "degree": 184, + "event": 26052, + "wire": 132 + }, + "P": { + "J": "10632335516156845470267/4096", + "J_by_category": { + "adapter": "5413950274051752469/128", + "add": "4426833844834375166319/2048", + "child": "75241476382820606935/512", + "map": "0", + "scale": "1003489606655874203141/4096" + }, + "P": "5413950274051752469/256", + "degree": 184, + "event": 26052, + "wire": 132 + } + }, + "changed_cuts": 26089, + "clear_sites": 32, + "cut_table_sha256": "c1173022432dcce87a03c7d4a160dd3178906d5a5bef1f50bf6b7be3993eed04", + "defect_category_counts": { + "adapter": 1570, + "add": 20278, + "child": 3494, + "scale": 715 + }, + "defect_sites": 26057, + "degree_max": 184, + "event_counts": { + "adapter": 1090, + "climb": 3486, + "native_line": 8, + "phase": 10, + "residual_adapter": 480, + "scalar": 21025 + }, + "event_sha256": "4c1ee518a6513c115741a3834c49490c6e8e68f5e2357af8dac782c3d40958e7", + "events": 26099, + "terminal": { + "data": { + "J": "10632335516156845470267/4096", + "J_by_category": { + "adapter": "5413950274051752469/128", + "add": "4426833844834375166319/2048", + "child": "75241476382820606935/512", + "map": "0", + "scale": "1003489606655874203141/4096" + }, + "P": "5413950274051752469/256", + "degree": 184, + "event": 26098, + "wire": 132 + }, + "helpers": { + "J": "4031638139577443210809/16384", + "J_by_category": { + "adapter": "2765345294379392599/512", + "add": "1593141449370532149625/8192", + "child": "32901256914647896607/2048", + "map": "0", + "scale": "493654136099055175535/16384" + }, + "P": "2765345294379392599/1024", + "degree": 130, + "event": 26098, + "wire": 349 + } + } + } + }, + "composition": { + "B_entry_bound": "2^(delta+6) H", + "B_persistent_J": "34778728470688788237067911/8", + "B_tolerance_offset": 102, + "F_entry_bound": "2^delta H", + "F_persistent_J": "10632335516156845470267/4096", + "F_tolerance_offset": 71, + "common_relative_offset": 102, + "count_guard": 16, + "decoded_error_ratio": "7587/8192" + }, + "ideal_endpoint_calibration": { + "F_data_norm_over_H": "58", + "K_row_sum": "1", + "R_row_sum": "56", + "X_A_T_U": [ + "4", + "56", + "57" + ], + "Y_A_T_U": [ + "6", + "58", + "58" + ] + }, + "schema": "qq16-rounded-producer-envelope-v1" +} diff --git a/research/qq16-rounded-producer-envelope/SOURCES.json b/research/qq16-rounded-producer-envelope/SOURCES.json new file mode 100644 index 0000000000..0ad06613ab --- /dev/null +++ b/research/qq16-rounded-producer-envelope/SOURCES.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/joint-query/certificate.json.gz", + "usage": "input", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + }, + { + "path": "research/joint-query/evidence/BRIDGE-REVIEW.md", + "usage": "input", + "git_blob": "86139908c418235588045324f0873de6ac9f9707", + "sha256": "d01b5f4959f7c91f835496d050dfae3eeab9dee2f581571c316a42571eaa1cd3" + }, + { + "path": "research/joint-query/evidence/CONSERVED-QQ16.md", + "usage": "input", + "git_blob": "4639583c1be02c2fb60ed8a8072c9969ef1569ce", + "sha256": "60f0de3a7205ba5046b5ae7ffa8bf2b1ea42ea46b498face0a77966b59e7f3fb" + }, + { + "path": "research/qq16-producer-defect-transfer/README.md", + "usage": "input", + "git_blob": "16903a0090c020d033d24712cce11c633031e688", + "sha256": "30cf4389425f7704b1ed45af6cf4b5165e7b5c04af5077640ac96399c61cd703" + }, + { + "path": "research/joint-query/evidence/NATIVE-REVIEW.md", + "usage": "input", + "git_blob": "525b38dbdefed0e8192a9c5165e802136cc05034", + "sha256": "2247e3cbe73f3f0da55c647ffae15f98dd9445b2366ba9e255b9bebc9f742b70" + }, + { + "path": "research/qq16-zero-retention-defects/PROOF.md", + "usage": "input", + "git_blob": "449e1a181d177c7f2ee663e5d9d13898d2872834", + "sha256": "11edf91802c08c75bbddcea5220e04fa612b46e916ca14c44f63263cdd76fa3c" + }, + { + "path": "research/qq16-line-normalized-decoder/README.md", + "usage": "input", + "git_blob": "e2032842955492d3765d9d8f99c1bead1ba17ae4", + "sha256": "017bb0a0ec15a5c5df446f721e9e68d4eeffac8bfe6fab2a4016a6dc0a666f14" + } + ], + "predecessors": { + "joint_query": "a6e6ad3936f67b8f63b5b68c5e75d540610a65e7", + "2965": "526f2c242202b31b15e09a7502dfb8ff757b2bad", + "2736": "eba0d6111a773cd13f5c0afb4354af2c85d04c3a", + "2707": "efa51a6c7ffec6edd556a98deedfe9deeba65809" + }, + "comparisons_not_runtime_dependencies": { + "3181": "80fc72d14546088e9fce3c06dc12bc67270da0af", + "3189": "70537595e46444c8a63455523d9851a5efe55385", + "3017": "0f493f4c264fbc70ee14364b68af260d858c143c", + "3067": "e1e28b4070ae52efa5a9d0aa826bc588be7206f2" + } +} diff --git a/research/qq16-rounded-producer-envelope/TASK.json b/research/qq16-rounded-producer-envelope/TASK.json new file mode 100644 index 0000000000..65a62d7fbb --- /dev/null +++ b/research/qq16-rounded-producer-envelope/TASK.json @@ -0,0 +1,185 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 6, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "original_card": { + "id": "joint-query-controller", + "question": "Can a literal QQ16 producer meet the proposed completed-output error budgets with dirty helpers and an affordable physical consumer?", + "starting_points": [ + "docs/research/research-family-status.md", + "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", + "research/qq16-producer-defect-transfer/README.md" + ], + "methods": [ + "Derive one literal producer's completed-output defects and intermediate dirty-helper bounds, with its physical bill.", + "Design or audit one consumer, retention or hosting boundary and its complete cost for the pinned producer/decoder." + ], + "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. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the revision-6 family record and #2965 producer-defect transfer after the local QQ16 decoder contract. Its author-checked output-error estimate does not implement producer interiors, bound dirty helpers, or pay for the consumer; independently check the implication used.", + "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": "Pin one literal F0/B1 producer and its native-child contracts; derive the actual intermediate magnitude ledger and completed-output defects, including dirty helpers and correlations. Compare with #2965 budgets and price storage, movement, cleanup and F17 consumption. Stop with a precise missing bound if no producer contract supplies it; do not optimize another decoder precision constant in isolation.", + "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.", + "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain." + ], + "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.", + "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.", + "Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969", + "2540", + "early record", + "output-bank retention", + "complete native decoder", + "2965", + "producer defect", + "dirty-helper range", + "F17 consumer" + ] + }, + "scope_status": "refined", + "actual_scope": "A sufficient completed-operation relative-defect envelope for the literal F0 and B_1_2 words, including nonzero scalar/native errors, bounded dirty helpers and noisy helper carry between stages.", + "scope_change_reason": "Take PR2965's producer handoff as one conditional numerical implication. Unlike ideal-only scalar-projection grids, permit every declared rounded ADD/SCALE/child/adapter/map and use native isometry norm bounds without signed route cancellation.", + "bottleneck_link": "A completed-output decoder tolerance does not bound faults inside its producer. This source-bound ledger gives sufficient local producer contracts and carries actual helper ranges, while leaving their physical realization and affordable consumer explicit.", + "budget_minutes": 60, + "stop_rule": "Stop at the stated conditional interface lemma and its exact finite checks; no native implementation campaign, supplier admission or selected-frontier change.", + "outcome": "completed", + "evidence": "PASS: all 53098 rational and independently implemented integer P/J rows; six reverse covectors across five derivative categories; ten behavioral groups; normal and optimized registered replay, metadata/source pins, and Git-free direct replay.", + "author": "commdata2338", + "ai_assistance": "Substantial OpenAI Codex assistance in derivation, implementation, checking and writing; no independent human review is claimed.", + "open_questions": [ + { + "question": "Can one actual native child and its scratch satisfy the completed destination-local relative defect contract at finite range/grid?", + "why_it_matters": "The theorem supplies a sufficient tolerance, not an implementation achieving it.", + "first_step": "Bind one child followed by a literal half-ADD and include all primitive rounding and scratch side effects.", + "blocked_by": "No finite priced native child is supplied by this package." + }, + { + "question": "Can the required borrowed-helper return contract be met exactly?", + "why_it_matters": "A small returned-helper error is not restoration of arbitrary borrowed bits.", + "first_step": "Choose exact arithmetic or a fully charged restoration/correction protocol, including its propagated errors.", + "blocked_by": "The present lemma only bounds helper return error." + }, + { + "question": "Can a complete F17 consumer and owner/sweep schedule fit the full recursive invoice?", + "why_it_matters": "A numerical implication cannot establish supplier affordability.", + "first_step": "Join the retained producer/decoder counts with actual owners, lifetimes, movement and centre coverage.", + "blocked_by": "Physical tariffs, consumer and centre/coverage convention remain unspecified here." + } + ], + "scope_key": "qq16-f0-b12-rounded-completed-operations-dirty-bounded", + "catalog_scope_key": "42581d429acc9509d503", + "selection": { + "method": "handoff-first, then specific-card lookup", + "thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2727#discussioncomment-18975580", + "seed": "e5076c40813b9e1c577c98b0ce46a680", + "track": "recursive-interfaces", + "existing_checks": [], + "existing_checks_meaning": "Unknown coverage, not evidence of novelty." + }, + "declared_milestone": "conditional interface lemma / finite certificate", + "family_decision": "narrow and stop", + "optimistic_full_cost_budget": "No changed word or claimed saving. Source scalar/native/map counts are retained; implementing local tolerances, exact helper return, ownership, movement, storage, recursive tariffs, centre coverage and an F17 consumer remain unknown. Unknowns are not zero.", + "inherited_obligations": [ + "Ideal native operator, frame and full-cover sweep semantics", + "Ideal helper return and helper-independent data maps", + "PR2965 completed-error transfer; PR2736 decoder numerical premise" + ], + "unchecked_obligations": [ + "Actual finite completed child/adapter/map/ADD/SCALE defect contracts, including scratch side effects", + "Finite grid and component width, overflow and native internal ranges", + "Exact restoration of borrowed helper bits", + "Physical owner allocation, access, movement, storage and tape/control", + "Affordable F17 consumer and full recursive/supplier invoice", + "All-size compiler, selected cold replay, formal-kernel or human review" + ], + "nearest_overlaps": [ + { + "pr": 2965, + "head": "526f2c242202b31b15e09a7502dfb8ff757b2bad", + "difference": "Endpoint transfer only; this result supplies a conditional literal producer-interior envelope." + }, + { + "pr": 3181, + "head": "80fc72d14546088e9fce3c06dc12bc67270da0af", + "difference": "Signed scalar-projection cancellation and ideal grid; this result is a positive physical norm majorant with nonzero scalar errors." + }, + { + "pr": 3189, + "head": "70537595e46444c8a63455523d9851a5efe55385", + "difference": "Defect lattice closure and one projected error direction; no lattice or native-direction claim here." + }, + { + "pr": 3017, + "head": "0f493f4c264fbc70ee14364b68af260d858c143c", + "difference": "Dirty-helper obstruction; this result adds a sufficient dirty-bounded contract." + }, + { + "pr": 3067, + "head": "e1e28b4070ae52efa5a9d0aa826bc588be7206f2", + "difference": "Concrete finite F0 rounding witness; this result is an all-pattern completed-operation norm theorem for the two-stage pair." + } + ], + "overlap": { + "mode": "cached remote snapshot plus current main and canonical thread", + "open_prs_fetched_at": "2026-10-17T17:26:19.594925+00:00", + "open_prs_records": 249, + "discussions_fetched_at": "2026-10-17T17:27:03.117721+00:00", + "discussions_records": 2001, + "complete_pagination": true, + "limits": "Snapshot searches do not cover every code diff or unpublished investigation; merged-source checks supplement open PRs.", + "submission_check": { + "open_prs": { + "fetched_at": "2026-10-17T17:37:12.534077+00:00", + "complete_pagination": true, + "records": 251 + }, + "discussions": { + "fetched_at": "2026-10-17T17:39:04.580509+00:00", + "complete_pagination": true, + "records": 2015 + } + } + }, + "evidence_status": "author-checked scoped proof and finite certificate; no independent human review", + "validation": { + "environment": { + "python": "3.12.3", + "platform": "Linux x86_64" + }, + "registered_replay": "passed normal and optimized primary, independent all-cut and reverse checker, optimized controls", + "git_free_export": "passed direct optimized primary, independent checker and controls; current sweep guards also pass in the source export", + "selected_cold_replay": "not run; inherited construction unchanged", + "formal_kernel": "not run", + "human_review": "none claimed" + }, + "refresh_checkpoint": { + "checked_at": "2026-10-17T17:46:17.024133+00:00", + "base": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "canonical_main": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "changed_paths": [], + "priority_revision": 6 + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2727#discussioncomment-19001931" +} diff --git a/research/qq16-rounded-producer-envelope/VERIFY.json b/research/qq16-rounded-producer-envelope/VERIFY.json new file mode 100644 index 0000000000..10a87e6b77 --- /dev/null +++ b/research/qq16-rounded-producer-envelope/VERIFY.json @@ -0,0 +1,63 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/joint-query/certificate.json.gz", + "research/joint-query/evidence/BRIDGE-REVIEW.md", + "research/joint-query/evidence/CONSERVED-QQ16.md", + "research/qq16-producer-defect-transfer/README.md", + "research/joint-query/evidence/NATIVE-REVIEW.md", + "research/qq16-zero-retention-defects/PROOF.md", + "research/qq16-line-normalized-decoder/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-Werror", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate sources; exact rational P/J category recurrence at all 53,098 changed-field cuts and sufficient composed tolerance." + }, + { + "argv": [ + "{python}", + "-Werror", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete receipt with Python assertions disabled." + }, + { + "argv": [ + "{python}", + "-Werror", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Separate exact-integer replay of every P/J cut, six reverse covectors and all five derivative categories." + }, + { + "argv": [ + "{python}", + "-Werror", + "-I", + "-O", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 60, + "checks": "Ten behavioral groups: noncommuting state-dependent defects, positive polynomials, feedback, dirty carry, native/map omissions, private transients/ownership, scalar prices, sufficient tolerances and endpoint geometry and corrupted input." + } + ] +} diff --git a/research/qq16-rounded-producer-envelope/independent.py b/research/qq16-rounded-producer-envelope/independent.py new file mode 100644 index 0000000000..72419b34a3 --- /dev/null +++ b/research/qq16-rounded-producer-envelope/independent.py @@ -0,0 +1,191 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Separate forward-load / reverse-adjoint check; no primary-code imports. + +Prepared for commdata2338, with substantial OpenAI Codex assistance. +This independently checks every P/J cut with integers and six reported +category rows with reverse adjoints. Native semantics remain inherited. +""" +from fractions import Fraction +import gzip +import hashlib +import json +from pathlib import Path + +BASE = Path(__file__).resolve().parent +ROOT = BASE.parents[1] +SOURCE = ROOT / "research/joint-query/certificate.json.gz" +SOURCE_HASH = "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" +PAYLOAD_HASH = "2efe83c59978aa9c0db2c3e4eccc14cbfdcd3c9ce499432601b5dd34083472ef" + + +def check(ok, message): + if not ok: + raise ValueError(message) + + +def register(token): + check(token[0] in ("L", "C"), "register namespace") + return token[1] + (704 if token[0] == "C" else 0) + + +def events_for(packet, name): + events = [] + for entry in packet["programs"][name]: + if entry[0] == "retained_core": + events += packet["core_words"][entry[1]] + elif entry[0] in ("cover_sweep", "private_sweep"): + events += entry[2] + else: + events.append(entry) + return events + + +def instructions(events): + """Independent event decoder, preserving the unfiltered indices.""" + rows = [] + for e in events: + kind = e[0] + if kind == "phase": + rows.append(("none", -1, -1, Fraction(0), None)) + elif kind == "scalar": + g = e[1] + d = register(g[1]) + if g[0] == "clear": + rows.append(("zero", d, -1, Fraction(0), None)) + elif g[0] == "scale": + rows.append(("mul", d, -1, abs(Fraction(g[2], g[3])), "scale")) + else: + check(g[0] == "add", "scalar kind") + rows.append(("sum", d, register(g[2]), abs(Fraction(g[3], g[4])), "add")) + elif kind in ("climb", "adapter", "residual_adapter"): + rows.append(("one", e[2], -1, Fraction(1), "child" if kind == "climb" else "adapter")) + else: + check(kind in ("native_line", "cover_map"), "native kind") + rows.append(("one", register(e[1]), -1, Fraction(1), + "child" if kind == "native_line" else "map")) + return rows + + +def load_trace(rows): + values = [Fraction(1)] * 704 + [Fraction(0)] * 8 + initialized = set(range(704)) + loads = [] + for kind, d, s, c, _ in rows: + if kind == "none": + loads.append(Fraction(0)) + continue + if kind == "zero": + check(d >= 704, "clear ownership") + values[d] = Fraction(0) + initialized.add(d) + else: + check(d in initialized and (s < 0 or s in initialized), "uninitialized field") + if kind == "mul": + values[d] *= c + elif kind == "sum": + values[d] += c * values[s] + loads.append(values[d]) + return loads + + +def dual_row(rows, loads, end, wire): + covector = [Fraction(0) for _ in range(712)] + covector[wire] = Fraction(1) + gains = {key: Fraction(0) for key in ("add", "scale", "child", "adapter", "map")} + for t in range(end, -1, -1): + kind, d, s, c, category = rows[t] + if category is not None: + gains[category] += covector[d] * loads[t] + if kind == "zero": + covector[d] = Fraction(0) + elif kind == "mul": + covector[d] *= c + elif kind == "sum": + covector[s] += c * covector[d] + return sum(covector[:704]), gains + + +def integer_all_cuts(rows, case): + """Use one deliberately oversized exact dyadic integer grid, not Fractions. + + Paying every scalar denominator in series is sufficient for this verifier; + it is not a proposed arithmetic format for the physical producer. + """ + powers = [c.denominator.bit_length() - 1 for _, _, _, c, _ in rows if c] + check(all(c.denominator & (c.denominator - 1) == 0 for _, _, _, c, _ in rows), + "dyadic scalar coefficients") + quantum = 1 << sum(powers) + p, j = [quantum] * 704 + [0] * 8, [0] * 712 + digest, cut_count, sites = hashlib.sha256(), 0, 0 + maxima = {"P": (quantum, -1, 0), "J": (0, -1, 0)} + for t, (kind, d, s, c, category) in enumerate(rows): + if kind == "none": + continue + cut_count += 1 + if kind == "zero": + p[d], j[d] = 0, 0 + elif kind in ("mul", "sum"): + source = d if kind == "mul" else s + pn, pr = divmod(p[source] * c.numerator, c.denominator) + jn, jr = divmod(j[source] * c.numerator, c.denominator) + check(pr == jr == 0, "independent integer grid exhausted") + if kind == "mul": + p[d], j[d] = pn, jn + else: + p[d], j[d] = p[d] + pn, j[d] + jn + if category is not None: + j[d] += p[d] + sites += 1 + record = [t, d, str(Fraction(p[d], quantum)), str(Fraction(j[d], quantum))] + digest.update(json.dumps(record, sort_keys=True, separators=(",", ":")).encode() + b"\n") + for key, value in (("P", p[d]), ("J", j[d])): + if value > maxima[key][0]: + maxima[key] = (value, t, d) + check(cut_count == case["changed_cuts"] and sites == case["defect_sites"], "cut coverage") + check(digest.hexdigest() == case["P_J_cut_table_sha256"], "all-cut P/J digest") + for key, (value, t, d) in maxima.items(): + target = case["all_cut"][key] + check(Fraction(value, quantum) == Fraction(target[key]), "independent maximum") + check((t, d) == (target["event"], target["wire"]), "maximum cut") + for name, indices in (("data", range(224)), ("helpers", range(224, 704))): + d = max(indices, key=lambda index: j[index]) + check(d == case["terminal"][name]["wire"], "terminal argmax") + check(Fraction(j[d], quantum) == Fraction(case["terminal"][name]["J"]), "terminal maximum") + check(p[704:] == j[704:] == [0] * 8, "private final zeros") + return cut_count + + +def main(): + compressed = SOURCE.read_bytes() + check(hashlib.sha256(compressed).hexdigest() == SOURCE_HASH, "source hash") + payload = gzip.decompress(compressed) + check(hashlib.sha256(payload).hexdigest() == PAYLOAD_HASH, "payload hash") + packet = json.loads(payload) + report = json.loads((BASE / "RESULT.json").read_bytes()) + count, cuts = 0, 0 + for name, case in report["cases"].items(): + rows = instructions(events_for(packet, name)) + cuts += integer_all_cuts(rows, case) + loads = load_trace(rows) + targets = list(case["all_cut"].values()) + list(case["terminal"].values()) + unique = {(r["event"], r["wire"]): r for r in targets} + for (end, wire), target in unique.items(): + p, gains = dual_row(rows, loads, end, wire) + check(p == Fraction(target["P"]), "reverse input gain") + check(sum(gains.values()) == Fraction(target["J"]), "reverse derivative") + for category, value in gains.items(): + check(value == Fraction(target["J_by_category"][category]), + "reverse category: " + category) + count += 1 + c = report["composition"] + check(Fraction(49, 256) + Fraction(1923, 8192) + Fraction(1, 2) == Fraction(7587, 8192), + "completed decoder budget") + check(Fraction(c["F_persistent_J"]) < 2**62, "F sufficient bound") + check(Fraction(c["B_persistent_J"]) < 2**82, "B sufficient bound") + check(c["common_relative_offset"] == 102 and c["count_guard"] == 16, "tolerance offsets") + print(f"PASS_QQ16_PRODUCER_ENVELOPE_INDEPENDENT integer_cuts={cuts} reverse_rows={count} categories=5") + + +if __name__ == "__main__": + main() diff --git a/research/qq16-rounded-producer-envelope/test_verify.py b/research/qq16-rounded-producer-envelope/test_verify.py new file mode 100644 index 0000000000..f70e18456c --- /dev/null +++ b/research/qq16-rounded-producer-envelope/test_verify.py @@ -0,0 +1,226 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Behavioral controls for the conditional producer envelope. + +Prepared for commdata2338, with substantial OpenAI Codex assistance. +""" +from copy import deepcopy +from fractions import Fraction as Q +import json +from pathlib import Path +import tempfile +import types +import unittest + +HERE = Path(__file__).resolve().parent +V = types.ModuleType("producer_envelope") +V.__file__ = str(HERE / "verify.py") +exec(compile((HERE / "verify.py").read_bytes(), V.__file__, "exec"), V.__dict__) + + +def clear_all(): + return [["scalar", ["clear", ["C", i]], 0] for i in range(8)] + + +def add(d, s, a=1, b=1): + return ["scalar", ["add", d, s, a, b], 0] + + +def scalar_norm2(v): + return sum(x * x for x in v) + + +def plus(a, b, c=Q(1)): + return tuple(x + c * y for x, y in zip(a, b)) + + +def rotate(v): + return (-v[1], v[0]) + + +def reflect(v): + return (v[0], -v[1]) + + +def oracle_step(states, event): + """Actual two-dimensional noncommuting isometries, not a scalar shadow.""" + if event[0] == "scalar": + g = event[1] + d = g[1][1] + (704 if g[1][0] == "C" else 0) + if g[0] == "clear": + return d, (Q(0), Q(0)), True + if g[0] == "scale": + return d, tuple(Q(g[2], g[3]) * x for x in states[d]), False + s = g[2][1] + (704 if g[2][0] == "C" else 0) + return d, plus(states[d], states[s], Q(g[3], g[4])), False + d = event[1][1] + (704 if event[1][0] == "C" else 0) + f = rotate if event[0] == "native_line" else reflect + return d, f(states[d]), False + + +class EnvelopeTests(unittest.TestCase): + def test_inherited_endpoint_geometry_and_mutants(self): + packet = V.load() + self.assertEqual(V.endpoint_calibration(packet)["F_data_norm_over_H"], "58") + wrong = deepcopy(packet) + wrong["K_rows"][0]["0"] = "1/2" + with self.assertRaisesRegex(ValueError, "K=R"): + V.endpoint_calibration(wrong) + wrong = deepcopy(packet) + wrong["A_ports"][0] = wrong["T_ports"][0] + with self.assertRaisesRegex(ValueError, "port partition"): + V.endpoint_calibration(wrong) + + def test_noncommuting_state_dependent_errors_at_every_cut(self): + l0, l1, h, c = ["L", 0], ["L", 1], ["L", 224], ["C", 0] + events = clear_all() + [ + ["native_line", h, "R", 0, 0], add(l0, h, 3, 4), + ["cover_map", l0, "S", 0, 0], add(c, l0, -1, 2), + ["native_line", c, "R", 0, 0], add(l1, c), + ["scalar", ["scale", h, -1, 2], 0], + ["native_line", h, "R", 0, 0], add(l0, l1, -1)] + clear_all() + trace = [] + report = V.stage(events, trace) + self.assertNotEqual(rotate(reflect((1, 2))), reflect(rotate((1, 2)))) + for u in (Q(0), Q(1, 64), Q(1, 128)): + self.assertLessEqual(report["defect_sites"] * u, Q(1, 2)) + ideal = [(Q(0), Q(0)) for _ in range(712)] + ideal[0], ideal[1], ideal[224] = (Q(1), Q(0)), (Q(0), Q(1)), (Q(-1), Q(0)) + noisy = ideal.copy() + for t, (event, row) in enumerate(zip(events, trace)): + d, ideal_value, cleared = oracle_step(ideal, event) + _, actual_value, _ = oracle_step(noisy, event) + ideal[d] = ideal_value + # A coherent, state-dependent error rotated away from its operand. + noise = (Q(0), Q(0)) if cleared else tuple(u * x for x in rotate(actual_value)) + noisy[d] = plus(actual_value, noise) + error = plus(noisy[d], ideal[d], -1) + bound = 2 * u * Q(row["J"]) + self.assertLessEqual(scalar_norm2(error), bound * bound, (u, t)) + self.assertLessEqual(scalar_norm2(noisy[d]), (2 * Q(row["P"]))**2, (u, t)) + + def test_positive_polynomial_derivative(self): + events = clear_all() + [add(["L", 0], ["L", 224], -3, 4), + ["native_line", ["L", 224], "R", 0, 0], + add(["C", 0], ["L", 0]), add(["L", 1], ["C", 0], 1, 2)] + clear_all() + trace = [] + V.stage(events, trace) + polynomials = [{0: Q(1)} for _ in range(704)] + [{} for _ in range(8)] + for e, record in zip(events, trace): + if e[0] == "scalar": + g = e[1] + d = g[1][1] + 704 * (g[1][0] == "C") + if g[0] == "clear": + polynomials[d] = {} + else: + s = g[2][1] + 704 * (g[2][0] == "C") + p = dict(polynomials[d]) + for power, value in polynomials[s].items(): + p[power] = p.get(power, Q(0)) + abs(Q(g[3], g[4])) * value + polynomials[d] = {k + 1: v for k, v in p.items()} + else: + d = e[1][1] + polynomials[d] = {k + 1: v for k, v in polynomials[d].items()} + self.assertEqual(sum(polynomials[d].values()), Q(record["P"])) + self.assertEqual(sum(k * v for k, v in polynomials[d].items()), Q(record["J"])) + + def test_feedback_factor_cannot_be_dropped(self): + u = Q(1, 4) + actual_error = (1 + u)**2 - 1 + self.assertGreater(actual_error, 2 * u) + self.assertLessEqual(actual_error, 2 * u * (1 + u)) + self.assertLessEqual(actual_error, 2 * u * 2) + + def test_dirty_ratio_and_noisy_helper_carry(self): + # x+=h; x-=h, with a legal final relative fault, restores h exactly. + u, dirty = Q(1, 1024), Q(2**20) + data_error = 2 * u * dirty + self.assertGreater(data_error, 2 * u) # data-only input bound is insufficient. + # F: h+=x; h-=x with the final defect 2u, starting x=1,h=0. + returned_h = 2 * u + self.assertGreater(returned_h, 0) # reusing the old D=0 bound is invalid. + # B: t+=h with defect u*h; t-=h exactly. The carried error is an operand. + terminal = (1 + u) * returned_h - returned_h + self.assertEqual(terminal, 2 * u * u) + self.assertGreater(terminal, 0) + self.assertLessEqual(returned_h, 0 + 2 * u) + + def test_native_and_map_defects_must_be_counted(self): + for event in (["native_line", ["L", 0], "R", 0, 0], + ["cover_map", ["L", 0], "S", 0, 0]): + full = V.stage(clear_all() + [event]) + omitted = V.stage(clear_all()) + self.assertEqual(Q(full["terminal"]["data"]["J"]), 1) + self.assertEqual(Q(omitted["terminal"]["data"]["J"]), 0) + self.assertGreater(Q(1, 64), 2 * Q(1, 64) * Q(omitted["terminal"]["data"]["J"])) + + def test_private_transient_and_clear_ownership(self): + events = clear_all() + [add(["C", 0], ["L", 0]), + ["native_line", ["C", 0], "R", 0, 0]] + clear_all() + r = V.stage(events) + self.assertGreater(Q(r["all_cut"]["J"]["J"]), 0) + self.assertEqual(Q(r["terminal"]["data"]["J"]), 0) + with self.assertRaisesRegex(ValueError, "uninitialized"): + V.stage([add(["C", 0], ["L", 0])] + clear_all()) + with self.assertRaisesRegex(ValueError, "owned CLEAR"): + V.stage([["scalar", ["clear", ["L", 224]], 0]] + clear_all()) + with self.assertRaisesRegex(ValueError, "unknown event"): + V.stage([["unpriced_multiwire_child", 0]]) + body = [clear_all()[0], ["cover_map", ["L", 0], "S", 0, 0], clear_all()[0]] + malformed = {"programs": {"F_0": [["private_sweep", "bad", body]]}} + with self.assertRaisesRegex(ValueError, "owner-local"): + V.expand(malformed, "F_0") + malformed["programs"]["F_0"][0][2] = [add(["C", 0], ["L", 0]), clear_all()[0]] + with self.assertRaisesRegex(ValueError, "first/last"): + V.expand(malformed, "F_0") + + def test_sign_invariance_and_scalar_price_change(self): + events = clear_all() + [add(["L", 0], ["L", 224], -1, 2)] + a = V.stage(events) + changed = deepcopy(events) + changed[-1][1][3] *= -1 + b = V.stage(changed) + self.assertEqual(a["all_cut"], b["all_cut"]) + self.assertNotEqual(a["event_sha256"], b["event_sha256"]) + changed[-1][1][4] = 1 + self.assertGreater(Q(V.stage(changed)["all_cut"]["J"]["J"]), Q(a["all_cut"]["J"]["J"])) + + def test_exact_budget_and_logarithm_controls(self): + r = json.loads((HERE / "RESULT.json").read_text()) + c = r["composition"] + jf, jb = Q(c["F_persistent_J"]), Q(c["B_persistent_J"]) + self.assertTrue(2**61 < jf < 2**62) + self.assertTrue(2**81 < jb < 2**82) + for beta, delta in ((0, 0), (64, 0), (64, 12), (127, 300)): + uf, ub = Q(2)**(-beta-delta-71), Q(2)**(-beta-delta-102) + self.assertLessEqual(2 * uf * jf * 2**delta, Q(2)**(-beta-8)) + self.assertLessEqual(2 * ub * jb * 2**(delta+6), Q(2)**(-beta-13)) + self.assertLess(26977 * max(uf, ub), Q(1, 2)) + # One fewer bit fails this particular majorant, not every implementation. + self.assertGreater(2 * Q(2)**-101 * jb * 64, Q(2)**-13) + self.assertEqual(Q(c["decoded_error_ratio"]), Q(7587, 8192)) + for value, expected in ((Q(1, 8), -3), (1, 0), (Q(3, 2), 1), (2, 1), (Q(17, 8), 2)): + self.assertEqual(V.ceil_log2(value), expected) + + def test_corrupted_input_rejected_before_math(self): + original_root = V.ROOT + sources = json.loads((HERE / "SOURCES.json").read_text()) + with tempfile.TemporaryDirectory(dir=HERE) as temp: + root = Path(temp) + for item in sources["files"]: + if item["usage"] == "input": + target = root / item["path"] + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes((original_root / item["path"]).read_bytes()) + target = root / V.CERT + target.write_bytes(target.read_bytes() + b"changed") + try: + V.ROOT = root + with self.assertRaisesRegex(ValueError, "source hash"): + V.load() + finally: + V.ROOT = original_root + + +if __name__ == "__main__": + unittest.main() diff --git a/research/qq16-rounded-producer-envelope/verify.py b/research/qq16-rounded-producer-envelope/verify.py new file mode 100644 index 0000000000..1a76ac36d1 --- /dev/null +++ b/research/qq16-rounded-producer-envelope/verify.py @@ -0,0 +1,248 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Positive, noise-aware completed-operation ledger for the two QQ16 stages. + +Prepared for commdata2338, with substantial OpenAI Codex assistance. +Native isometry semantics are inherited; no native operator is replaced by +identity in a signed physical-state calculation. This is a norm majorant. +""" +import argparse +from collections import Counter +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] +CATEGORIES = ("add", "scale", "child", "adapter", "map") +WIDTH = 712 +PERSISTENT = 704 +CERT = "research/joint-query/certificate.json.gz" + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def encoded(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + + +def read_json(path, limit=2_000_000): + raw = path.read_bytes() + require(len(raw) <= limit, "oversize JSON: " + str(path)) + return json.loads(raw) + + +def load(): + sources = read_json(HERE / "SOURCES.json") + for item in sources["files"]: + if item["usage"] == "input": + raw = (ROOT / item["path"]).read_bytes() + require(len(raw) <= 16_000_000, "oversize source") + require(hashlib.sha256(raw).hexdigest() == item["sha256"], + "source hash: " + item["path"]) + with gzip.open(ROOT / CERT, "rb") as stream: + raw = stream.read(16_000_001) + require(len(raw) <= 16_000_000, "oversize certificate payload") + packet = json.loads(raw) + require(packet["schema"] == "conserved-qq16-full-cover-native-words-v1", + "source schema") + return packet + + +def wire(token): + require(isinstance(token, list) and len(token) == 2, "register token") + kind, index = token + require(type(index) is int and kind in ("L", "C"), "register type") + require(0 <= index < (704 if kind == "L" else 8), "register index") + return index + (704 if kind == "C" else 0) + + +def expand(packet, name): + result = [] + for event in packet["programs"][name]: + if event[0] == "retained_core": + expected = "forward" if name == "F_0" else "backward" + require(event[1] == expected, "core orientation") + result.extend(packet["core_words"][expected]) + elif event[0] == "private_sweep": + body = event[2] + require(body and all(e[0] in ("scalar", "native_line") for e in body), + "private sweep must be owner-local") + require(body[0][0] == body[-1][0] == "scalar" and + body[0][1] == body[-1][1] == ["clear", ["C", 0]], + "private sweep needs first/last C0 CLEAR") + result.extend(body) + elif event[0] == "cover_sweep": + result.extend(event[2]) + else: + result.append(event) + require(len(result) <= 28_000, "event bound") + return result + + +def operation(event): + """Return kind, target, source, absolute coefficient, defect category.""" + kind = event[0] + if kind == "phase": + return ("marker", -1, -1, Q(0), None) + if kind == "scalar": + gate = event[1] + d = wire(gate[1]) + if gate[0] == "clear": + require(len(gate) == 2 and d >= 704, "owned CLEAR only") + return ("clear", d, -1, Q(0), None) + if gate[0] == "scale": + require(len(gate) == 4 and gate[2] != 0, "SCALE syntax") + return ("scale", d, -1, abs(Q(gate[2], gate[3])), "scale") + require(gate[0] == "add" and len(gate) == 5, "ADD syntax") + s = wire(gate[2]) + require(s != d and gate[3] != 0, "nonzero distinct-source ADD") + return ("add", d, s, abs(Q(gate[3], gate[4])), "add") + if kind in ("native_line", "cover_map"): + return ("isometry", wire(event[1]), -1, Q(1), + "child" if kind == "native_line" else "map") + require(kind in ("climb", "adapter", "residual_adapter"), "unknown event") + d = event[2] + require(type(d) is int and 0 <= d < 704, "native target") + return ("isometry", d, -1, Q(1), "child" if kind == "climb" else "adapter") + + +def row_record(index, d, p, j, degree): + return {"event": index, "wire": d, "P": str(p[d]), + "J": str(sum(j[d])), "degree": degree[d], + "J_by_category": dict(zip(CATEGORIES, map(str, j[d])))} + + +def stage(events, trace=None): + """At z=1 compute each positive path polynomial and its derivatives.""" + p = [Q(1)] * 704 + [Q(0)] * 8 + j = [[Q(0) for _ in CATEGORIES] for _ in range(WIDTH)] + degree = [0] * WIDTH + initialized = [True] * 704 + [False] * 8 + maxima = {"P": row_record(-1, 0, p, j, degree), + "J": row_record(-1, 0, p, j, degree)} + counts, categories = Counter(), Counter() + digest, simple_digest = hashlib.sha256(), hashlib.sha256() + changed, degree_max = 0, 0 + for index, event in enumerate(events): + kind, d, s, c, category = operation(event) + counts[event[0]] += 1 + if kind == "marker": + continue + changed += 1 + if kind == "clear": + p[d], j[d], degree[d], initialized[d] = Q(0), [Q(0)] * 5, 0, True + else: + require(initialized[d] and (s < 0 or initialized[s]), "uninitialized read") + categories[category] += 1 + if kind == "add": + p[d] += c * p[s] + j[d] = [a + c * b for a, b in zip(j[d], j[s])] + degree[d] = max(degree[d], degree[s]) + elif kind == "scale": + p[d] *= c + j[d] = [c * a for a in j[d]] + j[d][CATEGORIES.index(category)] += p[d] + degree[d] = degree[d] + 1 if p[d] else 0 + record = row_record(index, d, p, j, degree) + if trace is not None: + trace.append(record) + digest.update(encoded(record) + b"\n") + simple_digest.update(encoded([index, d, record["P"], record["J"]]) + b"\n") + for label in ("P", "J"): + if Q(record[label]) > Q(maxima[label][label]): + maxima[label] = record + degree_max = max(degree_max, degree[d]) + require(all(initialized), "private initialization coverage") + require(all(p[d] == 0 and sum(j[d]) == 0 for d in range(704, 712)), + "private fields must finish at exact zero") + terminals = {} + for name, lo, hi in (("data", 0, 224), ("helpers", 224, 704)): + d = max(range(lo, hi), key=lambda i: sum(j[i])) + terminals[name] = row_record(len(events) - 1, d, p, j, degree) + return {"events": len(events), "changed_cuts": changed, "event_counts": dict(counts), + "defect_category_counts": dict(categories), + "defect_sites": changed - sum( + e[0] == "scalar" and e[1][0] == "clear" for e in events), + "clear_sites": sum(e[0] == "scalar" and e[1][0] == "clear" for e in events), + "event_sha256": hashlib.sha256(encoded(events)).hexdigest(), + "cut_table_sha256": digest.hexdigest(), "degree_max": degree_max, + "P_J_cut_table_sha256": simple_digest.hexdigest(), + "all_cut": maxima, "terminal": terminals} + + +def ceil_log2(value): + value = Q(value) + require(value > 0, "positive logarithm argument") + k = value.numerator.bit_length() - value.denominator.bit_length() + power = Q(2) ** k + return k if power >= value else k + 1 + + +def endpoint_calibration(packet): + """Check the geometry used by the inherited ideal F0 endpoint bound 58.""" + a, t, ordinary = packet["A_ports"], packet["T_ports"], packet["U_ports"] + require(len(a) == len(t) == 8 and len(ordinary) == 96, "port class sizes") + require(sorted(a + t + ordinary) == list(range(112)), "port partition") + r = [{int(i): Q(v) for i, v in row.items()} for row in packet["R_rows"]] + k = [{int(i): Q(v) for i, v in row.items()} for row in packet["K_rows"]] + require(len(r) == 8 and len(k) == 112, "R/K dimensions") + for port, row in enumerate(k): + require(row == {i: r[i][port] / 4 for i in range(8) if port in r[i]}, "K=R*/4") + require(sum(map(abs, row.values())) == 1, "K absolute row sum") + for section in (a, t): + for i in range(8): + require(sum(abs(r[i].get(p, 0)) for p in section) == 4, "selected row sum") + for j in range(8): + require(sum(r[i].get(p, 0) * r[j].get(p, 0) for p in section) + == (4 if i == j else 0), "section identity") + query = [sum(map(abs, row.values())) for row in r] + require(query == [56] * 8, "full query row sums") + x = [sum(abs(c) * (4 if p in a else query[i]) for i, c in row.items()) + + (1 if p in ordinary else 0) for p, row in enumerate(k)] + y = [value + (1 if p in ordinary else 2) for p, value in enumerate(x)] + require(max(x + y) == 58, "inherited F0 endpoint majorant") + return {"F_data_norm_over_H": "58", "K_row_sum": "1", "R_row_sum": "56", + "X_A_T_U": ["4", "56", "57"], "Y_A_T_U": ["6", "58", "58"]} + + +def result(packet): + cases = {name: stage(expand(packet, name)) for name in ("F_0", "B_1_2")} + j = {name: max(Q(r["J"]) for r in case["terminal"].values()) + for name, case in cases.items()} + f_offset, b_offset = 9 + ceil_log2(j["F_0"]), 20 + ceil_log2(j["B_1_2"]) + count_guard = ceil_log2(2 * max(c["defect_sites"] for c in cases.values())) + return {"schema": "qq16-rounded-producer-envelope-v1", "cases": cases, + "ideal_endpoint_calibration": endpoint_calibration(packet), + "composition": {"F_persistent_J": str(j["F_0"]), + "B_persistent_J": str(j["B_1_2"]), + "F_tolerance_offset": f_offset, "B_tolerance_offset": b_offset, + "count_guard": count_guard, + "common_relative_offset": max(f_offset, b_offset, count_guard), + "F_entry_bound": "2^delta H", "B_entry_bound": "2^(delta+6) H", + "decoded_error_ratio": str(Q(49, 256) + Q(1923, 8192) + Q(1, 2))}} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="create a new receipt, never overwrite") + args = parser.parse_args() + report = result(load()) + if args.write: + with args.write.open("x") as stream: + stream.write(json.dumps(report, indent=2, sort_keys=True) + "\n") + else: + require(encoded(report) == encoded(read_json(HERE / "RESULT.json")), "receipt mismatch") + cuts = sum(case["changed_cuts"] for case in report["cases"].values()) + print("PASS_QQ16_ROUNDED_PRODUCER_ENVELOPE", + "stages=2", "cuts=" + str(cuts), "offset=" + str(report["composition"]["common_relative_offset"]), + "conditional_completed_operations no_new_kappa") + + +if __name__ == "__main__": + main()