diff --git a/research/qq16-final-record-obstruction/PROOF.md b/research/qq16-final-record-obstruction/PROOF.md new file mode 100644 index 0000000000..894b028152 --- /dev/null +++ b/research/qq16-final-record-obstruction/PROOF.md @@ -0,0 +1,297 @@ +# The final records do not recover the recorded first-pair cut + +This is a scoped theorem for the actual routed QQ16 maps, on the retained +ordinary-bank schedule with no added selected intervention before the +completion of F2. It upgrades Philippe Van Velzen's finite-model +final-only failure to a regular-cover argument. It does not contradict +PR #2174: that recovery theorem explicitly grants the selected state at +the cut after B1, whereas the observation contract here grants only the +final selected state. + +The result is not a claim about every selected controller. In particular, +this package does **not** identify an unprovided historical first-six-swap +selected program with the ordinary-only bridges used below. A swap or +other intervention before F2 changes this theorem's hypotheses. + +## 1. Exact contract and conclusion + +Let G be the finite actual owner cover group, N=|G|. Work with +rational-valued logical fields on G, constant in the payload coordinates. +The actual cover maps preserve this subspace: their payload translations +act trivially, while their right owner actions remain genuine regular +actions. One may use the subgroup generated by the actual route matrices +or a full owner group containing it with its regular action; the latter +decomposes into free orbits. This proof does not apply to an arbitrary +nonregular quotient action. It applies at every positive tensor payload +size. Invertible native input/output frames transport the logical kernel +family to the corresponding native interface; those frames need not +preserve the payload-constant subspace themselves. + +Use the retained local forward and conserved backward maps from +`research/joint-query/evidence/CONSERVED-QQ16.md`, equations (1)--(3). +Write + + B_s = R_s iota_U, + P_(s,A) = D_s^-1 iota_A R_A^-1, + ell_(s,A) = R_A pi_A D_s, + +and similarly for T. Selected sections and their selected readers are +mutual inverses on their eight selected fields. U has 96 ports; A and T +are the eight-port sets in the source packet. + +The exact 19-event recipe is read from the source-bound selected archive. +The local calls at stages 0,...,8 use pairs + + 0, 0, 0, 1, 1, 2, 2, 3, 3. + +Even stages are forward F_s; odd stages are backward B_(s,s+1). +An ordinary bridge `src=i,dst=j,coefficient=c` acts only on U: + + X_j,U += c X_i,U; + Y_i,U -= c Y_j,U. + +Between local calls there are no additional selected operations in the +base contract. The final ordinary terminal is `(X_U,Y_U) -> (Y_U,-X_U)`. +Any homogeneous selected terminal, including the same signed exchange, +has the same zero selected output on the family below. +The named final Y fields are the completed-X descendants; named final X +fields have the former-Y type. + +The observation O consists of: + +1. Every final selected X and Y field of all four pairs. +2. Every final completed-X ordinary field, namely final Y_(k,U). +3. All five forward query histories f0,f2,f4,f6,f8. +4. The following eight initial ordinary-query records, each of dimension + eight per owner (64 coordinates per owner in total): + + pair 0: B0 X_(0,U), B2 X_(0,U); + pair 1: B3 X_(1,U), B4 X_(1,U); + pair 2: B5 X_(2,U), B6 X_(2,U); + pair 3: B7 X_(3,U), B8 X_(3,U). + +These are exactly the bank-local initial records used in the credited +four-bank final-only experiment. Their storage and reads are granted +without cost for this impossibility statement. No post-B1 selected cut, +former-Y ordinary endpoint, or additional ordinary read is observed. + +**Theorem.** If J selects the original A/T inputs of pair 0, then + + dim J(ker O) >= ceil(8N/7) > 0. + +Consequently no decoder, linear or otherwise, can recover those original +selected inputs from this observation contract. In particular, these +final records do not imply the post-B1-cut premise of PR #2174. This is +an information obstruction for this fixed contract, not a native cost +bound, a failure of the selected supplier, or a new kappa claim. + +## 2. Actual source-bound trace identities + +The checker reconstructs the centre matrix R from the original scalar +program before its centre cut, and compares it with the retained QQ16 +packet. It checks + + B_s B_s* = 48 I_(8N), + ||r_p||^2 = 4 for every ordinary port p, + +where * is the transpose and inverse regular action. The first identity +also follows directly from `R_U R_U^T=48 I_8`: in each same-port term the +route cancels with its inverse. + +For each of the six distinct stage pairs + + (0,1), (0,2), (1,2), (2,3), (2,4), (3,4), + +the checker reconstructs all 96 actual relative owner-route matrices +and verifies that they are pairwise distinct. Routes come from the +73-dimensional DATA-PHASES source, and all 1008 reconstructed stage/port +routes are matched to owner matrices at their exact stage/port positions in the +native forward programs (stage zero has its separately checked identity +route base case). They are not +random permutation fixtures or a quotient that identifies owners. + +For s != t among those pairs, let C=B_s B_t*. A nonidentity regular +translation has trace zero. Distinct relative routes imply that the +identity coefficient of C C* receives contributions only from equal +port indices. Its eight-by-eight matrix is + + sum_p (r_p r_p^T)^2 + = sum_p ||r_p||^2 r_p r_p^T + = 4 R_U R_U^T + = 192 I_8. + +Therefore the full regular trace is 1536N, not 192N. Define orthogonal +projections on the ordinary-coordinate space by + + Q_s = B_s* B_s / 48. + +Their traces satisfy + + tr Q_s = 8N, + tr(Q_s Q_t) = 1536N / 48^2 = (2/3)N. + +For either triple I={0,1,2} or I={2,3,4}, set S_I=sum_(s in I) Q_s. +It is positive semidefinite, and + + tr S_I = 24N, + tr(S_I^2) = 3(8N) + 6(2N/3) = 28N. + +Cauchy--Schwarz on its nonzero eigenvalues gives + + rank S_I >= (tr S_I)^2 / tr(S_I^2) = 144N/7. (1) + +Its kernel is the common kernel of the three B_s, so (1) is also a +lower bound on the rank of the stacked three-reader map. Rational and +real matrix ranks agree. The trace argument is a proof for the actual +finite regular action; the checker certifies its finite route and +coefficient premises without enumerating G. + +## 3. A nonzero compatible pair of ordinary inputs exists + +Let the two subspaces of the 8N-dimensional query space be + + V = B1(ker B0 intersect ker B2), + W = B2(ker B3 intersect ker B4). + +For linear maps A and B on the same domain, + + dim B(ker A) = rank [A;B] - rank A. + +Applying (1), and bounding each two-reader rank above by 16N, gives + + dim V >= ceil(32N/7), + dim W >= ceil(32N/7). (2) + +The transport M=-ell_(2,A) P_(1,A) is invertible between the two query +spaces: both factors are selected-coordinate isomorphisms. Hence + + dim(M V intersect W) + >= dim V + dim W - 8N + >= 2 ceil(32N/7) - 8N + >= ceil(8N/7). (3) + +For every nonzero w in this intersection choose ordinary vectors z0,z1 +with + + B0 z0 = B2 z0 = 0, + B3 z1 = B4 z1 = 0, + B2 z1 = -ell_(2,A) P_(1,A) B1 z0 = w != 0. (4) + +Set + + d = -P_(1,A) B1 z0, + +so `ell_(2,A)d=w`, and d is nonzero. Everything is rational, so finite +rational linear sections can choose z0,z1 linearly in w. This proves +existence of an actual regular-cover family; it does not emit a compact +individual owner vector or assert an efficient native way to prepare it. +No support-size, coefficient-bitlength or precision bound is supplied. + +## 4. The exact two-bank trajectory + +Initialize pair 0 by + + X_(0,U)=z0, Y_(0,U)=0, + X_(0,A)=d, Y_(0,A)=-d, + X_(0,T)=-P_(0,T) ell_(0,A)d, + Y_(0,T)=-X_(0,T). + +Initialize pair 1 with `X_(1,U)=z1` and every other field zero. All +fields of pairs 2 and 3 are zero. The sixteen selected pair sums are +zero in every pair. All eight initial query records vanish by (4). + +At F0, `f0=B0 z0+ell_(0,A)d-ell_(0,A)d=0`. The selected output is +`X_A=-d,Y_A=d,X_T=Y_T=0`; the ordinary pair is `(z0,z0)`. + +At B_(1,2), the future A logger leaves d unchanged because `B2 z0=0`. +The old T driver is zero. Its current query is + + b1 = B1 z0 + ell_(1,A)d = 0. + +The state immediately after B1 is therefore + + pair 0 ordinary: (X_U,Y_U)=(0,z0), + pair 0 selected: (X_A,Y_A)=(-d,d), X_T=Y_T=0, + pair 1 ordinary: (z1,0), all its selected fields zero. (5) + +The first positive bridge adds z1 to X_(0,U) and subtracts z0 from +Y_(1,U). At F2 the full query is + + f2 = B2 z1 - ell_(2,A)d = 0. + +The forward rule moves the zero selected T value into A and writes the +zero query into T; conserved sums make every selected Y value zero too. +After the following negative bridge, all selected fields are zero and + + pair 0 ordinary: (0,z0+z1), + pair 1 ordinary: (z1,z1). (6) + +At B_(3,4), the future query is `B4 z1=0`, the old T driver is zero, +and the current query is `B3 z1=0`. It follows that pair 1 becomes +`(0,z1)` with all selected fields zero. + +The remaining positive and negative bridge around F4 cancels its +transient Y_(2,U) value. Every later active local source is zero, so +f4,f6,f8 are zero and every selected field stays zero. The final three +ordinary bridges leave, immediately before the terminal, + + all X_(k,U)=0, + Y_(0,U)=z0, Y_(1,U)=z1, Y_(2,U)=Y_(3,U)=0. + +After `(X,Y)->(Y,-X)`, the only possibly nonzero fields are the two +former-Y ordinary endpoints, final X_(0,U)=z0 and final X_(1,U)=z1. +Every allowed observation is zero, but the required original X_(0,A)=d +is nonzero. + +The verifier implements the local maps literally in a free ordered +linear-expression algebra, using only the selected inverse identities +and relations (4). It binds every event to the archive recipe and +records all nineteen intermediate ordinary states. Its universal force +comes from the written derivation and actual-source existence argument, +not a finite random model. + +For a linear section of the intersection in (3), the original A input +d is an injective function of w. Thus J maps this zero-observation +family to a space of dimension at least ceil(8N/7), proving the theorem. + +## 5. Scope, controls, and remaining obligations + +After complete F2 every selected field is zero. Accordingly the same +family remains invisible if arbitrary homogeneous selected-only linear +operations are inserted after that cut, without extra ordinary reads or +changes to the retained ordinary schedule. This extension does not allow +an earlier selected swap, affine input-dependent auxiliary state, or a +record of d at B1. A B1-cut record and the initial B1 X_(0,U) query both +detect the family, as the rejecting controls demonstrate. + +The primary checker rejects changed centre coefficients, collided owner +routes, wrong initial T sign, wrong selected-transport sign, wrong +cross-bank link sign, omitted B3/B4 kernel premises, a missing negative +bridge, wrong local pair/orientation or bridge sign, a native route placed +at the wrong port with its registry unchanged, and observations that incorrectly treat former-Y endpoints or +the B1 cut as available. The independent checker and package wrapper +provide separate evidence described in README.md. + +No full native word, supplier invoice, hosting or precision theorem is +claimed or replayed here. The original local native admission is +inherited. The result does not establish the selected multiplication +frontier, optimize the transcript dimension, or rule out other choices +of 64 initial query coordinates. Its useful consequence is narrower: +the specified bank-local records do not convert the recorded-cut +recovery into a final-only recovery on this actual routed schedule. + +## Credit + +Ali Romman (PR #1969) supplies the QQ16 local maps and retained packet. +The original owner embedding, centre geometry and selected recipe retain +their supplier and compiler lineage. Ross Richardson (PR #2104) supplies +the trace/rank method; @commdata2338 (PR #2174) supplies the explicitly +recorded-cut two-query recovery contract. Philippe Van Velzen's +`680d0997621a2cecfef2186ab143377658687825` four-bank experiment supplies +the earlier final-only finite-model failure and the all-bank record +choice. Adam Gall (PR #2093) supplies adjacent actual-route hidden-query +analysis. This contribution proves a new actual-cover two-bank +intersection obstruction for that final-only contract; it does not claim +those predecessor observations or methods as new. + +Prepared with substantial OpenAI Codex assistance. Apache-2.0. \ No newline at end of file diff --git a/research/qq16-final-record-obstruction/README.md b/research/qq16-final-record-obstruction/README.md new file mode 100644 index 0000000000..27092b97d8 --- /dev/null +++ b/research/qq16-final-record-obstruction/README.md @@ -0,0 +1,129 @@ +# QQ16 final records still lose selected inputs + +**Result:** for the actual routed QQ16 ordinary-only bridge/terminal replica, +the proposed **64 initial query coordinates per owner** still leave at least +`ceil(8|G|/7)` dimensions of pair 0's original selected inputs invisible. +This holds even when every final selected field, every completed-X descendant +and all five forward-query histories are supplied free. Here `G` is the finite +regular owner group. This is a scoped proof with finite source certificates; +**no new supplier or kappa is claimed**. + +The contribution closes a precise negative branch of [PR2174's +handoff](https://github.com/CrocSwap/integer-mult-bounds/pull/2174): its correct +decoder requires a recorded post-B1 cut, which these final records cannot +replace. It upgrades [philippeVV's earlier finite-model +failure](https://github.com/philippeVV/integer-mult-bounds/tree/680d0997621a2cecfef2186ab143377658687825/research/joint-query-first-pair-catalogue/four-bank) +to an actual regular-cover theorem. That predecessor already supplied the +finite-model observation, the all-bank record choice, and an actual-route +moment census; none is presented here as a new discovery. + +## Exact boundary + +The local calls use pairs `0,0,0,1,1,2,2,3,3`. Bridges and the terminal act on +the 96 ordinary ports. No selected intervention is inserted before F2. The +initial read-only records are `(B0,B2)` on pair 0 and `(B3,B4)`, `(B5,B6)`, +`(B7,B8)` on pairs 1, 2, 3. These eight queries have eight coordinates each +per owner. The observation includes final Y ordinary fields (completed-X), +not the final X fields carrying former-Y values. + +This is **not** a theorem about arbitrary early selected controllers or the +separate first-six-selected-swap program. Selected fields are nonzero after +B1 and become zero only after F2. Homogeneous selected-only linear operations +after that cut preserve this family. The theorem does not price the queries, +claim 64 paid native ranks, or contradict the selected conditional exponent +`0.001672660197076918`. + +## Why the obstruction exists + +[PROOF.md](PROOF.md) derives two constrained query-image spaces from the actual +routes. The credited exact moments `(24,28)|G|` give each image dimension at +least `ceil(32|G|/7)`. After the required invertible selected transport, their +intersection has dimension at least `ceil(8|G|/7)`. Rational sections provide +two ordinary inputs whose nonzero original selected data cancel through F2. +The complete 19-event trajectory then leaves every permitted observation zero. +At the post-B1 cut, however, `Y_A=d` is nonzero. That is the missing record. + +All named observations and their access, storage and restoration are granted +zero additional cost in this screen. Paying more for the same read-only +records cannot repair its kernel; a viable successor must change the record +or early dynamics. No large owner group is enumerated and no compact witness +vector or coefficient-bitlength bound is supplied. + +## Replay and evidence + +Python 3.12, standard library, from the repository root: + +```sh +python -I -B scripts/research_package.py --package research/qq16-final-record-obstruction +python -I -O -B research/qq16-final-record-obstruction/verify.py +``` + +Expected marker: `PASS_QQ16_FINAL_RECORD_OBSTRUCTION`. + +- `verify_core.py` reconstructs R by forward propagation of the original + scalar word, binds 1,008 actual owner routes to the native packet at their + exact stage/port positions, checks six relative-route sets, and executes + all 19 events in ordered symbolic algebra. +- `independent_moments.py` imports no research code. It reconstructs R by + backward covectors and owner maps by swaps in a full orthonormal basis, + then accumulates collision-aware group-algebra coefficients. Its matrix + and route digests must agree with the primary checker. +- `independent_algebra.py` uses separately factored local maps on five exact + rational models with noncommuting selected charts. It checks the full + schedule and two sign controls. These fixtures check algebra only; the + actual-cover existence argument is in the proof. +- `RESULT.json` stores the complete deterministic result. Default replay + compares every field without writing. Semantic controls exercise wrong + coefficients, route placement/collision, constraints, signs, schedule and + observation types; adding the missing cut record is a detecting control. +- `test_integrity.py` runs a Git-free relocated copy, checks replay leaves + its bytes unchanged, and requires altered receipts and sources to fail. + +`python -I -B research/qq16-final-record-obstruction/verify.py --write` is the +explicit receipt generator. It is not needed for normal verification. + +The source-bound baseline orientation passed on Windows/Python 3.12.2 using +an extended-length script path; ordinary Windows paths initially hid seven +long pinned inputs. No input was changed or pin weakened. The selected +`make frontier1094-verify` full cold replay was **not** run: this contribution +changes neither supplier nor selected record. Native compilation, physical +hosting, precision/tape, all-size admission and a full multiplication theorem +remain outside this package. The written argument establishes the regular- +cover statement; finite checker success is not formal theorem verification. + +## Provenance and credit + +Base main: `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority revision 4. +Task `uniform-transfer-audit`, refined without reroll, seed +`b477785a8515f4c055aa3f8bcf59935f`. [Claim and +handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/2074#discussioncomment-18941784). +`TASK.json` records scope, overlap coverage, environment and next questions; +`SOURCES.json` pins every consumed main input and names exact predecessor heads. +No pending executable is imported. + +Credit Ali Romman (#1969) for the QQ16 maps and source construction; Ross +Richardson (#2104) for the two-moment method; Adam Gall (#2093) for adjacent +actual-route query analysis; @commdata2338 (#2174/#2189) and Nick Petalas +(#2181) for the cut-recovery and higher-moment work; and philippeVV for the +four-bank final-only lead. The Rohan Arun, Jeremy Kothe, Hao Yan and earlier +supplier lineage and licenses remain in the unchanged [QQ16 source +notice](../joint-query/NOTICE.md) and archive. New material is Apache-2.0. + +Prepared for @alephnan with substantial OpenAI Codex assistance in research, +proof, implementation, writing and separate agent checks. Independent agent +review is not independent human or proof-assistant review. + +## Open next questions + +1. **Change the controller before F2.** Test one explicit typed intervention + against the full observation kernel, then price its frames and cleanup. + It matters because this theorem deliberately fixes that early dynamics; + a legal completed replacement is not constructed here. +2. **Retain the post-B1 A record.** It detects this family. Specify native + access, storage lifetime and inverse cleanup, then test full recovery + rather than only this family. Physical implementation and pricing block + admission. +3. **Emit a compact actual-cover witness.** Solve the displayed four kernel + constraints and transport identity in a source-bound function basis. + A compact vector would enable direct routed regression; support size + and precision bounds are currently unknown. diff --git a/research/qq16-final-record-obstruction/RESULT.json b/research/qq16-final-record-obstruction/RESULT.json new file mode 100644 index 0000000000..4eb06f2113 --- /dev/null +++ b/research/qq16-final-record-obstruction/RESULT.json @@ -0,0 +1,1556 @@ +{ + "independent_algebra": { + "cases": [ + { + "initial_A": [ + "3", + "-11" + ], + "initial_records": 8, + "seed": 0, + "zero_histories": 5 + }, + { + "initial_A": [ + "5", + "-22" + ], + "initial_records": 8, + "seed": 1, + "zero_histories": 5 + }, + { + "initial_A": [ + "7", + "-37" + ], + "initial_records": 8, + "seed": 2, + "zero_histories": 5 + }, + { + "initial_A": [ + "9", + "-56" + ], + "initial_records": 8, + "seed": 3, + "zero_histories": 5 + }, + { + "initial_A": [ + "11", + "-79" + ], + "initial_records": 8, + "seed": 4, + "zero_histories": 5 + } + ], + "model_count": 5, + "ordinary_dimension": 4, + "query_dimension": 2, + "recipe_events": 19, + "rejected_controls": [ + "wrong_link_sign", + "wrong_bridge_sign" + ], + "scope": "exact noncommuting algebra fixtures; actual-cover existence is proved separately", + "status": "PASS_INDEPENDENT_FACTORIZED_QQ16_TRAJECTORY" + }, + "independent_moments": { + "R_columns_sha256": "38664b168db7ae1158c3c4cbd56622d5cf0ff22911e02c2c4aed323316566d82", + "archive_members": { + "phases": { + "path": "t16/global/base/work/complex-nine-native/DATA-PHASES.json", + "sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + "program": { + "path": "slots/local/LOCAL-PROGRAMS.json.gz", + "sha256": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a" + }, + "word": { + "path": "slots/local/CANONICAL-WORD.json.gz", + "sha256": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219" + } + }, + "archive_sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "centre_sha256": "70055070e6f0465dcb9f99773769809f032043e7a1cba4f0c0fe5e5c365f0213", + "conditional_image_lower_per_owner": "32/7", + "controls": [ + "changed R coefficient rejected", + "wrong selected port rejected", + "colliding route rejected", + "collapsed-owner action rejected; regular-action trace domain required" + ], + "normalized_moment1_per_owner": "24", + "normalized_moment2_per_owner": "28", + "ordinary_gram": 48, + "pairs": [ + { + "cross_identity_matrix": [ + [ + 192, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 192, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 192, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 192, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 192, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 192, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 192, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 192 + ] + ], + "cross_trace_per_owner": 1536, + "relative_route_sha256": "3ab11c32aa2a2fe41cfcd48af4156bfdab95d1dccdc0a52cec01ff9544b5e8fa", + "routes": 96, + "stages": [ + 0, + 1 + ] + }, + { + "cross_identity_matrix": [ + [ + 192, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 192, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 192, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 192, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 192, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 192, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 192, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 192 + ] + ], + "cross_trace_per_owner": 1536, + "relative_route_sha256": "a071cc6f2fdd1335103470d6092a9ad86ec37f43534621dd4b4de7319e0edbd5", + "routes": 96, + "stages": [ + 0, + 2 + ] + }, + { + "cross_identity_matrix": [ + [ + 192, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 192, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 192, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 192, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 192, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 192, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 192, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 192 + ] + ], + "cross_trace_per_owner": 1536, + "relative_route_sha256": "57c975bc42b34a7130779c11944eda6d3ad3ff82ee46af1de94ae4b3d7828c4d", + "routes": 96, + "stages": [ + 1, + 2 + ] + }, + { + "cross_identity_matrix": [ + [ + 192, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 192, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 192, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 192, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 192, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 192, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 192, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 192 + ] + ], + "cross_trace_per_owner": 1536, + "relative_route_sha256": "62ca2e5961e6827ac1cbed926c0478bfc3b036643a3cbc7d7fafd4a6715e129b", + "routes": 96, + "stages": [ + 2, + 3 + ] + }, + { + "cross_identity_matrix": [ + [ + 192, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 192, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 192, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 192, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 192, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 192, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 192, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 192 + ] + ], + "cross_trace_per_owner": 1536, + "relative_route_sha256": "41a3a72993afb7b125579d1d5c012b024926565d39aa7bc70329b224e55c1180", + "routes": 96, + "stages": [ + 2, + 4 + ] + }, + { + "cross_identity_matrix": [ + [ + 192, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 192, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 192, + 0, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 192, + 0, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 192, + 0, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 192, + 0, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 192, + 0 + ], + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 192 + ] + ], + "cross_trace_per_owner": 1536, + "relative_route_sha256": "97c458285e6f8858d4a3cfc1157b8dac4de824409bbf163fe6615497af0dfe90", + "routes": 96, + "stages": [ + 3, + 4 + ] + } + ], + "scope": "Independent source-bound corroboration of credited moments, not a new moment theorem or verification of final-only controller trajectory.", + "stack_rank_lower_per_owner": "144/7", + "status": "PASS_INDEPENDENT_QQ16_FINAL_ONLY_MOMENTS", + "trace_domain": "finite regular owner representation on payload-constant fields; not an arbitrary quotient or nonfree owner action", + "triples": [ + [ + 0, + 1, + 2 + ], + [ + 2, + 3, + 4 + ] + ] + }, + "input_paths_checked": [ + "research/joint-query/certificate.json.gz", + "research/joint-query/evidence/CONSERVED-QQ16.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json", + "research/community-frontier1042-audit/selected-replay.tar.gz" + ], + "primary": { + "claim": "actual regular-cover selected defect >= ceil(8|G|/7); no supplier or kappa claim", + "rejected_controls": [ + "centre_coefficient", + "relative_route_collision", + "native_route_placement", + "wrong_initial_T_sign", + "wrong_d_sign", + "wrong_link_sign", + "omit_B3_kernel", + "omit_B4_kernel", + "omit_negative_bridge", + "wrong_local_pair", + "wrong_local_orientation", + "wrong_bridge_sign", + "observe_former_Y", + "observe_B1_cut", + "observe_B1_initial" + ], + "sources": { + "R_columns_sha256": "38664b168db7ae1158c3c4cbd56622d5cf0ff22911e02c2c4aed323316566d82", + "bound_native_routes": 1008, + "centre_sha256": "70055070e6f0465dcb9f99773769809f032043e7a1cba4f0c0fe5e5c365f0213", + "constrained_image_lower_per_owner": "32/7", + "pair_checks": [ + { + "cross_gram_identity_diagonal": "192", + "cross_gram_identity_trace": "1536", + "distinct_relative_routes": 96, + "projection_product_trace_per_owner": "2/3", + "relative_routes_sha256": "3ab11c32aa2a2fe41cfcd48af4156bfdab95d1dccdc0a52cec01ff9544b5e8fa", + "stages": [ + 0, + 1 + ] + }, + { + "cross_gram_identity_diagonal": "192", + "cross_gram_identity_trace": "1536", + "distinct_relative_routes": 96, + "projection_product_trace_per_owner": "2/3", + "relative_routes_sha256": "a071cc6f2fdd1335103470d6092a9ad86ec37f43534621dd4b4de7319e0edbd5", + "stages": [ + 0, + 2 + ] + }, + { + "cross_gram_identity_diagonal": "192", + "cross_gram_identity_trace": "1536", + "distinct_relative_routes": 96, + "projection_product_trace_per_owner": "2/3", + "relative_routes_sha256": "57c975bc42b34a7130779c11944eda6d3ad3ff82ee46af1de94ae4b3d7828c4d", + "stages": [ + 1, + 2 + ] + }, + { + "cross_gram_identity_diagonal": "192", + "cross_gram_identity_trace": "1536", + "distinct_relative_routes": 96, + "projection_product_trace_per_owner": "2/3", + "relative_routes_sha256": "62ca2e5961e6827ac1cbed926c0478bfc3b036643a3cbc7d7fafd4a6715e129b", + "stages": [ + 2, + 3 + ] + }, + { + "cross_gram_identity_diagonal": "192", + "cross_gram_identity_trace": "1536", + "distinct_relative_routes": 96, + "projection_product_trace_per_owner": "2/3", + "relative_routes_sha256": "41a3a72993afb7b125579d1d5c012b024926565d39aa7bc70329b224e55c1180", + "stages": [ + 2, + 4 + ] + }, + { + "cross_gram_identity_diagonal": "192", + "cross_gram_identity_trace": "1536", + "distinct_relative_routes": 96, + "projection_product_trace_per_owner": "2/3", + "relative_routes_sha256": "97c458285e6f8858d4a3cfc1157b8dac4de824409bbf163fe6615497af0dfe90", + "stages": [ + 3, + 4 + ] + } + ], + "selected_defect_lower_per_owner": "8/7", + "stacked_rank_lower_per_owner": "144/7", + "triple_square_trace_per_owner": "28", + "triple_trace_per_owner": "24", + "triples": [ + [ + 0, + 1, + 2 + ], + [ + 2, + 3, + 4 + ] + ] + }, + "status": "PASS_QQ16_FINAL_RECORD_OBSTRUCTION", + "trajectory": { + "events": [ + { + "event": { + "kind": "local", + "pair": 0, + "reverse": false, + "stage": 0 + }, + "ordinary": [ + [ + [ + [], + "z0", + 1 + ] + ], + [ + [ + [], + "z0", + 1 + ] + ], + [ + [ + [], + "z1", + 1 + ] + ], + [], + [], + [], + [], + [] + ], + "selected_nonzero_blocks": 2 + }, + { + "event": { + "kind": "local", + "pair": 0, + "reverse": true, + "stage": 1 + }, + "ordinary": [ + [], + [ + [ + [], + "z0", + 1 + ] + ], + [ + [ + [], + "z1", + 1 + ] + ], + [], + [], + [], + [], + [] + ], + "selected_nonzero_blocks": 2 + }, + { + "event": { + "coefficient": 1, + "dst": 0, + "kind": "bridge", + "src": 1 + }, + "ordinary": [ + [ + [ + [], + "z1", + 1 + ] + ], + [ + [ + [], + "z0", + 1 + ] + ], + [ + [ + [], + "z1", + 1 + ] + ], + [ + [ + [], + "z0", + -1 + ] + ], + [], + [], + [], + [] + ], + "selected_nonzero_blocks": 2 + }, + { + "event": { + "kind": "local", + "pair": 0, + "reverse": false, + "stage": 2 + }, + "ordinary": [ + [ + [ + [], + "z1", + 1 + ] + ], + [ + [ + [], + "z0", + 1 + ], + [ + [], + "z1", + 1 + ] + ], + [ + [ + [], + "z1", + 1 + ] + ], + [ + [ + [], + "z0", + -1 + ] + ], + [], + [], + [], + [] + ], + "selected_nonzero_blocks": 0 + }, + { + "event": { + "coefficient": -1, + "dst": 0, + "kind": "bridge", + "src": 1 + }, + "ordinary": [ + [], + [ + [ + [], + "z0", + 1 + ], + [ + [], + "z1", + 1 + ] + ], + [ + [ + [], + "z1", + 1 + ] + ], + [ + [ + [], + "z1", + 1 + ] + ], + [], + [], + [], + [] + ], + "selected_nonzero_blocks": 0 + }, + { + "event": { + "kind": "local", + "pair": 1, + "reverse": true, + "stage": 3 + }, + "ordinary": [ + [], + [ + [ + [], + "z0", + 1 + ], + [ + [], + "z1", + 1 + ] + ], + [], + [ + [ + [], + "z1", + 1 + ] + ], + [], + [], + [], + [] + ], + "selected_nonzero_blocks": 0 + }, + { + "event": { + "coefficient": 1, + "dst": 1, + "kind": "bridge", + "src": 2 + }, + "ordinary": [ + [], + [ + [ + [], + "z0", + 1 + ], + [ + [], + "z1", + 1 + ] + ], + [], + [ + [ + [], + "z1", + 1 + ] + ], + [], + [ + [ + [], + "z1", + -1 + ] + ], + [], + [] + ], + "selected_nonzero_blocks": 0 + }, + { + "event": { + "kind": "local", + "pair": 1, + "reverse": false, + "stage": 4 + }, + "ordinary": [ + [], + [ + [ + [], + "z0", + 1 + ], + [ + [], + "z1", + 1 + ] + ], + [], + [ + [ + [], + "z1", + 1 + ] + ], + [], + [ + [ + [], + "z1", + -1 + ] + ], + [], + [] + ], + "selected_nonzero_blocks": 0 + }, + { + "event": { + "coefficient": -1, + "dst": 1, + "kind": "bridge", + "src": 2 + }, + "ordinary": [ + [], + [ + [ + [], + "z0", + 1 + ], + [ + [], + "z1", + 1 + ] + ], + [], + [ + [ + [], + "z1", + 1 + ] + ], + [], + [], + [], + [] + ], + "selected_nonzero_blocks": 0 + }, + { + "event": { + "kind": "local", + "pair": 2, + "reverse": true, + "stage": 5 + }, + "ordinary": [ + [], + [ + [ + [], + "z0", + 1 + ], + [ + [], + "z1", + 1 + ] + ], + [], + [ + [ + [], + "z1", + 1 + ] + ], + [], + [], + [], + [] + ], + "selected_nonzero_blocks": 0 + }, + { + "event": { + "coefficient": 1, + "dst": 2, + "kind": "bridge", + "src": 3 + }, + "ordinary": [ + [], + [ + [ + [], + "z0", + 1 + ], + [ + [], + "z1", + 1 + ] + ], + [], + [ + [ + [], + "z1", + 1 + ] + ], + [], + [], + [], + [] + ], + "selected_nonzero_blocks": 0 + }, + { + "event": { + "kind": "local", + "pair": 2, + "reverse": false, + "stage": 6 + }, + "ordinary": [ + [], + [ + [ + [], + "z0", + 1 + ], + [ + [], + "z1", + 1 + ] + ], + [], + [ + [ + [], + "z1", + 1 + ] + ], + [], + [], + [], + [] + ], + "selected_nonzero_blocks": 0 + }, + { + "event": { + "coefficient": -1, + "dst": 2, + "kind": "bridge", + "src": 3 + }, + "ordinary": [ + [], + [ + [ + [], + "z0", + 1 + ], + [ + [], + "z1", + 1 + ] + ], + [], + [ + [ + [], + "z1", + 1 + ] + ], + [], + [], + [], + [] + ], + "selected_nonzero_blocks": 0 + }, + { + "event": { + "kind": "local", + "pair": 3, + "reverse": true, + "stage": 7 + }, + "ordinary": [ + [], + [ + [ + [], + "z0", + 1 + ], + [ + [], + "z1", + 1 + ] + ], + [], + [ + [ + [], + "z1", + 1 + ] + ], + [], + [], + [], + [] + ], + "selected_nonzero_blocks": 0 + }, + { + "event": { + "kind": "local", + "pair": 3, + "reverse": false, + "stage": 8 + }, + "ordinary": [ + [], + [ + [ + [], + "z0", + 1 + ], + [ + [], + "z1", + 1 + ] + ], + [], + [ + [ + [], + "z1", + 1 + ] + ], + [], + [], + [], + [] + ], + "selected_nonzero_blocks": 0 + }, + { + "event": { + "coefficient": 1, + "dst": 3, + "kind": "bridge", + "src": 2 + }, + "ordinary": [ + [], + [ + [ + [], + "z0", + 1 + ], + [ + [], + "z1", + 1 + ] + ], + [], + [ + [ + [], + "z1", + 1 + ] + ], + [], + [], + [], + [] + ], + "selected_nonzero_blocks": 0 + }, + { + "event": { + "coefficient": 1, + "dst": 2, + "kind": "bridge", + "src": 1 + }, + "ordinary": [ + [], + [ + [ + [], + "z0", + 1 + ], + [ + [], + "z1", + 1 + ] + ], + [], + [ + [ + [], + "z1", + 1 + ] + ], + [], + [], + [], + [] + ], + "selected_nonzero_blocks": 0 + }, + { + "event": { + "coefficient": 1, + "dst": 1, + "kind": "bridge", + "src": 0 + }, + "ordinary": [ + [], + [ + [ + [], + "z0", + 1 + ] + ], + [], + [ + [ + [], + "z1", + 1 + ] + ], + [], + [], + [], + [] + ], + "selected_nonzero_blocks": 0 + }, + { + "event": { + "kind": "terminal", + "pairs": 4 + }, + "ordinary": [ + [ + [ + [], + "z0", + 1 + ] + ], + [], + [ + [ + [], + "z1", + 1 + ] + ], + [], + [], + [], + [], + [] + ], + "selected_nonzero_blocks": 0 + } + ], + "final_former_Y": [ + [ + [ + [], + "z0", + 1 + ] + ], + [ + [ + [], + "z1", + 1 + ] + ], + [], + [] + ], + "initial_record_contract": [ + { + "coordinates_per_stage_per_owner": 8, + "pair": 0, + "source": "initial ordinary X", + "stages": [ + 0, + 2 + ] + }, + { + "coordinates_per_stage_per_owner": 8, + "pair": 1, + "source": "initial ordinary X", + "stages": [ + 3, + 4 + ] + }, + { + "coordinates_per_stage_per_owner": 8, + "pair": 2, + "source": "initial ordinary X", + "stages": [ + 5, + 6 + ] + }, + { + "coordinates_per_stage_per_owner": 8, + "pair": 3, + "source": "initial ordinary X", + "stages": [ + 7, + 8 + ] + } + ], + "original_X0_A": [ + [ + [], + "d", + 1 + ] + ], + "scope": "ordinary-only bridges; no selected interventions before complete F2; homogeneous selected-only operations after F2 preserve this family", + "zero_forward_stages": [ + 0, + 2, + 4, + 6, + 8 + ], + "zero_initial_record_coordinates_per_owner": 64 + } + }, + "proof_scope": "Actual regular owner action; ordinary-only bridge/terminal replica; fixed local maps through F2; all 64 named initial record coordinates granted free. No first-six-swap, supplier, native-cost or kappa claim.", + "schema_version": 1, + "status": "PASS_QQ16_FINAL_RECORD_OBSTRUCTION" +} diff --git a/research/qq16-final-record-obstruction/SOURCES.json b/research/qq16-final-record-obstruction/SOURCES.json new file mode 100644 index 0000000000..0dd15339ac --- /dev/null +++ b/research/qq16-final-record-obstruction/SOURCES.json @@ -0,0 +1,86 @@ +{ + "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/JOINT-QUERY-TRANSFER.md", + "usage": "input", + "git_blob": "a6805c58f23132f9420efebf90f5b7e863c2e179", + "sha256": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75" + }, + { + "path": "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json", + "usage": "input", + "git_blob": "5082d791d0b993492cbc5bf61ac3b69e82c96f3f", + "sha256": "e35e5868a1322e406191079c0675975b139692ba50b1e2e5fb8a40b6480519f4" + }, + { + "path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754" + } + ], + "predecessors": [ + { + "pr": 1969, + "head": "a6e6ad3936f67b8f63b5b68c5e75d540610a65e7", + "role": "Ali Romman: retained QQ16 maps and native route sources; consumed from current main." + }, + { + "pr": 2104, + "head": "4bdc574da394a39f955e8cf4637075649c43a632", + "role": "Ross Richardson: credited two-moment rank method; no executable imported." + }, + { + "pr": 2093, + "head": "8b21a900eb520e4f11ea177b310f66316f8e8983", + "role": "Adam Gall: adjacent actual-route hidden-query counterexample; no executable imported." + }, + { + "pr": 2174, + "head": "f79470a7931f3943360c10d15b428e0e4e479c22", + "role": "@commdata2338: recorded-cut positive decoder and explicit final-retention handoff; no executable imported." + }, + { + "pr": 2181, + "head": "e18ca76987f5945c6a4b5b6bebbe73cdab3c4561", + "role": "Nick Petalas: higher-moment predecessor; not needed for the new bound." + }, + { + "pr": 2189, + "head": "968ccd289de1130c437cb4936608c4ee419a27de", + "role": "@commdata2338: fourth-moment predecessor; not needed for the new bound." + }, + { + "repository": "philippeVV/integer-mult-bounds", + "head": "680d0997621a2cecfef2186ab143377658687825", + "path": "research/joint-query-first-pair-catalogue/four-bank", + "role": "Earlier final-only finite-model failure, exact all-bank record choice and actual-route moment census. The new delta is the actual regular-cover obstruction, not discovery of finite-model failure." + } + ] +} diff --git a/research/qq16-final-record-obstruction/TASK.json b/research/qq16-final-record-obstruction/TASK.json new file mode 100644 index 0000000000..ec6c2ddaa2 --- /dev/null +++ b/research/qq16-final-record-obstruction/TASK.json @@ -0,0 +1,156 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "starting_points": [ + "certificates/selected-result.json", + "docs/audit.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected review scope and choose one exact all-size or precision implication.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "Choose one tape, precision, hosting or restoration lemma." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision" + ] + }, + "scope_status": "refined", + "actual_scope": "Actual routed QQ16 final-only information loss for the ordinary-only bridge/terminal replica, with pair-local initial records on all four banks; no selected intervention before F2.", + "scope_change_reason": "Follow PR2174's explicit cut-retention handoff and upgrade philippeVV/680d0997 finite random-route evidence to a source-bound ordered dimension theorem. This is a restoration audit of a proposed controller, not selected-supplier admission.", + "bottleneck_link": "The local QQ16 words cannot form this proposed final-only controller if the original selected inputs remain unrecoverable even with all proposed initial records granted free.", + "budget_minutes": 120, + "stop_rule": "Finish one actual-route obstruction or exact recovery statement. Stop construction work if a dimension obstruction holds; reserve final 30 minutes for verification and handoff.", + "outcome": "negative-result", + "evidence": "PROOF.md gives dim J(ker O)>=ceil(8|G|/7); RESULT.json binds exact routes, the complete 19-event ordered trajectory, two independent source reconstructions and separately factored rational algebra fixtures. verify.py recomputes and compares the complete receipt.", + "author": "@alephnan, with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in research, proof, code, independent agent checks and writing; no independent human review.", + "open_questions": [ + { + "question": "Can an explicitly typed selected intervention before F2 preserve the missing cut information?", + "why_it_matters": "The theorem fixes the dynamics through F2, so a changed early controller could escape this exact obstruction.", + "first_step": "Write its ordered map and test the complete observation kernel, then price native frames, all observations and restoration.", + "blocked_by": "No such intervention or favorable complete bill is constructed here." + }, + { + "question": "Can the post-B1 A record be retained legally to the final interface?", + "why_it_matters": "That record equals d and detects this family, explaining the precise extra premise in PR2174.", + "first_step": "Specify its native source and output frames, storage lifetime and inverse cleanup; combine with PR2174 only after all required observations are accessible.", + "blocked_by": "Detecting this family alone is not full recovery; physical access and the complete cost remain open." + }, + { + "question": "Can one emit a compact actual-cover member of the proven invisible subspace?", + "why_it_matters": "A short exact vector would make a direct literal routed regression possible without a dimension-existence argument.", + "first_step": "Solve B0z0=B2z0=B3z1=B4z1=0 and B2z1=-ell2A P1A B1z0 with nonzero B1z0 in a source-bound function basis.", + "blocked_by": "No bound on support size or coefficient bitlength is proved." + } + ], + "selection_seed": "b477785a8515f4c055aa3f8bcf59935f", + "session_start_utc": "2026-10-15T05:34:20Z", + "verification_reserve_start_utc": "2026-10-15T07:04:20Z", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2074#discussioncomment-18941784", + "initial_overlap": { + "open_prs": { + "fetched_at": "2026-10-15T05:37:37Z", + "records": 546, + "complete_pagination": true + }, + "discussions": { + "fetched_at": "2026-10-15T05:39:57Z", + "records": 1049, + "complete_pagination": true + }, + "narrow_queries": [ + "final-only", + "final records", + "four-bank" + ], + "coverage_limit": "No code diff search; exact named predecessor files were read separately. Absence of matches does not establish novelty." + }, + "baseline": { + "command": "python -B scripts/research_baseline.py", + "status": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY using Windows extended-length script path", + "initial_limitation": "Ordinary Windows path failed to see seven long pinned paths. The extended-length invocation passed unchanged; no source pin was weakened.", + "selected_kappa": "836330098538459/500000000000000000", + "full_replay": "make frontier1094-verify", + "full_replay_run": false + }, + "environment": { + "python": "3.12.2", + "platform": "Windows-11-10.0.26300-SP0", + "dependencies": "Python standard library only" + }, + "verification": { + "registered_replay_command": "python -I -B scripts/research_package.py --package research/qq16-final-record-obstruction", + "status": "PASS_REGISTERED_RESEARCH_PACKAGE", + "checks": [ + "normal and optimized isolated Python replay", + "15 primary semantic rejection controls", + "4 independent source/moment controls", + "5 independent rational noncommuting algebra fixtures and 2 sign controls", + "Git-free relocated read-only replay", + "changed canonical receipt rejected", + "changed source packet rejected" + ], + "independent_agent_review": "Two final separate agent reviews found no mathematical or source-binding blockers; this is not human or formal proof review.", + "reviewed_sha256": { + "PROOF.md": "109490f1d9c4288445e11e65e77616d84555ce9f212df97c81e6efde0c2ebf43", + "README.md": "314c36f863d134841eed8474752efc207c880cf8e59cb6fd4a73518bb360f725", + "verify_core.py": "4f2da2c3f3ba384ac9d9226b610915e659d6595ee8e97afcc9c8901cbdf86b51", + "verify.py": "c033c5558af9e075317c77c2a3709e0273036b4d9ef5852dea0b71aa771fcd2a", + "independent_moments.py": "a95a167e13637fbee64335bd5827cf71b3fde51fd34e0951cb4b24cd120f77d7", + "independent_algebra.py": "bcbf79311d046d144ee714dfbc35bc0b97877ccf4f19188e5a3a3565aa9d08ea" + }, + "reviewed_hash_policy": "SHA-256 of LF-normalized reviewed files; normalization changes only line endings." + }, + "submission_checkpoint": { + "upstream_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "fork_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "checked_at_utc": "2026-10-15T06:03:00Z", + "selected_record_unchanged": true, + "open_prs": { + "fetched_at": "2026-10-15T05:59:13.531714Z", + "records": 556, + "complete_pagination": true + }, + "discussions": { + "fetched_at": "2026-10-15T06:01:31.888372Z", + "records": 1065, + "complete_pagination": true + }, + "narrow_query": [ + "final-only", + "final records", + "four-bank", + "8|G|/7" + ], + "narrow_hits": 14, + "assessment": "Includes this package and its claim, plus the credited recorded-cut, transcript-bound and four-bank predecessors. No duplicate actual-cover intersection theorem found among these exact nearest sources. PR2174 head remains f79470a7931f3943360c10d15b428e0e4e479c22. No exhaustive novelty claim.", + "limits": "Open PR bodies, discussions/replies and local READMEs/TASK metadata searched, not code diffs or all closed submissions. Narrow query used the just-refreshed cached snapshot." + } +} diff --git a/research/qq16-final-record-obstruction/VERIFY.json b/research/qq16-final-record-obstruction/VERIFY.json new file mode 100644 index 0000000000..1909aa8ea0 --- /dev/null +++ b/research/qq16-final-record-obstruction/VERIFY.json @@ -0,0 +1,46 @@ +{ + "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/JOINT-QUERY-TRANSFER.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json", + "research/community-frontier1042-audit/selected-replay.tar.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Both independent exact source reconstructions, full ordered trajectory, semantic controls and complete canonical receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete check with assertions disabled; all required checks are explicit." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_integrity.py" + ], + "timeout_seconds": 180, + "checks": "Git-free relocated replay, read-only replay integrity, and altered receipt/source rejection." + } + ] +} diff --git a/research/qq16-final-record-obstruction/independent_algebra.py b/research/qq16-final-record-obstruction/independent_algebra.py new file mode 100644 index 0000000000..ef3ab19476 --- /dev/null +++ b/research/qq16-final-record-obstruction/independent_algebra.py @@ -0,0 +1,157 @@ +"""Independent exact factored-map evidence for the QQ16 final-record theorem. + +Five rational models exercise noncommuting selected charts. These are algebra +fixtures, not actual-cover rank evidence. No research module is imported. +Apache-2.0; prepared with substantial OpenAI Codex assistance. +""" +from copy import deepcopy +from fractions import Fraction as Q +from hashlib import sha256 +from io import BytesIO +from pathlib import Path +import gzip +import json +import tarfile + +ARCHIVE = "research/community-frontier1042-audit/selected-replay.tar.gz" +ARCHIVE_SHA = "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754" +MEMBER = "t16/global/base/split-centres/GLOBAL-TEMPLATE.json.gz" +MEMBER_SHA = "a179dad87651aba340a5a8ddbcd86a8e757cad87b8a1f8bad48106fbecd38518" + + +def need(ok, reason): + if not ok: + raise ValueError(reason) + + +def zero(n): return [Q(0)] * n + +def add(a, b): return [x + y for x, y in zip(a, b)] + +def scale(c, a): return [c * x for x in a] + +def sub(a, b): return add(a, scale(-1, b)) + +def mv(matrix, vector): return [sum(a*b for a, b in zip(row, vector)) for row in matrix] + +def mm(a, b): return [[sum(x*y for x, y in zip(row, column)) for column in zip(*b)] for row in a] + + +def inverse(a): + x, y = a[0]; z, w = a[1]; determinant = x*w-y*z + need(determinant != 0, "invertible selected chart") + return [[w/determinant, -y/determinant], [-z/determinant, x/determinant]] + + +def frame(k): + return [[Q(1+k*(k+1)), Q(k)], [Q(k+1), Q(1)]] + + +def schedule(root): + data = (Path(root)/ARCHIVE).read_bytes() + need(sha256(data).hexdigest() == ARCHIVE_SHA, "independent archive pin") + with tarfile.open(fileobj=BytesIO(data), mode="r:gz") as archive: + members = [item for item in archive.getmembers() if item.name == MEMBER] + need(len(members) == 1 and members[0].isfile(), "one independent recipe member") + raw = archive.extractfile(members[0]).read() + need(sha256(raw).hexdigest() == MEMBER_SHA, "independent recipe pin") + recipe = json.loads(gzip.decompress(raw))["recipe"] + local = [event for event in recipe if event["kind"] == "local"] + need(len(recipe) == 19 and [event["stage"] for event in local] == list(range(9)), "complete schedule") + need([event["pair"] for event in local] == [0,0,0,1,1,2,2,3,3], "actual local pairs") + need(all(event["reverse"] == bool(event["stage"] % 2) for event in local), "actual orientations") + return recipe + + +def check_case(recipe, seed, mutation=None): + la = [frame(seed+s+1) for s in range(9)] + lt = [frame(seed+2*s+2) for s in range(9)] + pa, pt = [inverse(a) for a in la], [inverse(a) for a in lt] + need(mm(la[0], la[1]) != mm(la[1], la[0]), "noncommuting selected charts") + unit = [[Q(1), Q(0)], [Q(0), Q(1)]] + need(all(mm(a, b) == mm(b, a) == unit for a, b in zip(la+lt, pa+pt)), "two-sided selected units") + z0, z1, v = [Q(1),Q(0),Q(0),Q(0)], [Q(0),Q(1),Q(0),Q(0)], [Q(1),Q(2)] + d = scale(-1, mv(pa[1], v)); linked = mv(la[2], d) + readers, centres = [], [] + for s in range(9): + columns = [[Q(s+1),Q(s+2)], [Q(s+3),Q(-s-1)], [Q(1),Q(0)], [Q(0),Q(1)]] + if s == 0: columns[0] = zero(2) + if s == 1: columns[0] = v + if s == 2: + columns[0] = zero(2) + columns[1] = scale(-1 if mutation == "wrong_link_sign" else 1, linked) + if s in (3,4): columns[1] = zero(2) + readers.append([list(row) for row in zip(*columns)]) + centres.append([[Q(0),Q(0)], [Q(0),Q(0)], [Q(12),Q(0)], [Q(0),Q(12)]]) + need(all(mm(b, k) == [[Q(12),Q(0)], [Q(0),Q(12)]] for b, k in zip(readers, centres)), "centre response 12I") + need(mv(readers[1], z0) == scale(-1, mv(la[1], d)), "first selected cancellation") + if mutation != "wrong_link_sign": + need(mv(readers[2], z1) == mv(la[2], d), "ordered cross-bank compatibility") + def query(s, fields): + return add(add(mv(readers[s], fields[0]), mv(la[s], fields[1])), mv(lt[s], fields[2])) + banks = [[[zero(4),zero(2),zero(2)] for _ in range(2)] for _ in range(4)] + xt = scale(-1, mv(pt[0], mv(la[0], d))) + banks[0] = [[z0,d,xt], [zero(4),scale(-1,d),scale(-1,xt)]] + banks[1][0][0] = z1 + records = [mv(readers[s], banks[k][0][0]) for k in range(4) + for s in ([0,2] if k == 0 else [2*k+1,2*k+2])] + need(len(records) == 8 and not any(any(record) for record in records), "all eight initial records") + histories = [] + events = deepcopy(recipe) + if mutation == "wrong_bridge_sign": + next(event for event in events if event["kind"] == "bridge")["coefficient"] *= -1 + for event in events: + if event["kind"] == "bridge": + i,j,c = event["src"],event["dst"],event["coefficient"] + banks[j][0][0] = add(banks[j][0][0], scale(c, banks[i][0][0])) + banks[i][1][0] = sub(banks[i][1][0], scale(c, banks[j][1][0])) + elif event["kind"] == "terminal": + for pair in banks: + pair[0],pair[1] = pair[1], [scale(-1,field) for field in pair[0]] + else: + s,k = event["stage"],event["pair"]; x,y = banks[k] + if not event["reverse"]: + # Three source assignments, rather than the final-row formula. + z,a,c = x[0],mv(la[s],x[1]),mv(lt[s],x[2]) + c = add(c,add(mv(readers[s],z),a)); histories.append(c) + z = sub(z,mv(centres[s],c)) + a = sub(scale(-1,a),add(mv(readers[s],z),scale(11,c))) + nx = [z,mv(pa[s],a),mv(pt[s],c)] + ny = [add(y[0],z),sub(add(x[1],y[1]),nx[1]),sub(add(x[2],y[2]),nx[2])] + else: + # Separate E, full-query exchange, then H=I+(K_U-12P)R. + t = s+1 + u = [y[0],add(y[1],mv(pa[t],add(mv(readers[t],y[0]),mv(lt[t],y[2])))),y[2]] + a,b = mv(lt[s],x[2]),query(s,u) + intermediate = [u[0],u[1],add(u[2],mv(pt[s],sub(a,b)))] + current = query(s,intermediate) + ny = [add(intermediate[0],mv(centres[s],current)),intermediate[1],sub(intermediate[2],mv(pt[s],scale(12,current)))] + nx = [sub(x[0],y[0]),sub(add(x[1],y[1]),ny[1]),sub(add(x[2],y[2]),ny[2])] + banks[k] = [nx,ny] + need(len(histories) == 5 and not any(any(f) for f in histories), "forward histories vanish") + need(all(not any(field) for pair in banks for field in pair[0][1:]+pair[1]), "final selected and completed-X vanish") + need([pair[0][0] for pair in banks] == [z0,z1,zero(4),zero(4)], "former-Y residuals") + need(any(d), "nonzero original selected A") + return {"seed":seed, "initial_A":list(map(str,d)), "initial_records":len(records), "zero_histories":len(histories)} + + +def verify(root): + recipe = schedule(root) + cases = [check_case(recipe, seed) for seed in range(5)] + rejected = [] + for mutation in ("wrong_link_sign", "wrong_bridge_sign"): + try: + check_case(recipe, 0, mutation) + except ValueError as error: + need(str(error) == "forward histories vanish", "independent control failed for unrelated reason") + rejected.append(mutation) + else: + raise ValueError("independent mutation accepted: " + mutation) + return {"status":"PASS_INDEPENDENT_FACTORIZED_QQ16_TRAJECTORY", "model_count":len(cases), + "query_dimension":2, "ordinary_dimension":4, "recipe_events":len(recipe), + "cases":cases, "rejected_controls":rejected, + "scope":"exact noncommuting algebra fixtures; actual-cover existence is proved separately"} + + +if __name__ == "__main__": + print(json.dumps(verify(Path(__file__).resolve().parents[2]), indent=2)) diff --git a/research/qq16-final-record-obstruction/independent_moments.py b/research/qq16-final-record-obstruction/independent_moments.py new file mode 100644 index 0000000000..5f490c8191 --- /dev/null +++ b/research/qq16-final-record-obstruction/independent_moments.py @@ -0,0 +1,249 @@ +#!/usr/bin/env python3 +"""Independent QQ16 two-moment route oracle; no research module imports. + +R is reconstructed by backward scalar covectors. Owner routes are reconstructed +as coordinate swaps in a complete orthonormal basis (rather than transvections). +The actual six pairs are checked as full 73-by-73 binary maps. This corroborates +credited moment results; it does not prove the new final-only observation map. + +Credit: Ali Romman/#1969 supplies QQ16; Ross Richardson/#2104 supplies the +two-moment rank method; Nick Petalas/#2181 and commdata2338/#2189 extend it. +Philippe Van Velzen commit680d0997621a2cecfef2186ab143377658687825 checks +actual-route moments for all stage triples. This code is an independent +source-binding check, written with substantial OpenAI Codex assistance. +Apache-2.0. +""" +from fractions import Fraction +from pathlib import Path +import argparse +import gzip +import hashlib +import io +import json +import tarfile + +ARCHIVE = 'research/community-frontier1042-audit/selected-replay.tar.gz' +ARCHIVE_SHA256 = '22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754' +MEMBERS = { + 'word': ('slots/local/CANONICAL-WORD.json.gz','16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219'), + 'program': ('slots/local/LOCAL-PROGRAMS.json.gz','241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a'), + 'phases': ('t16/global/base/work/complex-nine-native/DATA-PHASES.json','c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa'), +} +A=(0,7,20,27,36,46,57,111) +T=(21,37,47,76,81,87,92,110) +U=tuple(p for p in range(112) if p not in A+T) +TRIPLES=((0,1,2),(2,3,4)) +IDENTITY=tuple(1<>i&1: + result^=column + return result + + +def matrix_product(left,right): + return tuple(xor_images(left,column) for column in right) + + +def actual_routes(word,phases): + require(phases['m']==73 and len(phases['recipes'])==112,'phase dimensions') + routes={stage:[] for stage in range(5)} + for port,record in enumerate(phases['recipes']): + require(record['port']==port and record['q']==word['ports'][port],'phase port binding') + basis=tuple([record['q']]+record['idle_children'][0]['orthogonal_axes'][:8])+IDENTITY[9:] + require(len(basis)==73 and all(((basis[i]&basis[j]).bit_count()%2)==int(i==j) for i in range(73) for j in range(73)),'full orthonormal route basis') + for stage in range(5): + permutation=list(range(73)) + if stage: + for i in range(8): + first,second=1+i,9+8*(stage-1)+i + permutation[first],permutation[second]=permutation[second],permutation[first] + columns=[] + for unit in IDENTITY: + value=0 + for i,axis in enumerate(basis): + if (unit&axis).bit_count()%2: + value^=basis[permutation[i]] + columns.append(value) + actual=tuple(columns) + require(matrix_product(actual,actual)==IDENTITY,'owner involution') + require(xor_images(actual,record['q'])==record['q'],'fixed port normal') + if stage==0: + require(actual==IDENTITY,'stage-zero identity') + else: + for i in range(8): + require(xor_images(actual,basis[1+i])==IDENTITY[9+8*(stage-1)+i],'actual q-perp to stage-axis swap') + routes[stage].append(actual) + return routes + + +def cross_square(columns,relative): + # M_g is the complete 8x8 coefficient of owner route g in B_s B_t*. + coeff={} + for port,g in zip(U,relative): + block=coeff.setdefault(g,[[0]*8 for _ in range(8)]) + for i in range(8): + for j in range(8): + block[i][j]+=columns[port][i]*columns[port][j] + # Identity coefficient of C C*: sum_g M_g M_g^T, valid even on collisions. + square=[[sum(sum(block[i][k]*block[j][k] for k in range(8)) for block in coeff.values()) for j in range(8)] for i in range(8)] + return coeff,square + + +def check_cross(columns,relative): + coeff,square=cross_square(columns,relative) + require(len(coeff)==96,'distinct actual relative routes') + require(square==diagonal(192),'cross identity matrix') + return coeff,square + + +def verify(root): + inputs=load(root) + columns=backward_columns(inputs['word'],inputs['program']['forward']) + check_geometry(columns) + routes=actual_routes(inputs['word'],inputs['phases']) + pairs=sorted({tuple(sorted((s,t))) for triple in TRIPLES for s in triple for t in triple if s!=t}) + checks=[] + for s,t in pairs: + relative=[matrix_product(routes[s][p],routes[t][p]) for p in U] + coeff,square=check_cross(columns,relative) + reverse=[matrix_product(routes[t][p],routes[s][p]) for p in U] + _,reverse_square=cross_square(columns,reverse) + require(reverse_square==square,'anti-homomorphism convention') + checks.append({'stages':[s,t],'routes':len(coeff),'relative_route_sha256':digest(relative),'cross_identity_matrix':square,'cross_trace_per_owner':sum(square[i][i] for i in range(8))}) + m1=Fraction(3*8) + m2=Fraction(3*8)+6*Fraction(1536,48**2) + rank=m1*m1/m2 + defect=rank-16 + require((m1,m2,rank,defect)==(24,28,Fraction(144,7),Fraction(32,7)),'trace/rank arithmetic') + controls=[] + bad=[list(c) for c in columns] + bad[U[0]][0]+=1 + try: + check_geometry(bad) + except ValueError: + controls.append('changed R coefficient rejected') + else: + raise ValueError('R mutation passed') + try: + check_geometry(columns,(1,)+A[1:],T) + except ValueError: + controls.append('wrong selected port rejected') + else: + raise ValueError('selected-port mutation passed') + relative=[matrix_product(routes[0][p],routes[1][p]) for p in U] + relative[1]=relative[0] + try: + check_cross(columns,relative) + except ValueError: + controls.append('colliding route rejected') + else: + raise ValueError('route collision passed') + collapsed=[IDENTITY for p in U] + _,collapsed_square=cross_square(columns,collapsed) + require(collapsed_square==diagonal(2304), + 'nonregular collapsed-owner action is a distinct trace model') + try: + check_cross(columns,collapsed) + except ValueError: + controls.append('collapsed-owner action rejected; regular-action trace domain required') + else: + raise ValueError('collapsed owner action passed') + return {'status':'PASS_INDEPENDENT_QQ16_FINAL_ONLY_MOMENTS','archive_sha256':ARCHIVE_SHA256,'archive_members':{name:{'path':path,'sha256':pin} for name,(path,pin) in MEMBERS.items()},'trace_domain':'finite regular owner representation on payload-constant fields; not an arbitrary quotient or nonfree owner action','R_columns_sha256':digest(columns),'centre_sha256':digest([[str(columns[p][i]) for p in range(112)] for i in range(8)]),'ordinary_gram':48,'triples':[list(t) for t in TRIPLES],'pairs':checks,'normalized_moment1_per_owner':str(m1),'normalized_moment2_per_owner':str(m2),'stack_rank_lower_per_owner':str(rank),'conditional_image_lower_per_owner':str(defect),'controls':controls,'scope':'Independent source-bound corroboration of credited moments, not a new moment theorem or verification of final-only controller trajectory.'} + + +if __name__=='__main__': + parser=argparse.ArgumentParser() + parser.add_argument('--repo',type=Path,default=Path(__file__).resolve().parents[2]) + args=parser.parse_args() + print(json.dumps(verify(args.repo),indent=2,sort_keys=True)) diff --git a/research/qq16-final-record-obstruction/test_integrity.py b/research/qq16-final-record-obstruction/test_integrity.py new file mode 100644 index 0000000000..6ad30596b1 --- /dev/null +++ b/research/qq16-final-record-obstruction/test_integrity.py @@ -0,0 +1,77 @@ +#!/usr/bin/env python3 +"""Relocated read-only replay and tampering controls; standard library only. + +Apache-2.0. Substantial OpenAI Codex assistance. +""" +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +class ExportIntegrity(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.temporary = tempfile.TemporaryDirectory(prefix="qq16-final-record-") + cls.addClassCleanup(cls.temporary.cleanup) + cls.root = Path(cls.temporary.name) + cls.package = cls.root / "research" / PACKAGE.name + shutil.copytree(PACKAGE, cls.package, ignore=shutil.ignore_patterns("__pycache__")) + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + for row in sources["files"]: + if row["usage"] == "input": + source = ROOT / row["path"] + destination = cls.root / row["path"] + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(source, destination) + + def run_export(self): + return subprocess.run([sys.executable, "-I", "-O", "-B", str(self.package / "verify.py")], + cwd=self.root, text=True, capture_output=True, timeout=120) + + def snapshot(self): + return {str(p.relative_to(self.root)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in self.root.rglob("*") if p.is_file()} + + def test_01_git_free_read_only_replay(self): + self.assertFalse((self.root / ".git").exists()) + before = self.snapshot() + result = self.run_export() + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn("PASS_QQ16_FINAL_RECORD_OBSTRUCTION", result.stdout) + self.assertEqual(before, self.snapshot()) + + def test_02_complete_receipt_rejects_changed_bound(self): + path = self.package / "RESULT.json" + original = path.read_bytes() + try: + altered = json.loads(original) + altered["primary"]["sources"]["selected_defect_lower_per_owner"] = "9/7" + path.write_text(json.dumps(altered), encoding="utf-8") + result = self.run_export() + self.assertNotEqual(result.returncode, 0) + self.assertIn("complete canonical RESULT.json differs", result.stderr) + finally: + path.write_bytes(original) + + def test_03_source_pin_rejects_changed_packet(self): + path = self.root / "research/joint-query/certificate.json.gz" + original = path.read_bytes() + try: + path.write_bytes(original + b"changed") + result = self.run_export() + self.assertNotEqual(result.returncode, 0) + self.assertIn("input hash: research/joint-query/certificate.json.gz", result.stderr) + finally: + path.write_bytes(original) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/qq16-final-record-obstruction/verify.py b/research/qq16-final-record-obstruction/verify.py new file mode 100644 index 0000000000..73f2f14617 --- /dev/null +++ b/research/qq16-final-record-obstruction/verify.py @@ -0,0 +1,84 @@ +#!/usr/bin/env python3 +"""Read-only replay of the QQ16 final-record obstruction and independent oracle. + +Apache-2.0. Substantial OpenAI Codex assistance; no human review claimed. +""" +import argparse +import hashlib +import importlib.util +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def read_module(name): + spec = importlib.util.spec_from_file_location("qq16_final_" + name, PACKAGE / (name + ".py")) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def check_inputs(root): + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + checked = [] + for row in sources["files"]: + if row["usage"] != "input": + continue + path = (root / row["path"]).resolve() + need(path.is_relative_to(root.resolve()) and path.is_file(), "input path: " + row["path"]) + need(hashlib.sha256(path.read_bytes()).hexdigest() == row["sha256"], "input hash: " + row["path"]) + checked.append(row["path"]) + return checked + + +def compute(root=ROOT): + inputs = check_inputs(root) + primary = read_module("verify_core").report(root) + independent = read_module("independent_moments").verify(root) + algebra = read_module("independent_algebra").verify(root) + left, right = primary["sources"], independent + need(left["R_columns_sha256"] == right["R_columns_sha256"], "independent centre matrix") + comparisons = {tuple(row["stages"]): row for row in right["pairs"]} + for row in left["pair_checks"]: + other = comparisons[tuple(row["stages"])] + need(row["relative_routes_sha256"] == other["relative_route_sha256"], "independent relative owner routes") + need(row["distinct_relative_routes"] == other["routes"] == 96, "independent route census") + need(int(row["cross_gram_identity_trace"]) == other["cross_trace_per_owner"] == 1536, "independent full trace") + need(left["triple_trace_per_owner"] == right["normalized_moment1_per_owner"] == "24", "first moment") + need(left["triple_square_trace_per_owner"] == right["normalized_moment2_per_owner"] == "28", "second moment") + need(left["stacked_rank_lower_per_owner"] == right["stack_rank_lower_per_owner"] == "144/7", "stacked rank bound") + need(left["constrained_image_lower_per_owner"] == right["conditional_image_lower_per_owner"] == "32/7", "constrained image bound") + need(left["selected_defect_lower_per_owner"] == "8/7", "selected defect bound") + return {"schema_version": 1, "status": "PASS_QQ16_FINAL_RECORD_OBSTRUCTION", + "input_paths_checked": inputs, "primary": primary, "independent_moments": independent, + "independent_algebra": algebra, + "proof_scope": "Actual regular owner action; ordinary-only bridge/terminal replica; fixed local maps through F2; all 64 named initial record coordinates granted free. No first-six-swap, supplier, native-cost or kappa claim."} + + +def verify_receipt(result): + expected = json.loads((PACKAGE / "RESULT.json").read_text(encoding="utf-8")) + need(expected == result, "complete canonical RESULT.json differs") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="explicitly regenerate the complete deterministic result") + args = parser.parse_args() + result = compute() + if args.write: + (PACKAGE / "RESULT.json").write_text(json.dumps(result, indent=2, sort_keys=True) + "\n", encoding="utf-8") + else: + verify_receipt(result) + print("PASS_QQ16_FINAL_RECORD_OBSTRUCTION actual_routes=1008 pairs=6 events=19 initial_records=64 defect>=ceil(8|G|/7) controls=" + + str(len(result["primary"]["rejected_controls"])) + " independent_oracles=PASS no_new_kappa") + + +if __name__ == "__main__": + main() diff --git a/research/qq16-final-record-obstruction/verify_core.py b/research/qq16-final-record-obstruction/verify_core.py new file mode 100644 index 0000000000..bf0837aadb --- /dev/null +++ b/research/qq16-final-record-obstruction/verify_core.py @@ -0,0 +1,332 @@ +"""Independent source-bound QQ16 final-record obstruction checks. + +New code: Apache-2.0; substantial OpenAI Codex assistance. The retained +QQ16 maps are credited to Ali Romman; route and centre sources retain +all upstream attribution. No predecessor executable is imported. +""" +from copy import deepcopy +from fractions import Fraction as Q +from hashlib import sha256 +from io import BytesIO +from itertools import combinations +from pathlib import Path +import gzip +import json +import tarfile + +A = (0, 7, 20, 27, 36, 46, 57, 111) +T = (21, 37, 47, 76, 81, 87, 92, 110) +U = tuple(p for p in range(112) if p not in A + T) +ARCHIVE = "research/community-frontier1042-audit/selected-replay.tar.gz" +PACKET = "research/joint-query/certificate.json.gz" +INPUT_PINS = { + ARCHIVE: "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + PACKET: "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7", +} +MEMBER_PINS = { + "slots/local/CANONICAL-WORD.json.gz": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "slots/local/LOCAL-PROGRAMS.json.gz": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a", + "t16/global/base/work/complex-nine-native/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "t16/global/base/split-centres/GLOBAL-TEMPLATE.json.gz": "a179dad87651aba340a5a8ddbcd86a8e757cad87b8a1f8bad48106fbecd38518", +} +PAIRS = ((0, 1), (0, 2), (1, 2), (2, 3), (2, 4), (3, 4)) +AXES = tuple(1 << j for j in range(73)) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")) + + +def load(root): + raw = {} + for name, pin in INPUT_PINS.items(): + data = (Path(root) / name).read_bytes() + need(sha256(data).hexdigest() == pin, "source hash: " + name) + raw[name] = data + members = {} + with tarfile.open(fileobj=BytesIO(raw[ARCHIVE]), mode="r:gz") as archive: + for name, pin in MEMBER_PINS.items(): + found = [m for m in archive.getmembers() if m.name == name] + need(len(found) == 1 and found[0].isfile(), "one regular archive member") + data = archive.extractfile(found[0]).read() + need(sha256(data).hexdigest() == pin, "archive member hash: " + name) + members[name.rsplit("/", 1)[-1]] = json.loads(gzip.decompress(data) if name.endswith(".gz") else data) + return members, json.loads(gzip.decompress(raw[PACKET])) + + +def plus(*terms): + out = {} + for coefficient, row in terms: + for key, value in row.items(): + out[key] = out.get(key, 0) + coefficient * value + return {key: value for key, value in out.items() if value} + + +def reconstruct_R(word, program): + need((word["v"], word["R"], word["h"]) == (112, 480, 9), "source geometry") + rows = [{p: Q(1)} if p < 112 else {} for p in range(712)] + for event in program: + if event == ["phase", "centers"]: + return [[rows[c].get(p, Q(0)) for p in range(112)] for c in word["centers"]] + if event[0] != "scalar": + continue + op = event[1] + target = op[1][1] + (704 if op[1][0] == "C" else 0) + if op[0] == "clear": + rows[target] = {} + elif op[0] == "scale": + rows[target] = plus((Q(op[2], op[3]), rows[target])) + else: + need(op[0] in ("add", "copy"), "source scalar alphabet") + source = op[2][1] + (704 if op[2][0] == "C" else 0) + rows[target] = rows[source].copy() if op[0] == "copy" else plus((1, rows[target]), (Q(op[3], op[4]), rows[source])) + raise ValueError("missing source centre cut") + + +def act(columns, vector): + result = 0 + while vector: + bit = vector & -vector + result ^= columns[bit.bit_length() - 1] + vector ^= bit + return result + + +def route(basis, stage): + if stage == 0: + return AXES + result = [] + for vector in AXES: + for i, local in enumerate(basis): + swap = local ^ AXES[9 + 8 * (stage - 1) + i] + if (vector & swap).bit_count() & 1: + vector ^= swap + result.append(vector) + return tuple(result) + + +def gram(R, ports): + return [[sum(R[i][p] * R[j][p] for p in ports) for j in range(8)] for i in range(8)] + + +def source_checks(members, packet, mutation=None): + if mutation == "native_route_placement": + packet = deepcopy(packet) + first = packet["programs"]["F_1"] + first[1][2], first[2][2] = first[2][2], first[1][2] + R = reconstruct_R(members["CANONICAL-WORD.json.gz"], members["LOCAL-PROGRAMS.json.gz"]["forward"]) + expected = [[Q(row.get(str(p), 0)) for p in range(112)] for row in packet["R_rows"]] + if mutation == "centre_coefficient": + R[0][U[0]] += 1 + need(R == expected, "operation-derived centre matrix") + need((packet["A_ports"], packet["T_ports"], packet["U_ports"]) == (list(A), list(T), list(U)), "port partition") + for ports, scalar in ((U, 48), (A, 4), (T, 4)): + need(gram(R, ports) == [[Q(scalar * (i == j)) for j in range(8)] for i in range(8)], "Gram identity") + need(all(sum(R[i][p] ** 2 for i in range(8)) == 4 for p in U), "ordinary column norm") + phases = members["DATA-PHASES.json"] + need(phases["m"] == 73 and len(phases["recipes"]) == 112, "actual phase dimension") + registry = {tuple(row["owner_right_matrix_columns"]) for row in packet["map_registry"].values()} + routes = {} + for p, record in enumerate(phases["recipes"]): + basis = tuple(record["idle_children"][0]["orthogonal_axes"][:8]) + need(record["port"] == p, "phase port binding") + local = (record["q"],) + basis + need(all(0 < v < (1 << 9) for v in local), "local chart domain") + need(all((local[i] & local[j]).bit_count() % 2 == (i == j) for i in range(9) for j in range(9)), "local chart orthonormality") + for s in range(9): + columns = route(basis, s) + need(all(act(columns, column) == AXES[i] for i, column in enumerate(columns)), "route involution") + need(columns in registry, "route absent from native packet") + native = packet["programs"]["F_" + str(s)] + need(native[0][:3] == ["retained_core", "forward", s], "native forward stage") + if s: + event = native[p + 1] + need(event[:2] == ["cover_map", ["L", p]], "native route field placement") + actual = tuple(packet["map_registry"][event[2]]["owner_right_matrix_columns"]) + need(actual == columns, "native route stage/port binding") + else: + need(native[1][0] == "cover_sweep", "stage zero has no route prefix") + routes[s, p] = columns + if mutation == "relative_route_collision": + routes[1, U[1]] = routes[1, U[0]] + checks = [] + for s, t in PAIRS: + labels = [tuple(act(routes[s, p], v) for v in routes[t, p]) for p in U] + need(len(set(labels)) == len(U), "relative route collision") + coefficient = [[sum(4 * R[i][p] * R[j][p] for p in U) for j in range(8)] for i in range(8)] + need(coefficient == [[Q(192 * (i == j)) for j in range(8)] for i in range(8)], "cross-Gram identity coefficient") + trace = sum(coefficient[i][i] for i in range(8)) + normalized = trace / (48 * 48) + need(normalized == Q(2, 3), "normalized pair trace") + checks.append({"stages": [s, t], "distinct_relative_routes": len(set(labels)), + "relative_routes_sha256": sha256(canonical(labels).encode()).hexdigest(), + "cross_gram_identity_diagonal": "192", "cross_gram_identity_trace": str(trace), + "projection_product_trace_per_owner": str(normalized)}) + triple_rank = Q(24 * 24, 28) + image_rank = triple_rank - 16 + defect = 2 * image_rank - 8 + need((triple_rank, image_rank, defect) == (Q(144, 7), Q(32, 7), Q(8, 7)), "rank arithmetic") + recipe = members["GLOBAL-TEMPLATE.json.gz"]["recipe"] + pairs = [e["pair"] for e in recipe if e["kind"] == "local"] + need(pairs == [0, 0, 0, 1, 1, 2, 2, 3, 3], "literal local pair binding") + need(len(recipe) == 19, "literal recipe length") + return {"R_columns_sha256": sha256(canonical([[int(R[k][p]) for k in range(8)] for p in range(112)]).encode()).hexdigest(), + "centre_sha256": sha256(canonical([[str(x) for x in row] for row in R]).encode()).hexdigest(), + "bound_native_routes": len(routes), "pair_checks": checks, + "triples": [[0, 1, 2], [2, 3, 4]], "triple_trace_per_owner": "24", + "triple_square_trace_per_owner": "28", "stacked_rank_lower_per_owner": str(triple_rank), + "constrained_image_lower_per_owner": str(image_rank), "selected_defect_lower_per_owner": str(defect)}, recipe + + +# Formal typed linear expressions. A monomial is (ordered operator word, +# variable). Only same-stage selected inverse identities and the four +# explicitly stated ordinary-query constraints are reduced. +INVERSE = {"LA": "PA", "PA": "LA", "LT": "PT", "PT": "LT"} + + +def variable(name): + return {((), name): 1} + + +def operated(name, expression, mutation=None): + out = {} + for (word, symbol), coefficient in expression.items(): + if word and name[:-1] in INVERSE and word[0] == INVERSE[name[:-1]] + name[-1]: + out = plus((1, out), (coefficient, {(word[1:], symbol): 1})) + elif not word and name.startswith("B"): + zero = {("B0", "z0"), ("B2", "z0"), ("B3", "z1"), ("B4", "z1")} + if mutation == "omit_B3_kernel": + zero.remove(("B3", "z1")) + if mutation == "omit_B4_kernel": + zero.remove(("B4", "z1")) + if (name, symbol) in zero: + continue + if (name, symbol) == ("B1", "z0"): + sign = 1 if mutation == "wrong_d_sign" else -1 + out = plus((1, out), (sign * coefficient, {(("LA1",), "d"): 1})) + elif (name, symbol) == ("B2", "z1"): + sign = -1 if mutation == "wrong_link_sign" else 1 + out = plus((1, out), (sign * coefficient, {(("LA2",), "d"): 1})) + else: + out = plus((1, out), (coefficient, {((name,) + word, symbol): 1})) + else: + out = plus((1, out), (coefficient, {((name,) + word, symbol): 1})) + return out + + +def expr_json(expression): + return [[list(word), symbol, coefficient] for (word, symbol), coefficient in sorted(expression.items())] + + +def trajectory(recipe, mutation=None): + recipe = deepcopy(recipe) + if mutation == "wrong_local_pair": + next(e for e in recipe if e.get("stage") == 2)["pair"] = 1 + elif mutation == "wrong_local_orientation": + next(e for e in recipe if e.get("stage") == 2)["reverse"] = True + elif mutation == "wrong_bridge_sign": + next(e for e in recipe if e["kind"] == "bridge")["coefficient"] *= -1 + def op(name, v): + return operated(name, v, mutation) + def query(s, fields): + return plus((1, op("B" + str(s), fields[0])), (1, op("LA" + str(s), fields[1])), (1, op("LT" + str(s), fields[2]))) + def forward(s, x, y): + f = query(s, x) + nx = [plus((1, x[0]), (-1, op("K" + str(s), f))), + op("PA" + str(s), op("LT" + str(s), x[2])), op("PT" + str(s), f)] + ny = [plus((1, y[0]), (1, nx[0]))] + [plus((1, x[j]), (1, y[j]), (-1, nx[j])) for j in (1, 2)] + return nx, ny, f + def backward(s, t, x, y): + u = deepcopy(y) + u[1] = plus((1, y[1]), (1, op("PA" + str(t), plus((1, op("B" + str(t), y[0])), (1, op("LT" + str(t), y[2])))))) + a, b = op("LT" + str(s), x[2]), query(s, u) + ny = [plus((1, y[0]), (1, op("K" + str(s), a))), u[1], + plus((1, u[2]), (-1, op("PT" + str(s), plus((1, b), (11, a)))))] + nx = [plus((1, x[0]), (-1, y[0])), plus((1, x[1]), (1, y[1]), (-1, u[1])), + op("PT" + str(s), plus((1, b), (12, a)))] + return nx, ny + d, z0, z1 = map(variable, ("d", "z0", "z1")) + sign = 1 if mutation == "wrong_initial_T_sign" else -1 + xt = plus((sign, op("PT0", op("LA0", d)))) + banks = [[[z0, d, xt], [{}, plus((-1, d)), plus((-1, xt))]], + [[z1, {}, {}], [{}, {}, {}]]] + [[[{},{},{}], [{},{},{}]] for _ in range(2)] + records = [op("B0", z0), op("B2", z0), op("B3", z1), op("B4", z1)] + need(not any(records), "all 64 initial query coordinates vanish") + histories, states = {}, [] + for index, event in enumerate(recipe): + if mutation == "omit_negative_bridge" and event == {"kind": "bridge", "src": 1, "dst": 0, "coefficient": -1}: + continue + if event["kind"] == "local": + s, k = event["stage"], event["pair"] + need(event["reverse"] == bool(s % 2), "literal local orientation") + x, y = banks[k] + if event["reverse"]: + banks[k] = list(backward(s, s + 1, x, y)) + else: + nx, ny, histories[s] = forward(s, x, y) + banks[k] = [nx, ny] + elif event["kind"] == "bridge": + i, j, c = event["src"], event["dst"], event["coefficient"] + banks[j][0][0] = plus((1, banks[j][0][0]), (c, banks[i][0][0])) + banks[i][1][0] = plus((1, banks[i][1][0]), (-c, banks[j][1][0])) + else: + need(event == {"kind": "terminal", "pairs": 4}, "literal terminal") + for pair in banks: + old_x, old_y = pair[0][0], pair[1][0] + pair[0][0], pair[1][0] = old_y, plus((-1, old_x)) + if index == 1: + need(banks[0] == [[{}, plus((-1, d)), {}], [z0, d, {}]], "post-B1 state") + if index >= 3: + need(not any(field for pair in banks for fields in pair for field in fields[1:]), "selected fields vanish after F2") + states.append({"event": event, "ordinary": [expr_json(fields[0]) for pair in banks for fields in pair], + "selected_nonzero_blocks": sum(bool(field) for pair in banks for fields in pair for field in fields[1:])}) + need(sorted(histories) == [0, 2, 4, 6, 8] and not any(histories.values()), "all five forward histories vanish") + need(not any(fields[1] or fields[2] for pair in banks for fields in pair), "final selected zero") + need(not any(pair[1][0] for pair in banks), "final completed-X zero") + need([pair[0][0] for pair in banks] == [z0, z1, {}, {}], "former-Y residual endpoints") + if mutation == "observe_former_Y": + need(not any(pair[0][0] for pair in banks), "former-Y is not an allowed observation") + if mutation == "observe_B1_cut": + need(not d, "B1-cut record detects family") + if mutation == "observe_B1_initial": + need(not op("B1", z0), "missing initial chart detects family") + return {"events": states, "zero_forward_stages": sorted(histories), "zero_initial_record_coordinates_per_owner": 64, + "initial_record_contract": [{"pair": k, "stages": [0, 2] if k == 0 else [2*k+1, 2*k+2], + "source": "initial ordinary X", "coordinates_per_stage_per_owner": 8} for k in range(4)], + "original_X0_A": expr_json(d), "final_former_Y": [expr_json(pair[0][0]) for pair in banks], + "scope": "ordinary-only bridges; no selected interventions before complete F2; homogeneous selected-only operations after F2 preserve this family"} + + +def report(root): + members, packet = load(root) + sources, recipe = source_checks(members, packet) + algebra = trajectory(recipe) + rejected = [] + for mutation in ("centre_coefficient", "relative_route_collision", "native_route_placement"): + try: + source_checks(members, packet, mutation) + except ValueError: + rejected.append(mutation) + else: + raise ValueError("source mutation accepted: " + mutation) + for mutation in ("wrong_initial_T_sign", "wrong_d_sign", "wrong_link_sign", "omit_B3_kernel", "omit_B4_kernel", + "omit_negative_bridge", "wrong_local_pair", "wrong_local_orientation", "wrong_bridge_sign", + "observe_former_Y", "observe_B1_cut", "observe_B1_initial"): + try: + trajectory(recipe, mutation) + except ValueError: + rejected.append(mutation) + else: + raise ValueError("trajectory mutation accepted: " + mutation) + return {"status": "PASS_QQ16_FINAL_RECORD_OBSTRUCTION", "sources": sources, "trajectory": algebra, + "rejected_controls": rejected, "claim": "actual regular-cover selected defect >= ceil(8|G|/7); no supplier or kappa claim"} + + +if __name__ == "__main__": + root = Path(__file__).resolve().parents[2] + print(json.dumps(report(root), indent=2)) \ No newline at end of file