diff --git a/research/qq16-coordinate-cut-decoder/README.md b/research/qq16-coordinate-cut-decoder/README.md new file mode 100644 index 0000000000..1ae3d3eb97 --- /dev/null +++ b/research/qq16-coordinate-cut-decoder/README.md @@ -0,0 +1,213 @@ +# QQ16 coordinate decoding with two retained cuts + +**Scoped ordered proof; no supplier or new kappa.** For the unchanged conserved +`F0/B_1_2` pair, 88 ordinary coordinate arrays suffice to recover **all original +pair-0 inputs**, provided the selected fields and completed-X block listed below +are available at the two specified cuts. The inputs may be arbitrary, not just +members of the eight local-axis families tested by +[PR2432](https://github.com/CrocSwap/integer-mult-bounds/pull/2432). + +This answers a restricted version of PR2432's next question. It does **not** +show that the final controller exposes these cut values, that retaining them +is free, or that 88 reads are a favorable physical implementation. It supplies +an explicit decoder once those observations are granted. + +## Exact observation contract + +Write `(x1,y1)=F0(x,y)` and `(x2,y2)=B_1_2(x1,y1)`, with no intervening +modification. Use the retained disjoint selected sets + +```text +A = [0,7,20,27,36,46,57,111] +T = [21,37,47,76,81,87,92,110] +U = {0,...,111} \ (A union T) +J = [1,2,3,4,5,6,8,12] +S = U \ J +``` + +The decoder receives only: + +- `x1_A`, `x1_T`, `y1_A`, `y1_T`, retained immediately after complete F0; +- `y2_A` and the completed-X ordinary block `C=x2_U`, immediately after B1; +- `x1_S`, the 88 ordinary arrays read after F0. + +An array includes its complete owner and payload coordinates. Reads are +side-effect-free. No original selected input, initial dense ordinary query, +`y2_U`, or former-Y final endpoint is an observation. This is a two-cut +information contract, not a bound of 88 total stored arrays: the selected +records and the complete `C` block are additional granted observations. +Other bank pairs can have arbitrary initial values; they do not participate +in these first two events. No recovery claim for those other pairs is made. + +## Ordered proof + +All equations are over rational-valued owner/payload arrays. Let `D_(s,p)` be +the actual invertible cover map for port p in chart s. The scalar centre matrix +is R. For a port set V, write + +```text +B_(s,V) z = sum_(p in V) r_p D_(s,p) z_p +B_s = B_(s,U) +ell_(s,V) = B_(s,V), for V=A or T +P_(s,V) q = D_(s,V)^(-1) R_V^(-1) q, for V=A or T. +``` + +Here `D_(s,V)` is block diagonal in ports; its entries are operators, not +commuting scalar coefficients. The actual selected Grams are +`R_A R_A^T = R_T R_T^T = 4I`, so `R_V^(-1)=R_V^T/4`. +The source normalization is `K=R^T/4`; its routed restriction to U is `K_(s,U)`. +These are the conserved maps in the retained +[ordered contract](../joint-query/evidence/JOINT-QUERY-TRANSFER.md), sections +“A variant that preserves both selected pair sums” and +“A forward map with the same conserved inputs.” + +### Recover the missing post-F0 ordinary arrays + +The forward equations give + +```text +f = R_0 x +x1_U = x_U - K_(0,U) f +y1_U = y_U + x1_U +x1_A = P_(0,A) ell_(0,T) x_T +x1_T = P_(0,T) f. +``` + +The backward U target is an exact subtraction. Its future logger changes +only A, and its source output at A is that logger's output. Consequently, + +```text +C = x2_U = x1_U - y1_U = -y_U +q = ell_(2,A) (y2_A - y1_A) + = B_2 y1_U + ell_(2,T) y1_T +v = q - ell_(2,T) y1_T + B_2 C + = B_2 x1_U. +``` + +Every expression on the left is determined by the allowed observations. +Subtract the known coordinates: + +```text +w = v - B_(2,S) x1_S + = R_J D_(2,J) x1_J. +``` + +The actual rational `R_J` is invertible. The checker derives its inverse +from the pinned R, verifies both inverse orders, and records the matrices in +[RESULT.json](RESULT.json). Thus + +```text +x1_J = D_(2,J)^(-1) (R_J^(-1) w). +``` + +The order is essential: first apply the scalar inverse, then undo each +port's cover map. Moving the different port maps through `R_J^(-1)` is not +valid. This step recovers all of `x1_U`, with no hypothesis on how its +owner or payload values were generated. + +### Recover the original inputs + +Use the selected sections and the recovered ordinary block: + +```text +f = ell_(0,T) x1_T +t = P_(0,T) ell_(0,A) x1_A +x_U = x1_U + K_(0,U) f +x_T = t +x_A = P_(0,A) (f - B_0 x_U - ell_(0,T) t) +y_U = -C +y_V = x1_V + y1_V - x_V, V=A,T. +``` + +The first two formulas invert the two selected forward records. The third +inverts its ordinary update. The fourth and fifth recover the selected +components of `R_0 x=f`. Finally, the unchanged selected pair sums recover +the original Y values. Therefore this decoder composed with the stated +observation map is the identity on all 224 original port arrays. + +This is an ordered algebraic argument for arbitrary arrays under the inherited +local contract. The finite fixtures below check its source-specific premises +and implementation; they are not the proof of the arbitrary-array statement. + +## Evidence and reproduction + +From the repository root, with Python 3.12 and its standard library: + +```sh +python3.12 scripts/research_package.py --package research/qq16-coordinate-cut-decoder +``` + +The registered commands run the direct check and the optimized replay and +source-corruption controls. Direct entry point: + +```sh +python3.12 -I -B research/qq16-coordinate-cut-decoder/verify.py +``` + +Expected status: `PASS_QQ16_COORDINATE_CUT_DECODER`. + +The check binds the actual packet, two archive members, the first F0/B1 events, +selected Grams, `K=R^T/4`, the two-sided unread-minor inverse, and 224 registered +port-route/inverse pairs, including their payload-translation inverse equations. +It implements the conserved logical maps directly, rather than executing the +native words or importing a predecessor verifier. + +Finite execution covers each of the 224 input-port placements using nonconstant +owner bit-functions and one dense signed/dyadic fixture with every field dirty. +All five incorrect decoders have explicit nonzero residuals: wrong C sign, +missing future-T subtraction, missing old-A subtraction, missing forward K +correction, and reversed route/scalar inverse order. Each of the five external +source-file corruptions is rejected. Checks remain active under `-O`, and the +optimized replay must match the committed result without modifying package files. + +The finite functions are constant in payload. The universal proof uses the +inherited invertibility of the full cover maps, not an extrapolation from these +functions. Native kernels, the remaining 17 schedule events, a proof assistant, +and the selected full cold replay were not run. + +## Relation to earlier work and limits + +- Gareth Davidson's [PR2432](https://github.com/CrocSwap/integer-mult-bounds/pull/2432), + pinned at `cbede349fc764aa38379aa533befe3215916cfcd`, supplies the unread basis + and the eight-family threshold. This package adds arbitrary-input sufficiency + under the explicit two-cut contract. It does not reprove the threshold or + claim a new unrestricted read minimum. +- commdata2338's [PR2174](https://github.com/CrocSwap/integer-mult-bounds/pull/2174), + pinned at `f79470a7931f3943360c10d15b428e0e4e479c22`, uses two initial dense + queries and a post-B1 selected cut to recover pair-0 selected inputs. It + reconstructs a transient F0 record which this package explicitly retains. + The observation and retention contracts differ; neither cost nor controller + superiority follows from this comparison. +- commdata2338's PR2384 exact `Model.forward/backward` implementation, as + retained by PR2432, was consulted. Its owner-function representation informed + the finite checker; no predecessor executable is imported or vendored. +- Ali Romman / PR1969 supplies the conserved maps, native contract and cover + semantics. Adam Gall / PR2093, kyzer1023 / PR2354, PR2389 and its PR2419 audit + supply the hidden-family and coordinate-read lineage. The retained Rohan Arun, + Jeremy Kothe, DreamingOfClouds and supplier contributors retain their credit. + +No read, storage, chart-map, cleanup, hosting, precision, tape or recursive-child +cost is certified here. In particular, the `B_2 C` read must be legal at the +completed-X type; an algebraic formula alone does not establish that access. +The selected frontier and frozen predecessors are unchanged. + +Base and exact input pins are in [SOURCES.json](SOURCES.json); scope and overlap +are in [TASK.json](TASK.json). Coordination: +[Discussion 2424](https://github.com/CrocSwap/integer-mult-bounds/discussions/2424#discussioncomment-18946004). +New work is Apache-2.0, submitted by `starship-s` with substantial assistance from +Hermes Agent (`gpt-6-astra-900k`: derivation and proof) and Codex +(`gpt-6-astra`, max effort: implementation and review). No independent human or +proof-assistant verification is claimed. + +## Open next questions + +1. **Can an actual controller retain or reconstruct these two-cut records?** + This is necessary to turn the information lemma into a usable decoder. + First trace `x1_A/T`, `y1_A/T`, `y2_A` and `C` through the remaining schedule, + with their native endpoint types. The blocker is legal retention and access, + not the local inverse. +2. **Does a fully charged implementation have a favorable budget?** + First price the 88 reads, `B_2 C`, scalar minor inversion, per-port chart + maps, storage and cleanup together. No physical implementation or favorable + complete bill has been supplied; stop this route if even its optimistic bill + misses the declared supplier target. diff --git a/research/qq16-coordinate-cut-decoder/RESULT.json b/research/qq16-coordinate-cut-decoder/RESULT.json new file mode 100644 index 0000000000..77782d5eb1 --- /dev/null +++ b/research/qq16-coordinate-cut-decoder/RESULT.json @@ -0,0 +1,2055 @@ +{ + "R_J": [ + [ + "0", + "1", + "0", + "0", + "0", + "0", + "0", + "1" + ], + [ + "1", + "1", + "1", + "1", + "1", + "1", + "1", + "0" + ], + [ + "1", + "0", + "0", + "0", + "0", + "1", + "0", + "1" + ], + [ + "0", + "0", + "1", + "1", + "1", + "0", + "-1", + "0" + ], + [ + "-1", + "0", + "-1", + "0", + "0", + "1", + "1", + "1" + ], + [ + "0", + "0", + "0", + "-1", + "1", + "0", + "0", + "0" + ], + [ + "0", + "1", + "1", + "0", + "0", + "0", + "1", + "1" + ], + [ + "-1", + "-1", + "0", + "-1", + "-1", + "1", + "0", + "0" + ] + ], + "R_J_inverse": [ + [ + "-1/4", + "0", + "1/2", + "-1/4", + "-1/4", + "0", + "0", + "-1/4" + ], + [ + "5/4", + "1/2", + "-1/2", + "-1/4", + "-1/4", + "0", + "-1/2", + "1/4" + ], + [ + "-1/4", + "0", + "0", + "1/4", + "-1/4", + "0", + "1/2", + "1/4" + ], + [ + "-1/4", + "0", + "0", + "1/4", + "1/4", + "-1/2", + "0", + "-1/4" + ], + [ + "-1/4", + "0", + "0", + "1/4", + "1/4", + "1/2", + "0", + "-1/4" + ], + [ + "1/2", + "1/2", + "0", + "0", + "0", + "0", + "-1/2", + "1/2" + ], + [ + "-3/4", + "0", + "0", + "-1/4", + "1/4", + "0", + "1/2", + "-1/4" + ], + [ + "-1/4", + "-1/2", + "1/2", + "1/4", + "1/4", + "0", + "1/2", + "-1/4" + ] + ], + "archive_member_sha256": { + "t16/global/base/split-centres/GLOBAL-TEMPLATE.json.gz": "a179dad87651aba340a5a8ddbcd86a8e757cad87b8a1f8bad48106fbecd38518", + "t16/global/base/work/complex-nine-native/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa" + }, + "formula_corrections": [], + "function_vectors": [ + 131085, + 262157, + 4294967309, + 18446744073709551629 + ], + "grams": { + "A": [ + [ + "4", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "4", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "4", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "4", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "4", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4" + ] + ], + "T": [ + [ + "4", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "4", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "4", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "4", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "4", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "4", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "4", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "4" + ] + ], + "U": [ + [ + "48", + "0", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "48", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "48", + "0", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "48", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "48", + "0", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "48", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "48", + "0" + ], + [ + "0", + "0", + "0", + "0", + "0", + "0", + "0", + "48" + ] + ] + }, + "limitations": [ + "finite function fixtures are not arbitrary-function exhaustiveness", + "ordered conserved contract inherited, native words not replayed", + "remaining 17 schedule events not replayed", + "no final-only or native-cost claim" + ], + "negative_control_witnesses": { + "omit_forward_K_correction": { + "actual": "67035/256", + "bank": "x", + "expected": "129/128", + "owner_word": [], + "port": 0, + "residual": "66777/256" + }, + "omit_future_T_subtraction": { + "actual": "51457/1024", + "bank": "x", + "expected": "129/128", + "owner_word": [], + "port": 0, + "residual": "50425/1024" + }, + "omit_y1_A_subtraction": { + "actual": "3911/4096", + "bank": "x", + "expected": "129/128", + "owner_word": [], + "port": 0, + "residual": "-217/4096" + }, + "route_inverse_before_R_inverse": { + "actual": "-34753/2048", + "bank": "x", + "expected": "129/128", + "owner_word": [], + "port": 0, + "residual": "-36817/2048" + }, + "wrong_C_sign": { + "actual": "-48563/1024", + "bank": "x", + "expected": "129/128", + "owner_word": [], + "port": 0, + "residual": "-49595/1024" + } + }, + "owner_evaluations_per_function": 5, + "partition": { + "A": [ + 0, + 7, + 20, + 27, + 36, + 46, + 57, + 111 + ], + "J": [ + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 12 + ], + "S": [ + 9, + 10, + 11, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 22, + 23, + 24, + 25, + 26, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 56, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 72, + 73, + 74, + 75, + 77, + 78, + 79, + 80, + 82, + 83, + 84, + 85, + 86, + 88, + 89, + 90, + 91, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109 + ], + "T": [ + 21, + 37, + 47, + 76, + 81, + 87, + 92, + 110 + ], + "U": [ + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 9, + 10, + 11, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 22, + 23, + 24, + 25, + 26, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 56, + 58, + 59, + 60, + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 72, + 73, + 74, + 75, + 77, + 78, + 79, + 80, + 82, + 83, + 84, + 85, + 86, + 88, + 89, + 90, + 91, + 93, + 94, + 95, + 96, + 97, + 98, + 99, + 100, + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109 + ] + }, + "replayed_cases": { + "dense_signed_dyadic": 1, + "port_basis_placements": 224 + }, + "route_bindings": [ + [ + 2, + 0, + "m89", + "m201" + ], + [ + 1, + 0, + "m1", + "m3" + ], + [ + 2, + 1, + "m90", + "m202" + ], + [ + 1, + 1, + "m313", + "m409" + ], + [ + 2, + 2, + "m91", + "m203" + ], + [ + 1, + 2, + "m314", + "m410" + ], + [ + 2, + 3, + "m92", + "m204" + ], + [ + 1, + 3, + "m315", + "m411" + ], + [ + 2, + 4, + "m93", + "m205" + ], + [ + 1, + 4, + "m316", + "m412" + ], + [ + 2, + 5, + "m94", + "m206" + ], + [ + 1, + 5, + "m317", + "m413" + ], + [ + 2, + 6, + "m95", + "m207" + ], + [ + 1, + 6, + "m318", + "m414" + ], + [ + 2, + 7, + "m96", + "m208" + ], + [ + 1, + 7, + "m15", + "m16" + ], + [ + 2, + 8, + "m97", + "m209" + ], + [ + 1, + 8, + "m319", + "m415" + ], + [ + 2, + 9, + "m98", + "m210" + ], + [ + 1, + 9, + "m320", + "m416" + ], + [ + 2, + 10, + "m99", + "m211" + ], + [ + 1, + 10, + "m321", + "m417" + ], + [ + 2, + 11, + "m100", + "m212" + ], + [ + 1, + 11, + "m322", + "m418" + ], + [ + 2, + 12, + "m101", + "m213" + ], + [ + 1, + 12, + "m323", + "m419" + ], + [ + 2, + 13, + "m102", + "m214" + ], + [ + 1, + 13, + "m324", + "m420" + ], + [ + 2, + 14, + "m103", + "m215" + ], + [ + 1, + 14, + "m325", + "m421" + ], + [ + 2, + 15, + "m104", + "m216" + ], + [ + 1, + 15, + "m326", + "m422" + ], + [ + 2, + 16, + "m105", + "m217" + ], + [ + 1, + 16, + "m327", + "m423" + ], + [ + 2, + 17, + "m106", + "m218" + ], + [ + 1, + 17, + "m328", + "m424" + ], + [ + 2, + 18, + "m107", + "m219" + ], + [ + 1, + 18, + "m329", + "m425" + ], + [ + 2, + 19, + "m108", + "m220" + ], + [ + 1, + 19, + "m330", + "m426" + ], + [ + 2, + 20, + "m109", + "m221" + ], + [ + 1, + 20, + "m25", + "m27" + ], + [ + 2, + 21, + "m110", + "m222" + ], + [ + 1, + 21, + "m26", + "m427" + ], + [ + 2, + 22, + "m111", + "m223" + ], + [ + 1, + 22, + "m331", + "m428" + ], + [ + 2, + 23, + "m112", + "m224" + ], + [ + 1, + 23, + "m332", + "m429" + ], + [ + 2, + 24, + "m113", + "m225" + ], + [ + 1, + 24, + "m333", + "m430" + ], + [ + 2, + 25, + "m114", + "m226" + ], + [ + 1, + 25, + "m334", + "m431" + ], + [ + 2, + 26, + "m115", + "m227" + ], + [ + 1, + 26, + "m335", + "m432" + ], + [ + 2, + 27, + "m116", + "m228" + ], + [ + 1, + 27, + "m39", + "m40" + ], + [ + 2, + 28, + "m117", + "m229" + ], + [ + 1, + 28, + "m336", + "m433" + ], + [ + 2, + 29, + "m118", + "m230" + ], + [ + 1, + 29, + "m337", + "m434" + ], + [ + 2, + 30, + "m119", + "m231" + ], + [ + 1, + 30, + "m338", + "m435" + ], + [ + 2, + 31, + "m120", + "m232" + ], + [ + 1, + 31, + "m339", + "m436" + ], + [ + 2, + 32, + "m121", + "m233" + ], + [ + 1, + 32, + "m340", + "m437" + ], + [ + 2, + 33, + "m122", + "m234" + ], + [ + 1, + 33, + "m341", + "m438" + ], + [ + 2, + 34, + "m123", + "m235" + ], + [ + 1, + 34, + "m342", + "m439" + ], + [ + 2, + 35, + "m124", + "m236" + ], + [ + 1, + 35, + "m343", + "m440" + ], + [ + 2, + 36, + "m125", + "m237" + ], + [ + 1, + 36, + "m49", + "m50" + ], + [ + 2, + 37, + "m126", + "m238" + ], + [ + 1, + 37, + "m29", + "m441" + ], + [ + 2, + 38, + "m127", + "m239" + ], + [ + 1, + 38, + "m344", + "m442" + ], + [ + 2, + 39, + "m128", + "m240" + ], + [ + 1, + 39, + "m345", + "m443" + ], + [ + 2, + 40, + "m129", + "m241" + ], + [ + 1, + 40, + "m346", + "m444" + ], + [ + 2, + 41, + "m130", + "m242" + ], + [ + 1, + 41, + "m347", + "m445" + ], + [ + 2, + 42, + "m131", + "m243" + ], + [ + 1, + 42, + "m348", + "m446" + ], + [ + 2, + 43, + "m132", + "m244" + ], + [ + 1, + 43, + "m349", + "m447" + ], + [ + 2, + 44, + "m133", + "m245" + ], + [ + 1, + 44, + "m350", + "m448" + ], + [ + 2, + 45, + "m134", + "m246" + ], + [ + 1, + 45, + "m351", + "m449" + ], + [ + 2, + 46, + "m135", + "m247" + ], + [ + 1, + 46, + "m59", + "m60" + ], + [ + 2, + 47, + "m136", + "m248" + ], + [ + 1, + 47, + "m31", + "m450" + ], + [ + 2, + 48, + "m137", + "m249" + ], + [ + 1, + 48, + "m352", + "m451" + ], + [ + 2, + 49, + "m138", + "m250" + ], + [ + 1, + 49, + "m353", + "m452" + ], + [ + 2, + 50, + "m139", + "m251" + ], + [ + 1, + 50, + "m354", + "m453" + ], + [ + 2, + 51, + "m140", + "m252" + ], + [ + 1, + 51, + "m355", + "m454" + ], + [ + 2, + 52, + "m141", + "m253" + ], + [ + 1, + 52, + "m356", + "m455" + ], + [ + 2, + 53, + "m142", + "m254" + ], + [ + 1, + 53, + "m357", + "m456" + ], + [ + 2, + 54, + "m143", + "m255" + ], + [ + 1, + 54, + "m358", + "m457" + ], + [ + 2, + 55, + "m144", + "m256" + ], + [ + 1, + 55, + "m359", + "m458" + ], + [ + 2, + 56, + "m145", + "m257" + ], + [ + 1, + 56, + "m360", + "m459" + ], + [ + 2, + 57, + "m146", + "m258" + ], + [ + 1, + 57, + "m69", + "m70" + ], + [ + 2, + 58, + "m147", + "m259" + ], + [ + 1, + 58, + "m361", + "m460" + ], + [ + 2, + 59, + "m148", + "m260" + ], + [ + 1, + 59, + "m362", + "m461" + ], + [ + 2, + 60, + "m149", + "m261" + ], + [ + 1, + 60, + "m363", + "m462" + ], + [ + 2, + 61, + "m150", + "m262" + ], + [ + 1, + 61, + "m364", + "m463" + ], + [ + 2, + 62, + "m151", + "m263" + ], + [ + 1, + 62, + "m365", + "m464" + ], + [ + 2, + 63, + "m152", + "m264" + ], + [ + 1, + 63, + "m366", + "m465" + ], + [ + 2, + 64, + "m153", + "m265" + ], + [ + 1, + 64, + "m367", + "m466" + ], + [ + 2, + 65, + "m154", + "m266" + ], + [ + 1, + 65, + "m368", + "m467" + ], + [ + 2, + 66, + "m155", + "m267" + ], + [ + 1, + 66, + "m369", + "m468" + ], + [ + 2, + 67, + "m156", + "m268" + ], + [ + 1, + 67, + "m370", + "m469" + ], + [ + 2, + 68, + "m157", + "m269" + ], + [ + 1, + 68, + "m371", + "m470" + ], + [ + 2, + 69, + "m158", + "m270" + ], + [ + 1, + 69, + "m372", + "m471" + ], + [ + 2, + 70, + "m159", + "m271" + ], + [ + 1, + 70, + "m373", + "m472" + ], + [ + 2, + 71, + "m160", + "m272" + ], + [ + 1, + 71, + "m374", + "m473" + ], + [ + 2, + 72, + "m161", + "m273" + ], + [ + 1, + 72, + "m375", + "m474" + ], + [ + 2, + 73, + "m162", + "m274" + ], + [ + 1, + 73, + "m376", + "m475" + ], + [ + 2, + 74, + "m163", + "m275" + ], + [ + 1, + 74, + "m377", + "m476" + ], + [ + 2, + 75, + "m164", + "m276" + ], + [ + 1, + 75, + "m378", + "m477" + ], + [ + 2, + 76, + "m165", + "m277" + ], + [ + 1, + 76, + "m2", + "m478" + ], + [ + 2, + 77, + "m166", + "m278" + ], + [ + 1, + 77, + "m379", + "m479" + ], + [ + 2, + 78, + "m167", + "m279" + ], + [ + 1, + 78, + "m380", + "m480" + ], + [ + 2, + 79, + "m168", + "m280" + ], + [ + 1, + 79, + "m381", + "m481" + ], + [ + 2, + 80, + "m169", + "m281" + ], + [ + 1, + 80, + "m382", + "m482" + ], + [ + 2, + 81, + "m170", + "m282" + ], + [ + 1, + 81, + "m5", + "m483" + ], + [ + 2, + 82, + "m171", + "m283" + ], + [ + 1, + 82, + "m383", + "m484" + ], + [ + 2, + 83, + "m172", + "m284" + ], + [ + 1, + 83, + "m384", + "m485" + ], + [ + 2, + 84, + "m173", + "m285" + ], + [ + 1, + 84, + "m385", + "m486" + ], + [ + 2, + 85, + "m174", + "m286" + ], + [ + 1, + 85, + "m386", + "m487" + ], + [ + 2, + 86, + "m175", + "m287" + ], + [ + 1, + 86, + "m387", + "m488" + ], + [ + 2, + 87, + "m176", + "m288" + ], + [ + 1, + 87, + "m7", + "m489" + ], + [ + 2, + 88, + "m177", + "m289" + ], + [ + 1, + 88, + "m388", + "m490" + ], + [ + 2, + 89, + "m178", + "m290" + ], + [ + 1, + 89, + "m389", + "m491" + ], + [ + 2, + 90, + "m179", + "m291" + ], + [ + 1, + 90, + "m390", + "m492" + ], + [ + 2, + 91, + "m180", + "m292" + ], + [ + 1, + 91, + "m391", + "m493" + ], + [ + 2, + 92, + "m181", + "m293" + ], + [ + 1, + 92, + "m9", + "m494" + ], + [ + 2, + 93, + "m182", + "m294" + ], + [ + 1, + 93, + "m392", + "m495" + ], + [ + 2, + 94, + "m183", + "m295" + ], + [ + 1, + 94, + "m393", + "m496" + ], + [ + 2, + 95, + "m184", + "m296" + ], + [ + 1, + 95, + "m394", + "m497" + ], + [ + 2, + 96, + "m185", + "m297" + ], + [ + 1, + 96, + "m395", + "m498" + ], + [ + 2, + 97, + "m186", + "m298" + ], + [ + 1, + 97, + "m396", + "m499" + ], + [ + 2, + 98, + "m187", + "m299" + ], + [ + 1, + 98, + "m397", + "m500" + ], + [ + 2, + 99, + "m188", + "m300" + ], + [ + 1, + 99, + "m398", + "m501" + ], + [ + 2, + 100, + "m189", + "m301" + ], + [ + 1, + 100, + "m399", + "m502" + ], + [ + 2, + 101, + "m190", + "m302" + ], + [ + 1, + 101, + "m400", + "m503" + ], + [ + 2, + 102, + "m191", + "m303" + ], + [ + 1, + 102, + "m401", + "m504" + ], + [ + 2, + 103, + "m192", + "m304" + ], + [ + 1, + 103, + "m402", + "m505" + ], + [ + 2, + 104, + "m193", + "m305" + ], + [ + 1, + 104, + "m403", + "m506" + ], + [ + 2, + 105, + "m194", + "m306" + ], + [ + 1, + 105, + "m404", + "m507" + ], + [ + 2, + 106, + "m195", + "m307" + ], + [ + 1, + 106, + "m405", + "m508" + ], + [ + 2, + 107, + "m196", + "m308" + ], + [ + 1, + 107, + "m406", + "m509" + ], + [ + 2, + 108, + "m197", + "m309" + ], + [ + 1, + 108, + "m407", + "m510" + ], + [ + 2, + 109, + "m198", + "m310" + ], + [ + 1, + 109, + "m408", + "m511" + ], + [ + 2, + 110, + "m199", + "m311" + ], + [ + 1, + 110, + "m33", + "m512" + ], + [ + 2, + 111, + "m200", + "m312" + ], + [ + 1, + 111, + "m79", + "m80" + ] + ], + "scope": "F0/B_1_2 only; full-array observations retained across two cuts; rational owner-bit functions, constant payload", + "source_sha256": { + "research/community-frontier1042-audit/selected-replay.tar.gz": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "research/joint-query/certificate.json.gz": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7", + "research/joint-query/evidence/CONSERVED-QQ16.md": "60f0de3a7205ba5046b5ae7ffa8bf2b1ea42ea46b498face0a77966b59e7f3fb", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75", + "research/joint-query/evidence/QQ16-COVER-ACTION-ADDENDUM.md": "4bb4a68d8b4811b6d8364150612056bc124d38f1974d6f603dae68a99c4682fb" + }, + "status": "PASS_QQ16_COORDINATE_CUT_DECODER", + "two_sided_R_J_inverse": true, + "two_sided_registered_map_inverses": 224 +} diff --git a/research/qq16-coordinate-cut-decoder/SOURCES.json b/research/qq16-coordinate-cut-decoder/SOURCES.json new file mode 100644 index 0000000000..69b9533b9d --- /dev/null +++ b/research/qq16-coordinate-cut-decoder/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754" + }, + { + "path": "research/joint-query/certificate.json.gz", + "usage": "input", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + }, + { + "path": "research/joint-query/evidence/CONSERVED-QQ16.md", + "usage": "input", + "git_blob": "4639583c1be02c2fb60ed8a8072c9969ef1569ce", + "sha256": "60f0de3a7205ba5046b5ae7ffa8bf2b1ea42ea46b498face0a77966b59e7f3fb" + }, + { + "path": "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "usage": "input", + "git_blob": "a6805c58f23132f9420efebf90f5b7e863c2e179", + "sha256": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75" + }, + { + "path": "research/joint-query/evidence/QQ16-COVER-ACTION-ADDENDUM.md", + "usage": "input", + "git_blob": "3dd1a990d7b9d57cfb20cf8e8dd45548f043a944", + "sha256": "4bb4a68d8b4811b6d8364150612056bc124d38f1974d6f603dae68a99c4682fb" + } + ] +} diff --git a/research/qq16-coordinate-cut-decoder/TASK.json b/research/qq16-coordinate-cut-decoder/TASK.json new file mode 100644 index 0000000000..9190d997a7 --- /dev/null +++ b/research/qq16-coordinate-cut-decoder/TASK.json @@ -0,0 +1,286 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "joint-query-controller", + "question": "Can one explicitly changed QQ16 interface recover the missing chart query and close a two-call controller within a favorable full budget?", + "starting_points": [ + "research/joint-query/README.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Add one explicitly priced ordinary-to-selected observation and derive the ordered two-call map and inverse.", + "Change the first local pair or retained state, then test the existing lost-observation witness and price all new operations." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the fixed-first-pair QQ16 witness before designing a controller. The checked #1969 local words do not evade that witness or supply global placement.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Apply the existing witness to one proposed extra observation or changed first pair. If it still loses the required record, stop. Otherwise derive one ordered two-call identity and charge the added read, chart maps and restoration before extending to more stages.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969" + ] + }, + "scope_status": "refined", + "actual_scope": "Arbitrary first-pair input recovery for the conserved F0/B_1_2 maps from 88 post-F0 ordinary coordinate arrays, retained post-F0 selected fields, post-B1 Y_A and completed-X ordinary block.", + "scope_change_reason": "Takes PR2432’s explicit other-input-family handoff as a two-cut information lemma. It grants retention/access and does not meet full physical controller admission.", + "bottleneck_link": "Separates arbitrary-input information recovery from still-open native access, retention and paid controller obligations.", + "budget_minutes": 60, + "stop_rule": "Complete or falsify this ordered inverse and its prescribed exact fixtures; no larger search or native supplier construction.", + "outcome": "completed", + "evidence": "README.md ordered proof; RESULT.json exact source-bound premises, 224 port placements, one dense dirty fixture and five failing decoder controls; test_verify.py optimized and source corruption checks.", + "author": "starship-s", + "ai_assistance": "Hermes Agent gpt-6-astra-900k: derivation/proof/specification. Codex gpt-6-astra at max effort: executable checker and review. No independent human review.", + "selection": { + "seed": "f570d76f248354dc276a9100f2baf892", + "track": "recursive-interfaces", + "suggestions": [ + { + "task_id": "joint-query-controller", + "scope_key": "0e34adbc1dd119161c3a", + "question": "Can one explicitly changed QQ16 interface recover the missing chart query and close a two-call controller within a favorable full budget?", + "method": "Change the first local pair or retained state, then test the existing lost-observation witness and price all new operations.", + "starting_points": [ + "research/joint-query/README.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "docs/research/community-efficient1000-review.md" + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the fixed-first-pair QQ16 witness before designing a controller. The checked #1969 local words do not evade that witness or supply global placement.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Apply the existing witness to one proposed extra observation or changed first pair. If it still loses the required record, stop. Otherwise derive one ordered two-call identity and charge the added read, chart maps and restoration before extending to more stages.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969" + ], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + }, + { + "task_id": "centre-path-sharing", + "scope_key": "184695337cedab03152e", + "question": "Can the 64-per-call centre path (eight rank-8 COPY/ERASE totals through the private temporary) be shared across calls or shrunk?", + "method": "Derive a fully charged favorable relaxation for sharing one centre path across k calls, including restoration, hosting and precision.", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt", + "certificates/selected-result.json" + ], + "acceptance_gate": "Show the changed centre charge and copy profile per call with every added restoration or hosting cost charged, and its ceiling via ceiling.ceiling(centre=...).", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write the per-call centre charge and copy children for sharing across k = 2 calls, charge the sharing overhead, and screen it; stop this route if even the ideal sharing gains under 10%. Ideal budgets: free 2.80x, shared by two 1.90x (levers.py).", + "bottleneck_link": "The centre path consumes 64 of about 99.6 unpaid coordinates per call, i.e. about 64% of the raw deficit.", + "allowed_variations": [ + "One sharing pattern across a fixed number of calls.", + "One reduced copied-total contract for the existing decoder.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Removing copies without a replacement contract for the decoder's copied totals." + ], + "overlap_terms": [ + "centre path", + "copied totals", + "private temporary", + "shared centre", + "batching" + ], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + }, + { + "task_id": "coverage-law-change", + "scope_key": "f383d8fc405ee6982cdd", + "question": "Can a template or call contract leave two or more unpaid coordinates per live family?", + "method": "Find an obstruction: show which data-endpoint obligation forces exactly one unpaid coordinate in the current template.", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/idle-axis-hosting/PROOF.md", + "certificates/selected-result.json" + ], + "acceptance_gate": "An explicit replacement identity, verified on a small complete instance with dirty inputs, priced with ceiling.ceiling(unpaid=...).", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Explain where the single unpaid coordinate per family comes from in the hosted template; propose one change and price it. Ideal budget: two unpaid coordinates per family is 3.77x (levers.py).", + "bottleneck_link": "The deficit is one coordinate per family minus the centre charge; doubling unpaid coordinates per family scales it directly.", + "allowed_variations": [ + "One template change or one endpoint-contract change.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Counting a coordinate as unpaid while leaving it unadvanced in the data endpoint." + ], + "overlap_terms": [ + "coverage identity", + "unpaid coordinate", + "deficit law", + "W - 64N" + ], + "scope_rule": "If you change the card's premise, record scope_status=changed and explain why. A package metadata check cannot establish mathematical relevance." + } + ], + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "catalog_assessed_on": "2026-10-14", + "priority_revision": 4, + "priority_log": "docs/research/research-priority-log.md", + "catalog_sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "selected": { + "kappa": "836330098538459/500000000000000000", + "review": "docs/research/community-batch1099-review.md", + "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "reproduce": "make frontier1094-verify" + }, + "status": "SUGGESTIONS_ONLY_NOT_RESERVED", + "next_step": "Check live overlap, refine one question's object and domain, and record a bounded task card. A different seed or scope key is not evidence of novelty." + }, + "scope_key": "QQ16/F0-B12/88-coordinate-read/arbitrary-input/two-retained-cuts", + "predecessors": [ + { + "pr": 2432, + "head": "cbede349fc764aa38379aa533befe3215916cfcd", + "role": "Unread basis, eight-axis family criterion and follow-up question; Gareth Davidson." + }, + { + "pr": 2174, + "head": "f79470a7931f3943360c10d15b428e0e4e479c22", + "role": "Different two-dense-query post-B1 selected recovery contract; commdata2338." + }, + { + "pr": 1969, + "head": "a6e6ad3936f67b8f63b5b68c5e75d540610a65e7", + "role": "Ali Romman conserved maps and inherited native contract, consumed through pinned main files." + } + ], + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2424#discussioncomment-18946004", + "overlap": { + "status": "POSSIBLE_OVERLAP_NOT_A_NOVELTY_CERTIFICATE", + "searched_at": "2026-10-15T09:43:39.601858+00:00", + "terms": [ + "88-port", + "all-axis", + "basis-complement" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-15T09:39:36.744398+00:00", + "complete_pagination": true, + "records": 635 + }, + "discussions": { + "fetched_at": "2026-10-15T09:41:51.001535+00:00", + "complete_pagination": true, + "records": 1167 + } + }, + "local_records": 1536, + "warnings": [], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "matches_total": 2, + "matches": [ + { + "number": 2424, + "title": "DONE: QQ16 all-axis read criterion and sharp 88-port threshold", + "kind": "discussion", + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2424", + "updated_at": "2026-10-15T09:31:05Z", + "matched_terms": [ + "88-port", + "all-axis", + "basis-complement" + ], + "score": 7, + "excerpt": "on is credited PR2384 reuse; the separate certificate checker imports neither verifier. Next test a basis-complement88-port set against other input families, or specify a genuinely different dense-query interface with full native cost.\n\nGareth Davidson with substantial OpenAI Codex assistance. commdata2338, kyzer1023, Adam Gall, Ali Romman, the PR2389/2419 reviewers and retained source contributors keep the credit listed in NOTICE.md. No independent human review claimed.\n" + }, + { + "kind": "pr", + "number": 2432, + "title": "Prove QQ16’s 88-port threshold for all eight local-axis families", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/2432", + "head": "cbede349fc764aa38379aa533befe3215916cfcd", + "updated_at": "2026-10-15T09:30:09Z", + "draft": false, + "state": "open", + "matched_terms": [ + "88-port" + ], + "score": 3, + "excerpt": "PR2384 leaves open which ordinary read sets eliminate all eight QQ16 local-axis hidden-input families. This proves an exact criterion and sharp thresholds: **66,76,84,88 reads** for the first1,2,3,4 axes, with88 also sharp for all eight. The66 figure is credited prior work; this adds the simultaneous-axis criterion and the76/84/88 bounds.\n\nA read set handles all eight families exactly when its unread R columns are independent. Leaving `[1,2,3,4,5,6,8,12]` unread attains88. The proof uses invaria" + } + ] + }, + "open_questions": [ + { + "question": "Can an actual controller retain or reconstruct the two-cut records?", + "why_it_matters": "The ordered inverse cannot use inaccessible final endpoint data.", + "first_step": "Trace x1_A/T, y1_A/T, y2_A and C through the remaining schedule with endpoint types.", + "blocked_by": "No legal native retention/access implementation is provided." + }, + { + "question": "Does a fully charged implementation have a favorable supplier budget?", + "why_it_matters": "Algebraic recoverability alone does not imply lower recursive cost.", + "first_step": "Price 88 reads, B2 C, the minor inverse, port maps, storage and cleanup together; stop if even an optimistic bill misses the target.", + "blocked_by": "No physical implementation, hosting proof or complete bill is supplied." + } + ] +} diff --git a/research/qq16-coordinate-cut-decoder/VERIFY.json b/research/qq16-coordinate-cut-decoder/VERIFY.json new file mode 100644 index 0000000000..e8d78c26dd --- /dev/null +++ b/research/qq16-coordinate-cut-decoder/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/community-frontier1042-audit/selected-replay.tar.gz", + "research/joint-query/certificate.json.gz", + "research/joint-query/evidence/CONSERVED-QQ16.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "research/joint-query/evidence/QQ16-COVER-ACTION-ADDENDUM.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Pinned source contracts, exact unread minor and registered map inverses, 224 nonconstant owner-function port placements, dense dirty fixture and five incorrect decoders." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Optimized subprocess matches committed receipt without writes; injected corruption of each external source is rejected." + } + ] +} diff --git a/research/qq16-coordinate-cut-decoder/test_verify.py b/research/qq16-coordinate-cut-decoder/test_verify.py new file mode 100644 index 0000000000..e243d996ca --- /dev/null +++ b/research/qq16-coordinate-cut-decoder/test_verify.py @@ -0,0 +1,53 @@ +#!/usr/bin/env python3 +"""Source-corruption and optimized-entry-point controls, standard library only.""" +import hashlib +import importlib.util +import json +from pathlib import Path +import re +import subprocess +import sys +import unittest +from unittest.mock import patch + +PACKAGE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("coordinate_decoder", PACKAGE / "verify.py") +verify = importlib.util.module_from_spec(spec) +spec.loader.exec_module(verify) + + +class EntryPointControls(unittest.TestCase): + def test_source_corruption(self): + original_read = Path.read_bytes + for relative in verify.PINS: + with self.subTest(source=relative): + target = verify.ROOT / relative + data = bytearray(original_read(target)) + data[len(data) // 2] ^= 1 + damaged = bytes(data) + + def read_corrupted(path): + return damaged if path == target else original_read(path) + + with patch.object(Path, "read_bytes", read_corrupted): + with self.assertRaisesRegex(ValueError, "source hash mismatch: " + re.escape(relative)): + verify.load_sources() + + def test_optimized_replay(self): + before = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in PACKAGE.iterdir() if p.is_file()} + replay = subprocess.run([sys.executable, "-I", "-O", "-B", str(PACKAGE / "verify.py")], + capture_output=True, text=True, timeout=600, check=True) + summary = json.loads(replay.stdout) + self.assertEqual(summary["status"], "PASS_QQ16_COORDINATE_CUT_DECODER") + self.assertEqual(summary["replayed_cases"], {"port_basis_placements": 224, "dense_signed_dyadic": 1}) + self.assertEqual(summary["controls_rejected"], 5) + self.assertEqual(summary["result_sha256"], before["RESULT.json"]) + after = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in PACKAGE.iterdir() if p.is_file()} + self.assertEqual(before, after, "normal replay must not mutate package files") + print(json.dumps({"optimized_replay": summary}), flush=True) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/qq16-coordinate-cut-decoder/verify.py b/research/qq16-coordinate-cut-decoder/verify.py new file mode 100644 index 0000000000..e4bcea403a --- /dev/null +++ b/research/qq16-coordinate-cut-decoder/verify.py @@ -0,0 +1,354 @@ +#!/usr/bin/env python3 +"""Exact finite check of the QQ16 F0/B_1_2 coordinate-cut decoder. + +Direct implementation of Ali Romman's pinned conserved contract (PR1969). +Question/J from Gareth Davidson's PR2432; commdata2338's PR2384 Model was +consulted, not imported or vendored. Apache-2.0; OpenAI Codex assistance. +Functions below are rational sums of bit_0(d*v), constant in payload. +""" +import argparse +from fractions import Fraction as Q +import gzip +import hashlib +import io +import json +from pathlib import Path +import platform +import tarfile +import time + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +ARCHIVE = "research/community-frontier1042-audit/selected-replay.tar.gz" +PACKET = "research/joint-query/certificate.json.gz" +PINS = { + ARCHIVE: "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + PACKET: "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7", + "research/joint-query/evidence/CONSERVED-QQ16.md": + "60f0de3a7205ba5046b5ae7ffa8bf2b1ea42ea46b498face0a77966b59e7f3fb", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md": + "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75", + "research/joint-query/evidence/QQ16-COVER-ACTION-ADDENDUM.md": + "4bb4a68d8b4811b6d8364150612056bc124d38f1974d6f603dae68a99c4682fb", +} +MEMBERS = { + "t16/global/base/work/complex-nine-native/DATA-PHASES.json": + "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "t16/global/base/split-centres/GLOBAL-TEMPLATE.json.gz": + "a179dad87651aba340a5a8ddbcd86a8e757cad87b8a1f8bad48106fbecd38518", +} +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) +J = (1, 2, 3, 4, 5, 6, 8, 12) +S = tuple(p for p in U if p not in J) +IDENTITY = tuple(1 << i for i in range(73)) +FAULTS = ("wrong_C_sign", "omit_future_T_subtraction", "omit_y1_A_subtraction", + "omit_forward_K_correction", "route_inverse_before_R_inverse") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate(data, digest, label): + require(hashlib.sha256(data).hexdigest() == digest, "source hash mismatch: " + label) + return data + + +def load_sources(): + raw = {path: authenticate((ROOT / path).read_bytes(), pin, path) + for path, pin in PINS.items()} + decoded = [] + with tarfile.open(fileobj=io.BytesIO(raw[ARCHIVE]), mode="r:gz") as archive: + for name, pin in MEMBERS.items(): + matches = [member for member in archive if member.name == name] + require(len(matches) == 1 and matches[0].isfile(), "unique regular member: " + name) + data = authenticate(archive.extractfile(matches[0]).read(), pin, name) + decoded.append(json.loads(gzip.decompress(data) if name.endswith(".gz") else data)) + return json.loads(gzip.decompress(raw[PACKET])), *decoded + + +def act(columns, vector): + value = 0 + while vector: + bit = vector & -vector + value ^= columns[bit.bit_length() - 1] + vector ^= bit + return value + + +def linear(coefficients, functions): + out = {} + for c, function in zip(coefficients, functions, strict=True): + if c: + for v, a in function.items(): + out[v] = out.get(v, Q(0)) + c * a + return {v: a for v, a in out.items() if v and a} + + +def add(a, b, scale=1): + return linear((1, scale), (a, b)) + + +def route(function, columns): + # An invertible owner map permutes vector labels; it is not a payload map. + return {act(columns, v): a for v, a in function.items()} + + +def evaluate(function, owner): + return sum((a * (act(owner, v) & 1) for v, a in function.items()), Q(0)) + + +def multiply(a, b): + return [[sum((x * y for x, y in zip(row, col, strict=True)), Q(0)) + for col in zip(*b, strict=True)] for row in a] + + +def inverse(matrix): + n = len(matrix) + rows = [list(row) + [Q(i == j) for j in range(n)] for i, row in enumerate(matrix)] + for col in range(n): + pivot = next((i for i in range(col, n) if rows[i][col]), None) + require(pivot is not None, "singular R_J") + rows[col], rows[pivot] = rows[pivot], rows[col] + divisor = rows[col][col] + rows[col] = [v / divisor for v in rows[col]] + for i in range(n): + if i != col: + c = rows[i][col] + rows[i] = [v - c * w for v, w in zip(rows[i], rows[col], strict=True)] + return [row[n:] for row in rows] + + +def bind_routes(packet, phases, template): + require(phases["m"] == 73 and len(phases["recipes"]) == 112, "route dimensions") + require(template["recipe"][:2] == [ + {"kind": "local", "pair": 0, "reverse": False, "stage": 0}, + {"kind": "local", "pair": 0, "reverse": True, "stage": 1}], "first two events") + for case, orientation, stage in (("F_0", "F", 0), ("B_1_2", "B", 1)): + parameters = packet["case_parameters"][case] + require(parameters["orientation"] == orientation and parameters["stage"] == stage, + "case binding: " + case) + require(packet["case_parameters"]["B_1_2"]["future"] == 2, "future chart") + require(packet["case_parameters"]["F_0"]["explicit_cover_maps"] == 0, "D_0 = I") + program = packet["programs"]["B_1_2"] + sweeps = {e[1]: i for i, e in enumerate(program) if e[0] == "cover_sweep"} + require(list(sweeps) == ["future_E_t", "Y_U_from_X_T", "eight_unsigned_swaps", + "Y_T_query_subtract"], "ordered B1 sweep binding") + forward = {(0, p): IDENTITY for p in range(112)} + backward = dict(forward) + bindings = [] + for p, recipe in enumerate(phases["recipes"]): + basis = recipe["idle_children"][0]["orthogonal_axes"][:8] + local = [recipe["q"], *basis] + require(recipe["port"] == p and len(local) == 9, "port chart binding") + require(all(0 < v < 512 for v in local), "local nine-axis support") + require(all(((v & w).bit_count() % 2) == (i == j) + for i, v in enumerate(local) for j, w in enumerate(local)), "local chart Gram") + entries = [(i, e[2]) for i, e in enumerate(program) + if e[0] == "cover_map" and e[1] == ["L", 112 + p]] + require(len(entries) == 4, "four actual Y alignment maps") + positions = [i for i, _ in entries] + require(positions[0] < sweeps["future_E_t"] < positions[1] < positions[2] + < sweeps["Y_U_from_X_T"] < sweeps["Y_T_query_subtract"] < positions[3], + "actual alignment/inverse order") + for stage, offset in ((2, 0), (1, 2)): + names = [entries[offset + i][1] for i in range(2)] + maps = [packet["map_registry"][name] for name in names] + g, h = [tuple(m["owner_right_matrix_columns"]) for m in maps] + delta, undo = [m["payload_translation_at_identity_owner"] for m in maps] + deltas = [b ^ (1 << (9 + 8 * (stage - 1) + i)) for i, b in enumerate(basis)] + expected = tuple(e ^ act(deltas, sum(((e & d).bit_count() % 2) << i + for i, d in enumerate(deltas))) for e in IDENTITY) + require(g == expected and len(h) == 73, "registered port route differs from chart") + require(all(act(g, h[i]) == act(h, g[i]) == IDENTITY[i] for i in range(73)), + "two-sided port route inverse") + beta_lift = sum((((b.bit_count() - 1) // 2) % 2) << (9 + 8 * (stage - 1) + i) + for i, b in enumerate(basis)) + require(delta == recipe["q"] ^ beta_lift, "actual Y payload translation") + require(delta ^ act(g, undo) == undo ^ act(h, delta) == 0, + "two-sided registered full-map inverse") + forward[stage, p], backward[stage, p] = g, h + bindings.append([stage, p, *names]) + return forward, backward, bindings + + +class FirstPair: + def __init__(self, packet, phases, template): + require(tuple(packet["A_ports"]) == A and tuple(packet["T_ports"]) == T + and tuple(packet["U_ports"]) == U, "actual R partition") + self.R = [[Q(row.get(str(p), 0)) for p in range(112)] for row in packet["R_rows"]] + require(len(self.R) == 8, "eight query coordinates") + self.grams = {} + for name, ports, scale in (("A", A, 4), ("T", T, 4), ("U", U, 48)): + block = [[row[p] for p in ports] for row in self.R] + gram = multiply(block, list(zip(*block, strict=True))) + require(gram == [[Q(scale * (i == j)) for j in range(8)] for i in range(8)], + "actual Gram: " + name) + self.grams[name] = gram + require(len(packet["K_rows"]) == 112 and all( + Q(packet["K_rows"][p].get(str(i), 0)) == self.R[i][p] / 4 + for p in range(112) for i in range(8)), "actual K = R^T/4") + self.RJ = [[row[p] for p in J] for row in self.R] + self.RJ_inverse = inverse(self.RJ) + identity = [[Q(i == j) for j in range(8)] for i in range(8)] + require(multiply(self.RJ, self.RJ_inverse) == multiply(self.RJ_inverse, self.RJ) + == identity, "two-sided R_J inverse") + self.routes, self.inverses, self.bindings = bind_routes(packet, phases, template) + + def query(self, bank, stage, ports): + values = [route(bank[p], self.routes[stage, p]) for p in ports] + return [linear([row[p] for p in ports], values) for row in self.R] + + def section(self, query, stage, ports): + return {p: route(linear([row[p] / 4 for row in self.R], query), self.inverses[stage, p]) + for p in ports} + + def forward(self, x, y): + f = self.query(x, 0, range(112)) + kf = self.section(f, 0, U + T) + old_t = self.section(self.query(x, 0, T), 0, A) + xx = [add(x[p], kf[p], -1) if p in U else old_t[p] if p in A else kf[p] + for p in range(112)] + yy = [add(y[p], xx[p]) if p in U else add(add(x[p], y[p]), xx[p], -1) + for p in range(112)] + return xx, yy + + def backward(self, x, y): + logger = self.section(self.query(y, 2, U + T), 2, A) + u = [add(y[p], logger[p]) if p in A else y[p] for p in range(112)] + a, b = self.query(x, 1, T), self.query(u, 1, range(112)) + ku = self.section(a, 1, U) + correction = self.section([add(bb, aa, 11) for aa, bb in zip(a, b)], 1, T) + target = self.section([add(bb, aa, 12) for aa, bb in zip(a, b)], 1, T) + xx = [add(x[p], y[p], -1) if p in U else add(add(x[p], y[p]), u[p], -1) + if p in A else target[p] for p in range(112)] + yy = [add(y[p], ku[p]) if p in U else u[p] if p in A else add(u[p], correction[p], -1) + for p in range(112)] + return xx, yy + + +def decode(model, x1_selected, y1_selected, y2_A, C, x1_read, fault=None): + for fields, ports in ((x1_selected, A + T), (y1_selected, A + T), + (y2_A, A), (C, U), (x1_read, S)): + require(set(fields) == set(ports), "decoder observation boundary") + require(fault is None or fault in FAULTS, "unknown control") + f = model.query(x1_selected, 0, T) + t = model.section(model.query(x1_selected, 0, A), 0, T) + baseline = 0 if fault == "omit_y1_A_subtraction" else -1 + q = model.query({p: add(y2_A[p], y1_selected[p], baseline) for p in A}, 2, A) + if fault == "wrong_C_sign": + C = {p: linear([-1], [value]) for p, value in C.items()} + future_t, bc = model.query(y1_selected, 2, T), model.query(C, 2, U) + v = [linear([1, 0 if fault == "omit_future_T_subtraction" else -1, 1], values) + for values in zip(q, future_t, bc, strict=True)] + known = model.query(x1_read, 2, S) + rhs = [add(a, b, -1) for a, b in zip(v, known, strict=True)] + if fault == "route_inverse_before_R_inverse": + rhs = [route(value, model.inverses[2, p]) for p, value in zip(J, rhs, strict=True)] + solved = [linear(row, rhs) for row in model.RJ_inverse] + x1_U = dict(x1_read) + for p, value in zip(J, solved, strict=True): + x1_U[p] = value if fault == "route_inverse_before_R_inverse" else route(value, model.inverses[2, p]) + kf = model.section(f, 0, U) + x_U = {p: x1_U[p] if fault == "omit_forward_K_correction" else add(x1_U[p], kf[p]) for p in U} + b0, ell_t = model.query(x_U, 0, U), model.query(t, 0, T) + x_A = model.section([linear([1, -1, -1], values) for values in zip(f, b0, ell_t)], 0, A) + x = [x_U[p] if p in U else x_A[p] if p in A else t[p] for p in range(112)] + y = [linear([-1], [C[p]]) if p in U else linear([1, 1, -1], [x1_selected[p], y1_selected[p], x[p]]) + for p in range(112)] + return x, y + + +def observe(x1, y1, x2, y2): + return ({p: x1[p] for p in A + T}, {p: y1[p] for p in A + T}, + {p: y2[p] for p in A}, {p: x2[p] for p in U}, {p: x1[p] for p in S}) + + +def residual(expected, actual, owners): + for bank, (want, got) in enumerate(zip(expected, actual, strict=True)): + for p, (a, b) in enumerate(zip(want, got, strict=True)): + if a != b: + for word, owner in owners: + av, bv = evaluate(a, owner), evaluate(b, owner) + if av != bv: + return {"bank": "xy"[bank], "port": p, "owner_word": word, + "expected": str(av), "actual": str(bv), "residual": str(bv - av)} + return None + + +def build_result(): + packet, phases, template = load_sources() + model = FirstPair(packet, phases, template) + # These are actual registered owners, not an invented full orthogonal group. + owners = [([], IDENTITY)] + [([entry], model.routes[stage, p]) + for stage, p, entry, _ in model.bindings if p in (0, 1)] + base_vector = phases["recipes"][0]["idle_children"][0]["orthogonal_axes"][0] + vectors = [base_vector ^ (1 << i) for i in (17, 18, 32, 64)] + functions = [{v: Q(1)} for v in vectors] + require(all(len({evaluate(f, owner) for _, owner in owners}) > 1 for f in functions), + "basis functions must vary on registered owners") + + def replay(x, y, label): + x1, y1 = model.forward(x, y) + x2, y2 = model.backward(x1, y1) + observed = observe(x1, y1, x2, y2) + restored = decode(model, *observed) + require(restored == (x, y), "decoder failure: " + json.dumps({ + "fixture": label, "witness": residual((x, y), restored, owners), + "note": "a null witness means an unresolved symbolic residual, not a counterexample"})) + return observed + + for bank in range(2): + for p in range(112): + inputs = [[{} for _ in range(112)] for _ in range(2)] + inputs[bank][p] = functions[(p + 2 * bank) % 4] + replay(*inputs, f"{'xy'[bank]}[{p}]") + dense = [[linear([Q((-1) ** (p + bank) * (p % 7 + 1), 1 << ((p + bank) % 4)), + Q((-1) ** (p // 3 + bank) * (p % 5 + 1), 1 << (7 + (p + bank) % 3))], + [functions[(p + bank) % 4], functions[(p + bank + 1) % 4]]) + for p in range(112)] for bank in range(2)] + require(all(evaluate(f, IDENTITY) for bank in dense for f in bank), "all 224 dense fields dirty") + observed = replay(*dense, "dense_signed_dyadic") + controls = {fault: residual(tuple(dense), decode(model, *observed, fault=fault), owners) + for fault in FAULTS} + ineffective = [fault for fault, witness in controls.items() if witness is None] + require(not ineffective, "ineffective controls (no witnessed nonzero residual): " + str(ineffective)) + return { + "status": "PASS_QQ16_COORDINATE_CUT_DECODER", + "source_sha256": PINS, "archive_member_sha256": MEMBERS, + "partition": {"A": A, "T": T, "U": U, "J": J, "S": S}, + "grams": model.grams, "R_J": model.RJ, "R_J_inverse": model.RJ_inverse, + "two_sided_R_J_inverse": True, + "route_bindings": model.bindings, "two_sided_registered_map_inverses": 224, + "replayed_cases": {"port_basis_placements": 224, "dense_signed_dyadic": 1}, + "function_vectors": vectors, "owner_evaluations_per_function": len(owners), + "negative_control_witnesses": controls, "formula_corrections": [], + "scope": "F0/B_1_2 only; full-array observations retained across two cuts; rational owner-bit functions, constant payload", + "limitations": ["finite function fixtures are not arbitrary-function exhaustiveness", + "ordered conserved contract inherited, native words not replayed", + "remaining 17 schedule events not replayed", "no final-only or native-cost claim"], + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-result", type=Path, help="explicitly create a new result JSON; refuses overwrite") + args = parser.parse_args() + started = time.perf_counter() + result = build_result() + encoded = json.dumps(result, default=str, sort_keys=True, indent=2) + "\n" + if args.emit_result: + with args.emit_result.open("x") as output: + output.write(encoded) + print(json.dumps({"status": result["status"], "replayed_cases": result["replayed_cases"], + "controls_rejected": len(result["negative_control_witnesses"]), + "result_sha256": hashlib.sha256(encoded.encode()).hexdigest(), + "elapsed_seconds": round(time.perf_counter() - started, 3), + "python": platform.python_version(), "implementation": platform.python_implementation()})) + + +if __name__ == "__main__": + main()