diff --git a/research/no-edge-dim4-image-five/PROOF.md b/research/no-edge-dim4-image-five/PROOF.md new file mode 100644 index 0000000000..b2350589ee --- /dev/null +++ b/research/no-edge-dim4-image-five/PROOF.md @@ -0,0 +1,289 @@ +# An irreducible no-edge pool of pattern dimension 4 and joint image 5 + +Prepared by unpaidmoon with substantial Cursor Grok assistance. New work is +Apache-2.0. This is a written existence proof for one explicit pool, checked +again by a finite pattern census and by the subspace lattice of its joint +image. **No new κ.** The selected frontier stays `781451/250000000`. + +## 1. Statement + +Work over F2. For a matrix N, write off(N) for the matrix obtained by +deleting its diagonal. Let P be a linear space of zero-diagonal W-by-W +matrices, and define the complete noncoordinate pool + + C(P) = {N = x y^T : y^T x = 1, off(N) in P, off(N) != 0}. + +The condition y^T x = 1 makes N a rank-one idempotent. Put + + V(P) = sum_{N in C(P)} im(N), + +and let e(P) be the number of matrix units E_ab, a != b, contained in P. +A subspace W ⊆ V(P) is invariant when N(W) ⊆ W for every N in C(P). The +action is irreducible when no subspace 0 < W < V(P) is invariant. + +**Theorem.** For every ambient width W ≥ 5 there is a pattern space P of +dimension 4 with e(P) = 0 whose complete pool acts irreducibly on a joint +image of dimension 5. Explicitly, on coordinates {0, 1, 2, 3, 4}, + + N_v = (e_0 + e_2)(e_1 + e_2)^T, + N_u = (e_1 + e_2)(e_0 + e_2)^T, + N_o = (e_0 + e_1 + e_2)(e_0 + e_1 + e_2)^T, + N_a = (e_2 + e_3)(e_0 + e_1 + e_3)^T, + N_b = (e_0 + e_2 + e_3 + e_4)(e_1 + e_4)^T, + +and P is the span of their off-diagonal patterns, padded by zero rows and +columns when W > 5. Thus C(P) = {N_v, N_u, N_o, N_a, N_b}, dim V(P) = 5, +and the action is irreducible. + +The first three projectors are the normal-form triple of #6921. On their +own three-dimensional image that triple is reducible. The two added +projectors are what make the joint image five-dimensional and the action +irreducible. This note does not reprove the pattern-dimension-at-most-3 +theorem, and it does not replace the four-cycle of #6962. + +The same hypotheses as those two results are in force: a complete +noncoordinate rank-one idempotent pool over F2, and no matrix unit in P. +The result is an existence proof. It is not an upper bound, and it is not +a classification of every pattern-dimension-4 pool. + +## 2. The five patterns + +Write x_v, y_v for the factors of N_v, and likewise for u, o, a, b. Each +pairing y · x equals 1: + + y_v · x_v = (e_1 + e_2) · (e_0 + e_2) = 1, + y_u · x_u = (e_0 + e_2) · (e_1 + e_2) = 1, + y_o · x_o = (e_0 + e_1 + e_2) · (e_0 + e_1 + e_2) = 1, + y_a · x_a = (e_0 + e_1 + e_3) · (e_2 + e_3) = 1, + y_b · x_b = (e_1 + e_4) · (e_0 + e_2 + e_3 + e_4) = 1. + +The off-diagonal patterns, with every unlisted row zero, are + + p_v: row 0 = e_1 + e_2, row 2 = e_1, + p_u: row 1 = e_0 + e_2, row 2 = e_0, + p_a: row 2 = e_0 + e_1 + e_3, row 3 = e_0 + e_1, + p_b: row 0 = e_1 + e_4, row 2 = e_1 + e_4, + row 3 = e_1 + e_4, row 4 = e_1. + +Their weights are 3, 3, 5 and 7. Adding the displayed rows gives +p_o = p_v + p_u, with + + row 0 = e_1 + e_2, row 1 = e_0 + e_2, row 2 = e_0 + e_1, + +which is the pattern of N_o. Thus p_o lies in span(p_v, p_u, p_a, p_b). + +These four patterns are independent. In a linear relation +α_v p_v + α_u p_u + α_a p_a + α_b p_b = 0, row 4 receives a contribution +only from p_b, and that row is e_1, so α_b = 0. Row 3 then receives a +contribution only from p_a, namely e_0 + e_1, so α_a = 0. Row 1 receives +a contribution only from p_u, so α_u = 0. Row 0 then receives e_1 + e_2 +from p_v, so α_v = 0. Hence dim P = 4, where P is the span of the four +patterns, padded by zero outside coordinates {0, 1, 2, 3, 4} when W > 5. + +## 3. No matrix unit, and no single-column pattern + +Every nonzero element of P is a nonempty sum of {p_v, p_u, p_a, p_b}. + +If the coefficient of p_b is 1, row 4 of the sum is e_1, and row 0 is + + (e_1 + e_4) + α_v (e_1 + e_2), + +which equals e_1 + e_4 or e_2 + e_4. Both have weight 2, and neither uses +only column 1, so the sum has at least two columns and weight at least 3. + +If the coefficient of p_b is 0 and the coefficient of p_a is 1, row 3 of +the sum is e_0 + e_1. That is already two columns and weight 2. + +If both of those coefficients are 0 and the sum is nonzero, the sum is +p_v, p_u, or p_v + p_u. The first has columns 1 and 2, the second has +columns 0 and 2, and the third has columns 0, 1 and 2. Each has weight +at least 3. + +Every nonzero pattern therefore has weight at least 2 and at least two +columns, so e(P) = 0. The same column count is the input to the +realizability argument in the next section. + +## 4. The pool is exactly the five projectors + +First let t ≥ 5, and suppose some pool element has image bit x_t = 1. +Row t of every matrix in P is zero, so the off-diagonal part of row t of +x y^T is zero. That row, with its diagonal entry removed, is y with +coordinate t cleared. Thus y = e_t. Idempotence gives the remaining bit +1. Column t of P is zero, so x vanishes off t. The pattern is zero, +which is excluded from C(P). If instead y_t = 1 and x_t = 0, column t +equals x and must vanish, so x = 0, contradicting the pairing. Every +pool element is therefore supported on {0, 1, 2, 3, 4}. It is enough to +classify patterns inside that coordinate block. The block is +five-dimensional as a vector space of coordinate masks, and P meets it +in the four-dimensional space already described. There are exactly +fifteen nonzero patterns. + +A nonzero pattern M = off(x y^T) can have a zero row on the support of +x only in one situation. If x_i = 1 and row i of M is zero, then y +vanishes off i. The pairing forces y = e_i, and M is supported in column +i. Section 3 says P contains no such nonzero pattern. Consequently every +realizable pattern in P has nonzero rows exactly on the support of x. +Each of those rows equals y with its own diagonal bit removed, so the +rows determine every off-support bit of y. A disagreement between two +rows on such a bit means that M has no rank-one idempotent lift. + +The fifteen patterns fall into two lists. + +**Realizable.** The rows force one covector, and the pairing equals 1. + +| pattern | forced image | forced covector | projector | +| --- | --- | --- | --- | +| p_v | e_0 + e_2 | e_1 + e_2 | N_v | +| p_u | e_1 + e_2 | e_0 + e_2 | N_u | +| p_v + p_u | e_0 + e_1 + e_2 | e_0 + e_1 + e_2 | N_o | +| p_a | e_2 + e_3 | e_0 + e_1 + e_3 | N_a | +| p_b | e_0 + e_2 + e_3 + e_4 | e_1 + e_4 | N_b | + +For p_v, row 0 forces y_1 = y_2 = 1 and y_3 = y_4 = 0, while row 2 forces +y_0 = 0. For p_u, row 1 forces y_0 = y_2 = 1 and y_3 = y_4 = 0, while row 2 +forces y_1 = 0. For p_v + p_u the three nonzero rows are e_1 + e_2, +e_0 + e_2 and e_0 + e_1; together they force every bit of +y = e_0 + e_1 + e_2, including y_3 = y_4 = 0. For p_a, row 2 forces +y_0 = y_1 = y_3 = 1 and y_4 = 0, while row 3 forces y_2 = 0. For p_b, row 4 +forces y_0 = y_2 = y_3 = 0 and y_1 = 1, while row 0 forces y_4 = 1. In each +case every covector bit is fixed by a row, so the pairing has one solution. + +**Unrealizable.** Two nonzero rows require opposite values of one +covector bit. The bit is off both row indices, so both rows constrain it. + +| sum | rows | bit | values | +| --- | --- | --- | --- | +| p_v + p_a | 0, 2 | y_1 | 1, 0 | +| p_u + p_a | 1, 2 | y_0 | 1, 0 | +| p_v + p_u + p_a | 1, 2 | y_0 | 1, 0 | +| p_v + p_b | 2, 3 | y_1 | 0, 1 | +| p_u + p_b | 0, 1 | y_2 | 0, 1 | +| p_v + p_u + p_b | 0, 1 | y_4 | 1, 0 | +| p_a + p_b | 0, 2 | y_1 | 1, 0 | +| p_v + p_a + p_b | 0, 2 | y_1 | 0, 1 | +| p_u + p_a + p_b | 0, 1 | y_2 | 0, 1 | +| p_v + p_u + p_a + p_b | 0, 1 | y_4 | 1, 0 | + +Each row of a sum is the sum of the corresponding basis rows from Section +2. For instance row 0 of p_v + p_a is e_1 + e_2, so it requires y_1 = 1, +while row 2 is e_1 + (e_0 + e_1 + e_3) = e_0 + e_3, so it requires y_1 = 0. +The other nine lines are the same one-bit comparison. None of these ten +patterns has a lift. + +Therefore C(P) = {N_v, N_u, N_o, N_a, N_b} at every width W ≥ 5. + +## 5. The joint image and the covectors + +The five images are + + x_v = e_0 + e_2, + x_u = e_1 + e_2, + x_o = e_0 + e_1 + e_2, + x_a = e_2 + e_3, + x_b = e_0 + e_2 + e_3 + e_4. + +Suppose a linear combination vanishes. Coordinate 4 appears only in x_b, +so that coefficient is 0. Coordinate 3 then appears only in x_a, so that +coefficient is 0. Coordinate 1 leaves the relation α_u + α_o = 0, and +coordinate 0 leaves α_v + α_o = 0. Coordinate 2 then reads +α_v + α_u + α_o = α_o = 0. The five images are independent. They lie in +E = span(e_0, e_1, e_2, e_3, e_4), so they are a basis of E. Section 4 +puts every image in E, and V(P) = E has dimension 5. + +The five covectors are + + y_v = e_1 + e_2, + y_u = e_0 + e_2, + y_o = e_0 + e_1 + e_2, + y_a = e_0 + e_1 + e_3, + y_b = e_1 + e_4. + +The same coordinate chase shows they are independent: coordinate 4 fixes +the coefficient of y_b, coordinate 3 fixes the coefficient of y_a, +coordinate 0 leaves β_u + β_o = 0, coordinate 1 leaves β_v + β_o = 0, and +coordinate 2 gives β_o = 0. Restricted to E they are a basis of E*. Their +common kernel on V(P) is zero. + +## 6. The hit digraph + +Draw a directed edge j → i, for distinct labels, when y_j · x_i = 1. The +six edges used below are + + a → v: (e_0 + e_1 + e_3) · (e_0 + e_2) = 1, + v → b: (e_1 + e_2) · (e_0 + e_2 + e_3 + e_4) = 1, + b → o: (e_1 + e_4) · (e_0 + e_1 + e_2) = 1, + o → a: (e_0 + e_1 + e_2) · (e_2 + e_3) = 1, + a → u: (e_0 + e_1 + e_3) · (e_1 + e_2) = 1, + u → a: (e_0 + e_2) · (e_2 + e_3) = 1. + +Thus (a → v → b → o → a) is a directed 4-cycle and (a → u → a) is a +directed 2-cycle. Each of v, b and o lies on the 4-cycle, and u lies on +the 2-cycle, so every vertex reaches a and is reached from a. The digraph +on {v, u, o, a, b} is strongly connected. + +**Cut lemma.** In a strongly connected digraph, every nonempty proper +vertex subset A has an edge into A from its complement. Indeed, take a +vertex p in A and a vertex q outside A. A directed path from q to p has +a last vertex outside A, and the next vertex of the path lies in A. + +Applied here: for every nonempty proper subset A of the five projectors, +some j outside A and some i in A satisfy y_j · x_i = 1. + +## 7. The action is irreducible + +Let W ⊆ V(P) be invariant, and let A be the set of pool labels whose +covector does not vanish on W. + +If i is in A, some vector of W is sent to x_i, so x_i lies in W. The span +of {x_i : i in A} is therefore contained in W. If j is outside A, then +y_j vanishes on W, so W is contained in the intersection of those kernels. + +The empty active set forces W into the common kernel, which Section 5 +shows is zero. The full active set forces W to contain every image, hence +W = V(P). Suppose A is nonempty and proper. The cut lemma supplies +y_j · x_i = 1 with i in A and j outside A. Then x_i lies in the span of +the active images and outside ker(y_j), so that span is not contained in +the complementary intersection. This contradicts the containment forced +by invariance. + +No proper nonzero subspace is invariant. The action on the +five-dimensional joint image is irreducible. + +The same three projectors without N_a and N_b are the normal-form triple. +On their image, the line span(x_u) is invariant: y_u · x_u = 1 with image +x_u, while y_v · x_u = 0 and y_o · x_u = 0. The two added projectors are +what breaks that line. y_b · x_u = 1 and the image x_b is outside the +line, so N_b carries x_u out of span(x_u). + +## 8. Evidence class and scope + +The argument above is a proof for one explicit pool, valid at every width +W ≥ 5. The fifteen-pattern list is the complete set of nonzero vectors in +this four-dimensional P; it is not a census of all four-dimensional pattern +spaces. The verifier repeats those fifteen weights and lifts, scans every +rank-one idempotent at widths 5, 6 and 7, checks the six digraph edges, +and enumerates every subspace of the joint image. The number of subspaces +of F2^5 is the sum of the Gaussian binomial coefficients, 374, including +the zero subspace and the whole space. That lattice check is corroboration. +The written argument does not depend on it. + +This existence result does not give a replacement upper bound. Dimension +6 and higher, at the same pattern dimension, stay open. A search that +finds no further example would not decide them: nothing here bounds the +ambient support of an arbitrary pattern space. The four-cycle of #6962 +remains the example that irreducible dimension 4 occurs, and the +dimension-at-most-3 theorem of #6921 is cited rather than reproved. The +parity pool of #6838 still shows that total dimension 5 can be reducible; +the pool in this note is a different one. + +The selected κ and its five framework assumptions are unchanged. The note +produces no rational-address word, native primitive, supplier admission, +or multiplication identity. + +## Open next questions + +The packaged question is whether some complete no-edge pool of pattern +dimension 4 acts irreducibly in joint-image dimension 6 or more. The pool +above attains 5, so any upper bound is at least 5. One explicit witness +with a written invariant-subspace check, or a scoped upper bound under +the same hypotheses, would be the next useful step. diff --git a/research/no-edge-dim4-image-five/README.md b/research/no-edge-dim4-image-five/README.md new file mode 100644 index 0000000000..18641f6bbb --- /dev/null +++ b/research/no-edge-dim4-image-five/README.md @@ -0,0 +1,98 @@ +# No-edge pattern dimension 4, joint image 5 + +**Result.** A complete no-edge pool of pattern dimension 4 can act +irreducibly on a joint image of dimension 5. For every ambient width at +least 5, the five projectors + +```text +N_v = (e_0 + e_2)(e_1 + e_2)^T, +N_u = (e_1 + e_2)(e_0 + e_2)^T, +N_o = (e_0 + e_1 + e_2)(e_0 + e_1 + e_2)^T, +N_a = (e_2 + e_3)(e_0 + e_1 + e_3)^T, +N_b = (e_0 + e_2 + e_3 + e_4)(e_1 + e_4)^T +``` + +are the complete pool of their pattern span. That span is four-dimensional +and contains no matrix unit. The joint image is the coordinate span of +e_0 through e_4, and the action is irreducible. **No new κ.** The selected +value remains `781451/250000000`. + +This is an existence proof under the same complete-pool and no-matrix-unit +hypotheses as #6921 and #6962. It is not an upper bound, and it is not a +classification of every pattern-dimension-4 pool. The first three +projectors are the normal-form triple, which by itself is reducible on a +three-dimensional image. N_a and N_b are the added data. + +## Scope and evidence + +Catalogue card: `bit-new-register-model`, priority revision 8, base commit +`17469fff78c22941280f04d39dc5a1faee09c840`. Scope status: **changed**. The +card asks for a new register alphabet. This package answers the open +question of #6962: whether irreducible joint image 5 occurs for a complete +no-edge pool in pattern dimension 4. The reason is recorded in +[TASK.json](TASK.json). The original native acceptance gate is unmet, and +the selected frontier is unchanged. + +[PROOF.md](PROOF.md) is the argument. Section 3 shows every nonzero pattern +has weight at least 2 and at least two columns. Section 4 uses that column +count to reconstruct every lift inside the fifteen-element pattern space, +then rules out support outside the first five coordinates. Section 6 +records a strongly connected hit digraph, and Section 7 turns that +connectivity into the invariant-subspace exclusion. + +[verify.py](verify.py) repeats the finite parts: the fifteen pattern +weights and lifts, the six digraph edges, the complete pool at widths 5, 6 +and 7, and every subspace of the joint image. The subspace count is 374, +the sum of the Gaussian binomial coefficients on F2^5. The normal-form +triple is retained as a reducible control, and its old invariant line is +checked to be broken by the full pool. These checks corroborate the +width-independent argument. They do not enumerate all four-dimensional +pattern spaces. + +Source pins are in [SOURCES.json](SOURCES.json). The catalogue and selected +record are provenance at the base commit. Full Git history is needed to +resolve them. Nothing here reruns the selected baseline as a scientific +replay. + +Overlap was checked on 2026-11-10 against upstream main +`17469fff78c22941280f04d39dc5a1faee09c840`. The question is the open item +in merged #6962 and in its finding, discussion comment 19507179. #6921 +stops at pattern dimension 3. A search of open upstream pull requests for +this question returned no match. #6785 is a one-edge exclusion. No match +is not a novelty certificate; those distinctions are from reading the +records. + +## Reproduce + +From the repository root, with Python 3.12 and the standard library only: + +```sh +python3 -B research/no-edge-dim4-image-five/verify.py +python3 -I -O -B research/no-edge-dim4-image-five/verify.py +python3 -B scripts/research_package.py --package research/no-edge-dim4-image-five --check-only +python3 -B scripts/research_package.py --package research/no-edge-dim4-image-five +``` + +The verifier prints `PASS_NO_EDGE_DIM4_IMAGE_FIVE`. + +## Open next questions + +1. **Irreducible dimension above 5, still at pattern dimension 4.** Can a + complete no-edge pool of pattern dimension 4 act irreducibly on a joint + image of dimension 6 or more? The pool above attains 5, so any upper + bound is at least 5. The smallest next step is one explicit pool with a + written invariant-subspace check, or a scoped upper bound under these + same hypotheses. No support reduction here makes an exhaustive search + finite, so a search that finds nothing would not be a proof. + +## Credit + +#6921 isolated the normal-form triple and proved the irreducible bound 3 +for pattern dimension at most 3; that theorem is not reproved, and the +triple is used here only as an explicit reducible subconfiguration. +#6962 showed that the bound 3 fails in pattern dimension 4 and left joint +image 5 open; the four-cycle is not redone. CubeJerry, #6838, for the +parity pool, which attains total dimension 5 and is reducible, so it is +not this witness. Nick Petalas, #5921, for the fiber lemma; this proof +reconstructs lifts from rows and does not rely on that lemma. Prepared by +unpaidmoon with substantial Cursor Grok assistance. New work is Apache-2.0. diff --git a/research/no-edge-dim4-image-five/SOURCES.json b/research/no-edge-dim4-image-five/SOURCES.json new file mode 100644 index 0000000000..41a0d8e4ed --- /dev/null +++ b/research/no-edge-dim4-image-five/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/no-edge-dim4-image-five/TASK.json b/research/no-edge-dim4-image-five/TASK.json new file mode 100644 index 0000000000..35b09af2d9 --- /dev/null +++ b/research/no-edge-dim4-image-five/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Whether a complete no-edge pool of pattern dimension 4 can act irreducibly on a joint image of dimension 5 or more.", + "scope_change_reason": "The card asks for a larger or nonabelian register alphabet. This package instead answers the open question of #6962: one explicit complete no-edge pattern-dimension-4 pool with irreducible joint image at least 5, or an upper bound under those hypotheses. No new alphabet, word, or kappa is claimed. The same card was already moved to scalar pattern-pool questions by #5921, #6838, #6921 and #6962.", + "bottleneck_link": "Side result. Irreducible joint image 5 occurs in pattern dimension 4, so a later word argument cannot quote an irreducible ceiling of 4 there. The original native acceptance gate remains unmet, and the selected frontier is unchanged.", + "budget_minutes": 60, + "stop_rule": "Stop once one explicit complete no-edge pool of pattern dimension 4 is proved to act irreducibly on a five-dimensional joint image at every width at least 5. Do not classify all pattern-dimension-4 pools or claim an upper bound.", + "outcome": "completed", + "evidence": "PROOF.md exhibits five rank-one idempotents whose patterns span a four-dimensional no-edge space, reconstructs every lift among the fifteen nonzero patterns, and shows that the hit digraph is strongly connected, so the action on the five-dimensional joint image is irreducible. verify.py repeats the pattern census, the width-5 through width-7 pool scan, the F2^5 subspace lattice, and the reducible normal-form control.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance with the pool search, the case analysis, and the package verifier. Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a complete no-edge pool of pattern dimension 4 act irreducibly on a joint image of dimension 6 or more?", + "why_it_matters": "The five-projector pool shows that irreducible dimension 5 occurs, so an upper bound must be at least 5, but it does not decide whether 5 is the maximum.", + "first_step": "Either give one explicit complete no-edge pattern-dimension-4 pool with joint-image dimension at least 6 and a written invariant-subspace check, or prove that 5 is an upper bound under these same hypotheses.", + "blocked_by": "No support reduction in this package bounds the search, and a search that finds no example would not be a proof." + } + ], + "coordination": { + "thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166", + "question_source": "https://github.com/CrocSwap/integer-mult-bounds/pull/6962", + "depends_on": [ + "https://github.com/CrocSwap/integer-mult-bounds/pull/6962", + "https://github.com/CrocSwap/integer-mult-bounds/pull/6921" + ] + } +} diff --git a/research/no-edge-dim4-image-five/VERIFY.json b/research/no-edge-dim4-image-five/VERIFY.json new file mode 100644 index 0000000000..8a2b415276 --- /dev/null +++ b/research/no-edge-dim4-image-five/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Fifteen-pattern weight and lift census, hit-digraph edges, complete pools at widths 5 through 7, F2^5 subspace lattice, normal-form reducible control, selected kappa unchanged." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same checks with assert statements disabled; the verifier raises SystemExit instead of using assert." + } + ] +} diff --git a/research/no-edge-dim4-image-five/verify.py b/research/no-edge-dim4-image-five/verify.py new file mode 100644 index 0000000000..5f1343260b --- /dev/null +++ b/research/no-edge-dim4-image-five/verify.py @@ -0,0 +1,353 @@ +#!/usr/bin/env python3 +"""Exact checks for one irreducible no-edge pool of pattern dimension 4. + +PROOF.md is the all-width argument. This program repeats the finite parts: +the fifteen-pattern weight and realizability census, the hit-digraph edges, +the width-5 through width-7 pool scan, and the subspace lattice of the +five-dimensional joint image. It also runs negative controls. It does not +use assert, so python -O does not skip checks. Standard library only. +""" + +import itertools +import json +from pathlib import Path + +MARKER = "PASS_NO_EDGE_DIM4_IMAGE_FIVE" +WIDTHS = (5, 6, 7) +# Order: v, u, o, a, b. The first two and their sum are the normal-form triple. +POOL = ( + (0b00101, 0b00110), # v: (e0+e2)(e1+e2)^T + (0b00110, 0b00101), # u: (e1+e2)(e0+e2)^T + (0b00111, 0b00111), # o: (e0+e1+e2)(e0+e1+e2)^T + (0b01100, 0b01011), # a: (e2+e3)(e0+e1+e3)^T + (0b11101, 0b10010), # b: (e0+e2+e3+e4)(e1+e4)^T +) +# Nonempty sums of the basis (v, u, a, b), written as coefficient tuples, +# that PROOF.md records as unrealizable, with one disagreeing covector bit. +# (coefficients, row_p, row_q, bit, value_on_row_p, value_on_row_q). +CONFLICTS = ( + ((1, 0, 1, 0), 0, 2, 1, 1, 0), + ((0, 1, 1, 0), 1, 2, 0, 1, 0), + ((1, 1, 1, 0), 1, 2, 0, 1, 0), + ((1, 0, 0, 1), 2, 3, 1, 0, 1), + ((0, 1, 0, 1), 0, 1, 2, 0, 1), + ((1, 1, 0, 1), 0, 1, 4, 1, 0), + ((0, 0, 1, 1), 0, 2, 1, 1, 0), + ((1, 0, 1, 1), 0, 2, 1, 0, 1), + ((0, 1, 1, 1), 0, 1, 2, 0, 1), + ((1, 1, 1, 1), 0, 1, 4, 1, 0), +) +CYCLE_EDGES = ( + ("a", "v"), + ("v", "b"), + ("b", "o"), + ("o", "a"), + ("a", "u"), + ("u", "a"), +) +LABELS = ("v", "u", "o", "a", "b") + + +def fail(message): + raise SystemExit("FAIL: " + message) + + +def require(condition, message): + if not condition: + fail(message) + + +def dot(left, right): + return (left & right).bit_count() & 1 + + +def pattern_mask(image, covector, width): + mask = 0 + for row in range(width): + if ((image >> row) & 1) == 0: + continue + for col in range(width): + if row != col and ((covector >> col) & 1): + mask |= 1 << (row * width + col) + return mask + + +def row_vector(mask, row, width): + bits = 0 + for col in range(width): + if (mask >> (row * width + col)) & 1: + bits |= 1 << col + return bits + + +def gaussian(masks): + pivots = {} + for mask in masks: + value = mask + while value: + bit = value & -value + known = pivots.get(bit) + if known is None: + for other, vector in list(pivots.items()): + if vector & bit: + pivots[other] = vector ^ value + pivots[bit] = value + break + value ^= known + return pivots + + +def in_span(pivots, mask): + value = mask + while value: + bit = value & -value + known = pivots.get(bit) + if known is None: + return False + value ^= known + return True + + +def span_vectors(pivots): + vectors = [0] + for vector in pivots.values(): + vectors += [old ^ vector for old in vectors] + return vectors + + +def gaussian_count(dimension): + total = 0 + for rank in range(dimension + 1): + numerator = 1 + denominator = 1 + for step in range(rank): + numerator *= (1 << dimension) - (1 << step) + denominator *= (1 << rank) - (1 << step) + total += numerator // denominator + return total + + +def basis_patterns(width): + """Return p_v, p_u, p_a, p_b at the given width.""" + images = (POOL[0], POOL[1], POOL[3], POOL[4]) + return tuple(pattern_mask(image, covector, width) for image, covector in images) + + +def combination(coefficients, width): + mask = 0 + for bit, pattern in zip(coefficients, basis_patterns(width)): + if bit: + mask ^= pattern + return mask + + +def implied_bit(mask, row, bit, width): + require(bit != row, "a row does not determine its own diagonal bit") + return (row_vector(mask, row, width) >> bit) & 1 + + +def single_column(mask, width): + columns = set() + for row in range(width): + for col in range(width): + if (mask >> (row * width + col)) & 1: + columns.add(col) + return len(columns) <= 1 + + +def realize(mask, width): + """Return idempotent lifts whose off-diagonal pattern is mask. + + For a pattern that is not supported in a single column, the image support + is exactly the set of nonzero rows, so the scan below is exhaustive. + """ + supports = [] + for row in range(width): + if row_vector(mask, row, width): + supports.append(row) + if not supports: + return [] + image = 0 + for row in supports: + image |= 1 << row + forced = {} + for row in supports: + bits = row_vector(mask, row, width) + if (bits >> row) & 1: + return [] + for col in range(width): + if col == row: + continue + value = (bits >> col) & 1 + previous = forced.get(col) + if previous is not None and previous != value: + return [] + forced[col] = value + free = [col for col in range(width) if col not in forced] + lifts = [] + for choice in range(1 << len(free)): + covector = 0 + for col, value in forced.items(): + if value: + covector |= 1 << col + for index, col in enumerate(free): + if (choice >> index) & 1: + covector |= 1 << col + if dot(image, covector) == 1 and pattern_mask(image, covector, width) == mask: + lifts.append((image, covector)) + return lifts + + +def idempotents(width): + for image in range(1, 1 << width): + pivot = (image & -image).bit_length() - 1 + free = [index for index in range(width) if index != pivot] + for choice in range(1 << (width - 1)): + covector = 0 + for bit, index in enumerate(free): + if (choice >> bit) & 1: + covector |= 1 << index + if dot(image, covector) == 0: + covector |= 1 << pivot + yield image, covector + + +def subspaces_of(universe): + """Every subspace of the ambient span `universe`, which includes 0.""" + empty = frozenset([0]) + found = {empty} + pending = [empty] + while pending: + current = pending.pop() + for vector in universe: + if vector in current: + continue + enlarged = frozenset(old ^ vector for old in current) | current + if enlarged not in found: + found.add(enlarged) + pending.append(enlarged) + return found + + +def is_invariant(space, projectors): + members = set(space) + for image, covector in projectors: + if any(dot(covector, vector) for vector in members) and image not in members: + return False + return True + + +def check_pattern_space(): + patterns = basis_patterns(5) + require(len(gaussian(patterns)) == 4, "basis patterns are not independent") + weights = [] + realizable = [] + for coefficients in itertools.product((0, 1), repeat=4): + if coefficients == (0, 0, 0, 0): + continue + mask = combination(coefficients, 5) + weight = mask.bit_count() + weights.append(weight) + require(weight >= 2, "pattern weight below 2 for %s" % (coefficients,)) + require(not single_column(mask, 5), "single-column pattern %s" % (coefficients,)) + lifts = realize(mask, 5) + if lifts: + realizable.append((coefficients, lifts)) + require(sorted(weights)[0] == 3, "minimum pattern weight moved: %s" % (sorted(weights)[0],)) + require(len(realizable) == 5, "expected 5 realizable patterns, found %s" % len(realizable)) + expected = { + (1, 0, 0, 0): POOL[0], + (0, 1, 0, 0): POOL[1], + (1, 1, 0, 0): POOL[2], + (0, 0, 1, 0): POOL[3], + (0, 0, 0, 1): POOL[4], + } + for coefficients, lifts in realizable: + require(len(lifts) == 1, "more than one lift for %s" % (coefficients,)) + require(lifts[0] == expected[coefficients], "unexpected lift %s -> %s" % (coefficients, lifts)) + seen = {item[0] for item in realizable} + for coefficients, row_p, row_q, bit, value_p, value_q in CONFLICTS: + require(coefficients not in seen, "conflict listed for a realizable pattern %s" % (coefficients,)) + mask = combination(coefficients, 5) + require(implied_bit(mask, row_p, bit, 5) == value_p, "row value drifted for %s" % (coefficients,)) + require(implied_bit(mask, row_q, bit, 5) == value_q, "row value drifted for %s" % (coefficients,)) + require({item[0] for item in CONFLICTS} | seen == set(itertools.product((0, 1), repeat=4)) - {(0, 0, 0, 0)}, + "the conflict table does not cover every unrealizable pattern") + + +def check_pool_scan(): + for width in WIDTHS: + pivots = gaussian(pattern_mask(image, covector, width) for image, covector in POOL) + require(len(pivots) == 4, "pattern dimension drifted at width %s" % width) + for row in range(width): + for col in range(width): + if row != col and in_span(pivots, 1 << (row * width + col)): + fail("matrix unit entered the pattern space at width %s" % width) + found = [] + for image, covector in idempotents(width): + mask = pattern_mask(image, covector, width) + if mask and in_span(pivots, mask): + found.append((image, covector)) + require(sorted(found) == sorted(POOL), + "width %s pool %s" % (width, sorted(found))) + + +def check_ranks_and_edges(): + images = [image for image, _covector in POOL] + covectors = [covector for _image, covector in POOL] + require(len(gaussian(images)) == 5, "images do not span a five-dimensional space") + require(len(gaussian(covectors)) == 5, "covectors do not span a five-dimensional space") + for index in range(5): + require(in_span(gaussian(images), 1 << index), "coordinate e_%s is outside the image span" % index) + require(in_span(gaussian(covectors), 1 << index), "coordinate functional e_%s is outside the covector span" % index) + label_index = {label: index for index, label in enumerate(LABELS)} + for source, target in CYCLE_EDGES: + image = images[label_index[target]] + covector = covectors[label_index[source]] + require(dot(covector, image) == 1, "missing hit edge %s -> %s" % (source, target)) + common = [vector for vector in range(32) if all(dot(covector, vector) == 0 for covector in covectors)] + require(common == [0], "common kernel is %s" % (common,)) + + +def check_subspace_lattice(): + universe = span_vectors(gaussian(image for image, _covector in POOL)) + require(len(universe) == 32, "joint image is not all of the coordinate five-space") + spaces = subspaces_of(universe) + require(len(spaces) == gaussian_count(5), + "subspace census %s != %s" % (len(spaces), gaussian_count(5))) + invariant = [space for space in spaces if len(space) not in (1, 32) and is_invariant(space, POOL)] + require(invariant == [], "found %s invariant subspaces" % len(invariant)) + + +def check_normal_form_control(): + triple = POOL[:3] + universe = span_vectors(gaussian(image for image, _covector in triple)) + require(len(universe) == 8, "normal-form image is not three-dimensional") + line = frozenset((0, POOL[1][0])) + require(line <= frozenset(universe), "the control line is outside the normal-form image") + require(is_invariant(line, triple), "normal-form line failed to be invariant") + require(not is_invariant(line, POOL), "the extra projectors left the normal-form line invariant") + spaces = subspaces_of(universe) + require(len(spaces) == gaussian_count(3), "normal-form lattice count drifted") + invariant = [space for space in spaces if len(space) not in (1, 8) and is_invariant(space, triple)] + require(line in invariant, "normal-form census missed the invariant line") + + +def check_selected_frontier_untouched(): + selected = json.loads(Path("certificates/selected-result.json").read_text(encoding="utf-8")) + require(selected["kappa"] == "781451/250000000", "selected kappa moved") + require(selected["decimal"] == "0.003125804", "selected decimal moved") + + +def main(): + check_pattern_space() + check_pool_scan() + check_ranks_and_edges() + check_subspace_lattice() + check_normal_form_control() + check_selected_frontier_untouched() + print(MARKER) + + +if __name__ == "__main__": + main()