From 8be0f6dc6c8d704f1b9bbe3b497a3fdd6729408b Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Sun, 25 Oct 2026 23:13:43 -0500 Subject: [PATCH 1/3] research: retain E7 minimum-support source and credit --- .../vendor/PR5238.md | 178 ++++++++++++ .../vendor/PR5238.py | 262 ++++++++++++++++++ 2 files changed, 440 insertions(+) create mode 100644 research/e7-minimum-support-classification/vendor/PR5238.md create mode 100644 research/e7-minimum-support-classification/vendor/PR5238.py diff --git a/research/e7-minimum-support-classification/vendor/PR5238.md b/research/e7-minimum-support-classification/vendor/PR5238.md new file mode 100644 index 0000000000..5dc8029611 --- /dev/null +++ b/research/e7-minimum-support-classification/vendor/PR5238.md @@ -0,0 +1,178 @@ +# Sharp support twelve for trace-zero E7 quadratics + +This contribution was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +## Result and claim type + +**Scoped mathematical proof with an exact finite certificate.** Every nonzero +rational trace-zero quadratic form on the seven-dimensional orthogonal +complement of an E8 root is nonzero on at least **twelve** of its 63 root +lines. Twelve is attained. + +This proves the trace-zero replacement for auxiliary statement (2) in +[JoyboyBrian's released handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1502#discussioncomment-19145642). +The unrestricted statement there needs correction: products of two linear +forms can have support eleven, as already follows from the 52-line two-flat +union in DreamingOfClouds's #595 and DaysSky's +[#897](https://github.com/CrocSwap/integer-mult-bounds/pull/897). +DreamingOfClouds's open +[#3045](https://github.com/CrocSwap/integer-mult-bounds/pull/3045) +also records an E7 intersection of supports of size eleven. The eleven-line +example first reported in this contribution's progress post is therefore +credited to that existing coverage, not claimed as an original result. +The new result is the sharp trace-zero bound and its frame-code certificate. + +The arbitrary-deletion quadratic extension in handoff statement (1) remains +open. This package does not prove the seven-deletion rigidity shortcut. + +## Finite certificate + +Use doubled E8 roots, with canonical line representatives +`2e_i +/- 2e_j`, `i < j`, and `(1,s_1,...,s_7)` with an even number of +negative coordinates. All have squared norm eight. Coordinates run from zero +through seven. Fix `a=2e_0+2e_4`, and let `R` be the 63 root lines in `a`-perp. +An orthogonal frame consists of seven mutually orthogonal lines in `R`. + +The verifier constructs every frame by an increasing-clique traversal, +retaining a branch only when enough candidates remain to complete it. +It finds 135 frames. Their binary incidence matrix `H`, of shape `135 x 63`, +has rank 36 and kernel dimension 27. The verifier constructs a kernel basis +with an identity submatrix on its free coordinates, checks every basis vector +against every row, and enumerates every one of its **134,217,727 nonzero +vectors**. Their minimum Hamming weight is **12**. + +The enumeration uses a Gray traversal. At step `i`, toggling basis vector +`v_((i & -i).bit_length()-1)` changes the coefficient vector to `i xor (i>>1)`. +These coefficient vectors visit every nonzero element of `F2^27` once. +The identity on the free coordinates proves that their images are distinct. +The finite minimum is recomputed on every registered replay; no saved census +or external solver is trusted. + +## Proof of the rational lower bound + +More generally, every nonzero rational function on `R` whose sum on every +orthogonal frame is zero has support at least twelve. Clear its denominators +and divide its integer values by their greatest common divisor. The resulting +primitive integer vector still has zero frame sums, and its reduction modulo +two is nonzero. That reduction lies in `ker(H)`, and its support is contained +in the original support. The finite certificate therefore proves the bound. + +For a trace-zero quadratic `q`, every frame has zero sum: its seven roots +are an orthogonal basis of `a`-perp with squared norm eight, so +`sum(q(r): r in frame) = 8 trace(q) = 0`. +It remains to check that a nonzero quadratic cannot vanish on all of `R`. +Here is an elementary injectivity argument. + +Write `J={1,2,3,5,6,7}` and `y=x_0=-x_4` on `a`-perp. If a quadratic +vanishes on every `2e_i +/- 2e_j`, with `i,j` in `J`, subtracting the two +evaluations kills each mixed coefficient within `J`, and adding them shows +that every pair of diagonal coefficients sums to zero. Three distinct indices +then force all six diagonal coefficients to vanish over the rationals. +The root `2e_0-2e_4` kills the coefficient of `y^2`. Only +`y sum(b_i x_i: i in J)` remains. The 32 half-root lines have `y=1`, with +all odd-parity six-sign rows `s`. These rows satisfy `sum(s s^T)=32 I_6`, +so vanishing on them forces every `b_i=0`. Thus the original quadratic was zero. + +This proves the lower bound for the stated rational domain. To transport it +to any E8 root, the verifier checks nine orthogonal root-set automorphisms: +seven adjacent coordinate swaps, negation of coordinates zero and one, and +reflection in `(1,-1,-1,-1,1,-1,-1,-1)`. Their orbit on `a` contains all +120 root lines. Orthogonal rational transport preserves trace and support. + +## A twelve-line attainer + +Restrict + +\[ + q_0(x)=x_0^2+x_1^2+x_2^2+x_3^2-x_4^2-x_5^2-x_6^2-x_7^2 +\] + +to `a`-perp. The ambient trace is zero and `q_0(a)=0`, so the restricted +trace is zero. On `R`, the six coordinate-root lines within `{1,2,3}` have +value `+8`, the six within `{5,6,7}` have value `-8`, and the other 51 lines +have value zero. Indeed, cross-part coordinate roots cancel, `2e_0-2e_4` +cancels, and every half-root has four positive and four negative square terms. +The verifier checks the twelve nonzero values and all 135 literal frame sums. + +## Relation to the handoff and limits + +The delivered scope repairs the proposed auxiliary support statement by adding +trace zero. If an ambient trace-zero quadratic vanishes on the pivot, its +restriction to the pivot's orthogonal complement is trace-zero: in an +orthonormal basis beginning with the pivot direction, that first diagonal +entry and the total trace are both zero. The new lemma can therefore supply +the support step in the handoff's proposed reduction, conditional on its +separate arbitrary-deletion extension statement and the remaining hypotheses. + +The advance claim asked about the unrestricted statement. Semantic overlap +checking identified the earlier eleven-line coverage before any commit. +The original contribution delivered here is the trace-zero replacement. +Neither the earlier flat census nor any predecessor's rigidity result is +replayed or re-verified as this contribution. + +The binary minimum is a complete finite enumeration, not a formal proof-kernel +certificate. The rational implication and injectivity argument are written +proofs. Native realization, physical supplier admission, selected cold replay, +Lean and the complete multiplication theorem are outside scope. No new kappa +or selected-frontier change is claimed. + +## Reproduction + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/e7-quadratic-support/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/e7-quadratic-support/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/e7-quadratic-support +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/e7-quadratic-support --check-source-history +``` + +Another CPython 3.12 path can replace the local interpreter path. +Expected status is `PASS_E7_TRACE_ZERO_SUPPORT`, with 63 lines, 135 frames, +binary rank 36, dimension 27, 134217727 nonzero codewords, minimum weight 12, +a quadratic attainer with six positive and six negative values, and 92 +rejecting controls. Normal and optimized modes use explicit checks, not assertions. + +The verifier constructs E8 and the intrinsic E7 slice separately and checks the +root orbit. Omission controls reject every incomplete 63-line domain; basis +controls reject every one-bit-corrupted basis vector and wrong dimensions. +It uses bounded traversals, no recursion, and a constant-memory Gray census. +Python runtime allocation is unavoidable; the stored geometry has only 120 +root lines, 135 frames and 27 kernel vectors. Optional +`--receipt /absolute/path/outside/the/package.json` writes a generated receipt +bound to all five package source hashes. Direct replay needs no Git or +predecessor imports and writes nothing into its source package. + +## Open next questions + +1. Does every live-frame zero-sum rational function on P112 minus at most + seven lines extend to an ambient trace-zero quadratic? This is handoff + statement (1) and is the remaining uniform bridge in that reduction. + First prove an extension lemma retaining every deletion quantifier. + Its existing finite fixtures do not establish that implication. +2. Which trace-zero quadratics attain support twelve? A classification could + identify all possible sparse equality obstructions. First determine the + rational kernels on the weight-twelve supports; no equality classification + is claimed or required for the present minimum. + +## Sources and credit + +The immediate question comes from +[JoyboyBrian's released handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1502#discussioncomment-19145642). +The full-family shortcut and its eight-deletion counterexamples are Josie +Elliston's [#1668](https://github.com/CrocSwap/integer-mult-bounds/pull/1668), +following [#1650](https://github.com/CrocSwap/integer-mult-bounds/pull/1650) +and [#1616](https://github.com/CrocSwap/integer-mult-bounds/pull/1616). +Andrey Mas's [#1560](https://github.com/CrocSwap/integer-mult-bounds/pull/1560) +supplies the incidence criterion. Aaron Wang's +[#1649](https://github.com/CrocSwap/integer-mult-bounds/pull/1649) separates +the subfamily question. DreamingOfClouds / #595 and #3045 and DaysSky / #897 +retain credit for the earlier unrestricted eleven-line support coverage. +The retained E8 model and rigidity lineage credit Brett Halligan / #1212, +themilkman216 / #968, and DreamingOfClouds / #717. + +These are motivation and provenance, not mathematical inputs to the new +self-contained certificate. `SOURCES.json` pins the originating catalogue and +predecessor notes at canonical main +`ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c`. diff --git a/research/e7-minimum-support-classification/vendor/PR5238.py b/research/e7-minimum-support-classification/vendor/PR5238.py new file mode 100644 index 0000000000..781a074d45 --- /dev/null +++ b/research/e7-minimum-support-classification/vendor/PR5238.py @@ -0,0 +1,262 @@ +#!/usr/bin/env python3 +"""Sharp support twelve for rational trace-zero E7 quadratics. Exact integers.""" + +import argparse +from collections import Counter +import hashlib +import itertools +import json +from pathlib import Path +import platform + + +PIVOT = (2, 0, 0, 0, 2, 0, 0, 0) +DIAGONAL = (1, 1, 1, 1, -1, -1, -1, -1) +N = 63 +DIMENSION = 27 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dot(left, right): + require(len(left) == len(right) == 8, "eight coordinates required") + return sum(left[i] * right[i] for i in range(8)) + + +def e8_lines(): + roots = [] + for i, j in itertools.combinations(range(8), 2): + for sign in (-1, 1): + root = [0] * 8 + root[i], root[j] = 2, 2 * sign + roots.append(tuple(root)) + for tail in itertools.product((-1, 1), repeat=7): + root = (1,) + tail + if root.count(-1) % 2 == 0: + roots.append(root) + require(len(roots) == len(set(roots)) == 120, "E8 line count") + require(all(dot(root, root) == 8 for root in roots), "E8 norms") + return tuple(sorted(roots)) + + +def intrinsic_e7(): + roots = [] + for i, j in itertools.combinations((1, 2, 3, 5, 6, 7), 2): + for sign in (-1, 1): + root = [0] * 8 + root[i], root[j] = 2, 2 * sign + roots.append(tuple(root)) + roots.append((2, 0, 0, 0, -2, 0, 0, 0)) + for signs in itertools.product((-1, 1), repeat=6): + if signs.count(-1) % 2 == 1: + roots.append((1,) + signs[:3] + (-1,) + signs[3:]) + return tuple(sorted(roots)) + + +def validate_domain(roots): + require(len(roots) == len(set(roots)) == N, "63 distinct root lines") + require(tuple(sorted(roots)) == intrinsic_e7(), "intrinsic E7 agreement") + require(all(dot(PIVOT, root) == 0 for root in roots), "orthogonal slice") + + +def root_transport(root, generator): + out = list(root) + if generator < 7: + out[generator], out[generator + 1] = out[generator + 1], out[generator] + elif generator == 7: + out[0], out[1] = -out[0], -out[1] + else: + require(generator == 8, "nine fixed orthogonal generators") + normal = (1, -1, -1, -1, 1, -1, -1, -1) + inner = dot(root, normal) + require(inner % 4 == 0, "integral E8 reflection") + out = [root[i] - inner // 4 * normal[i] for i in range(8)] + first = next(value for value in out if value) + return tuple(value if first > 0 else -value for value in out) + + +def check_root_transitivity(): + domain = set(e8_lines()) + for generator, root in itertools.product(range(9), domain): + require(root_transport(root, generator) in domain, "root-set automorphism") + orbit = {PIVOT} + stack = [PIVOT] + for _ in range(120): + if not stack: + break + root = stack.pop() + for generator in range(9): + image = root_transport(root, generator) + if image not in orbit: + orbit.add(image) + stack.append(image) + require(not stack and orbit == domain, "all 120 root lines reached") + return len(orbit) + + +def orthogonal_frames(roots): + adjacency = [{j for j in range(N) if j != i and dot(roots[i], roots[j]) == 0} + for i in range(N)] + frames = [] + stack = [((), tuple(range(N)))] + # Each state is an increasing orthogonal subset; 100000 is a fail-closed cap. + for _ in range(100000): + if not stack: + break + frame, candidates = stack.pop() + if len(frame) == 7: + frames.append(frame) + continue + for offset, j in enumerate(candidates): + tail = tuple(k for k in candidates[offset + 1:] if k in adjacency[j]) + if len(tail) >= 6 - len(frame): + stack.append((frame + (j,), tail)) + else: + raise ValueError("frame enumeration exceeded its state cap") + require(len(frames) == len(set(frames)) == 135, "135 complete frames") + for frame in frames: + require(len(frame) == 7 and all(j in adjacency[i] for i, j in + itertools.combinations(frame, 2)), "orthogonal frame") + return tuple(sorted(frames)) + + +def binary_kernel(rows): + echelon = {} + for row in rows: + for pivot in range(N - 1, -1, -1): + if row >> pivot & 1: + if pivot in echelon: + row ^= echelon[pivot] + else: + echelon[pivot] = row + break + free = tuple(j for j in range(N) if j not in echelon) + basis = [] + for j in free: + vector = 1 << j + for pivot in sorted(echelon): + if (echelon[pivot] & vector).bit_count() % 2: + vector |= 1 << pivot + basis.append(vector) + require(len(echelon) == 36 and len(free) == DIMENSION, "binary rank 36") + validate_basis(rows, basis, free) + return tuple(basis), free + + +def validate_basis(rows, basis, free): + require(len(basis) == len(free) == DIMENSION, "complete kernel dimension") + require(len(set(free)) == DIMENSION, "distinct free coordinates") + for index, vector in enumerate(basis): + require(0 < vector < 1 << N, "bounded nonzero kernel vector") + require(all((vector & row).bit_count() % 2 == 0 for row in rows), + "every frame parity vanishes") + require(tuple(vector >> j & 1 for j in free) == + tuple(int(k == index) for k in range(DIMENSION)), + "identity on free coordinates proves independence") + + +def full_weight_census(basis): + word = 0 + minimum = N + visited = 0 + for index in range(1, 1 << DIMENSION): + word ^= basis[(index & -index).bit_length() - 1] + weight = word.bit_count() + require(weight != 0, "independent basis cannot revisit zero") + if weight < minimum: + minimum = weight + visited += 1 + require(visited == 134217727, "every nonzero binary kernel vector visited") + require(minimum == 12, "binary frame code has minimum weight twelve") + return visited, minimum + + +def check_witness(roots, frames): + values = tuple(sum(DIAGONAL[i] * root[i] ** 2 for i in range(8)) + for root in roots) + require(sum(DIAGONAL) == 0, "ambient quadratic has trace zero") + require(sum(DIAGONAL[i] * PIVOT[i] ** 2 for i in range(8)) == 0, + "pivot diagonal entry vanishes, so restricted trace is zero") + require(Counter(values) == {0: 51, 8: 6, -8: 6}, "twelve-line attainer") + require(all(sum(values[j] for j in frame) == 0 for frame in frames), + "literal rational frame sums vanish") + # Odd-parity six-sign rows span all six remaining coordinates. Together + # with coordinate +/- pairs and e0-e4, this proves quadratic injectivity. + signs = [tuple(root[j] for j in (1, 2, 3, 5, 6, 7)) + for root in roots if root[0] == 1] + require(len(signs) == 32, "all odd-parity sign rows") + for i, j in itertools.product(range(6), repeat=2): + require(sum(row[i] * row[j] for row in signs) == 32 * int(i == j), + "sign-row Gram identity") + return values + + +def rejection_controls(roots, rows, basis, free): + rejected = 0 + for j in range(N): + try: + validate_domain(roots[:j] + roots[j + 1:]) + except ValueError: + rejected += 1 + else: + raise ValueError("incomplete root domain accepted") + for j in range(DIMENSION): + changed = list(basis) + changed[j] ^= 1 + try: + validate_basis(rows, changed, free) + except ValueError: + rejected += 1 + else: + raise ValueError("non-kernel basis accepted") + for changed in (basis[:-1], basis + (basis[0],)): + try: + validate_basis(rows, changed, free) + except ValueError: + rejected += 1 + else: + raise ValueError("wrong kernel dimension accepted") + require(rejected == 92, "all 92 omission and basis controls executed") + return rejected + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="write generated receipt outside package") + args = parser.parse_args() + orbit_size = check_root_transitivity() + roots = tuple(root for root in e8_lines() if dot(root, PIVOT) == 0) + validate_domain(roots) + frames = orthogonal_frames(roots) + rows = tuple(sum(1 << j for j in frame) for frame in frames) + basis, free = binary_kernel(rows) + values = check_witness(roots, frames) + controls = rejection_controls(roots, rows, basis, free) + visited, minimum = full_weight_census(basis) + package = Path(__file__).resolve().parent + files = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + receipt = { + "status": "PASS_E7_TRACE_ZERO_SUPPORT", "e7_lines": len(roots), + "pivot_orbit": orbit_size, + "frames": len(frames), "binary_rank": N - len(basis), + "binary_kernel_dimension": len(basis), "nonzero_codewords": visited, + "minimum_binary_weight": minimum, "quadratic_support": sum(v != 0 for v in values), + "positive_values": sum(v > 0 for v in values), + "negative_values": sum(v < 0 for v in values), "rejecting_controls": controls, + "python": platform.python_version(), + "source_sha256": {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in files}, + } + serialized = json.dumps(receipt, indent=2, sort_keys=True) + "\n" + if args.receipt is not None: + require(not args.receipt.resolve().is_relative_to(package), + "receipt must be outside the source package") + args.receipt.write_text(serialized, encoding="utf-8") + print(serialized, end="") + + +if __name__ == "__main__": + main() From fb38d6b41cb2847f7ec92152d0a8bbe9cd6e803a Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Sun, 25 Oct 2026 23:18:56 -0500 Subject: [PATCH 2/3] research: classify every minimum E7 frame relation --- .../PROOF.md | 130 ++++++++++++ .../README.md | 77 +++++++ .../RESULT.json | 190 +++++++++++++++++ .../SOURCES.json | 48 +++++ .../TASK.json | 89 ++++++++ .../VERIFY.json | 31 +++ .../verify.py | 197 ++++++++++++++++++ 7 files changed, 762 insertions(+) create mode 100644 research/e7-minimum-support-classification/PROOF.md create mode 100644 research/e7-minimum-support-classification/README.md create mode 100644 research/e7-minimum-support-classification/RESULT.json create mode 100644 research/e7-minimum-support-classification/SOURCES.json create mode 100644 research/e7-minimum-support-classification/TASK.json create mode 100644 research/e7-minimum-support-classification/VERIFY.json create mode 100644 research/e7-minimum-support-classification/verify.py diff --git a/research/e7-minimum-support-classification/PROOF.md b/research/e7-minimum-support-classification/PROOF.md new file mode 100644 index 0000000000..af4663e4a8 --- /dev/null +++ b/research/e7-minimum-support-classification/PROOF.md @@ -0,0 +1,130 @@ +# Equality in the E7 support bound + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +The source geometry and support bound are due to Nick Petalas, PR5238. + +## Statement + +Use doubled E8 roots, with squared norm eight. Fix +`a=(2,0,0,0,2,0,0,0)`. Let R be the 63 root lines perpendicular to a, +with one root on each line. Let H be the incidence matrix of all 135 +orthogonal seven-line frames in R. Let K be any field of characteristic zero. + +A nonzero function f:R -> K with Hf=0 has support at least twelve. +If its support has size twelve, there are exactly two possibilities up to +a nonzero scalar and E7 root reflections. Representatives are the +restrictions to a-perp of + +``` +A(x) = x0^2+x1^2+x2^2+x3^2-x4^2-x5^2-x6^2-x7^2, +B(x) = (x0-x1)(x2-x3). +``` + +The support orbit of A has 630 members. The support orbit of B has 1008 +members. They are disjoint and include all 1638 minimum supports. Each +support admits exactly one scalar family of frame relations. Every such +relation is the evaluation of a trace-zero quadratic. The two quadratic +ranks on a-perp are six and two. Thus the two types cannot be identified +by any orthogonal map and nonzero scalar. + +The same statement holds on the perpendicular slice of any E8 root, +by rational orthogonal transport. It also classifies every trace-zero +quadratic that attains support twelve. The zero quadratic is excluded. + +## Finite certificate and its completeness + +The retained PR5238 code constructs the 63 roots in two ways, constructs all +135 frames by increasing orthogonal cliques, and computes a binary kernel +basis of dimension 27. Its free-coordinate submatrix is the identity. +Each basis vector has zero parity on every frame. These checks prove that +all binary frame relations are in the generated code. + +The new checker traverses all 2^27-1 nonzero coefficient vectors in Gray +order. It uses every basis direction at its prescribed toggle. Independence +makes the resulting codewords distinct and nonzero. The minimum weight is +twelve. Exactly 1638 distinct supports have this weight. No saved support +list or numerical rank test supplies this result. + +For each root r in R, the map + +``` +s_r(x) = x - (x dot r) r / 4 +``` + +is an orthogonal reflection because r dot r=8. It fixes a. The checker +constructs its exact permutation of R and checks its action on every frame. +These 63 maps generate the E7 reflection action used here. Breadth-first +closure of the two representative supports gives sets of sizes 630 and +1008. Their union is exactly the exhaustive minimum-support set, and their +intersection is empty. This proves coverage; it does not require an assumed +Weyl-group order or an external group catalogue. + +The evaluations of A are six +8 values, six -8 values, and 51 zeros. +The evaluations of B are six +4 values, six -4 values, and 51 zeros. +The checker verifies all 135 frame sums for both vectors. Exact rational +elimination gives rank eleven for H restricted to either representative +support. Therefore each restricted kernel has dimension one. Reflection +transport gives the same rank and a nonzero quadratic lift on every support. +As a separate check, removal of any one coordinate from either support gives +column rank eleven and no nonzero relation. + +## From the binary certificate to characteristic zero + +First let f be rational and nonzero with Hf=0. Clear denominators and divide +all entries by their greatest common divisor. The result is a primitive +integer relation. Its reduction modulo two is nonzero, lies in the binary +kernel, and has support contained in that of f. Thus f has support at least +twelve. If f has support twelve, its binary reduction must have the same +support, which is in the two checked orbits. This is the PR5238 reduction, +now used with the full equality list. + +Now let f have values in any characteristic-zero field K, and let S be its +support. The integer matrix H restricted to S has the same rank over Q and +K: its nonzero rational minors stay nonzero in K. A nonzero K-kernel therefore +implies a nonzero rational kernel. A rational vector in that kernel has +support at most |S|, so the rational lower bound gives |S| >= 12. + +If |S|=12, any nonzero rational kernel vector has support exactly S. The +previous paragraph puts S in the two orbits. The checked restricted rank +is eleven over Q and hence over K. The K-kernel is the scalar span of the +transported representative. This proves the stated classification for +arbitrary characteristic zero, without reduction of K itself modulo two. + +## Quadratic interpretation + +On a-perp, set y=x0=-x4 and use the other coordinates +`x1,x2,x3,x5,x6,x7`. The Euclidean metric in this basis is +`diag(1,1,1,1,1,1,2)`. The trace of a quadratic matrix M in these coordinates +is the sum of its first six diagonal entries plus M_yy/2. +Both representatives have trace zero. Exact polarization gives ranks six +and two. A frame is an orthogonal basis of a-perp of equal squared length, +so every trace-zero quadratic gives a frame relation. + +The quadratic evaluation map is injective in characteristic zero. On the +six ordinary coordinates, the roots `2e_i +/- 2e_j` force all mixed +coefficients to zero and every pair of diagonal coefficients to sum to zero. +Three indices force all six diagonal coefficients to zero. The root +`2e0-2e4` then kills the y-square term. Only y times a linear form in the +six coordinates remains. The 32 odd-parity sign rows have Gram matrix +32I, so their evaluations kill all six remaining coefficients. These are +exact identities over Q and remain valid in every characteristic-zero field. +This is the injectivity argument retained from PR5238. + +Thus the relation classification gives the quadratic classification as well. +The retained nine ambient generators preserve the E8 roots and move a to +all 120 root lines. They are rational orthogonal maps. This transports the +whole result to every root slice. + +## Relevance and limits + +This resolves PR5238's equality-classification question. Sparse incidence +failures at the twelve-line threshold have two explicit quadratic types; +a diagonal balanced-pair ansatz alone misses the rank-two type. A future +sharp deletion-boundary proof can now use a complete equality list. + +The arbitrary-deletion extension statement in Discussion1502 remains open. +This result does not prove it, the seven-deletion incidence implication, +a decoder cost floor, a physical supplier, or an improvement in complete +kappa. The selected metadata still has conditional kappa 0.00310045, with +the main transform as its limiting outer row. No formal proof kernel or +independent human review is claimed. diff --git a/research/e7-minimum-support-classification/README.md b/research/e7-minimum-support-classification/README.md new file mode 100644 index 0000000000..ffb6879ecc --- /dev/null +++ b/research/e7-minimum-support-classification/README.md @@ -0,0 +1,77 @@ +# All minimum E7 frame relations: two quadratic types + +There are exactly **1638** twelve-line supports for a nonzero characteristic-zero +E7 frame relation. They form **two** root-reflection orbits, of sizes **630** +and **1008**. Each support has one scalar family of relations. Both families +are trace-zero quadratics, of ranks six and two. This completes the equality +question left by Nick Petalas's PR5238. No new kappa is claimed. + +[PROOF.md](PROOF.md) gives the exact statement and the characteristic-zero +argument. [RESULT.json](RESULT.json) gives the representatives, orbit hashes, +ranks and coverage. [SOURCES.json](SOURCES.json) pins the retained geometry +and predecessor proof. [verify.py](verify.py) recomputes the full census. + +For the slice perpendicular to `(2,0,0,0,2,0,0,0)`, representatives are +`x0^2+x1^2+x2^2+x3^2-x4^2-x5^2-x6^2-x7^2` and +`(x0-x1)(x2-x3)`. Their nonzero evaluations have equal magnitude, with six +of each sign. Rational orthogonal transport covers every E8 root slice. + +## Why this helps the decoder work + +PR5238 proves minimum support twelve but leaves equality open. The new +classification supplies all sparse equality obstructions at that boundary. +It also shows that the diagonal type alone does not cover all obstructions. +It does not supply the separate arbitrary-deletion extension lemma in the +[released handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1502#discussioncomment-19145642). +No decoder floor or physical caller follows without that missing implication. + +## Verification + +Python 3.12 and its standard library suffice. + +``` +python3.12 -B scripts/research_package.py --package research/e7-minimum-support-classification +python3.12 -B scripts/check_research_commit.py --package research/e7-minimum-support-classification +``` + +Expected: `PASS_E7_MINIMUM_SUPPORT_CLASSIFICATION`, +`PASS_REGISTERED_RESEARCH_PACKAGE`, and `PASS_RESEARCH_COMMIT_BYTES`. +The normal and optimized checks each enumerate all 134217727 nonzero binary +codewords. They check all 63 reflection generators on all 135 frames, the +complete two-orbit partition, exact rational lift ranks, quadratic ranks, +ambient transport, 24 coordinate omissions and four corruption controls. +The verifier authenticates retained sources before it executes them. +It writes no source file. The registered time cap is 600 seconds per mode. + +The same assistant supplied the proof and checker. These are exact finite +checks plus a written proof, not independent human or formal acceptance. +No native or selected cold replay, outer admission, full historical suite, +Lean or Docker run was used. Full source-history preflight is unavailable +in this shallow checkout; exact bytes and immediate source ancestry are +separate checks. Selected files are unchanged. + +## Open next questions + +1. Does every live-frame relation after at most seven P112 deletions extend + to an ambient trace-zero quadratic? Retain all deletion quantifiers. + The equality classification does not prove this separate extension. +2. At the next incidence boundary, which of the two equality types is + compatible with the literal deleted frame and pivot conditions? Start + from the two explicit representatives and charge every omitted line. + No new deletion census or reservation is made here. + +## Credit and scope + +Nick Petalas's [PR5238](https://github.com/CrocSwap/integer-mult-bounds/pull/5238) +supplies the minimum bound, root and frame code, and quadratic injectivity. +Its source files are retained byte for byte, with all source notices. +The originating handoff is JoyboyBrian's. The retained lineage includes +Josie Elliston, Andrey Mas, Aaron Wang, Brett Halligan, themilkman216 and +DreamingOfClouds; their individual contributions remain in the source note. +New equality census, orbit classification, characteristic-zero extension, +proof and checks: Ali Romman with substantial OpenAI Codex assistance. +Apache-2.0. + +Canonical base: `df0137efd35e11b4445734bf612bdd4c7ebc330c`, priority revision 7. +The selected source check passes at conditional kappa 0.00310045. This package +changes no selected result and reserves no physical construction. diff --git a/research/e7-minimum-support-classification/RESULT.json b/research/e7-minimum-support-classification/RESULT.json new file mode 100644 index 0000000000..d32035693b --- /dev/null +++ b/research/e7-minimum-support-classification/RESULT.json @@ -0,0 +1,190 @@ +{ + "ambient_root_slices": 120, + "binary_dimension": 27, + "binary_rank": 36, + "characteristic": "zero", + "frames": 135, + "minimum_support": 12, + "minimum_supports": 1638, + "nonzero_codewords": 134217727, + "orbits": [ + { + "orbit_sha256": "d08f659fab919baab7b2c87c0b7e55edb5a3e23e05a313522f0b17e684d8ee39", + "quadratic_rank": 6, + "rational_lift_dimension": 1, + "representative_support": [ + 0, + 1, + 2, + 3, + 4, + 5, + 12, + 19, + 20, + 21, + 28, + 29 + ], + "representative_values": [ + -8, + -8, + -8, + -8, + -8, + -8, + 0, + 0, + 0, + 0, + 0, + 0, + 8, + 0, + 0, + 0, + 0, + 0, + 0, + 8, + 8, + 8, + 0, + 0, + 0, + 0, + 0, + 0, + 8, + 8, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "restricted_frame_rank": 11, + "supports": 630, + "type": "diagonal" + }, + { + "orbit_sha256": "a9bb36def7396f184d343e38f410d705a50be3188b40725235f866ad0753309b", + "quadratic_rank": 2, + "rational_lift_dimension": 1, + "representative_support": [ + 20, + 21, + 28, + 29, + 34, + 35, + 36, + 37, + 38, + 39, + 40, + 41 + ], + "representative_values": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 4, + -4, + 0, + 0, + 0, + 0, + 0, + 0, + 4, + -4, + 0, + 0, + 0, + 0, + -4, + -4, + -4, + -4, + 4, + 4, + 4, + 4, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "restricted_frame_rank": 11, + "supports": 1008, + "type": "product" + } + ], + "reflection_generators": 63, + "rejecting_or_omission_controls": 28, + "root_lines": 63, + "status": "PASS_E7_MINIMUM_SUPPORT_CLASSIFICATION" +} diff --git a/research/e7-minimum-support-classification/SOURCES.json b/research/e7-minimum-support-classification/SOURCES.json new file mode 100644 index 0000000000..195cf52a31 --- /dev/null +++ b/research/e7-minimum-support-classification/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "research/e7-minimum-support-classification/vendor/PR5238.py", + "usage": "input", + "git_blob": "781a074d45126b1a84b92ee2393dc95790c0cb1b", + "sha256": "95502bb9e551302cbb0483097250441e96e5f858a5624745678875e3cedba9d2", + "pin": "head:8be0f6dc6c8d704f1b9bbe3b497a3fdd6729408b:research/e7-minimum-support-classification/vendor/PR5238.py" + }, + { + "path": "research/e7-minimum-support-classification/vendor/PR5238.md", + "usage": "input", + "git_blob": "5dc802961147c41af039e899d8baa3c8bb9e3909", + "sha256": "36e2263d28280043d6861caa4c81270be4800246e17647ec09da7cb4c2826085", + "pin": "head:8be0f6dc6c8d704f1b9bbe3b497a3fdd6729408b:research/e7-minimum-support-classification/vendor/PR5238.md" + } + ], + "external_inputs": [ + { + "local_path": "vendor/PR5238.py", + "source_repository": "CrocSwap/integer-mult-bounds", + "source_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "source_path": "research/e7-quadratic-support/verify.py", + "sha256": "95502bb9e551302cbb0483097250441e96e5f858a5624745678875e3cedba9d2" + }, + { + "local_path": "vendor/PR5238.md", + "source_repository": "CrocSwap/integer-mult-bounds", + "source_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "source_path": "research/e7-quadratic-support/README.md", + "sha256": "36e2263d28280043d6861caa4c81270be4800246e17647ec09da7cb4c2826085" + } + ] +} diff --git a/research/e7-minimum-support-classification/TASK.json b/research/e7-minimum-support-classification/TASK.json new file mode 100644 index 0000000000..4e4c65c25e --- /dev/null +++ b/research/e7-minimum-support-classification/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. 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", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Classify all minimum-support E7 frame relations and trace-zero quadratics in characteristic zero.", + "scope_change_reason": "Take the explicit released equality question in PR5238. It is a structural prerequisite at the decoder-incidence boundary, not a physical supplier.", + "bottleneck_link": "Identify every sparse equality obstruction for the proposed sharp incidence boundary. The separate arbitrary-deletion extension is still needed.", + "budget_minutes": 120, + "stop_rule": "Complete the two-type equality classification. Do not expand into an unpriced decoder or duplicate the minimum-support theorem.", + "outcome": "completed", + "evidence": "PROOF.md, RESULT.json and verify.py.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance. The same assistant supplied the proof and checker; no independent human review.", + "open_questions": [ + { + "question": "Does the arbitrary-deletion quadratic extension hold?", + "why_it_matters": "It is the missing bridge to the seven-deletion incidence claim.", + "first_step": "Prove the extension with all deletion quantifiers retained.", + "blocked_by": "No uniform extension proof is supplied." + }, + { + "question": "Which equality types meet the literal next-boundary deletion conditions?", + "why_it_matters": "The two complete orbit types restrict possible sparse obstructions.", + "first_step": "Compare the two representatives with the actual deleted-frame and pivot conditions.", + "blocked_by": "No new deletion classification is supplied." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1502#discussioncomment-19188245", + "nonce": "00770df06ad58b13ce127059b5948653", + "upstream": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "priority_revision": 7, + "overlap_utc": "2026-10-26T04:18:07.791584+00:00", + "local_notes": 7676, + "open_prs": 353, + "discussion_records": 4972, + "coverage": "All tracked main notes and complete cached PR/Discussion pagination; no unpublished-work coverage." + } +} diff --git a/research/e7-minimum-support-classification/VERIFY.json b/research/e7-minimum-support-classification/VERIFY.json new file mode 100644 index 0000000000..6ecba772c6 --- /dev/null +++ b/research/e7-minimum-support-classification/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/e7-minimum-support-classification/vendor/PR5238.py", + "research/e7-minimum-support-classification/vendor/PR5238.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Exhaust all binary words; classify all minimum supports; check exact rational and quadratic ranks, reflections, transport and negative controls." + }, + { + "argv": [ + "{python}", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Exhaust all binary words; classify all minimum supports; check exact rational and quadratic ranks, reflections, transport and negative controls." + } + ] +} diff --git a/research/e7-minimum-support-classification/verify.py b/research/e7-minimum-support-classification/verify.py new file mode 100644 index 0000000000..dc91e3362d --- /dev/null +++ b/research/e7-minimum-support-classification/verify.py @@ -0,0 +1,197 @@ +#!/usr/bin/env python3 +"""Classify minimum E7 supports. Ali Romman with OpenAI Codex. Apache-2.0.""" +from fractions import Fraction as F +from hashlib import sha256 +from pathlib import Path +from runpy import run_path +import json + +HERE = Path(__file__).resolve().parent + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def geometry(): + manifest = json.loads((HERE / 'SOURCES.json').read_text()) + for row in manifest['external_inputs']: + need(sha256((HERE / row['local_path']).read_bytes()).hexdigest() + == row['sha256'], 'retained source changed') + return run_path(str(HERE / 'vendor/PR5238.py'), run_name='retained_geometry') + + +def rank(rows): + basis = {} + for row in rows: + row = list(map(F, row)) + for p, b in basis.items(): + c = row[p] + if c: + row = [x-c*y for x, y in zip(row, b)] + p = next((i for i, x in enumerate(row) if x), None) + if p is not None: + c = row[p] + basis[p] = [x/c for x in row] + return len(basis) + + +def minimum_supports(basis): + word, minimum, supports = 0, 63, set() + for index in range(1, 1 << 27): + word ^= basis[(index & -index).bit_length()-1] + weight = word.bit_count() + if weight < minimum: + minimum, supports = weight, {word} + elif weight == minimum: + supports.add(word) + need(minimum == 12 and len(supports) == 1638, 'complete minimum census') + return supports + + +def reflections(roots, frames, dot): + lookup = {r: i for i, r in enumerate(roots)} + frame_set = set(frames) + out = [] + for normal in roots: + p = [] + for r in roots: + inner = dot(r, normal) + need(inner % 4 == 0, 'integral reflection') + image = tuple(r[i]-inner//4*normal[i] for i in range(8)) + if next(x for x in image if x) < 0: + image = tuple(-x for x in image) + need(image in lookup, 'root reflection closure') + p.append(lookup[image]) + need(sorted(p) == list(range(63)), 'root permutation') + need(all(tuple(sorted(p[j] for j in frame)) in frame_set + for frame in frames), 'frame reflection closure') + out.append(tuple(p)) + return out + + +def transport(mask, permutation): + image = 0 + while mask: + bit = mask & -mask + image |= 1 << permutation[bit.bit_length()-1] + mask ^= bit + return image + + +def orbit(mask, permutations): + seen, queue = {mask}, [mask] + for current in queue: + for p in permutations: + image = transport(current, p) + if image not in seen: + seen.add(image) + queue.append(image) + return seen + + +def form_a(x): + return sum(x[i]*x[i] for i in range(4))-sum(x[i]*x[i] for i in range(4, 8)) + + +def form_b(x): + return (x[0]-x[1])*(x[2]-x[3]) + + +def quadratic_matrix(form): + vectors = [] + for i in (1, 2, 3, 5, 6, 7): + x = [0]*8 + x[i] = 1 + vectors.append(x) + vectors.append([1, 0, 0, 0, -1, 0, 0, 0]) + matrix = [[F(form([x+y for x, y in zip(a, b)])-form(a)-form(b), 2) + for b in vectors] for a in vectors] + need(sum(matrix[i][i] for i in range(6))+matrix[6][6]/2 == 0, + 'restricted trace zero') + return matrix + + +def supported_rank(frames, support): + return rank([[int(j in frame) for j in support] for frame in frames]) + + +def check_relation(frames, values): + need(sum(x != 0 for x in values) == 12, 'twelve nonzero values') + need(all(sum(values[j] for j in frame) == 0 for frame in frames), + 'literal rational frame sums') + + +def partition(supports, orbits): + need(not orbits[0] & orbits[1], 'disjoint equality orbits') + need(orbits[0] | orbits[1] == supports, 'every minimum support classified') + + +def reject(fn): + try: + fn() + except ValueError: + return + raise ValueError('invalid control accepted') + + +def check(): + g = geometry() + roots = g['intrinsic_e7']() + g['validate_domain'](roots) + need(roots == tuple(r for r in g['e8_lines']() if g['dot'](r, g['PIVOT']) == 0), + 'ambient and intrinsic domains agree') + need(g['check_root_transitivity']() == 120, 'every ambient root slice') + frames = g['orthogonal_frames'](roots) + rows = tuple(sum(1 << j for j in frame) for frame in frames) + basis, free = g['binary_kernel'](rows) + supports = minimum_supports(basis) + permutations = reflections(roots, frames, g['dot']) + orbits, records, controls = [], [], 0 + for name, form, size, qrank, scale in ( + ('diagonal', form_a, 630, 6, 8), ('product', form_b, 1008, 2, 4)): + values = tuple(form(r) for r in roots) + check_relation(frames, values) + need(set(values) == {-scale, 0, scale}, 'constant nonzero magnitudes') + need(values.count(scale) == values.count(-scale) == 6, 'six values of each sign') + support = [j for j, x in enumerate(values) if x] + mask = sum(1 << j for j in support) + current = orbit(mask, permutations) + need(len(current) == size and current <= supports, 'complete attained orbit') + need(supported_rank(frames, support) == 11, 'one-dimensional rational lift') + need(rank(quadratic_matrix(form)) == qrank, 'quadratic rank') + for omitted in support: + need(supported_rank(frames, [j for j in support if j != omitted]) == 11, + 'every single omission has zero kernel') + controls += 1 + changed = list(values) + changed[support[0]] += 1 + reject(lambda: check_relation(frames, changed)) + controls += 1 + orbits.append(current) + records.append(dict(type=name, supports=size, representative_support=support, + representative_values=list(values), quadratic_rank=qrank, + restricted_frame_rank=11, rational_lift_dimension=1, + orbit_sha256=sha256(json.dumps(sorted(current)).encode()).hexdigest())) + partition(supports, orbits) + reject(lambda: partition(supports-{next(iter(supports))}, orbits)) + reject(lambda: partition(supports, [orbits[0], orbits[1] | orbits[0]])) + controls += 2 + return dict(status='PASS_E7_MINIMUM_SUPPORT_CLASSIFICATION', root_lines=63, + frames=135, binary_rank=36, binary_dimension=27, + nonzero_codewords=(1 << 27)-1, minimum_support=12, + minimum_supports=len(supports), reflection_generators=len(permutations), + ambient_root_slices=120, characteristic='zero', orbits=records, + rejecting_or_omission_controls=controls) + + +def main(): + result = check() + need(result == json.loads((HERE / 'RESULT.json').read_text()), 'fixed result receipt') + print(result['status']) + print('1638 minimum supports = 630 rank-six + 1008 rank-two; one scalar family per support') + + +if __name__ == '__main__': + main() From 700efb538a3d919409c9506d117846b7895b02ea Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Sun, 25 Oct 2026 23:20:46 -0500 Subject: [PATCH 3/3] research: record E7 replay and final overlap evidence --- .../TASK.json | 6 ++-- .../VALIDATION.md | 28 +++++++++++++++++++ 2 files changed, 31 insertions(+), 3 deletions(-) create mode 100644 research/e7-minimum-support-classification/VALIDATION.md diff --git a/research/e7-minimum-support-classification/TASK.json b/research/e7-minimum-support-classification/TASK.json index 4e4c65c25e..13006c1f4b 100644 --- a/research/e7-minimum-support-classification/TASK.json +++ b/research/e7-minimum-support-classification/TASK.json @@ -80,10 +80,10 @@ "nonce": "00770df06ad58b13ce127059b5948653", "upstream": "df0137efd35e11b4445734bf612bdd4c7ebc330c", "priority_revision": 7, - "overlap_utc": "2026-10-26T04:18:07.791584+00:00", + "overlap_utc": "2026-10-26T04:19:48.351555+00:00", "local_notes": 7676, - "open_prs": 353, - "discussion_records": 4972, + "open_prs": 357, + "discussion_records": 4977, "coverage": "All tracked main notes and complete cached PR/Discussion pagination; no unpublished-work coverage." } } diff --git a/research/e7-minimum-support-classification/VALIDATION.md b/research/e7-minimum-support-classification/VALIDATION.md new file mode 100644 index 0000000000..a42933b4d6 --- /dev/null +++ b/research/e7-minimum-support-classification/VALIDATION.md @@ -0,0 +1,28 @@ +# Validation record + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. + +The scientific package at `fb38d6b41cb2847f7ec92152d0a8bbe9cd6e803a` passed +the registered normal and optimized checks with CPython 3.12.14. Both checks +recomputed all 134217727 nonzero binary codewords and the exact two-orbit +partition. The same fixed result passed in a read-only Git-free export under +optimized Python, with an empty PATH. All ten exported files, including the +export manifest, kept their hashes. A separate copy with one appended line +in the retained source failed before execution with `retained source changed`. + +The nine package files passed committed-byte checks and official export +validation at that science commit. The base and retention commit are verified +ancestors. The final update adds this record and the refreshed coordination +counts; it changes no scientific code, source or receipt. Final committed bytes +and export integrity are checked separately before publication. + +Current main was refreshed to `df0137efd35e11b4445734bf612bdd4c7ebc330c`. +Guidance, priorities, catalogue and selected record have no drift. The selected +source check passes at conditional kappa 0.00310045. The final full cache has +357 open PRs and 4977 Discussion records. The complete tracked-note inventory +and targeted equality searches found only the predecessor and this claim. +Unpublished work and arbitrary PR diffs are outside this coverage. + +No full-history source preflight was run in the shallow checkout. No selected +cold replay, native supplier, outer admission, complete theorem, Lean, Docker +or independent human review was run. CI status is not asserted here.