diff --git a/research/qq16-fourth-moment-capacity/README.md b/research/qq16-fourth-moment-capacity/README.md new file mode 100644 index 0000000000..59f5e8d1fc --- /dev/null +++ b/research/qq16-fourth-moment-capacity/README.md @@ -0,0 +1,313 @@ +# QQ16: fifteen-coordinate linear records still lose selected inputs + +For the fixed QQ16 `F0/B_1_2` erasure and observation contract, every +read-only rational-linear record with at most **fifteen scalars per +regular-cover owner fails** to restore the original selected inputs. +The new exact fourth moment gives + +```text +tr(T^4) = (1823/36)|G|, +rank([B0;B1;B2]) >= (117/5)|G|, +selected A/T defect dimension >= ceil((77/5)|G|). +``` + +A rank-d record leaves at least `max(0,ceil(77|G|/5)-d)` selected +input dimensions invisible. At width fifteen the residual is at least +`ceil(2|G|/5)>0`. Thus an integer number of coordinates per owner must +be at least **sixteen**, strengthening the necessary width fourteen +from Nick Petalas's [PR #2181](https://github.com/CrocSwap/integer-mult-bounds/pull/2181). +This is a scoped proof with exact finite certificates, author-checked +by two different calculations. It is not an independently reviewed or +formalized theorem, a physical cost bound, or a new supplier or kappa. + +The claim is in [discussion #2074](https://github.com/CrocSwap/integer-mult-bounds/discussions/2074#discussioncomment-18935517), +following #2181's higher-moment handoff. The record encoder is linear; +the decoder may be arbitrary. Fixed offsets and common dirty baselines +are allowed. Changed first pairs, changed ordinary trajectories, +nonlinear encoders and uncounted independent payload storage are excluded. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3 -I -B scripts/research_package.py --package research/qq16-fourth-moment-capacity +``` + +The hook runs the primary certificate, the separate block-Gram oracle, +and the semantic/artifact controls in normal and optimized modes. Direct +read-only replay, also usable in a source export: + +```sh +python3 -I -O -B research/qq16-fourth-moment-capacity/verify.py +python3 -I -O -B research/qq16-fourth-moment-capacity/oracle.py +``` + +Expected lines include: + +```text +PASS_QQ16_FOURTH_MOMENT_CAPACITY moment4=1823/36 rank>=117|G|/5 defect>=77|G|/5 width>=16 no_new_kappa +PASS_QQ16_BLOCK_GRAM_ORACLE moments=24,28,109/3,1823/36 blocks=9 +``` + +[RESULT.json](RESULT.json) contains the exact pair-product census, its +six full-matrix digests, all stage-word counts and rational coefficients. +[SOURCES.json](SOURCES.json) pins the immutable main inputs; pending PR +checkouts, network access and third-party modules are unnecessary. +[TASK.json](TASK.json) records the scope change and exact predecessor heads. + +## 1. Operators and finite premises + +Use the actual 96 ordinary ports U and the three query operators +`B_s=R_s iota_U`, for s=0,1,2, of Ali Romman's retained +[joint-query package](../joint-query/README.md). Let G be a finite group +containing the literal owner-route matrices, acting regularly, and put +N=|G|. As in the inherited witness, restrict to fields constant in each +payload block: payload translations disappear, but arbitrary owner +values remain. This is not a quotient that identifies distinct routes. +The packet-to-native interpretation remains inherited. + +For ordinary port p, write r_p for its eight-component integer column +and g_s(p) for its owner route. The pinned packet checks establish + +```text +g_0(p)=1, g_s(p)^2=1, +r_p^T r_p=4, sum_p r_p r_p^T=48 I_8. +``` + +The stage-1 and stage-2 routes act on the first 25 binary axes and fix +the remaining 48 of the original 73 axes. The shared source binder +checks the entire 73-column input, the common orthonormal chart-swap +form, the A/T/U partition, both selected Grams, and agreement between +F1/F2 and the current/future B_1_2 alignment maps. Its extraction and +chart checks are adapted, with credit, from #2181. + +Let `h_st(p)=g_s(p)g_t(p)^-1` and +`C_st(p,q)=h_st(p)h_st(q)^-1`, for each ordered s!=t. A new exhaustive +exact binary-matrix census checks all **6*96^2 = 55,296** ordered products: + +* Each of the six tables has 9,121 distinct products. Its identity + fibre is precisely the 96 diagonal pairs `(p,p)`; every other fibre + is a singleton. +* For every s, with t and u the other two stages, the images of C_st + and C_su intersect only in the identity. + +All port pairs are included, even when their scalar coefficient is zero. +Matrix equality is on all active axes with the spectators checked as +fixed. No enumeration of the huge group G or probabilistic hashing is +used for equality; the digests are portable receipts of exact tables. + +Under the regular right action `Q_g f(d)=f(dg)`, `tr Q_g` is N for the +identity and zero otherwise. Put + +```text +P_s=B_s*B_s/48, T=P_0+P_1+P_2. +``` + +Since `B_s B_s*=48 I_(8N)`, each P_s is an orthogonal projection of +rank 8N. Moreover `rank T=rank [B0;B1;B2]`. All matrices are rational, +so real and rational ranks agree. + +## 2. The fourth trace + +Set `M_st=B_s B_t*` and `A_st=M_st M_ts`. The coefficient of A_st at +route C_st(p,q) is contributed by + +```text +(r_p^T r_q) r_p r_q^T. +``` + +At the identity, summing the diagonal fibre gives `192 I_8`. All other +coefficients have a unique ordered pair. For a self-adjoint group-algebra +matrix A, its regular trace satisfies + +```text +tr(A^2)/N = sum_g ||A[g]||_F^2. +``` + +Here the full root Gram square sum is +`sum_(p,q) (r_p^T r_q)^2 = tr((48 I_8)^2)=18432`; the diagonal contributes +`96*16=1536`. Therefore, for s!=t, + +```text +tr(P_s P_t P_s P_t)/N + = [8*192^2 + 16*(18432-1536)]/48^4 + = 565248/5308416 = 23/216. (1) +``` + +For distinct s,t,u the two A tables have only the identity in common. +The group-coefficient Frobenius inner product consequently gives + +```text +tr(P_s P_t P_s P_u)/N = 8*192^2/48^4 = 1/18. (2) +``` + +The lower moments retain #2104/#2181's argument. Relative routes are +distinct, so `tr(P_s P_t)/N=1536/48^2=2/3`. In a distinct-stage triple, +the identity condition is +`g_1(p)g_1(q)=g_2(r)g_2(q)`. The checked product intersection and identity +fibres force p=q=r. Thus the triple trace is `96*4^3/48^3=1/18`. +Cyclic invariance and transpose cover its six orderings. + +Cyclic removal of adjacent repeated projections partitions all 81 +stage words of length four as follows. These are traces, so the first +and last letters also count as adjacent. + +| Reduced type | Count | Trace divided by N | +|---|---:|---:| +| one stage | 3 | 8 | +| two adjacent stages | 36 | 2/3 | +| three distinct stages | 24 | 1/18 | +| alternating `s,t,s,t` | 6 | 23/216 | +| repeated-stage `s,t,s,u`, all three stages used | 12 | 1/18 | + +Their sum is `1823/36`. The complete first four moments are + +```text +(tr T, tr T^2, tr T^3, tr T^4)/N = (24,28,109/3,1823/36). (3) +``` + +### Separate contraction oracle + +[oracle.py](oracle.py) does not assume the collision classification, +use the primary binary multiplication, or reduce cyclic stage words. +It shares only the credited source binder. It converts routes to binary +row matrices and explicitly forms every group coefficient of the nine +blocks of `C^2`, where `C=(B_s B_t*)_(s,t)` is the 24N-dimensional +block Gram matrix. The two rank-one factors multiply as +`r_p(r_p^T r_q)r_q^T`; equal-stage blocks are `48I`. + +Because C is self-adjoint, coefficient Frobenius contractions compute +`tr(C^2)`, `tr(C^3)=` and `tr(C^4)=||C^2||_F^2`. Dividing by +48^k gives (3), since C/48 and T have the same nonzero eigenvalues. +For the fourth trace each diagonal block contributes 1187/108 and each +off-diagonal block 53/18. Their total is again 1823/36. This is a second +implementation and method, not an independent human review. + +## 3. Rational spectral certificate + +For every real t, + +```text +p(t) = 1-(1-81t/40+9t^2/10)^2 <= 1, p(0)=0 + = (81/20)t-(9441/1600)t^2+(729/200)t^3-(81/100)t^4. +``` + +Apply this inequality to each nonzero eigenvalue of T. The zero +eigenvalues contribute zero. Equation (3) gives + +```text +rank T >= tr p(T) = (117/5)N. (4) +``` + +No floating-point extremization is used for acceptance. The coefficients +come from the exact 2x2 moment system +`[[28,109/3],[109/3,1823/36]] [a,b]^T=[24,28]^T`, giving +`a=81/40,b=-9/10`, then `p=1-(1-a t-b t^2)^2`. The checker verifies the +polynomial identity and the rational trace evaluation exactly. + +## 4. Inherited selected-input implication + +This is the joint-defect argument of this account's +[PR #2153](https://github.com/CrocSwap/integer-mult-bounds/pull/2153), +restated to make the contract explicit. For h in `V=ker B1`, use only +pair 0 and set + +```text +X_U=h, Y_U=0, +X_A=-P_(0,A)B0h-P_(2,A)B2h, Y_A=-X_A, +X_T=P_(0,T)ell_(0,A)P_(2,A)B2h, Y_T=-X_T. +``` + +All other banks and helpers are zero. The original selected defect +`J(h)=(X_A,X_T)` determines and is determined by `(B0h,B2h)`: + +```text +B0h=-ell_(0,A)X_A-ell_(0,T)X_T, +B2h=ell_(2,A)P_(0,A)ell_(0,T)X_T. +``` + +The two-sided selected inverse relations preserve the displayed order. +Consequently + +```text +dim J(V)=rank([B0;B1;B2])-rank B1 >= ceil(77N/5). (5) +``` + +The original QQ16 witness establishes, for every such h, zero F0 query +and zero selected state after B1, with only Y_(0,U)=h remaining. Its +retained ordinary tail moves h into the former-Y hole. The allowed old +observations—selected values after B1 and later selected-only descendants, +completed-X descendants, and all five forward histories—are zero. +An independently saved transient F0 A value or a read of the former-Y +hole is additional information, not part of those old observations. +This trajectory and native-frame interpretation are inherited from the +pinned witness and rational review, not newly replayed by this package. + +If C is the restriction of an added record to V and rank C<=d, then +`dim J(ker C)>=dim J(V)-d`: a complement of ker C has dimension at most d +and its J-image adds at most d dimensions. Combining with (5) proves +the stated residual. Positive residual gives two inputs with identical +records and different required selected outputs; no decoder can +separate them. Common dirty baselines and fixed affine offsets cancel +when comparing the two executions. + +A q-coordinate record with one rational scalar per owner has capacity +at most qN. Every integer q<=15 fails. The inherited sixteen-coordinate +record `(B0 X_U,B2 X_U)` recovers this particular erased family, so its +integer-coordinate threshold is sixteen. This does not compute its +exact defect dimension, which lies between `ceil(77N/5)` and 16N. + +The lower bound also applies when all post-B1 selected values are +granted, as in [PR #2174](https://github.com/CrocSwap/integer-mult-bounds/pull/2174). +It therefore matches that PR's sixteen-coordinate logical upper bound +for pair 0 **under its explicit recorded-cut premise**. Its full-input +recovery proof is credited, not rerun or promoted to a final-only +controller here. Sixteen information coordinates are not sixteen paid +recursive ranks. + +## Verification limits + +The finite route facts, all four moments, polynomial identity and +rejection controls are executed. The spectral and capacity arguments +are written proofs. The two implementations share the source binder; +no formal kernel or independent human review is claimed. No full QQ16 +native replay, selected frontier cold replay, final-only controller, +compact actual-cover null vector, precision bound, chronological hosting, +physical record implementation or completed supplier bill was checked. +All source packages and the selected record remain unchanged. + +## Open next questions + +1. **Can an actual final-only controller recover the post-B1 selected + cut values used by #2174?** Trace one literal selected program and + express its cut values in its final observations. This is the missing + access premise; the integer width gap for the erased family no longer + motivates more moment searches. +2. **What is the completed native bill for the sixteen-coordinate + record and #2174's decoder?** Start by jointly pricing both pre-F0 + ordinary reads and the completed-X B2 read in their actual endpoint + frames. Record retention, dirty restoration, hosting, tape and + precision remain blockers. Stop construction if even the favorable + complete bill misses its target. + +## Credit + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. +New material is Apache-2.0. + +Ali Romman and the contributors in [joint-query/NOTICE.md](../joint-query/NOTICE.md) +supplied PR #1969's maps, ordered sections, actual routes and witness +(head `a6e6ad3936f67b8f63b5b68c5e75d540610a65e7`). Ross Richardson's +PR #2104 (`4bdc574da394a39f955e8cf4637075649c43a632`) supplied the +rank-moment method. Nick Petalas's PR #2181 +(`e18ca76987f5945c6a4b5b6bebbe73cdab3c4561`) supplied the third moment, +the polynomial approach and the source binder adapted here. This +account's PR #2153 (`5646398dcdc01769df83b939c6b3eb5ecb4d5ebd`) supplied +the joint A/T defect transfer; PR #2174 +(`f79470a7931f3943360c10d15b428e0e4e479c22`) supplies the distinct +recorded-cut recovery upper bound. Cinna Davis's #2079/#2122 and Adam +Gall's #2086/#2093 are adjacent observation obstructions. Rohan Arun, +Jeremy Kothe and the retained geometry/native/hosting lineage keep +their existing attribution. The new contribution is the fourth moment, +its separate contraction oracle, and the stronger transcript bound. diff --git a/research/qq16-fourth-moment-capacity/RESULT.json b/research/qq16-fourth-moment-capacity/RESULT.json new file mode 100644 index 0000000000..1ee25a8786 --- /dev/null +++ b/research/qq16-fourth-moment-capacity/RESULT.json @@ -0,0 +1,107 @@ +{ + "status": "PASS_QQ16_FOURTH_MOMENT_CAPACITY", + "pair_census": { + "01": { + "ordered_pairs": 9216, + "distinct_products": 9121, + "identity_fibre": 96, + "largest_nonidentity_fibre": 1, + "sha256": "36ae847b5477e3c6cd29a942351c442ebb076991f40d85166077a950c8b01764" + }, + "02": { + "ordered_pairs": 9216, + "distinct_products": 9121, + "identity_fibre": 96, + "largest_nonidentity_fibre": 1, + "sha256": "cde66a6b4797ef97bac6d0465415bbb13027d3e53f3730f526c1e14e732c46d5" + }, + "10": { + "ordered_pairs": 9216, + "distinct_products": 9121, + "identity_fibre": 96, + "largest_nonidentity_fibre": 1, + "sha256": "36ae847b5477e3c6cd29a942351c442ebb076991f40d85166077a950c8b01764" + }, + "12": { + "ordered_pairs": 9216, + "distinct_products": 9121, + "identity_fibre": 96, + "largest_nonidentity_fibre": 1, + "sha256": "cde66a6b4797ef97bac6d0465415bbb13027d3e53f3730f526c1e14e732c46d5" + }, + "20": { + "ordered_pairs": 9216, + "distinct_products": 9121, + "identity_fibre": 96, + "largest_nonidentity_fibre": 1, + "sha256": "cde66a6b4797ef97bac6d0465415bbb13027d3e53f3730f526c1e14e732c46d5" + }, + "21": { + "ordered_pairs": 9216, + "distinct_products": 9121, + "identity_fibre": 96, + "largest_nonidentity_fibre": 1, + "sha256": "36ae847b5477e3c6cd29a942351c442ebb076991f40d85166077a950c8b01764" + } + }, + "cross_stage_intersections": { + "0": 1, + "1": 1, + "2": 1 + }, + "trace_calculation": { + "gram_square_sum": 18432, + "identity_coefficient_diagonal": 192, + "identity_coefficient_square_trace": 294912, + "off_identity_square_trace": 270336, + "alternating_four_trace": "23/216", + "mixed_four_trace": "1/18", + "cyclic_stage_word_counts": [ + { + "single": 3 + }, + { + "pair": 6, + "single": 3 + }, + { + "pair": 18, + "single": 3, + "triple": 6 + }, + { + "alternating": 6, + "mixed": 12, + "pair": 36, + "single": 3, + "triple": 24 + } + ] + }, + "moments_per_owner": [ + "24", + "28", + "109/3", + "1823/36" + ], + "spectral_bound": { + "residual_polynomial": [ + "1", + "-81/40", + "9/10" + ], + "rank_polynomial": [ + "0", + "81/20", + "-9441/1600", + "729/200", + "-81/100" + ], + "stacked_rank_lower_per_owner": "117/5", + "selected_defect_lower_per_owner": "77/5", + "width_fourteen_residual_lower_per_owner": "7/5", + "width_fifteen_residual_lower_per_owner": "2/5", + "necessary_integer_record_width": 16 + }, + "scope": "Regular-owner information dimension under the inherited fixed-pair erased-family observation contract; no physical invoice or new kappa." +} diff --git a/research/qq16-fourth-moment-capacity/SOURCES.json b/research/qq16-fourth-moment-capacity/SOURCES.json new file mode 100644 index 0000000000..cb2e23e554 --- /dev/null +++ b/research/qq16-fourth-moment-capacity/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/joint-query/certificate.json.gz", + "usage": "input", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + }, + { + "path": "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "usage": "input", + "git_blob": "a6805c58f23132f9420efebf90f5b7e863c2e179", + "sha256": "9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75" + }, + { + "path": "research/joint-query/evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.md", + "usage": "input", + "git_blob": "c6ecf75654a084a9cc001bd62663f341976bae7a", + "sha256": "9a06ff40830ef80d3566fce77c78639cb64d519d487a0a7f57d543c3146e2c49" + }, + { + "path": "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json", + "usage": "input", + "git_blob": "5082d791d0b993492cbc5bf61ac3b69e82c96f3f", + "sha256": "e35e5868a1322e406191079c0675975b139692ba50b1e2e5fb8a40b6480519f4" + }, + { + "path": "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "usage": "input", + "git_blob": "307650f45e37c28d14fe913958efa4fb429242b7", + "sha256": "52f2ee565320f05282c637aa79eee100606c24240b1b5866f0c8d62e7913c9fc" + } + ] +} diff --git a/research/qq16-fourth-moment-capacity/TASK.json b/research/qq16-fourth-moment-capacity/TASK.json new file mode 100644 index 0000000000..94aa411856 --- /dev/null +++ b/research/qq16-fourth-moment-capacity/TASK.json @@ -0,0 +1,154 @@ +{ + "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": "changed", + "actual_scope": "Exact fourth spectral moment of the actual three-query QQ16 operator, a rational quartic rank certificate, and exclusion of all read-only rational-linear records of at most fifteen scalars per regular-cover owner under the inherited fixed F0/B_1_2 erasure contract.", + "scope_change_reason": "Take the released PR2181 higher-moment handoff in discussion #2074: strengthen a necessary information bound for a wider retained record instead of constructing the catalogue card's paid observation and complete controller.", + "bottleneck_link": "The native QQ16 local words lack a completed query-restoration controller. Closing the 14/15-coordinate information gap focuses follow-up on the already known sixteen-coordinate cut decoder and its missing final-only access and paid implementation.", + "budget_minutes": 60, + "stop_rule": "Stop after exact fourth-moment/capacity evidence and two-method verification. No additional moment search or physical construction; hand off the final-only access and complete invoice obligations.", + "outcome": "completed", + "evidence": "RESULT.json; README.md written scoped proof; verify.py full 55296-product census and rational polynomial; oracle.py separate row-matrix block-Gram contractions; tests.py semantic and artifact controls.", + "author": "commdata2338", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematics, implementation, review and writing. No independent human review or formal-kernel proof is claimed.", + "open_questions": [ + { + "question": "Does one actual final-only QQ16 controller determine the post-B1 selected cut values used by PR2174?", + "why_it_matters": "The sixteen-coordinate logical upper bound grants those values; the new lower bound rules out smaller integer record widths under that same granted-cut contract.", + "first_step": "Trace one literal selected controller and test recovery of its post-B1 p_A, p_T and d_A from final observations.", + "blocked_by": "No proved final-to-cut observation map or legal record retention schedule." + }, + { + "question": "What is the fully charged native bill of the sixteen-coordinate record and its decoder?", + "why_it_matters": "Information sufficiency is not a legal recursive supplier or favorable moment.", + "first_step": "Jointly bind and price both initial ordinary reads and the decoder B2 read using actual endpoint frames.", + "blocked_by": "Final-only access, record retention, dirty restoration, hosting, tape and precision remain unpriced." + } + ], + "selection": { + "seed": "65b001ccb2c98c18607f8043d2993ce6", + "track": "recursive-interfaces", + "task_id": "joint-query-controller", + "scope_key": "22e535909f1d243e7553", + "refined_scope_key": "QQ16-fixed-F0-B12/three-query-fourth-moment/quartic-transcript-capacity", + "reason": "Second suggested card, refined to PR2181 released central handoff." + }, + "predecessors": [ + { + "pr": 1969, + "head": "a6e6ad3936f67b8f63b5b68c5e75d540610a65e7", + "credit": "Ali Romman and retained joint-query contributors", + "use": "Maps, routes, selected sections, original erased witness and native interpretation; retained main sources." + }, + { + "pr": 2104, + "head": "4bdc574da394a39f955e8cf4637075649c43a632", + "credit": "Ross Richardson", + "use": "Rank-moment method; no executable imported." + }, + { + "pr": 2153, + "head": "5646398dcdc01769df83b939c6b3eb5ecb4d5ebd", + "credit": "commdata2338", + "use": "Joint A/T defect identity and arbitrary-record restriction; written argument restated." + }, + { + "pr": 2181, + "head": "e18ca76987f5945c6a4b5b6bebbe73cdab3c4561", + "credit": "Nick Petalas", + "use": "Third moment, spectral-polynomial approach and adapted source extraction/chart checks.", + "adapted_file": "research/qq16-third-moment-capacity/verify.py", + "adapted_file_sha256": "c208e8ddb7e4f85074a060db0280b98f650d48d8ce13e33dd1376f7167d4c099" + }, + { + "pr": 2174, + "head": "f79470a7931f3943360c10d15b428e0e4e479c22", + "credit": "commdata2338", + "use": "Adjacent sixteen-coordinate recorded-cut logical upper bound; not rerun and not needed for the lower bound." + } + ], + "unrun_obligations": [ + "Independent human review and formal-kernel proof", + "Full QQ16 native words and inherited erased-family tail replay", + "Final-only controller access to post-B1 selected values", + "Native reads, restoration, hosting, precision and tape bills", + "Full selected frontier cold replay and supplier admission", + "Compact actual-cover null-vector construction" + ], + "upstream_checkpoints": [ + { + "commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "utc": "2026-10-14T22:32:00Z", + "change": "Entry fetch: current main; no source migration." + }, + { + "commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "utc": "2026-10-14T22:46:08Z", + "change": "Pre-submission fetch: no changes to main, guidance, selected record or scientific inputs. Retain the original base." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2074#discussioncomment-18935517", + "overlap": { + "entry": { + "open_prs_fetched_at": "2026-10-14T22:27:37.725500Z", + "open_prs": 428, + "discussions_fetched_at": "2026-10-14T22:30:29.364283Z", + "discussions": 862 + }, + "final": { + "open_prs_fetched_at": "2026-10-14T22:41:55.402359Z", + "open_prs": 429, + "discussions_fetched_at": "2026-10-14T22:44:37.402621Z", + "discussions": 867 + }, + "complete_pagination": true, + "limitation": "Cached snapshot; later changes and unindexed code may be absent. Search is not a novelty certificate.", + "nearest": "PR2181 third moment; PR2153 defect; PR2174 cut recovery; own fourth-moment claim. No competing fourth-moment result found." + } +} diff --git a/research/qq16-fourth-moment-capacity/VERIFY.json b/research/qq16-fourth-moment-capacity/VERIFY.json new file mode 100644 index 0000000000..92d753529f --- /dev/null +++ b/research/qq16-fourth-moment-capacity/VERIFY.json @@ -0,0 +1,57 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/joint-query/certificate.json.gz", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "research/joint-query/evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All six exact pair-product tables; source pins; fourth moment; rational polynomial; complete typed receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/oracle.py" + ], + "timeout_seconds": 120, + "checks": "Separate row-matrix group algebra; all nine block-Gram contractions through fourth moment." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/tests.py" + ], + "timeout_seconds": 120, + "checks": "Eight semantic/artifact test groups, including source binding, pair collisions, polynomial, reversed accumulation and corrupt receipts." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/tests.py" + ], + "timeout_seconds": 120, + "checks": "The same failure controls with Python assertions disabled." + } + ] +} diff --git a/research/qq16-fourth-moment-capacity/oracle.py b/research/qq16-fourth-moment-capacity/oracle.py new file mode 100644 index 0000000000..7ddcaf8fc3 --- /dev/null +++ b/research/qq16-fourth-moment-capacity/oracle.py @@ -0,0 +1,107 @@ +#!/usr/bin/env python3 +"""Separate block-Gram/Frobenius calculation of all four moments. + +Only source extraction is shared with verify.py. This implementation uses +row matrices and direct coefficient contractions, with no collision-pattern +assumption or cyclic stage-word reduction. Apache-2.0. +Prepared for commdata2338, with substantial OpenAI Codex assistance. +""" +import argparse +from fractions import Fraction as Q +import importlib.util +from itertools import product +from pathlib import Path + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("qq16_source_oracle", HERE / "source.py") +src = importlib.util.module_from_spec(spec) +spec.loader.exec_module(src) + + +def rows(columns): + n = len(columns) + return tuple(sum(((columns[j] >> i) & 1) << j for j in range(n)) + for i in range(n)) + + +def row_product(A, B): + output = [] + for a in A: + value = 0 + for j, b in enumerate(B): + if (a >> j) & 1: + value ^= b + output.append(value) + return tuple(output) + + +def add_outer(table, route, coefficient, a, b): + if coefficient: + matrix = table.setdefault(route, [0]*64) + for i, x in enumerate(a): + for j, y in enumerate(b): + matrix[8*i+j] += coefficient*x*y + + +def calculate(R, routes, stage_order=(0, 1, 2)): + U = src.U + c = {p: tuple(R[i][p] for i in range(8)) for p in U} + dots = {(p, q): sum(x*y for x, y in zip(c[p], c[q])) for p, q in product(U, repeat=2)} + gs = [[rows(g) for g in stage] for stage in routes] + identity = tuple(1 << i for i in range(25)) + h = {(s, t): {p: row_product(gs[s][p], gs[t][p]) for p in U} + for s, t in product(range(3), repeat=2) if s != t} + m2 = m3 = m4 = 0 + blocks = {} + for s, u in product(range(3), repeat=2): + # C is the block matrix (B_s B_u*), normalized by 48 only at the end. + C = {} + if s == u: + C[identity] = [48*int(i == j) for i in range(8) for j in range(8)] + else: + for p in U: + add_outer(C, h[s, u][p], 1, c[p], c[p]) + C2 = {} + for t in stage_order: + if t == s or t == u: + if s == u: + out = C2.setdefault(identity, [0]*64) + for i in range(8): + out[9*i] += 2304 + else: + for g, matrix in C.items(): + out = C2.setdefault(g, [0]*64) + for i, x in enumerate(matrix): + out[i] += 48*x + else: + for p, q in product(U, repeat=2): + if dots[p, q]: + g = row_product(h[s, t][p], h[t, u][q]) + add_outer(C2, g, dots[p, q], c[p], c[q]) + b2 = sum(sum(x*x for x in matrix) for matrix in C.values()) + b3 = sum(sum(x*y for x, y in zip(C[g], C2[g])) + for g in C.keys() & C2.keys()) + b4 = sum(sum(x*x for x in matrix) for matrix in C2.values()) + m2 += b2 + m3 += b3 + m4 += b4 + blocks[f"{s}{u}"] = str(Q(b4, 48**4)) + return [Q(24), Q(m2, 48**2), Q(m3, 48**3), Q(m4, 48**4)], blocks + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--repo", type=Path, default=HERE.parents[1]) + args = parser.parse_args() + R, routes = src.packet_data(src.load_packet(args.repo)) + src.check_grams(R) + src.check_swap_charts(routes) + moments, blocks = calculate(R, routes) + src.need(moments == [Q(24), Q(28), Q(109, 3), Q(1823, 36)], "block-Gram moments") + src.need(blocks == {f"{s}{t}": str(Q(1187, 108) if s == t else Q(53, 18)) + for s, t in product(range(3), repeat=2)}, "block-Gram fourth traces") + print("PASS_QQ16_BLOCK_GRAM_ORACLE moments=24,28,109/3,1823/36 blocks=9") + + +if __name__ == "__main__": + main() diff --git a/research/qq16-fourth-moment-capacity/source.py b/research/qq16-fourth-moment-capacity/source.py new file mode 100644 index 0000000000..3ee32da466 --- /dev/null +++ b/research/qq16-fourth-moment-capacity/source.py @@ -0,0 +1,158 @@ +#!/usr/bin/env python3 +"""Shared QQ16 source binder; Apache-2.0. + +Adapted from Nick Petalas's PR2181 verify.py at + e18ca76987f5945c6a4b5b6bebbe73cdab3c4561. +The source extraction, Gram checks and chart-swap checks retain his credit. +Prepared for commdata2338, with substantial OpenAI Codex assistance. +""" +from fractions import Fraction as Q +import gzip +import hashlib +import io +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PACKET = "research/joint-query/certificate.json.gz" +PINS = { + 'research/joint-query/evidence/JOINT-QUERY-TRANSFER.md': '9e13e73ebf3192a6548798c2f1d13bd4d83957e8db0dc34de12b1a5311a52a75', + PACKET: "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md": + "52f2ee565320f05282c637aa79eee100606c24240b1b5866f0c8d62e7913c9fc", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json": + "e35e5868a1322e406191079c0675975b139692ba50b1e2e5fb8a40b6480519f4", + "research/joint-query/evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.md": + "9a06ff40830ef80d3566fce77c78639cb64d519d487a0a7f57d543c3146e2c49", +} +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) +IDENTITY = tuple(1 << i for i in range(25)) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def load_packet(repo): + raw_packet = None + for name, expected in PINS.items(): + path = repo / name + need(path.is_file() and path.stat().st_size <= 1_048_576, + "source size: " + name) + raw = path.read_bytes() + need(hashlib.sha256(raw).hexdigest() == expected, "source pin: " + name) + if name == PACKET: + raw_packet = raw + need(raw_packet is not None, "missing packet") + with gzip.GzipFile(fileobj=io.BytesIO(raw_packet)) as stream: + payload = stream.read(16_777_217) + need(len(payload) <= 16_777_216, "decompressed packet size") + return json.loads(payload) + + +def apply(columns, vector): + result = 0 + # Every vector is in the validated 25-axis space. + for _ in range(25): + if not vector: + return result + bit = vector & -vector + result ^= columns[bit.bit_length() - 1] + vector ^= bit + need(vector == 0, "binary vector bound") + return result + + +def compose(left, right): + return tuple(apply(left, c) for c in right) + + +def route(packet, event): + need(event[0] == "cover_map", "cover map event") + columns = packet["map_registry"][event[2]]["owner_right_matrix_columns"] + need(len(columns) == 73 and all(type(c) is int for c in columns), + "73 integer route columns") + need(all(0 < c < 1 << 25 for c in columns[:25]), "active route axes") + need(columns[25:] == [1 << i for i in range(25, 73)], + "route must fix all 48 spectator axes") + return tuple(columns[:25]) + + +def packet_data(packet): + need((tuple(packet["A_ports"]), tuple(packet["T_ports"]), + tuple(packet["U_ports"])) == (A, T, U), "selected partition") + need(len(packet["R_rows"]) == 8, "eight query rows") + R = [[Q(row.get(str(p), 0)) for p in range(112)] + for row in packet["R_rows"]] + need(all(x.denominator == 1 for row in R for x in row), "integer query") + R = [[int(x) for x in row] for row in R] + routes = [[IDENTITY] * 112] + for stage in (1, 2): + word = packet["programs"][f"F_{stage}"] + need(word[113][:2] == ["cover_sweep", "X_A_fused_query"], + "forward alignment cut") + events = word[1:113] + need([e[1] for e in events] == [["L", p] for p in range(112)], + "forward port order") + routes.append([route(packet, e) for e in events]) + need(packet["programs"]["F_0"][1][:2] == + ["cover_sweep", "X_A_fused_query"], "stage-zero identity cut") + word = packet["programs"]["B_1_2"] + need(len(word) <= 40_000, "backward event bound") + future = next(i for i, e in enumerate(word) + if e[:2] == ["cover_sweep", "future_E_t"]) + current = next(i for i, e in enumerate(word) + if e[:2] == ["cover_sweep", "Y_U_from_X_T"]) + for stage, events in ((2, word[future - 112:future]), + (1, word[current - 120:current - 8])): + need([e[1] for e in events] == [["L", 112+p] for p in range(112)], + "backward port order") + need([route(packet, e) for e in events] == routes[stage], + "forward/backward route binding") + return R, routes + + +def dot(left, right): + return sum(x*y for x, y in zip(left, right)) + + +def check_grams(R): + for ports, scale in ((U, 48), (A, 4), (T, 4)): + matrix = [[sum(R[i][p]*R[j][p] for p in ports) + for j in range(8)] for i in range(8)] + need(matrix == [[scale*int(i == j) for j in range(8)] + for i in range(8)], "query Gram") + need([sum(R[i][p]**2 for i in range(8)) for p in U] == [4]*96, + "ordinary column norms") + + +def check_swap_charts(routes): + """A separate certificate: chart swaps and disjoint external axes.""" + charts = [] + for p in U: + chart = tuple(routes[1][p][9+i] for i in range(8)) + need(all(0 < c < 512 for c in chart), "nine-axis chart") + need(all((x & y).bit_count() % 2 == int(i == j) + for i, x in enumerate(chart) for j, y in enumerate(chart)), + "orthonormal chart") + for stage, start in ((1, 9), (2, 17)): + need(tuple(routes[stage][p][start+i] for i in range(8)) == chart, + "common stage chart") + normals = tuple(chart[i] ^ (1 << (start+i)) for i in range(8)) + rebuilt = [] + for axis in range(25): + x, out = 1 << axis, 1 << axis + for n in normals: + if (x & n).bit_count() % 2: + out ^= n + rebuilt.append(out) + need(tuple(rebuilt) == routes[stage][p], "literal chart swap") + need(compose(routes[stage][p], routes[stage][p]) == IDENTITY, + "route involution") + charts.append(chart) + need(len(set(charts)) == 96, "distinct ordinary charts") + return len(set(charts)) diff --git a/research/qq16-fourth-moment-capacity/tests.py b/research/qq16-fourth-moment-capacity/tests.py new file mode 100644 index 0000000000..4061115e82 --- /dev/null +++ b/research/qq16-fourth-moment-capacity/tests.py @@ -0,0 +1,170 @@ +#!/usr/bin/env python3 +"""Semantic and artifact controls for the fourth-moment certificate. + +Prepared for commdata2338, with substantial OpenAI Codex assistance. +Apache-2.0. +""" +from copy import deepcopy +from fractions import Fraction as Q +import importlib.util +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def load(name): + spec = importlib.util.spec_from_file_location('qq16_test_'+name, HERE/(name+'.py')) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +v, oracle = load('verify'), load('oracle') +src = v.src + + +class Controls(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.packet = src.load_packet(ROOT) + cls.R, cls.routes = src.packet_data(cls.packet) + cls.receipt = json.loads((HERE/'RESULT.json').read_text()) + + def test_gram_and_chart_mutants(self): + bad = deepcopy(self.R) + bad[0][src.U[0]] += 1 + with self.assertRaisesRegex(ValueError, 'query Gram'): + src.check_grams(bad) + routes = deepcopy(self.routes) + for stage in (1, 2): + routes[stage][src.U[1]] = routes[stage][src.U[0]] + with self.assertRaisesRegex(ValueError, 'distinct ordinary charts'): + src.check_swap_charts(routes) + + def test_product_hypotheses(self): + with self.assertRaises(ValueError): + v.pair_census([self.routes[0], self.routes[1], self.routes[1]]) + # Distinct involutions alone do not imply singleton product fibres. + ident = src.IDENTITY + a, b = list(ident), list(ident) + a[1] ^= 1 + b[3] ^= 4 + a, b = tuple(a), tuple(b) + four = [ident, a, b, src.compose(a, b)] + with self.assertRaisesRegex(ValueError, 'nonidentity pair collision'): + v.pair_census([[ident]*4, four, four], ports=tuple(range(4))) + + def test_source_semantic_binding(self): + wrong = deepcopy(self.packet) + wrong['A_ports'][0] = wrong['U_ports'][0] + with self.assertRaisesRegex(ValueError, 'selected partition'): + src.packet_data(wrong) + wrong = deepcopy(self.packet) + event = wrong['programs']['F_1'][1] + wrong['map_registry'][event[2]]['owner_right_matrix_columns'][72] ^= 1 + with self.assertRaisesRegex(ValueError, 'spectator axes'): + src.packet_data(wrong) + wrong = deepcopy(self.packet) + word = wrong['programs']['B_1_2'] + cut = next(i for i,e in enumerate(word) if e[:2] == ['cover_sweep','future_E_t']) + # Keep event shape and port, change its chart to the other stage. + word[cut-112][2] = wrong['programs']['F_1'][1][2] + with self.assertRaisesRegex(ValueError, 'forward/backward route binding'): + src.packet_data(wrong) + + def test_noncommuting_multiplication_orientations(self): + a, b = self.routes[1][src.U[0]], self.routes[2][src.U[1]] + self.assertNotEqual(src.compose(a, b), src.compose(b, a)) + self.assertEqual(oracle.rows(src.compose(a, b)), + oracle.row_product(oracle.rows(a), oracle.rows(b))) + self.assertEqual(src.compose(a, a), src.IDENTITY) + # A third direct basis-action implementation checks the operator order. + for axis in range(25): + x = b[axis] + expected = 0 + for k in range(25): + if (x >> k) & 1: + expected ^= a[k] + self.assertEqual(src.compose(a, b)[axis], expected) + + def test_polynomial_and_capacity(self): + data = self.receipt['spectral_bound'] + p, q = [Q(x) for x in data['rank_polynomial']], [Q(x) for x in data['residual_polynomial']] + v.check_polynomial(p, q) + for index in (0, 2, 4): + bad = p.copy() + bad[index] += Q(1, 100) + with self.assertRaisesRegex(ValueError, 'polynomial square identity'): + v.check_polynomial(bad, q) + # The exact polynomial controls a small diagonal positive operator, + # including zero eigenvalues; counting ambient dimension is insufficient. + values = [Q(0), Q(0), Q(1, 2), Q(1), Q(3)] + evaluation = sum(sum(c*t**k for k,c in enumerate(p)) for t in values) + self.assertLessEqual(evaluation, 3) + moments = [Q(x) for x in self.receipt['moments_per_owner']] + self.assertEqual(sum(c*m for c,m in zip(p[1:], moments)), Q(117, 5)) + self.assertEqual(Q(data['selected_defect_lower_per_owner'])-15, Q(2, 5)) + self.assertGreaterEqual(16, Q(data['selected_defect_lower_per_owner'])) + altered = moments.copy() + altered[-1] -= Q(1, 36) + with self.assertRaisesRegex(ValueError, 'quartic rank bound'): + v.spectral_bound(altered) + + def test_direct_oracle_reordered_accumulation(self): + moments, blocks = oracle.calculate(self.R, self.routes, stage_order=(2, 1, 0)) + self.assertEqual(moments, [Q(24), Q(28), Q(109, 3), Q(1823, 36)]) + self.assertEqual(blocks, {f'{s}{t}': str(Q(1187, 108) if s == t else Q(53, 18)) + for s in range(3) for t in range(3)}) + + def test_receipt_type_and_duplicate_rejection(self): + with tempfile.TemporaryDirectory(prefix='qq16-fourth-') as directory: + path = Path(directory)/'receipt.json' + wrong = deepcopy(self.receipt) + wrong['cross_stage_intersections']['0'] = True + path.write_text(json.dumps(wrong)) + # Python's ordinary equality would accept this proof-field type change. + self.assertEqual(wrong, self.receipt) + self.assertNotEqual(v.canonical(v.read_receipt(path)), v.canonical(self.receipt)) + proc = subprocess.run([sys.executable, '-I', '-B', str(HERE/'verify.py'), + '--receipt', str(path)], capture_output=True, text=True) + self.assertNotEqual(proc.returncode, 0) + self.assertIn('receipt mismatch', proc.stderr) + path.write_text('{"x":1,"x":2}') + with self.assertRaisesRegex(ValueError, 'duplicate receipt key'): + v.read_receipt(path) + + def test_source_and_numeric_receipt_corruption(self): + with tempfile.TemporaryDirectory(prefix='qq16-fourth-') as directory: + root = Path(directory) + for name in src.PINS: + target = root/name + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT/name, target) + src.load_packet(root) + packet = root/src.PACKET + content = bytearray(packet.read_bytes()) + content[-1] ^= 1 + packet.write_bytes(content) + proc = subprocess.run([sys.executable, '-I', '-B', str(HERE/'verify.py'), + '--repo', str(root)], capture_output=True, text=True) + self.assertNotEqual(proc.returncode, 0) + self.assertIn('source pin', proc.stderr) + wrong = deepcopy(self.receipt) + wrong['moments_per_owner'][-1] = '1822/36' + path = root/'receipt.json' + path.write_text(json.dumps(wrong)) + proc = subprocess.run([sys.executable, '-I', '-B', str(HERE/'verify.py'), + '--receipt', str(path)], capture_output=True, text=True) + self.assertNotEqual(proc.returncode, 0) + self.assertIn('receipt mismatch', proc.stderr) + + +if __name__ == '__main__': + unittest.main(verbosity=2) diff --git a/research/qq16-fourth-moment-capacity/verify.py b/research/qq16-fourth-moment-capacity/verify.py new file mode 100644 index 0000000000..653297af1d --- /dev/null +++ b/research/qq16-fourth-moment-capacity/verify.py @@ -0,0 +1,197 @@ +#!/usr/bin/env python3 +"""Exact QQ16 fourth moment and transcript bound; Apache-2.0. + +Prepared for commdata2338, with substantial OpenAI Codex assistance. +See README.md for construction and method predecessors. +""" +import argparse +from collections import Counter +from fractions import Fraction as Q +import hashlib +import importlib.util +from itertools import product +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("qq16_source", HERE / "source.py") +src = importlib.util.module_from_spec(spec) +spec.loader.exec_module(src) +need = src.need +MARKER = "PASS_QQ16_FOURTH_MOMENT_CAPACITY" + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False) + + +def read_receipt(path): + def unique(pairs): + result = {} + for key, value in pairs: + need(key not in result, "duplicate receipt key") + result[key] = value + return result + return json.loads(path.read_text(), object_pairs_hook=unique) + + +def check_polynomial(polynomial, residual): + need(len(polynomial) == 5 and len(residual) == 3 and residual[0] == 1, + "polynomial shape") + square = [sum(residual[i]*residual[j] + for i in range(3) for j in range(3) if i+j == k) + for k in range(5)] + need(polynomial == [Q(int(k == 0))-square[k] for k in range(5)], + "polynomial square identity") + need(polynomial[0] == 0, "zero constant polynomial") + + +def pair_census(routes, ports=src.U): + """All pairs, including zero scalar coefficients, on all active axes.""" + tables, receipt = {}, {} + for s, t in product(range(3), repeat=2): + if s == t: + continue + h = {p: src.compose(routes[s][p], routes[t][p]) for p in ports} + inv = {p: src.compose(routes[t][p], routes[s][p]) for p in ports} + need(len(set(h.values())) == len(ports), "relative route distinctness") + table = {} + for p, q in product(ports, repeat=2): + key = src.compose(h[p], inv[q]) + table.setdefault(key, []).append((p, q)) + need(table.get(src.IDENTITY) == [(p, p) for p in ports], + "diagonal identity fibre") + need(all(len(v) == 1 for g, v in table.items() if g != src.IDENTITY), + "nonidentity pair collision") + need(len(table) == len(ports)**2-len(ports)+1, "pair coverage") + tables[s, t] = table + payload = [[list(g), v] for g, v in sorted(table.items())] + receipt[f"{s}{t}"] = { + "ordered_pairs": len(ports)**2, + "distinct_products": len(table), + "identity_fibre": len(table[src.IDENTITY]), + "largest_nonidentity_fibre": max(len(v) for g, v in table.items() + if g != src.IDENTITY), + "sha256": hashlib.sha256(json.dumps(payload, separators=(",", ":")) + .encode()).hexdigest(), + } + intersections = {} + for s in range(3): + t, u = [i for i in range(3) if i != s] + common = tables[s, t].keys() & tables[s, u].keys() + need(common == {src.IDENTITY}, "cross-stage product intersection") + intersections[str(s)] = len(common) + return receipt, intersections + + +def cyclic_reduce(word): + word = list(word) + changed = True + while changed and len(word) > 1: + changed = False + for i in range(len(word)): + if word[i] == word[(i+1) % len(word)]: + del word[i] + changed = True + break + return tuple(word) + + +def moments_from_columns(R): + c = [tuple(R[i][p] for i in range(8)) for p in src.U] + dots = [[src.dot(a, b) for b in c] for a in c] + square_sum = sum(x*x for row in dots for x in row) + need(square_sum == 18432, "full Gram Frobenius mass") + diagonal_mass = sum(dots[i][i]**2 for i in range(96)) + need(diagonal_mass == 1536, "diagonal Gram mass") + identity_coefficient = [[sum(src.dot(v, v)*v[i]*v[j] for v in c) + for j in range(8)] for i in range(8)] + need(identity_coefficient == [[192*int(i == j) for j in range(8)] + for i in range(8)], "identity coefficient") + diagonal_square = sum(x*x for row in identity_coefficient for x in row) + off_diagonal_square = 16*(square_sum-diagonal_mass) + alternating = Q(diagonal_square+off_diagonal_square, 48**4) + mixed = Q(diagonal_square, 48**4) + triple = Q(sum(src.dot(v, v)**3 for v in c), 48**3) + pair = Q(diagonal_mass, 48**2) + need((pair, triple, alternating, mixed) == + (Q(2, 3), Q(1, 18), Q(23, 216), Q(1, 18)), "trace classes") + moments, counts = [], [] + values = {"single": Q(8), "pair": pair, "triple": triple, + "alternating": alternating, "mixed": mixed} + for power in range(1, 5): + census = Counter() + for word in product(range(3), repeat=power): + reduced = cyclic_reduce(word) + if len(reduced) <= 3: + key = {1: "single", 2: "pair", 3: "triple"}[len(reduced)] + else: + key = "alternating" if len(set(reduced)) == 2 else "mixed" + census[key] += 1 + need(sum(census.values()) == 3**power, "stage-word coverage") + moments.append(sum(n*values[k] for k, n in census.items())) + counts.append(dict(sorted(census.items()))) + need(moments == [Q(24), Q(28), Q(109, 3), Q(1823, 36)], "moments") + return moments, { + "gram_square_sum": square_sum, + "identity_coefficient_diagonal": 192, + "identity_coefficient_square_trace": diagonal_square, + "off_identity_square_trace": off_diagonal_square, + "alternating_four_trace": str(alternating), + "mixed_four_trace": str(mixed), + "cyclic_stage_word_counts": counts, + } + + +def spectral_bound(moments): + m1, m2, m3, m4 = moments + det = m2*m4-m3*m3 + need(det > 0, "positive moment determinant") + a, b = (m4*m1-m3*m2)/det, (m2*m2-m3*m1)/det + # p(t)=1-(1-a*t-b*t^2)^2 is <=1 for EVERY real t, and p(0)=0. + coefficients = [Q(0), 2*a, 2*b-a*a, -2*a*b, -b*b] + check_polynomial(coefficients, [Q(1), -a, -b]) + bound = sum(x*y for x, y in zip(coefficients[1:], moments)) + need((a, b, bound) == (Q(81, 40), Q(-9, 10), Q(117, 5)), + "quartic rank bound") + need(bound-8-15 == Q(2, 5), "positive width-fifteen residual") + return { + "residual_polynomial": ["1", str(-a), str(-b)], + "rank_polynomial": list(map(str, coefficients)), + "stacked_rank_lower_per_owner": str(bound), + "selected_defect_lower_per_owner": str(bound-8), + "width_fourteen_residual_lower_per_owner": str(bound-22), + "width_fifteen_residual_lower_per_owner": str(bound-23), + "necessary_integer_record_width": 16, + } + + +def certificate(repo): + R, routes = src.packet_data(src.load_packet(repo)) + src.check_grams(R) + src.check_swap_charts(routes) + pairs, intersections = pair_census(routes) + moments, traces = moments_from_columns(R) + return { + "status": MARKER, + "pair_census": pairs, + "cross_stage_intersections": intersections, + "trace_calculation": traces, + "moments_per_owner": list(map(str, moments)), + "spectral_bound": spectral_bound(moments), + "scope": "Regular-owner information dimension under the inherited fixed-pair erased-family observation contract; no physical invoice or new kappa.", + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--repo", type=Path, default=HERE.parents[1]) + parser.add_argument("--receipt", type=Path, default=HERE / "RESULT.json") + args = parser.parse_args() + result = certificate(args.repo) + need(canonical(read_receipt(args.receipt)) == canonical(result), "receipt mismatch") + print(MARKER + " moment4=1823/36 rank>=117|G|/5 defect>=77|G|/5 width>=16 no_new_kappa") + + +if __name__ == "__main__": + main()