Prove P112 quadratic extension threshold is exactly 7 (no new κ)

research/p112-eight-deletion-extension-failure/README.md

@@ -0,0 +1,88 @@
+# Quadratic extension on P112 fails at eight deletions
+
+**Finite exact certificate; no new κ.** The global quadratic-extension
+threshold left open by
+[PR5697](https://github.com/CrocSwap/integer-mult-bounds/pull/5697) is
+exactly **7**.
+
+## Result
+
+Use the doubled E8 root lines, FRAME0 and P112 of Josie Elliston's
+[PR1650](https://github.com/CrocSwap/integer-mult-bounds/pull/1650). For
+X in P112 let L = P112 minus X and let M_L be the incidence matrix of all
+orthogonal eight-line frames contained in L. Global quadratic extension
+means ker(M_L) is exactly the 35-dimensional space of restrictions of
+ambient trace-zero quadratics.
+
+PR5697 proves extension for every |X| <= 7. This package shows that it
+fails for some |X| = 8. The maximum threshold is therefore exactly 7.
+
+Each of the 1260 frames avoiding FRAME0 has eight lines, and every P112
+line lies in 90 of them. For a line l, the other lines share 10 such frames
+with l (51 lines) or 15 (8 lines). Call those eight the heavy octet X_l.
+Every live frame through l meets X_l, so deleting X_l isolates l.
+
+The 112 lines produce 14 distinct octets, and they pair off. Deleting one
+octet isolates exactly the eight lines of its partner octet. For each of the
+14 octets, exact rational elimination gives:
+
+| Quantity | Value |
+|---|---:|
+| live lines | 104 |
+| live frames | 648 |
+| rank of M_L over Q | 62 |
+| dim ker(M_L) | 42 |
+| dim of quadratic restrictions to L | 35 |
+| dim of (quadratics + isolated-line indicators) | 42 |
+
+The kernel is seven dimensions larger than the quadratic restrictions, so
+extension fails. The excess is fully explained: the eight isolated-line
+indicator vectors and the quadratics span the whole kernel.
+
+The PR1668 eight-deletion fixtures recorded in PR5697 keep extension
+(rank 69). Those are D failures with extension intact. The octets here
+are extension failures. Eight deletions therefore contain both kinds.
+
+## Claim type and limits
+
+- Finite exact certificate for 14 explicit deletion sets: exact rational
+  ranks, with no modular or floating-point step.
+- The threshold value 7 combines this certificate with PR5697's theorem for
+  |X| <= 7. That theorem is cited, not rechecked here.
+- No classification of all eight-deletion failures, no new rigidity floor,
+  decoder, supplier, invoice or κ. The selected frontier is unchanged.
+- Author-checked only. Independent human and proof-kernel review are unclaimed.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+python3.12 -B research/p112-eight-deletion-extension-failure/verify.py
+python3.12 -B scripts/research_package.py --package research/p112-eight-deletion-extension-failure
+```
+
+Expected status: `PASS_P112_EIGHT_DELETION_EXTENSION_FAILURE` (about 15 s).
+The verifier pins and authenticates the PR1650 geometry source
+`research/complex-rank8-rigidity-p105/verify.py`. It also runs controls. All
+seven-subsets of one octet isolate nothing and have the PR5697 rank
+|L| - 35. A damaged octet fails to isolate its line.
+
+## Open next questions
+
+1. Classify all eight-deletion failures of global extension up to the FRAME0
+   stabilizer. A greedy eight-set found during this work isolates one line
+   and has kernel 37. It is not one of the octets, so isolation by a heavy
+   octet is not the only shape. First step: extend the PR1650 orbit cover to
+   eight deletions and run the exact global rank test on each representative.
+2. Find the maximum kernel excess over 35 at eight and nine deletions. Nine
+   is the uniform injectivity limit (|X| <= 9). No search beyond the
+   octets is claimed here.
+
+## Credit
+
+Produced by Nick Petalas. Geometry, FRAME0 and the frame enumeration are Josie
+Elliston's PR1650. The extension theorem through seven deletions and
+the open question are Ali Romman's PR5697, which builds on Josie
+Elliston's PR1668, Andrey Mas's PR1560 and Nick Petalas's PR5238.
+Apache-2.0.

research/p112-eight-deletion-extension-failure/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/complex-rank8-rigidity-p105/verify.py",
+      "usage": "input",
+      "git_blob": "d60ada8e40a03efb4506c1cfadd589d16df0a281",
+      "sha256": "8bab6588f19f0280a98dfce90835746387ef9845cdfb5768f84ac75247af7b01"
+    }
+  ]
+}

research/p112-eight-deletion-extension-failure/TASK.json

@@ -0,0 +1,81 @@
+{
+  "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": "Determine the maximum deletion threshold for the global quadratic-extension property on P112 (open next question of PR5697): the largest k such that, for every X in P112 with |X|<=k, the kernel of the all-live-frame incidence on P112 minus X equals the 35-dimensional space of trace-zero quadratic restrictions.",
+  "scope_change_reason": "The card asks for a priced decoder change. This package answers the explicitly open threshold question left by PR5697, a structural input to the P112 rigidity and decoder line; it is a side result with no supplier, invoice or kappa.",
+  "bottleneck_link": "Side result. It fixes the exact deletion range in which the uniform quadratic-extension argument of PR5697 can be reused for P112 incidence and decoder rigidity work. It prices nothing.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first exactly certified eight-deletion failure; with PR5697 this settles the threshold. Do not extend to a full classification of eight-deletion failures.",
+  "outcome": "completed",
+  "evidence": "Finite exact certificate: for each of 14 explicit eight-line deletion sets the live-frame incidence has rational rank 62 on 104 lines, kernel dimension 42 > 35, so global quadratic extension fails at eight deletions. With PR5697 (extension for every |X|<=7, cited, not rechecked here) the maximum threshold is exactly 7. verify.py: exact Fraction elimination for all 14 octets, quadratic restriction dimension 35 on each live set, isolated-line structure, seven-subset rank controls and a damaged-octet control.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Classify all eight-deletion sets X in P112 for which global quadratic extension fails, up to the FRAME0 stabilizer of order 172032.",
+      "why_it_matters": "It would show whether line isolation by a heavy-partner octet is the only failure mechanism at eight deletions, or whether rank loss without isolation also occurs.",
+      "first_step": "Extend the retained PR1650 orbit cover from seven to eight deletions and run the exact global rank test on each representative. A greedy eight-set found during this work has kernel 37 and is not one of the 14 octets.",
+      "blocked_by": "The eight-deletion orbit cover is not yet materialized; seven deletions already have 242802 representatives."
+    },
+    {
+      "question": "Does the 7-dimensional excess persist as the maximum kernel excess over all eight-deletion sets, and what is the maximum excess as a function of |X| up to the injectivity limit |X|<=9?",
+      "why_it_matters": "A sharp excess profile bounds how many extra non-quadratic kernel directions a decoder or rigidity argument must handle after deletions.",
+      "first_step": "Search eight- and nine-deletion sets for kernel dimension above 42 with an exact rank test.",
+      "blocked_by": "No complete search is supplied here; any search result would be a search failure unless exhaustive."
+    }
+  ]
+}

research/p112-eight-deletion-extension-failure/VERIFY.json

@@ -0,0 +1,20 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/complex-rank8-rigidity-p105/verify.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact rational ranks for 14 eight-deletion octets (kernel 42 > 35), quadratic restriction dimension, isolated-line structure, seven-subset rank controls and a damaged-octet control."
+    }
+  ]
+}

research/p112-eight-deletion-extension-failure/verify.py

@@ -0,0 +1,144 @@
+#!/usr/bin/env python3
+"""Certify eight-deletion failures of global quadratic extension on P112."""
+
+from collections import Counter
+from fractions import Fraction
+import hashlib
+import importlib.util
+import itertools
+import json
+from pathlib import Path
+
+ROOT = Path(__file__).resolve().parent
+REPO = ROOT.parents[1]
+GEOMETRY = 'research/complex-rank8-rigidity-p105/verify.py'
+
+
+def need(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+def load_geometry():
+    rows = json.loads((ROOT/'SOURCES.json').read_text())['files']
+    pin = next(r for r in rows if r['path'] == GEOMETRY)
+    need(hashlib.sha256((REPO/GEOMETRY).read_bytes()).hexdigest() == pin['sha256'], 'geometry source hash')
+    spec = importlib.util.spec_from_file_location('p105_source', REPO/GEOMETRY)
+    module = importlib.util.module_from_spec(spec)
+    spec.loader.exec_module(module)
+    return module
+
+
+def rank_q(rows):
+    """Exact rank over Q by Gaussian elimination on Fractions."""
+    rows = [[Fraction(x) for x in r] for r in rows]
+    rank = 0
+    for c in range(len(rows[0]) if rows else 0):
+        p = next((i for i in range(rank, len(rows)) if rows[i][c]), None)
+        if p is None:
+            continue
+        rows[rank], rows[p] = rows[p], rows[rank]
+        for i in range(len(rows)):
+            if i != rank and rows[i][c]:
+                f = rows[i][c]/rows[rank][c]
+                rows[i] = [a-f*b for a, b in zip(rows[i], rows[rank])]
+        rank += 1
+    return rank
+
+
+def quadratic_forms():
+    """Rational basis of the 35 trace-zero symmetric 8x8 matrices."""
+    forms = []
+    for i, j in itertools.combinations(range(8), 2):
+        h = [[0]*8 for _ in range(8)]
+        h[i][j] = h[j][i] = 1
+        forms.append(h)
+    for i in range(7):
+        h = [[0]*8 for _ in range(8)]
+        h[i][i], h[7][7] = 1, -1
+        forms.append(h)
+    return forms
+
+
+def evaluations(s, lines):
+    forms = quadratic_forms()
+    return [[sum(h[a][b]*s.LINES[i][a]*s.LINES[i][b] for a in range(8) for b in range(8)) for i in lines]
+            for h in forms]
+
+
+def live_frames(s, deleted):
+    dead = s.F0MASK | sum(1 << i for i in deleted)
+    return [F for F, m in zip(s.FRAMES, s.FMASK) if not m & dead]
+
+
+def certify(s, X):
+    """Return the exact kernel data of the live-frame incidence after deleting X."""
+    L = [i for i in s.P112 if i not in X]
+    frames = live_frames(s, X)
+    covered = {i for F in frames for i in F}
+    isolated = [i for i in L if i not in covered]
+    incidence_rank = rank_q([[int(i in F) for i in L] for F in frames])
+    kernel = len(L)-incidence_rank
+    # Quadratic restrictions to L span 35 dimensions and lie in the kernel.
+    need(rank_q(evaluations(s, L)) == 35, 'quadratic restriction dimension on L')
+    # Kernel vectors explained by quadratics plus indicator vectors of isolated lines.
+    units = [[int(i == j) for i in L] for j in isolated]
+    explained = rank_q(evaluations(s, L)+units)
+    need(explained <= kernel, 'isolated indicators and quadratics lie in the kernel')
+    return {'deleted': sorted(X), 'live_lines': len(L), 'live_frames': len(frames),
+            'isolated_lines': isolated, 'rank_q': incidence_rank, 'kernel_dimension': kernel,
+            'excess_over_quadratics': kernel-35,
+            'quadratics_plus_isolated_indicators': explained}
+
+
+def main():
+    s = load_geometry()
+    need(len(s.LINES) == 120 and len(s.FRAMES) == 2025 and len(s.P112) == 112, 'E8 line/frame geometry')
+    live = live_frames(s, [])
+    need(len(live) == 1260, 'live frames avoiding FRAME0')
+    need(Counter(i for F in live for i in F) == Counter({i: 90 for i in s.P112}), 'ninety live frames per line')
+
+    heavy = {}
+    for line in s.P112:
+        through = [F for F in live if line in F]
+        partners = Counter(i for F in through for i in F if i != line)
+        need(Counter(partners.values()) == Counter({10: 51, 15: 8}), 'partner frame counts')
+        X = tuple(sorted(i for i in partners if partners[i] == 15))
+        need(all(set(F) & set(X) for F in through), 'heavy partners hit every live frame through the line')
+        heavy[line] = X
+    families = sorted(set(heavy.values()))
+    need(len(families) == 14, 'fourteen distinct heavy-partner octets')
+    need(all(sum(v == X for v in heavy.values()) == 8 for X in families), 'each octet isolates eight lines')
+
+    certificates = [certify(s, X) for X in families]
+    for c in certificates:
+        need(sorted(c['isolated_lines']) == sorted(l for l, X in heavy.items() if list(X) == c['deleted']),
+             'isolated lines are exactly the lines owning this octet')
+        need(tuple(c['isolated_lines']) in families, 'isolated lines form the partner octet')
+        need((c['live_lines'], c['live_frames'], c['rank_q'], c['kernel_dimension']) == (104, 648, 62, 42),
+             'exact octet incidence data')
+        need(c['quadratics_plus_isolated_indicators'] == c['kernel_dimension'], 'kernel fully explained')
+        need(c['excess_over_quadratics'] > 0, 'extension fails')
+    excess = Counter(c['excess_over_quadratics'] for c in certificates)
+
+    # Controls: every seven-subset of the first octet keeps all lines covered and has
+    # the #5697 rank |L|-35; a damaged octet does not isolate its line.
+    X = families[0]
+    for drop in X:
+        Y = [i for i in X if i != drop]
+        frames = live_frames(s, Y)
+        L = [i for i in s.P112 if i not in Y]
+        need({i for F in frames for i in F} == set(L), 'seven deletions isolate nothing')
+        need(rank_q([[int(i in F) for i in L] for F in frames]) == len(L)-35, 'seven-deletion control rank')
+    owner = next(l for l, Y in heavy.items() if Y == X)
+    damaged = list(X[1:])+[next(i for i in s.P112 if i not in X and i != owner)]
+    need(any(owner in F for F in live_frames(s, damaged)), 'damaged octet control')
+
+    result = {'status': 'PASS_P112_EIGHT_DELETION_EXTENSION_FAILURE',
+              'octets': len(families), 'excess_histogram': dict(sorted(excess.items())),
+              'certificates': certificates, 'seven_subset_controls': len(X)}
+    print(json.dumps(result, indent=1))
+
+
+if __name__ == '__main__':
+    main()