Skip to content

Research bounded E6 one-extra frame decoder screen #2240

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Mister-Meeseeks merged 1 commit into from
Oct 15, 2026
Merged

Research bounded E6 one-extra frame decoder screen #2240

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
288 changes: 288 additions & 0 deletions research/e6-one-extra-frame-seed4dd9/CERTIFICATE.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,288 @@
{
"schema_version": 1,
"status": "scoped-negative-result",
"base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
"selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32",
"assignment_seed": "4dd9ff38bfc63aa200c17c947da92d9e",
"task_id": "complex-rank-shape-decoder",
"priority_revision": 4,
"root_input": {
"source": "research/root-unit-decoder-lemmas/lib/ade.py:E6b/E8 line order",
"root_lines": 36,
"canonical_root_sha256": "d2d26919a71a2f9a007d3c43f9806cb85a7142ebb45481ac4ad5fe6db8591263",
"basis_root_indices": [
0,
1,
2,
4,
6,
20
],
"ambient_basis_columns": [
0,
3,
4,
5,
6,
7
],
"basis_gram": [
[
"2",
"0",
"1",
"1",
"1",
"1"
],
[
"0",
"2",
"1",
"1",
"1",
"0"
],
[
"1",
"1",
"2",
"1",
"1",
"1"
],
[
"1",
"1",
"1",
"2",
"1",
"1"
],
[
"1",
"1",
"1",
"1",
"2",
"1"
],
[
"1",
"0",
"1",
"1",
"1",
"2"
]
],
"pairing_B0_rank_F2": 7
},
"model": {
"terms": 7,
"pairing": "B0_tt=1; off-diagonal B0_ts=1 iff Gram G_ts=0",
"per_term_floor_w": 5,
"fully_charged_cost": "sum(max(5, rank_F2(B0[R_j,A_j])))",
"raw_cost": "sum(rank_F2(B0[R_j,A_j]))",
"identity": "G = sum_{i=1}^6 X e_i (X(H e_i-lambda a_i a))^T + (Xa)(lambda Xa)^T"
},
"positive_controls": {
"six_term_reference_ranks": [
6,
7,
6,
6,
6,
6
],
"six_term_reference_raw_and_charged_cost": 37,
"one_extra_exact_identity_fixtures": 2
},
"negative_controls": [
"wrong sign on the seventh correction fails exact Gram identity",
"omitting the seventh term fails exact Gram identity",
"turning on a B0 edge between nonorthogonal roots fails admissibility"
],
"initial_root_direction_slice": {
"directions": 36,
"support_cells": 566,
"minimum_raw": 42,
"minimum_charged": 42
},
"bounded_domain": {
"root_directions": 36,
"projective_ternary_directions": 364,
"unique_union_directions": 365,
"lambda_domain": "all nonzero rational lambda; exact nonzero breakpoints and one rational representative per open interval",
"support_cells": 4672,
"all_support_cells_have_seven_active_terms": true,
"min_cells_per_direction": 6,
"max_cells_per_direction": 36,
"sum_distinct_nonzero_breakpoints": 1971
},
"result": {
"minimum_raw_cost": 40,
"minimum_fully_charged_cost": 40,
"charged_cost_histogram": {
"40": 6,
"41": 6,
"42": 12,
"43": 143,
"44": 4505
},
"raw_cost_histogram": {
"40": 6,
"41": 6,
"42": 12,
"43": 143,
"44": 4505
},
"no_raw_or_charged_cost_at_most_35": true,
"minimum_witnesses": [
{
"direction_index": 92,
"a": [
"0",
"1",
"0",
"1",
"1",
"0"
],
"lambda": "1",
"ranks": [
6,
6,
6,
5,
5,
6,
6
],
"raw": 40,
"charged": 40
},
{
"direction_index": 110,
"a": [
"0",
"1",
"1",
"0",
"1",
"0"
],
"lambda": "1",
"ranks": [
6,
6,
5,
6,
5,
6,
6
],
"raw": 40,
"charged": 40
},
{
"direction_index": 116,
"a": [
"0",
"1",
"1",
"1",
"0",
"0"
],
"lambda": "1",
"ranks": [
6,
6,
5,
5,
6,
6,
6
],
"raw": 40,
"charged": 40
},
{
"direction_index": 162,
"a": [
"1",
"-1",
"0",
"0",
"0",
"1"
],
"lambda": "1",
"ranks": [
5,
6,
6,
6,
6,
5,
6
],
"raw": 40,
"charged": 40
},
{
"direction_index": 282,
"a": [
"1",
"0",
"1",
"1",
"1",
"1"
],
"lambda": "1",
"ranks": [
6,
7,
5,
5,
5,
6,
6
],
"raw": 40,
"charged": 40
},
{
"direction_index": 363,
"a": [
"1",
"1",
"1",
"1",
"1",
"1"
],
"lambda": "1",
"ranks": [
5,
6,
6,
6,
6,
5,
6
],
"raw": 40,
"charged": 40
}
]
},
"limits": [
"Only the rank-one redundant extension of this pinned six-term Gram factorization is searched.",
"The direction set is the union of the 36 E6 root lines and all projective {-1,0,1}^6 directions in the pinned basis.",
"No claim is made about arbitrary rational directions, arbitrary seven-term decoders, sparse pairings, or other decoder identities.",
"No source/copy/frame/hosting/restoration/precision/interface supplier mapping or kappa improvement is established."
]
}
57 changes: 57 additions & 0 deletions research/e6-one-extra-frame-seed4dd9/OVERLAP.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,57 @@
{
"schema_version": 1,
"query": {
"command": "python3 scripts/find_overlap.py --offline --task complex-rank-shape-decoder --limit 40 --json",
"searched_at": "2026-10-15T01:36:12.289372+00:00",
"status": "POSSIBLE_OVERLAP_NOT_A_NOVELTY_CERTIFICATE",
"coverage": {
"open_prs": {
"fetched_at": "2026-10-15T01:35:36.447127+00:00",
"complete_pagination": true,
"records": 473
},
"discussions": {
"fetched_at": "2026-10-15T01:32:07.707839+00:00",
"complete_pagination": true,
"records": 934
}
},
"direct_live_check": "After package verification and immediately before PR submission, reran the task overlap query against the fresh complete snapshot, queried live Discussion #1166 comments and replies, and fetched current metadata for PRs #2228, #2137 and #2232. The only E6 m=7 claim is this cycle claim #18937856; scope update #18937916 adds no competing claim. PR #2228 and #2137 remain open and mergeable at the pinned heads; PR #2232 also remains open and mergeable at the pinned head."
},
"nearest": [
{
"reference": "Discussion #1166 comment #18936173",
"url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18936173",
"scope": "Unclaimed unrestricted question whether E6 admits m=7 cost <=35 or D5 m=6 cost <=18; this package selects only a bounded E6 mechanism family."
},
{
"reference": "Discussion #1166 claim #18937856",
"url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-18937856",
"scope": "This cycle\u2019s claim for the one-extra rank-one extension; no competitor in the live thread."
},
{
"pr": 2228,
"head": "ad1757e319225f3a5b86e3d3fa72897bd9f6db40",
"state": "open, mergeable",
"scope": "Dense-pairing root-code floors; explicitly leaves overcomplete E6 m=7 open."
},
{
"pr": 2137,
"head": "6a022d50e21bdcf2014a26937a34d44eed3473f0",
"state": "open, mergeable",
"scope": "Rank-four E6 B0 coordinate-form decoders."
},
{
"pr": 2232,
"head": "3391f27dd0f226f0e1ead8b2b829eb6d3ec567d3",
"state": "open, mergeable",
"scope": "Rank-four projected-Gram E6 screen with adapted pairing; same unit but fewer terms and variable pairing."
},
{
"discussion": 1622,
"scope": "Overcomplete E8 decoder; different root unit."
}
],
"scope_distinction": "Seven terms via one exact redundant rank-one frame; fixed Gram G and dense B0; finite root plus ternary directions; all rational lambda support cells. Not arbitrary E6 decoders, not rank-four screens and not an incumbent supplier profile.",
"selected_frontier_changed": false
}
52 changes: 52 additions & 0 deletions research/e6-one-extra-frame-seed4dd9/PROOF.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@
# Exact statement and support-cell proof

