diff --git a/research/pr1417-field-sensitive-rank-seed47/README.md b/research/pr1417-field-sensitive-rank-seed47/README.md new file mode 100644 index 0000000000..b5ad596236 --- /dev/null +++ b/research/pr1417-field-sensitive-rank-seed47/README.md @@ -0,0 +1,39 @@ +# Field-sensitive audit of PR1417 P112 graph tensors + +**Scoped independent verification. No new kappa and no theorem counterexample under the target proof's stated field.** + +## Finding + +PR1417 claims that the 5,824 ordered edge tensors from the selected P112 ports span dimension 80 in an 81-dimensional matrix space and uses the identity form as their nonzero null vector. The rank is characteristic-dependent. Reconstructing the actual selected ports and every edge gives rank 80 over `F2` but rank 81 over `F1009`. The audit supplies an 81-by-81 pivot minor whose determinant is nonzero modulo the prime 1009, so the same integer matrix has rank 81 over the rationals and complexes. + +The pinned PR1417 proof explicitly declares `F2^9` in its linear-lift statement and invokes characteristic two. The result therefore does **not** refute the theorem as written. It shows the rank-80 certificate cannot be carried over unchanged to characteristic zero. This is a field-contract result, not evidence of a larger or smaller supplier bound. + +A concrete identity-form check makes the distinction visible: selected port 0 has ordinary integer self-dot 3, and graph edge `(0,1)` has ordinary integer dot 2. Modulo two these become 1 and 0, respectively, as required by the stated binary model. Across all 112 ports, the integer weight distribution is 77 of weight 3 and 35 of weight 7; across 5,824 parity-selected ordered edges, integer dot products are 0 (1,400), 2 (3,948), and 6 (476). + +## Exact pins + +Research/source base: `410026dc5513b87db92ae98571d1d5984c69a983`. For publication the branch was rebased onto refreshed `main` at `4040a0f46d67b41c36a472a7cd4af791fd4c36cc`; the selected certificate and all three pinned repository inputs retain identical blobs across those commits. The ports come from the selected PR1094 canonical word inside the pinned replay archive. The target is PR1417 at exact head `c755bf393bea26d2275e1516b0560ca92de7a52e`. `SOURCES.json` records Git blob IDs and SHA256 values for the selected inputs and the target proof, certificate, geometry code and verifier. The proof and certificate snapshots in this package are byte-for-byte copies from that head. + +## Reproduce + +From the repository root with Python 3.12: + +```sh +python3.12 scripts/research_package.py --package research/pr1417-field-sensitive-rank-seed47 +``` + +Expected: `PASS_REGISTERED_RESEARCH_PACKAGE research/pr1417-field-sensitive-rank-seed47 outcome=completed`. The checker uses only the standard library. A nonzero 81-by-81 determinant modulo a certified prime proves the characteristic-zero rank is 81; the full theorem and supplier/cost interface are outside this audit. + +## Scope and limits + +This verifies the finite graph tensor ranks and the stated field marker in PR1417's proof. It does not dispute the intended `F2` result, prove that the full proof transfers to the retained complex supplier, or audit the dimension-18, all-size endpoint, 144-call cost, moment, controller, native or outer-bound arguments. No selected certificate or frontier value changes. + +The initial suspicion that the binary rank was being applied over characteristic zero was rejected after inspecting the pinned proof. This is an explicit field-sensitivity control, not a failed search for a new kappa. + +## Open next questions + +Trace the binary-field contract through PR1417's full endpoint and Fourier-rank cost argument. That would establish whether every linear map and bilinear form in the physical-supplier interface remains over `F2`. The present package supplies exact finite evidence but does not re-derive that theorem. + +## Credit + +Credit Ali Romman / PR1417 for the P112 graph and field-specific theorem, and the selected PR1094 contributors for the frozen source word and archive. Prepared by Cinna Davis (@1337isnot1337) with substantial OpenAI Codex assistance in source tracing, exact arithmetic, implementation and writing. This is a code-disjoint field audit, not independent human review. The copied proof and certificate retain their Apache-2.0 source context; new material is Apache-2.0. diff --git a/research/pr1417-field-sensitive-rank-seed47/RESULT.json b/research/pr1417-field-sensitive-rank-seed47/RESULT.json new file mode 100644 index 0000000000..560a0d4061 --- /dev/null +++ b/research/pr1417-field-sensitive-rank-seed47/RESULT.json @@ -0,0 +1,364 @@ +{ + "F1009_full_rank_minor_determinant": 548, + "F1009_full_rank_minor_edges": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 0, + 3 + ], + [ + 0, + 4 + ], + [ + 0, + 5 + ], + [ + 0, + 6 + ], + [ + 0, + 12 + ], + [ + 0, + 25 + ], + [ + 0, + 48 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 1, + 3 + ], + [ + 1, + 4 + ], + [ + 1, + 5 + ], + [ + 1, + 7 + ], + [ + 1, + 16 + ], + [ + 1, + 26 + ], + [ + 1, + 45 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ], + [ + 2, + 3 + ], + [ + 2, + 4 + ], + [ + 2, + 5 + ], + [ + 2, + 8 + ], + [ + 2, + 12 + ], + [ + 2, + 27 + ], + [ + 2, + 44 + ], + [ + 3, + 0 + ], + [ + 3, + 1 + ], + [ + 3, + 2 + ], + [ + 3, + 4 + ], + [ + 3, + 5 + ], + [ + 3, + 9 + ], + [ + 3, + 13 + ], + [ + 3, + 28 + ], + [ + 3, + 44 + ], + [ + 4, + 0 + ], + [ + 4, + 1 + ], + [ + 4, + 2 + ], + [ + 4, + 3 + ], + [ + 4, + 5 + ], + [ + 4, + 10 + ], + [ + 4, + 14 + ], + [ + 4, + 29 + ], + [ + 4, + 44 + ], + [ + 5, + 0 + ], + [ + 5, + 1 + ], + [ + 5, + 2 + ], + [ + 5, + 3 + ], + [ + 5, + 4 + ], + [ + 5, + 11 + ], + [ + 5, + 15 + ], + [ + 5, + 30 + ], + [ + 5, + 44 + ], + [ + 6, + 0 + ], + [ + 6, + 7 + ], + [ + 6, + 8 + ], + [ + 6, + 9 + ], + [ + 6, + 10 + ], + [ + 6, + 11 + ], + [ + 6, + 12 + ], + [ + 6, + 25 + ], + [ + 6, + 35 + ], + [ + 12, + 0 + ], + [ + 12, + 2 + ], + [ + 12, + 6 + ], + [ + 12, + 13 + ], + [ + 12, + 14 + ], + [ + 12, + 15 + ], + [ + 12, + 16 + ], + [ + 12, + 26 + ], + [ + 12, + 45 + ], + [ + 25, + 0 + ], + [ + 25, + 6 + ], + [ + 25, + 16 + ], + [ + 25, + 17 + ], + [ + 25, + 18 + ], + [ + 25, + 19 + ], + [ + 25, + 20 + ], + [ + 25, + 26 + ], + [ + 25, + 31 + ] + ], + "F1009_prime_divisors_checked_through": 31, + "base_commit": "410026dc5513b87db92ae98571d1d5984c69a983", + "controls": [ + "published 80-edge basis checked over F2", + "full 5824-edge graph independently reduced over F2 and F1009", + "nonzero 81x81 determinant modulo verified prime 1009", + "identity-form witnesses distinguished modulo 2 and over integers", + "pinned proof explicitly states F2 and characteristic two" + ], + "edge_integer_dot_histogram": { + "0": 1400, + "2": 3948, + "6": 476 + }, + "identity_form_witness": { + "edge_0_1_dot_mod2": 0, + "edge_0_1_dot_over_Z": 2, + "port_0_squared_norm_mod2": 1, + "port_0_squared_norm_over_Z": 3 + }, + "interpretation": "The rank-80 certificate is valid in the explicitly stated F2/characteristic-two contract. The rank-81 result over F1009 proves that it cannot be transported unchanged to characteristic zero. This is not a counterexample to PR1417 under its stated binary-field assumptions and does not audit the full endpoint or cost theorem.", + "ordered_edges": 5824, + "port_weight_histogram": { + "3": 77, + "7": 35 + }, + "rank_over_F1009": 81, + "rank_over_F2": 80, + "status": "PASS_PR1417_P112_EDGE_TENSOR_FIELD_SENSITIVITY_AUDIT", + "target_head": "c755bf393bea26d2275e1516b0560ca92de7a52e", + "target_pr": 1417, + "tensor_dimensions": [ + 5824, + 81 + ] +} diff --git a/research/pr1417-field-sensitive-rank-seed47/SOURCES.json b/research/pr1417-field-sensitive-rank-seed47/SOURCES.json new file mode 100644 index 0000000000..6f75dd160d --- /dev/null +++ b/research/pr1417-field-sensitive-rank-seed47/SOURCES.json @@ -0,0 +1,61 @@ +{ + "schema_version": 1, + "base_commit": "410026dc5513b87db92ae98571d1d5984c69a983", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + } + ], + "external_sources": { + "repository": "CrocSwap/integer-mult-bounds", + "pr": 1417, + "head": "c755bf393bea26d2275e1516b0560ca92de7a52e", + "files": [ + { + "name": "proof", + "path": "research/p112-linear-endpoint-lifts/PROOF.md", + "git_blob": "6b8e74c3eb2149cfb8e97f085d6a9069c9fd7fd3", + "sha256": "f99ece395c7c0f061efc41cd3feb9e35aeb9cca87a0ddbe44d99ee858b007602", + "snapshot": "TARGET-PROOF.md", + "snapshot_sha256": "f99ece395c7c0f061efc41cd3feb9e35aeb9cca87a0ddbe44d99ee858b007602" + }, + { + "name": "certificate", + "path": "research/p112-linear-endpoint-lifts/CERTIFICATE.json", + "git_blob": "5eb9e842318628a724943ee8701b20bc0de8b55c", + "sha256": "239cd68b2f56eb8d7ce0300517e89132638102d0a33cb9bb01682141cb5b322d", + "snapshot": "TARGET-CERTIFICATE.json", + "snapshot_sha256": "239cd68b2f56eb8d7ce0300517e89132638102d0a33cb9bb01682141cb5b322d" + } + ], + "provenance_files": [ + { + "name": "geometry", + "path": "research/p112-linear-endpoint-lifts/geometry.py", + "git_blob": "d86355c23c159f091cb0fa6b836a9452a44035d3", + "sha256": "db5bc0b59f183686afa833177c2f3217866ebedccd6ad4d4b99526a298b24625" + }, + { + "name": "verifier", + "path": "research/p112-linear-endpoint-lifts/verify.py", + "git_blob": "2a1b1394e2b6a3f24c69bb81871f4aed0b411183", + "sha256": "42ac87de6a670418a4f5886977672dbefe08d83bf7cad07608deefc962a6b203" + } + ] + } +} diff --git a/research/pr1417-field-sensitive-rank-seed47/TARGET-CERTIFICATE.json b/research/pr1417-field-sensitive-rank-seed47/TARGET-CERTIFICATE.json new file mode 100644 index 0000000000..5eb9e84231 --- /dev/null +++ b/research/pr1417-field-sensitive-rank-seed47/TARGET-CERTIFICATE.json @@ -0,0 +1,511 @@ +{ + "basis_edges": [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 0, + 3 + ], + [ + 0, + 4 + ], + [ + 0, + 5 + ], + [ + 0, + 6 + ], + [ + 0, + 12 + ], + [ + 0, + 25 + ], + [ + 1, + 0 + ], + [ + 1, + 2 + ], + [ + 1, + 3 + ], + [ + 1, + 4 + ], + [ + 1, + 5 + ], + [ + 1, + 7 + ], + [ + 1, + 16 + ], + [ + 1, + 26 + ], + [ + 2, + 0 + ], + [ + 2, + 1 + ], + [ + 2, + 3 + ], + [ + 2, + 4 + ], + [ + 2, + 5 + ], + [ + 2, + 8 + ], + [ + 2, + 12 + ], + [ + 2, + 27 + ], + [ + 3, + 0 + ], + [ + 3, + 1 + ], + [ + 3, + 2 + ], + [ + 3, + 4 + ], + [ + 3, + 5 + ], + [ + 3, + 9 + ], + [ + 3, + 13 + ], + [ + 3, + 28 + ], + [ + 4, + 0 + ], + [ + 4, + 1 + ], + [ + 4, + 2 + ], + [ + 4, + 3 + ], + [ + 4, + 5 + ], + [ + 4, + 10 + ], + [ + 4, + 14 + ], + [ + 4, + 29 + ], + [ + 5, + 0 + ], + [ + 5, + 1 + ], + [ + 5, + 2 + ], + [ + 5, + 3 + ], + [ + 5, + 4 + ], + [ + 5, + 11 + ], + [ + 5, + 15 + ], + [ + 5, + 30 + ], + [ + 6, + 0 + ], + [ + 6, + 7 + ], + [ + 6, + 8 + ], + [ + 6, + 9 + ], + [ + 6, + 10 + ], + [ + 6, + 11 + ], + [ + 6, + 12 + ], + [ + 6, + 25 + ], + [ + 7, + 1 + ], + [ + 7, + 8 + ], + [ + 8, + 2 + ], + [ + 9, + 3 + ], + [ + 10, + 4 + ], + [ + 11, + 5 + ], + [ + 12, + 0 + ], + [ + 12, + 2 + ], + [ + 12, + 6 + ], + [ + 12, + 13 + ], + [ + 12, + 14 + ], + [ + 12, + 15 + ], + [ + 12, + 16 + ], + [ + 12, + 26 + ], + [ + 13, + 3 + ], + [ + 25, + 0 + ], + [ + 25, + 6 + ], + [ + 25, + 16 + ], + [ + 25, + 17 + ], + [ + 25, + 18 + ], + [ + 25, + 19 + ], + [ + 25, + 20 + ], + [ + 25, + 26 + ], + [ + 26, + 1 + ] + ], + "anchors": [ + 0, + 1, + 2, + 54, + 55, + 76, + 82, + 89 + ], + "edge_vertices": [ + { + "pair": [ + 0, + 1 + ], + "vertex": 107 + }, + { + "pair": [ + 0, + 2 + ], + "vertex": 104 + }, + { + "pair": [ + 0, + 3 + ], + "vertex": 65 + }, + { + "pair": [ + 0, + 4 + ], + "vertex": 64 + }, + { + "pair": [ + 0, + 6 + ], + "vertex": 35 + }, + { + "pair": [ + 0, + 7 + ], + "vertex": 16 + }, + { + "pair": [ + 1, + 2 + ], + "vertex": 100 + }, + { + "pair": [ + 1, + 3 + ], + "vertex": 71 + }, + { + "pair": [ + 1, + 4 + ], + "vertex": 70 + }, + { + "pair": [ + 1, + 5 + ], + "vertex": 48 + }, + { + "pair": [ + 1, + 7 + ], + "vertex": 12 + }, + { + "pair": [ + 2, + 3 + ], + "vertex": 74 + }, + { + "pair": [ + 2, + 4 + ], + "vertex": 73 + }, + { + "pair": [ + 2, + 5 + ], + "vertex": 51 + }, + { + "pair": [ + 2, + 6 + ], + "vertex": 31 + }, + { + "pair": [ + 3, + 5 + ], + "vertex": 4 + }, + { + "pair": [ + 3, + 6 + ], + "vertex": 91 + }, + { + "pair": [ + 3, + 7 + ], + "vertex": 84 + }, + { + "pair": [ + 4, + 5 + ], + "vertex": 5 + }, + { + "pair": [ + 4, + 6 + ], + "vertex": 90 + }, + { + "pair": [ + 4, + 7 + ], + "vertex": 83 + }, + { + "pair": [ + 5, + 6 + ], + "vertex": 85 + }, + { + "pair": [ + 5, + 7 + ], + "vertex": 78 + }, + { + "pair": [ + 6, + 7 + ], + "vertex": 56 + } + ], + "archive_members": { + "candidate/strict/global/base/providers/gauge44/CANONICAL-WORD.json.gz": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "candidate/strict/global/base/providers/gauge44/LOCAL-PROGRAMS.json.gz": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a", + "candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "candidate/strict/global/hosted/GLOBAL-TEMPLATE.json.gz": "2acf02b418078e37090495c601fe550448751d4f35912757b13a1f778efc7760", + "candidate/strict/global/hosted/IDLE-REMAINDER-FRAMES.json.gz": "650c14a1de75015fdae5c02ea18f1d0fd2de35d249b5ff2cd77f3b1afe604985" + } +} diff --git a/research/pr1417-field-sensitive-rank-seed47/TARGET-PROOF.md b/research/pr1417-field-sensitive-rank-seed47/TARGET-PROOF.md new file mode 100644 index 0000000000..6b8e74c3eb --- /dev/null +++ b/research/pr1417-field-sensitive-rank-seed47/TARGET-PROOF.md @@ -0,0 +1,302 @@ +# Endpoint dimension and the cost of linear lifts + +All vector spaces in Sections 1--3 are over the field with two elements. +The ambient form is symmetric and nondegenerate. An endpoint subspace is +nondegenerate for the restricted form. Alternating endpoint planes are allowed. +No positivity assumption is used. + +## 1. The graph and two exact certificates + +Use the 112 binary ports in the selected canonical word. Join distinct +ports a,b when their binary dot product is zero. This is the P112 +source/target interaction graph used by the retained scalar identity. +It has 5,824 ordered edges. Each vertex has a label t_a in dimension 9, +with nondegenerate symmetric form S=I9, such that + + t_a^T S t_a = 1; t_a^T S t_b = 0 on every graph edge. + +The verifier reads the selected source bytes, checks all 12,544 binary +pairings, and checks the following two certificates. No graph isomorphism +to a different port model is assumed. + +**Certificate A.** The edge tensors `t_a tensor t_b` have rank 80 in the +81-dimensional matrix space. The 80 listed edges form a basis. S is a +nonzero null vector, so every bilinear form K that vanishes on graph edges +is `K = c S`. + +**Certificate B.** There is an eight-vertex clique with vertices a_0,...,a_7. +There are 24 further vertices b_ij, one for each edge ij of a graph J on +eight points. J is K8 with one perfect matching removed. Vertex b_ij is +adjacent to every a_k except a_i,a_j. Two b vertices are adjacent exactly +when their J edges have a common endpoint. In particular J is 6-regular. +The certificate lists the 32 distinct vertices. The verifier checks every +required and absent edge, rather than accepting a claimed graph name. + +The certificates are finite premises of the following all-size arguments. +The verifier is not a proof-assistant formalization of those arguments. + +## 2. Sharp dimension bound for arbitrary two-plane labels + +Suppose each graph vertex is assigned a nondegenerate two-dimensional +subspace U_a in an h-dimensional space, and graph edges give orthogonal +subspaces. The assignment need not depend linearly on the old labels. +Then **h >= 18**. The binary tensor construction `U_a = t_a tensor F2^2` +in the form `S tensor I2` attains 18. + +The eight anchor planes in Certificate B are mutually orthogonal. Their +orthogonal direct sum E has dimension 16. Thus h >= 16. Put +`H = E_0 perpendicular ... perpendicular E_7 perpendicular Z`. +For h <= 17, the dimension z of Z is zero or one. The plane U_ij lies in +`E_i + E_j + Z` because it is orthogonal to the other six anchor planes. + +Choose any basis for each U_ij. Its nondegenerate 2-by-2 Gram matrix is D_ij. +Let K_ij,i be the Gram matrix of its projection to E_i, and let R_ij be +the Gram matrix of its projection to Z. Thus + + D_ij = K_ij,i + K_ij,j + R_ij. (1) + +For a fixed i, collect the six incident planes in one matrix. Their E_i +projection has a Gram matrix K_i of rank at most two. Their Z projection +has a Gram matrix R_i of rank at most z. Distinct incident planes are +orthogonal, and their other anchor blocks differ. Therefore the off-diagonal +blocks of K_i and R_i agree. Hence + + H_i = K_i + R_i + +is block diagonal, with blocks `H_ij,i = K_ij,i + R_ij`, and + + sum_(j:ij in J) rank(H_ij,i) = rank(H_i) <= 2 + z. (2) + +If z=0, (1) gives `2 <= rank(H_ij,i) + rank(H_ij,j)`. +Summing over 24 edges contradicts (2): `48 <= 16`. + +If z=1, choose the unit basis of Z. Write its coordinate row on U_ij as +u_ij, so `R_ij = u_ij^T u_ij`. Characteristic two gives + + D_ij = H_ij,i + H_ij,j + u_ij^T u_ij. + +Thus `rank(H_ij,i) + rank(H_ij,j) >= 1`. Summing over J and using (2) +gives equality throughout: the total is 24, every vertex contributes 3, +and every edge contributes 1. Also every u_ij is nonzero; otherwise its +edge would need a contribution at least 2. + +At each vertex i there are therefore three rank-one diagonal blocks in +H_i and three zero blocks. Let u_i be the concatenation of its six rows +u_ij. It has a nonzero component at every zero block. Consequently +`u_i^T` is not in the image of H_i. A rank-one update by this vector +cannot reduce rank: if `(H_i + u_i^T u_i)x=0`, then +`H_i x = u_i^T (u_i x)`. Since `u_i^T` is not in the image of H_i, +we have `u_i x=0` and `H_i x=0`. The new kernel is contained in the old +kernel. Hence + + rank(K_i) = rank(H_i + u_i^T u_i) >= rank(H_i) = 3, + +contrary to `rank(K_i) <= 2`. This excludes h=17 and proves the bound. + +This theorem fixes the least ambient dimension. It does not classify all +dimension-18 assignments or bound the cost of every new word on them. + +## 3. Rigidity of all coupled linear lifts + +Let V have dimension r >= 1. Let `A: F2^9 tensor V -> H` be linear and +write `A(t)v = A(t tensor v)`. Assume all spaces `A(t_a)V` have dimension +r and a nondegenerate restricted form. Require them to be orthogonal on +every graph edge. There is no block-diagonal or independent-copy assumption. + +For v,w in V, the function + + K_(v,w)(x,y) = + +is a bilinear form on the old nine-dimensional space and vanishes on all +graph edges. Certificate A gives a scalar D(v,w) such that + + K_(v,w)(x,y) = (x^T S y) D(v,w). (3) + +Linearity shows that D is bilinear. Symmetry of the ambient form shows +that D is symmetric. At any vertex t_a, (3) restricts to D because +`t_a^T S t_a=1`. Nondegeneracy of the endpoint makes D nondegenerate. +Thus the pullback Gram matrix of A is `S tensor D`, of rank 9r. +The map A is injective, its image is nondegenerate, and h >= 9r. + +For every old subspace U, its image is `A(U tensor V)` and has dimension +`r dim(U)`. Intersections, sums and orthogonal complements inside this +image are the old ones tensored with V. This proves rigidity for every +fibre size, every ambient dimension, and all linear couplings. + +## 4. The complete accounting class + +The cost conclusion concerns an endpoint lift of a fixed complete supplier +and controller diagram. This condition matters. It does not cover a new +scalar program or a new controller that reuses stages in a different way. + +The reference diagram includes every source-access edge, helper edge, +copied-centre edge, restoration edge and idle child. It has ambient width m, +W live role streams of equal volume, and paid edge ranks t_e. Each scalar +gate uses a common exact frame on all its incident streams. In the selected +instance, `m=73`, `W=14336`, and the complete histogram is + + {1:349604, 2:60192, 3:62585, 4:20448, + 5:11808, 7:7, 8:1152, 48:4866}. + +The linear lift replaces the old core by its r-fold tensor image. In the +retained nine-stage orthogonal-slot controller, this has width 73r. At each +retained boundary, the lifted subspace has intersection with this core equal +to the image of the old boundary subspace. Additional ambient coordinates +are permitted, with arbitrary slanted subspaces, nonmonotone transitions, +and extra gates. Their entrance quotient dimension is zero and their final +quotient dimension is their full width on every live role. The complete +auxiliary/centre ledger must also be retained. An auxiliary input does not +become a known-zero input. All W physical live streams persist through the +serialized schedule. A local role can use a different owner in a later call; +this does not move a physical stream path to a private centre. Each scalar +operation has the same frame before and after on each incident live path. +Private centre paths can start and end at different padding dimensions. +Their costs are nonnegative. They are not used in the signed sum below. + +Each individual retained role-stream edge may use any exact native +factorization, with any number of rank-zero adapters. Joint children that +encode several arrays or combine different frozen edges are outside this class. No assumption that its old child is run r times is +made. Each native child acts on the original role-stream volume; creating +extra role streams does not create extra normalization weight. A factorization +that crosses a retained scalar-gate boundary changes the reference diagram +and is outside this class. + +### Source-bound minimum-rank bridge + +The selected archive is `research/community-frontier1094-audit/selected-replay.tar.gz` +at the base commit in SOURCES.json. The verifier reads five exact members from +this Git object. It does not use historical files with similar names. Each +member has a SHA256 pin in CERTIFICATE.json. + +The source frame lemma in `notes/general-clifford-frames.tex` gives + + rank B(T_V T_U^(-1)) = dim U + dim V - 2 dim(U intersect V). + +This is an exact Fourier-rank identity. It applies to degenerate U and V, +and does not require the operators T_U and T_V to commute. The verifier +checks that this note has the same bytes as the copy in the selected source +manifest. Reverse/complement words preserve the same transition distance. + +For each of the two emitted local programs, the verifier reads every `climb` +and `center` edge and computes this distance from its actual binary frame +bases. It checks equality with the paid rank, not only a lower bound. There +are 3,494 edges per orientation. All eight private-centre edges go between +the specified rank-eight centre frame and the zero frame. Each has minimum +rank eight. Copying the centre value at its high frame does not erase that +transition. The total local rank mass is 5,586. + +The selected global controller contains 144 complete calls. Its 704 local +roles per call have distinct owners in the live range [0,14336); the private +centre range is separate. The verifier checks this assignment, the complete +per-replica event order, and the final live-family range. Thus changing a +helper's owner between calls changes the local role name, not the identity +of a physical stream. The selected owner audit supplies the inherited exact +chart and busy-window validity. This package does not repeat that audit. + +For each of the 7,526 idle children, the verifier reads the actual remainder +axes, checks the matching controller row, and checks that they are the exact +suffix of the inherited pending axes. It checks that their Gram matrix is +identity. This is a coordinate Fourier child on that subspace, so its minimum +rank is the number of these axes. Its entrance and exit frames have this +exact distance. The idle histogram is `{1:2276, 3:377, 7:7, 48:4866}`. +Adding the 144 literal local histograms gives the full histogram above and +rank mass 1,041,408. All 510,662 reference native children are included. +There is no unexamined histogram entry that could conceal an overcharged +reference transition. + +Exact scalar identities, phases, source wrappers, and the controller's charts +remain inherited from the selected review. The fresh check covers ranks and +stream accounting; it is not a cold replay of the supplier or compiler. + +## 5. No native factorization or ambient padding improves the moment + +Write `p=1-b`, with `0= r t_e`. Since `sum_j k_j^p >= (sum_j k_j)^p`, its +moment charge is at least `(r t_e/(rm))^p = (t_e/m)^p`. +One rank-r t_e child attains this lower bound whenever it is available; +granting it for free as an interface is an optimistic relaxation otherwise. + +Now add z>0 ambient coordinates. Put `M'=rm+z` and `lambda=rm/M'`. +At a boundary B let q_B be its dimension outside the tensor core. +For an old edge U->V, let `d_e=|q_V-q_U|`. The subspace distance satisfies + + distance(U',V') >= r distance(U,V) + d_e. (4) + +To see this, the core part of `U' intersect V'` has dimension +`r dim(U intersect V)`, and its quotient part has dimension at most +`min(q_U,q_V)`. Substitute in `dim U' + dim V' - 2 dim(U' intersect V')`. +This proof allows slanted frames and does not assume an orthogonal splitting +at each gate. The same native-factorization argument bounds an edge's charge +below by `((r t_e+d_e)/M')^p`. + +Sum signed q changes separately along each physical live stream. Scalar +operations do not change q on that path. This includes a copy from a live +stream to a private centre: it creates a private value but preserves the +live path and its frame. Rank-zero adapters preserve the preimage frame. +The native transitions on each live path therefore have net change z. +Their absolute changes sum to at least z. Summing the W live paths gives +`sum_e d_e >= Wz`, before any private-path cost is added. Private descents +cannot cancel this lower bound. New edges have old rank zero. Also +`0<=d_e/z<=1`. Concavity gives, edge by edge, + + ((r t_e+d_e)/M')^p + >= lambda (t_e/m)^p + (1-lambda) (d_e/z)^p. + +Summing, and using `x^p>=x` on [0,1], gives + + M_lift(p) >= lambda M(p) + (1-lambda). (5) + +If the reference moment is at least one, the lifted moment is at least one. +This includes arbitrary padding size, all extra transitions and every native +factorization at the retained boundaries. The unpadded tensor lift attains the +same moment in the ideal native-child model. Thus the optimal complex moment +exponent cannot increase in this class. A second unpaid direction is offset by +the forced growth of every geometric rank and of the ambient denominator. + +## 6. Consequence for the selected kappa grid + +The exact accounting check reconstructs the selected full histogram and +checks + + M(1-b_low) < 1 < M(1-b_high), + b_low = 0.001675462676808103522925, + b_high = b_low + 10^-24. + +It also checks the exact rational inequality + + b_high/(1+b_high) < 0.001672660197076919. + +The retained balanced outer reduction requires `kappa < b/(1+b)`. +Equation (5) therefore excludes the next 10^-18 kappa grid point and every +larger one for this lift class, even before new scalar, chart, source-access, +movement, restoration, or finite-invoice costs are imposed. Those costs are +nonnegative. The original bit supplier is retained; its restriction can only +decrease the feasible outer saving. Its raw exponent is not substituted for +an outer kappa. This result neither changes nor reproves the selected supplier. + +The all-size compiler, exact common-frame realization, whole-call hosting, +precision/tape, analytic transfer and bit H1--H5 conditions remain inherited. +Arbitrary dimension-18 plane assignments, other interaction graphs, new scalar +programs, and new outer reductions remain outside the no-improvement theorem. + +## 7. Relation to general endpoint labels + +The arbitrary-plane theorem in Section 2 is stronger than the linear-lift +hypothesis as a statement about dimension. It does not imply Section 5 for +all plane assignments. In dimension 18, a nonlinear assignment might have +other intersections at internal frames and might admit a new scalar word. +No classification or cost bound for those words is proved here. + +PR791, at `f80382efd4cd3e37c67b2a966398b55bb56af53c`, proves a separate +rational-idempotent path formula. Its rank-two examples show that a generic +endpoint penalty need not double. This proof does not assume that rule. +Section 3 first forces a tensor pullback form in the linear class. The +actual preimage-frame distances then scale by r. Without that rigidity or +without the retained boundaries, this rank-scaling conclusion is not used. diff --git a/research/pr1417-field-sensitive-rank-seed47/TASK.json b/research/pr1417-field-sensitive-rank-seed47/TASK.json new file mode 100644 index 0000000000..a2b60097db --- /dev/null +++ b/research/pr1417-field-sensitive-rank-seed47/TASK.json @@ -0,0 +1,62 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 2, + "base_commit": "410026dc5513b87db92ae98571d1d5984c69a983", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one selected supplier obligation follow from its actual source-bound checks?", + "starting_points": [ + "certificates/selected-result.json", + "research/owner-boundary-audit/README.md" + ], + "methods": [ + "Trace one hypothesis through the source, checker and complete caller.", + "Construct one semantically invalid but superficially well-formed fixture and test rejection." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "research/owner-boundary-audit/verify.py" + ], + "expected": "PASS_PR626_NEXT_TOUCH_BOUNDARY_AUDIT", + "inspect": "Identify why the timing-only omission passes but the full production controller still rejects it.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Choose one current supplier obligation and trace whether its acceptance depends on an independent check.", + "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.", + "allowed_variations": [ + "Audit one named current condition using a new semantic counterexample." + ], + "scope_change_triggers": [ + "Reporting the historical timing-only diagnostic as a new current acceptance bug." + ], + "overlap_terms": [ + "owner boundary", + "bridge omission", + "hosting" + ] + }, + "scope_status": "changed", + "actual_scope": "Independently audit the field sensitivity of PR1417 Certificate A by rebuilding all 5,824 P112 edge tensors from the selected source archive, computing their ranks over F2 and F1009, and checking the theorem proof\u2019s explicit field contract.", + "scope_change_reason": "The user-assigned structural track has no dedicated catalogue card; this exact finite structural premise is an adjacent scoped audit. An initial characteristic-zero reading was rejected after the pinned proof explicitly stated F2 and characteristic two. The contribution therefore reports field sensitivity, not a theorem counterexample.", + "bottleneck_link": "A graph-rank premise used to constrain endpoint-plane structure must be applied over the same field as its subspace and lift maps. The result prevents an invalid cross-characteristic inference; it changes no supplier price or kappa.", + "budget_minutes": 60, + "stop_rule": "Recompute the complete ordered edge-tensor rank from the pinned selected port set over F2 and one certified odd prime; produce an 81x81 nonzero minor if the odd-characteristic rank is full; read and pin the target proof\u2019s field assumptions. Stop at this finite field-contract audit; do not infer or audit the full endpoint/cost theorem.", + "outcome": "completed", + "evidence": "The 5,824 edge tensors have rank 80 over F2 and 81 over F1009. An explicit 81x81 pivot minor has nonzero determinant modulo prime 1009, proving characteristic-zero rank 81. Exact witnesses show port 0 has integer self-dot 3 and edge (0,1) has integer dot 2; both identities reduce to the intended F2 values 1 and 0. PR1417 PROOF.md explicitly states F2^9 and characteristic two, so this does not refute its stated theorem.", + "author": "Cinna Davis (@1337isnot1337)", + "ai_assistance": "Substantial OpenAI Codex assistance in overlap review, exact source tracing, independent verifier design, modular certificate generation, interpretation and writing.", + "open_questions": [ + { + "question": "Does the full linear-lift cost argument state and preserve the binary-field contract at every interface to the retained complex supplier and controller?", + "why_it_matters": "The finite rank certificate is field-specific; any use with a characteristic-zero scalar model needs a separate bridge.", + "first_step": "Trace the PR1417 source-bound map from binary labels and F2-linear endpoint lifts through the Fourier-rank invoice, checking the field of every tensor and bilinear form.", + "blocked_by": "This package stops after the exact graph-tensor field audit and does not re-derive the full cost theorem." + } + ], + "assignment_seed": 47, + "track": "structural decoder research" +} diff --git a/research/pr1417-field-sensitive-rank-seed47/VERIFY.json b/research/pr1417-field-sensitive-rank-seed47/VERIFY.json new file mode 100644 index 0000000000..7ef12c8897 --- /dev/null +++ b/research/pr1417-field-sensitive-rank-seed47/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/pr1417-field-sensitive-rank-seed47/TARGET-PROOF.md", + "research/pr1417-field-sensitive-rank-seed47/TARGET-CERTIFICATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Reconstructs all selected P112 ports and 5,824 ordered edge tensors; independently computes ranks over F2 and F1009; checks the nonzero 81x81 modular minor, exact identity-form witnesses and the pinned proof field markers." + } + ] +} diff --git a/research/pr1417-field-sensitive-rank-seed47/verify.py b/research/pr1417-field-sensitive-rank-seed47/verify.py new file mode 100644 index 0000000000..2f1a56cd7a --- /dev/null +++ b/research/pr1417-field-sensitive-rank-seed47/verify.py @@ -0,0 +1,208 @@ +#!/usr/bin/env python3 +"""Recompute PR1417's P112 edge-tensor rank in two characteristics.""" +from collections import Counter +import gzip +import hashlib +import io +import json +from math import isqrt +from pathlib import Path +import tarfile + +ROOT = Path(__file__).resolve().parents[2] +PKG = Path(__file__).resolve().parent +BASE = "410026dc5513b87db92ae98571d1d5984c69a983" +TARGET_HEAD = "c755bf393bea26d2275e1516b0560ca92de7a52e" +PRIME = 1009 + + +def need(ok, message): + if not ok: + raise AssertionError(message) + + +def source_bytes(path): + return __import__("subprocess").check_output( + ["git", "show", f"{BASE}:{path}"], cwd=ROOT + ) + + +def rank_gf2(rows): + pivots = {} + for row in rows: + while row: + col = row.bit_length() - 1 + if col in pivots: + row ^= pivots[col] + else: + pivots[col] = row + break + return len(pivots) + + +def rank_mod(rows, p): + pivots = {} + pivot_edges = [] + for edge, raw in rows: + row = [x % p for x in raw] + for col in range(len(row)): + value = row[col] + if not value: + continue + old = pivots.get(col) + if old is not None: + row = [(x - value*y) % p for x, y in zip(row, old)] + continue + inv = pow(value, -1, p) + pivots[col] = [(x*inv) % p for x in row] + pivot_edges.append(edge) + break + return len(pivots), pivot_edges + + +def det_mod(matrix, p): + a = [[x % p for x in row] for row in matrix] + n = len(a) + need(all(len(row) == n for row in a), "square minor dimensions") + det = 1 + for col in range(n): + pivot = next((r for r in range(col, n) if a[r][col]), None) + need(pivot is not None, "selected minor has nonzero pivot") + if pivot != col: + a[col], a[pivot] = a[pivot], a[col] + det = -det + value = a[col][col] + det = det * value % p + inv = pow(value, -1, p) + a[col] = [(x*inv) % p for x in a[col]] + for r in range(col + 1, n): + factor = a[r][col] + if factor: + a[r] = [(x-factor*y) % p for x, y in zip(a[r], a[col])] + return det % p + + +def load_ports(): + archive_path = "research/community-frontier1094-audit/selected-replay.tar.gz" + archive_raw = source_bytes(archive_path) + with tarfile.open(fileobj=io.BytesIO(archive_raw), mode="r:gz") as archive: + member = "candidate/strict/global/base/providers/gauge44/CANONICAL-WORD.json.gz" + packed = archive.extractfile(member) + need(packed is not None, "selected canonical word member exists") + word = json.loads(gzip.decompress(packed.read())) + ports = word["ports"] + need(len(ports) == 112 and len(set(ports)) == 112, "112 distinct selected ports") + need(all(type(x) is int and 0 < x < 512 and x.bit_count() % 2 == 1 for x in ports), + "selected ports are odd nonzero 9-bit labels") + labels = [[(x >> j) & 1 for j in range(9)] for x in ports] + return ports, labels + + +def main(): + sources = json.loads((PKG / "SOURCES.json").read_text()) + need(sources["base_commit"] == BASE, "exact research base pin") + external = sources["external_sources"] + need(external["pr"] == 1417 and external["head"] == TARGET_HEAD, + "exact target PR head pin") + for row in external["files"]: + data = (PKG / row["snapshot"]).read_bytes() + need(hashlib.sha256(data).hexdigest() == row["snapshot_sha256"], + "target snapshot hash: " + row["name"]) + proof = (PKG / "TARGET-PROOF.md").read_text() + need("F2^9 tensor V" in proof and "Characteristic two" in proof, + "the target proof states the binary-field contract") + certificate = json.loads((PKG / "TARGET-CERTIFICATE.json").read_text()) + need(len(certificate["basis_edges"]) == 80, "published 80-edge basis receipt") + + ports, labels = load_ports() + weight_hist = Counter(map(sum, labels)) + edges = [] + gf2_rows = [] + modular_rows = [] + dots = Counter() + for a, x in enumerate(labels): + for b, y in enumerate(labels): + if a == b: + continue + dot = sum(u*v for u, v in zip(x, y)) + if dot % 2: + continue + edge = (a, b) + row = [x[i]*y[j] for i in range(9) for j in range(9)] + bitrow = sum(value << (9*i+j) + for i in range(9) for j, value in enumerate(y) + if x[i]) + edges.append(edge) + dots[dot] += 1 + gf2_rows.append(bitrow) + modular_rows.append((edge, row)) + need(len(edges) == 5824, "selected ordered graph edge count") + need(weight_hist == Counter({3: 77, 7: 35}), "exact port weight distribution") + need(dots == Counter({0: 1400, 2: 3948, 6: 476}), "exact integer dot distribution on parity edges") + edge_set = set(edges) + basis = [tuple(edge) for edge in certificate["basis_edges"]] + need(len(set(basis)) == 80 and all(e in edge_set for e in basis), + "published basis edges belong to the selected graph") + basis_rows = [] + for a, b in basis: + x, y = labels[a], labels[b] + basis_rows.append(sum(x[i]*y[j] << (9*i+j) + for i in range(9) for j in range(9))) + need(rank_gf2(basis_rows) == 80, "published basis independent over F2") + binary_rank = rank_gf2(gf2_rows) + need(binary_rank == 80, "full graph tensor rank over F2") + + need(all(PRIME % d for d in range(2, isqrt(PRIME)+1)), "1009 is prime") + odd_rank, pivot_edges = rank_mod(modular_rows, PRIME) + need(odd_rank == 81 and len(pivot_edges) == 81, + "full graph tensor rank over F1009") + by_edge = {edge: row for edge, row in modular_rows} + minor = [by_edge[e] for e in pivot_edges] + minor_det = det_mod(minor, PRIME) + need(minor_det != 0, "81x81 pivot minor has nonzero determinant mod 1009") + + port0_weight = sum(labels[0]) + edge01_dot = sum(u*v for u, v in zip(labels[0], labels[1])) + need((0, 1) in edge_set and port0_weight == 3 and edge01_dot == 2, + "concrete characteristic-zero S=I9 counterexample witnesses") + need(port0_weight % 2 == 1 and edge01_dot % 2 == 0, + "same witnesses satisfy the intended F2 identities") + + result = { + "status": "PASS_PR1417_P112_EDGE_TENSOR_FIELD_SENSITIVITY_AUDIT", + "base_commit": BASE, + "target_pr": 1417, + "target_head": TARGET_HEAD, + "ordered_edges": len(edges), + "port_weight_histogram": {str(k): v for k, v in sorted(weight_hist.items())}, + "edge_integer_dot_histogram": {str(k): v for k, v in sorted(dots.items())}, + "tensor_dimensions": [len(edges), 81], + "rank_over_F2": binary_rank, + "rank_over_F1009": odd_rank, + "F1009_prime_divisors_checked_through": isqrt(PRIME), + "F1009_full_rank_minor_edges": [list(e) for e in pivot_edges], + "F1009_full_rank_minor_determinant": minor_det, + "identity_form_witness": { + "port_0_squared_norm_over_Z": port0_weight, + "edge_0_1_dot_over_Z": edge01_dot, + "port_0_squared_norm_mod2": port0_weight % 2, + "edge_0_1_dot_mod2": edge01_dot % 2, + }, + "interpretation": "The rank-80 certificate is valid in the explicitly stated F2/characteristic-two contract. The rank-81 result over F1009 proves that it cannot be transported unchanged to characteristic zero. This is not a counterexample to PR1417 under its stated binary-field assumptions and does not audit the full endpoint or cost theorem.", + "controls": [ + "published 80-edge basis checked over F2", + "full 5824-edge graph independently reduced over F2 and F1009", + "nonzero 81x81 determinant modulo verified prime 1009", + "identity-form witnesses distinguished modulo 2 and over integers", + "pinned proof explicitly states F2 and characteristic two", + ], + } + expected_path = PKG / "RESULT.json" + if expected_path.exists(): + expected = json.loads(expected_path.read_text()) + need(result == expected, "stored exact field-sensitivity receipt") + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()