From 45695156d6170bf85f34f8d422079ad43bb6d750 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 15:35:27 +0000 Subject: [PATCH] feat(research): break P112 quadratic extension at eight deletions Fourteen heavy-partner octets give live-frame kernel 42 > 35. With the seven-deletion theorem of #5697 the extension threshold is exactly 7. --- .../README.md | 88 +++++++++++ .../SOURCES.json | 24 +++ .../TASK.json | 81 ++++++++++ .../VERIFY.json | 20 +++ .../verify.py | 144 ++++++++++++++++++ 5 files changed, 357 insertions(+) create mode 100644 research/p112-eight-deletion-extension-failure/README.md create mode 100644 research/p112-eight-deletion-extension-failure/SOURCES.json create mode 100644 research/p112-eight-deletion-extension-failure/TASK.json create mode 100644 research/p112-eight-deletion-extension-failure/VERIFY.json create mode 100644 research/p112-eight-deletion-extension-failure/verify.py diff --git a/research/p112-eight-deletion-extension-failure/README.md b/research/p112-eight-deletion-extension-failure/README.md new file mode 100644 index 0000000000..038aa88b00 --- /dev/null +++ b/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. diff --git a/research/p112-eight-deletion-extension-failure/SOURCES.json b/research/p112-eight-deletion-extension-failure/SOURCES.json new file mode 100644 index 0000000000..5716f1838d --- /dev/null +++ b/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" + } + ] +} diff --git a/research/p112-eight-deletion-extension-failure/TASK.json b/research/p112-eight-deletion-extension-failure/TASK.json new file mode 100644 index 0000000000..8d94535164 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/p112-eight-deletion-extension-failure/VERIFY.json b/research/p112-eight-deletion-extension-failure/VERIFY.json new file mode 100644 index 0000000000..82e3b4e651 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/p112-eight-deletion-extension-failure/verify.py b/research/p112-eight-deletion-extension-failure/verify.py new file mode 100644 index 0000000000..1b63137a26 --- /dev/null +++ b/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()