Bound E6 and E7 F2 shadow minranks by 8 and 11 (no new κ)

research/e6-e7-shadow-minrank-upper/README.md

@@ -0,0 +1,131 @@
+# F2 shadow minranks of the E6 and E7 root lines: upper bounds 8 and 11
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Claim type: finite exact certificate. No new κ.** On the root lines of E6
+and E7, explicit F2 matrices with unit diagonal and zeros on every orthogonal
+pair have exact F2 rank 8 and 11. Combined with the lower bounds cited from
+DreamingOfClouds's [PR #2277](https://github.com/CrocSwap/integer-mult-bounds/pull/2277):
+
+```text
+mr₂(Γ_E6) ∈ {7, 8},        8 ≤ mr₂(Γ_E7) ≤ 11.
+```
+
+Before this package, no upper bound was recorded for either value. PR #2277
+(`research/overcomplete-and-realisation-floors`, §8 Open next question 5)
+asks for both exact values. This package answers the upper side and leaves
+both exact values open.
+
+## Object
+
+Let `L` be the 36 E6 or 63 E7 root lines, one representative per `±` pair.
+A **shadow** is an F2 matrix `N` indexed by `L` with
+
+- `N_tt = 1` for every line `t`;
+- `N_ts = 0` whenever `t ≠ s` are orthogonal;
+- entries on non-orthogonal pairs free.
+
+`mr₂(Γ)` is the minimum F2 rank of a shadow. This is the definition used in
+PR #2277 §9.2 (SAT-2). In graph terms it is Haemers's F2 minrank of the
+non-orthogonality graph. By PR #2277's shadow lemma, a shadow of rank at most
+`m` is what a B-independent F2 certificate needs to certify all lines of a
+decoder with `m` terms.
+
+## Evidence
+
+[WITNESSES.json](WITNESSES.json) stores `N = U Vᵀ` with F2 factors `U`, `V` of
+widths 8 (E6) and 11 (E7). The lines are stored explicitly as E8 roots in
+doubled coordinates. The anchors are one root (E7, the orthogonal complement
+of an A1) or two roots with inner product ±4 (E6, the complement of an A2).
+
+[verify.py](verify.py) uses the standard library only. It:
+
+1. rebuilds all 240 E8 roots and checks that the stored lines are exactly the
+   lines orthogonal to the stored anchors (36 and 63 lines);
+2. checks every one of the 36² and 63² entries against the pattern: 36 and 63
+   unit diagonal entries, 270 and 945 orthogonal pairs (each in both orders)
+   forced to zero;
+3. computes the exact F2 rank of `N` by elimination: 8 and 11;
+4. rejects two mutations per unit, a cleared diagonal entry and a set
+   orthogonal entry, and calibrates the rank routine;
+5. enumerates every pairwise non-orthogonal 7-set and 8-set of E7 lines and
+   counts exact covers of the 63 lines by nine 7-sets (see Limitations).
+
+Output:
+
+```text
+PASS E6: 36 lines, 270 orthogonal pairs forced zero, 36 unit diagonal entries, 142/720 free entries set; exact F2 rank 8 <= 8
+PASS E6 controls: diagonal and orthogonal-entry mutations rejected; rank helper calibrated
+PASS E7: 63 lines, 945 orthogonal pairs forced zero, 63 unit diagonal entries, 321/2016 free entries set; exact F2 rank 11 <= 11
+PASS E7 controls: diagonal and orthogonal-entry mutations rejected; rank helper calibrated
+PASS E7 clique cover: no 8-set of pairwise non-orthogonal lines; 288 7-sets; 0 partitions of the 63 lines into nine 7-sets
+PASS e6-e7-shadow-minrank-upper: mr2(Gamma_E6) <= 8 and mr2(Gamma_E7) <= 11
+```
+
+The witnesses were found with a CaDiCaL search of the `U Vᵀ` encoding.
+[search_witness.py](search_witness.py) reproduces that search. It is optional,
+needs `python-sat`, and is not part of the registered replay. Fresh runs may
+return different witnesses; two such regenerated witnesses also passed
+`verify.py` before submission.
+
+## Reproduce
+
+From the repository root:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/e6-e7-shadow-minrank-upper/verify.py
+python3.12 -B scripts/research_package.py --package research/e6-e7-shadow-minrank-upper
+```
+
+Optional witness search (needs `python-sat`):
+
+```sh
+cd research/e6-e7-shadow-minrank-upper
+python3.12 -B search_witness.py E6 8 /tmp/e6.json 60
+python3.12 -B search_witness.py E7 11 /tmp/e7.json 60
+```
+
+## Limitations
+
+- The lower bounds 7 (E6) and 8 (E7) are PR #2277's DRAT-verified SAT-2
+  results. They are cited, not re-run.
+- Search failures are not proofs. Plain CaDiCaL runs, each fixing `U` on
+  one maximum set of pairwise orthogonal lines (4 for E6, 7 for E7), did not
+  finish: E6 rank 7 (stopped after 12 minutes), E7 rank 8
+  (stopped after 12 minutes), E7 rank 9 (600 s limit) and E7 rank 10 (150 s
+  limit). No UNSAT claim is made for any of them.
+- Only F2 is covered. Larger fields of characteristic 2 remain open, as in
+  PR #2277 §8.5; an F2 witness also works over every extension field, so the
+  upper bounds hold there.
+- No decoder, decoder floor, supplier, invoice or κ consequence is claimed.
+  The global fitting minrank of PR #2277 SAT-1 is a different problem (zeros
+  on non-orthogonal pairs) and is not touched.
+
+One structural finding narrows the E7 search. The largest pairwise
+non-orthogonal sets of E7 lines have size 7 (288 of them). An exhaustive
+exact-cover count in `verify.py` finds no partition of the 63 lines into nine such sets.
+So rank 9 cannot come from an all-ones block-diagonal clique cover. This is a
+statement about that one construction, not about rank 9.
+
+## Open next questions
+
+The structured versions are in [TASK.json](TASK.json).
+
+1. **Is `mr₂(Γ_E6)` 7 or 8?** Rank 7 would equal the global fitting minrank
+   of SAT-1. First step: rerun rank 7 with symmetry breaking under W(E6). A
+   possible model, not checked here, is the 36 non-singular points of an
+   elliptic quadric in F2⁶. Keep a DRAT proof if the result is UNSAT.
+2. **Which of 8, 9, 10, 11 is `mr₂(Γ_E7)`?** Decide rank 10 first. The 63
+   lines carry an Sp(6,2) structure that gives strong symmetry breaking.
+3. **Do extension fields of characteristic 2 lower either value?** Encode
+   GF(4) entries and repeat the E6 rank-7 test.
+
+## Credit
+
+DreamingOfClouds's PR #2277 supplies the shadow lemma, the definition of
+`mr₂(Γ)`, the lower bounds `mr₂(Γ_E6) ≥ 7` and `mr₂(Γ_E7) ≥ 8`, the E8/E7/E6
+line construction this package follows, and the open question. Those results
+are used as cited premises, not re-verified here. The `U Vᵀ` Tseitin encoding
+follows that package's `lib/satgen.py`. New here: the two explicit witnesses,
+their standalone checker and the exact-cover negative for E7. Independent
+human and formal proof-kernel review are unclaimed.

research/e6-e7-shadow-minrank-upper/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/overcomplete-and-realisation-floors/README.md",
+      "usage": "input",
+      "git_blob": "04894070db67d13a67f8587760b227e44d182671",
+      "sha256": "4128824937445ed3de10307da5cf1347a499da33f7ca8cdcf5297426a22b191a"
+    }
+  ]
+}

research/e6-e7-shadow-minrank-upper/TASK.json

@@ -0,0 +1,87 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "docs/research/recursive-invoice-preflight.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "coframe",
+      "signed moment",
+      "5693",
+      "5698"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Upper bounds for the F2 shadow minranks mr2(Gamma_E6) and mr2(Gamma_E7) left open in PR #2277 (research/overcomplete-and-realisation-floors, Open next question 5): minimum F2 rank of a matrix on the 36 E6 or 63 E7 root lines with unit diagonal and zeros on every orthogonal pair.",
+  "scope_change_reason": "Side result on the decoder-cost shadow lemma, not a decoder or coframe change. It answers part of a precisely stated open question in the decoder-floor lineage and needs no supplier or invoice.",
+  "bottleneck_link": "Side result. PR #2277's shadow lemma bounds the cost of any exact root-code decoder by rank_L(B o N). A rank bound on N limits how far F2-valued B-independent shadows can certify decoder floors; no kappa, decoder or supplier consequence is claimed.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified improvement: explicit witnesses giving new upper bounds. Do not continue into the E6 rank-7 or E7 rank-8..10 decision within the 60-minute budget.",
+  "outcome": "partial",
+  "evidence": "WITNESSES.json gives N = U V^T over F2 with U, V of widths 8 (E6) and 11 (E7). verify.py rebuilds both line sets from E8, checks all 1296 and 3969 pattern entries, computes exact F2 ranks 8 and 11, and rejects a diagonal and an orthogonal-entry mutation. With the cited PR #2277 lower bounds: mr2(Gamma_E6) in {7,8}, 8 <= mr2(Gamma_E7) <= 11.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Is mr2(Gamma_E6) equal to 7 or 8?",
+      "why_it_matters": "It is the last undecided value for E6; rank 7 would match the global fitting minrank of SAT-1.",
+      "first_step": "Run the rank-7 instance with symmetry breaking under W(E6), possibly via an elliptic-quadric model of the 36 lines (not checked here), and keep a DRAT proof if UNSAT.",
+      "blocked_by": "A plain CaDiCaL run fixing U on one maximum orthogonal 4-set was stopped unfinished after 12 minutes."
+    },
+    {
+      "question": "What is mr2(Gamma_E7) in {8,9,10,11}?",
+      "why_it_matters": "It fixes the exact F2 shadow capacity on E7; the lower bound is one above T = 7.",
+      "first_step": "Decide rank 10 first. The 63 lines carry the Sp(6,2) structure, which gives strong symmetry breaking.",
+      "blocked_by": "Plain CaDiCaL runs did not finish: rank 8 stopped after 12 minutes, rank 9 at a 600 s limit, rank 10 at a 150 s limit. No partition of the 63 lines into nine pairwise non-orthogonal 7-sets exists (verify.py), so the clique-cover route to rank 9 is closed."
+    },
+    {
+      "question": "Do larger fields of characteristic 2 lower either value?",
+      "why_it_matters": "PR #2277 section 8.5 leaves characteristic-2 extension fields open; the witnesses here are F2 matrices and transfer upward unchanged.",
+      "first_step": "Encode GF(4) entries and repeat the rank-7 E6 test.",
+      "blocked_by": "Not attempted."
+    }
+  ]
+}

research/e6-e7-shadow-minrank-upper/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/e6-e7-shadow-minrank-upper/WITNESSES.json",
+    "research/overcomplete-and-realisation-floors/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Rebuild the E6/E7 line sets from E8; check unit diagonal and every orthogonal-pair zero of N = U V^T; exact F2 ranks 8 and 11; diagonal and orthogonal-entry mutation controls rejected."
+    }
+  ]
+}