## Statement

Fix the 36 E6 root lines in the canonical order reconstructed from the pinned `ade.E6b()` source, the six-row rational basis chosen by its first independent root lines, and the dense pairing `B0` with `B0_tt=1` and off-diagonal `B0_ts=1` exactly when `G_ts=0`. Let `X` be the exact root-coordinate matrix and `H` the Gram matrix of the six basis roots, so `G=XHX^T`.

For each direction `a` in the union of (i) the 36 projective E6 root-coordinate rows and (ii) the 364 projective nonzero vectors in `{-1,0,1}^6`, and each nonzero rational `lambda`, form

```text
p_i = X e_i, q_i = X(H e_i - lambda a_i a), i=1,...,6,
p_7 = X a, q_7 = lambda X a.
```

Across all such directions and rational `lambda`, the least sum of the seven block ranks `r_j=rank_F2 B0[supp(p_j),supp(q_j)]` is 40. The least Theorem C charge `sum_j max(5,r_j)` is also 40. This is a finite statement about this declared family, not all seven-term decoders.

## Identity and admissibility

In the six-dimensional coefficient space,

```text
sum_{i=1}^6 e_i (H e_i - lambda a_i a)^T + a(lambda a)^T
= H^T - lambda a a^T + lambda a a^T
= H,
```

because `H` is symmetric. Multiplying on the left by `X` and on the right by `X^T` gives `sum_j p_j q_j^T=G`. Each root has norm squared 2, and `B0` has ones only on the diagonal and off-diagonal orthogonal pairs, so `B0` is admissible for this Gram decoder. The verifier reconstructs the 120 E8 root lines, filters the pinned A2-orthogonal E6 subsystem, derives `X` over `Q`, and checks `X H X^T` against all ambient inner products exactly.

The basis root indices are `[0,1,2,4,6,20]` and the first nonsingular ambient coordinate minor is `[0,3,4,5,6,7]`. The exact basis Gram and root-input digest are in [CERTIFICATE.json](CERTIFICATE.json). The F2 rank of `B0` is 7; Theorem C's per-total floor for this unit is `w=5`.

## Why the lambda census is exhaustive

The supports of `p_1,...,p_7` do not depend on `lambda`. For `lambda != 0`, the support of `q_7=lambda Xa` is also fixed. Each coordinate of each other right factor is affine in `lambda`:

```text
q_i(t) = X_t H e_i - lambda * a_i * (X_t a).
```

If its slope is nonzero, it can change zero/nonzero status only at the exact rational breakpoint

```text
lambda = (X_t H e_i) / (a_i * X_t a).
```

If the slope is zero, the coordinate is either identically zero or never zero, so it adds no breakpoint. For each direction the verifier takes the union of every nonzero breakpoint with `0`, evaluates each nonzero breakpoint, and selects one rational point in every open interval, including the two unbounded intervals. The zero point is excluded from the decoder domain but retained as a cut. Thus every allowed rational `lambda` has exactly the same seven supports as one enumerated point. All seven terms are nonzero at every enumerated point; the verifier rejects a degenerate total instead of charging it the per-total floor.

The full union has 365 directions and 1,971 distinct nonzero breakpoints across them. Including 0 as a cut, this gives `2 * (365 + 1,971) = 4,672` point/interval representatives. The 36-root-direction initial slice has 247 nonzero breakpoints and 566 representatives.

## Cost computation and result

For each support pair, binary Gaussian elimination computes `r_j` exactly over `F2`. The raw sum is `sum r_j`; the fully charged sum is `sum max(5,r_j)`. Both histograms and all six minimum witnesses appear in [CERTIFICATE.json](CERTIFICATE.json). The minimum witness directions use `lambda=1`; their raw and charged cost is 40. The six-term reference factorization is checked independently as an exact identity and has ranks `(6,7,6,6,6,6)`, cost 37. The separate square-decoder lower benchmark of 36 comes from the open request and is not used in the finite result.

The verifier also checks two positive exact identities, and negative controls for a reversed correction sign, an omitted seventh term, and an inadmissible pairing edge. No arithmetic for sources, copying, frames, hosting, restoration, precision, interfaces or recursive children is supplied by this factorization; the result therefore makes no multiplication-bound or `kappa` claim.
Loading
Loading