diff --git a/research/signed-triangle-tensor-gap/PROOF.md b/research/signed-triangle-tensor-gap/PROOF.md new file mode 100644 index 0000000000..cb2c949aff --- /dev/null +++ b/research/signed-triangle-tensor-gap/PROOF.md @@ -0,0 +1,154 @@ +# Exact signed subspace triangle + +This is a scoped theorem in a rank-distance relaxation. It does not assert +that the graph below is the contact graph of a legal scalar word. In +particular, its three negative edges are variable productive credits, not +three already implemented independent recursive targets. + +## Contract + +Let K be any field, let H=K^m with m a positive integer, and let S1,S2,S3 +be arbitrary subspaces. Write + +```math +d(A,B)=\dim A+\dim B-2\dim(A\cap B). +``` + +There are four vertices, 0,S1,S2,S3. Three positive edges join 0 to Si; +three negative edges join every pair Si,Sj. For 0=1, + +```math +\min J_1=-\lfloor3m/2\rfloor. +``` + +The minimizers are exactly the pairwise-disjoint triples with dimensions +(k,k,k) for m=2k, and a permutation of (k,k,k+1) for m=2k+1. +Pairwise-disjoint means each pair intersects only at zero. The sum of all +three spaces need not be direct. + +Put x_i=dim Si, D=x1+x2+x3, and +I=sum_(i=1, the right side is at most 3m/2-3/2, strictly smaller than +floor(3m/2). Thus equality forces I=0 and D=floor(3m/2). +Now xi+xj<=m implies each xi>=D-m. For m=2k this forces all three +dimensions to be k. For m=2k+1 it forces all three to be at least k and +their sum to be 3k+1, hence the claimed permutation. Conversely those +dimensions and zero pairwise intersections give equality in J1. + +For attainment, split H=U plus W with dimensions k and m-k. Choose an +injective linear map f:U->W. Set S1=U, S2=W, and S3=graph(f). +The three intersections are zero, and their dimensions are k,m-k,k. +This works over every field, including characteristic two and k=0. + +Consequently the normalized linear optimum is +-floor(3m/2)/m. It is -1 at one copy, -3/2 at every positive even width, +and -3/2+1/(2m) at odd width. The advantage is established in the signed +graph model; a supplier or exponent improvement does not follow. + +## Exact two-copy power optimum + +For m=2 let a=2^t, so 13/2, equivalently t>log_2(3/2). Equality holds at the +threshold. The threshold lies below 3/4 because 2^3>(3/2)^4. + +## What changes relative to fixed-boundary reduction + +PR6171 fixes each productive endpoint to a repeated space U^m. Here all +three productive pairs vary. At m=2, the attaining linear triple consists +of the three distinct lines of F2^2. No line is a repeated scalar boundary: +the repeated one-dimensional scalar choices are only zero and F2^2. +The coupled triple has three full-distance productive pairs. A one-copy +assignment has at most two nonzero pair distances. Their negative credits +therefore cannot be held constant during the common-copy choice. + +This gives an exact optimality gap and threshold, beyond the predecessor's +arithmetic control that negative terms can reverse an averaging inequality. +It neither contradicts that theorem nor extends the graph into a physical +construction. In particular, pairwise graph edges do not establish three +independent targets on arbitrary dirty inputs. Producing such a caller, +or proving that its legal graph constraints forbid this configuration, +is a separate question. + +## Verification boundary + +The written dimension argument and exhaustive two-dimensional table give +the all-field statements. The checker enumerates actual small subspaces, +checks every ordered triple, and compares all equality cases. Its binary +RREF inventory is independently checked by closure under adjoining vectors. +It also constructs the attaining binary triples at widths 1 through 64. +These are finite corroboration, not a proof-kernel formalization. + +The code uses finite, explicit bounds. Its managed-runtime allocations +are a Power of Ten deviation: finite calibration sizes bound the lists, +tables and loops. No recursion, external solver, network access, imported +predecessor executable or persistent mutable state is needed. + +This proof and verifier were produced by Nick Petalas. Standard dimension +identities, graph subspaces and affine-envelope comparisons are background; +no literature-priority claim is made. PR6171 retains its tensor-reduction +credit; Cinna Davis retains the projection inequality, icekylinx retains +the canonical subspace-frame construction, and all retained P104/native/ +helper/caller/compiler contributors retain their predecessor credit. diff --git a/research/signed-triangle-tensor-gap/README.md b/research/signed-triangle-tensor-gap/README.md new file mode 100644 index 0000000000..f5e2f1c1af --- /dev/null +++ b/research/signed-triangle-tensor-gap/README.md @@ -0,0 +1,90 @@ +# Sharp tensor gap with variable productive boundaries + +This scoped proof determines a signed subspace-distance invoice over every +field. Three variable spaces each pay their distance from zero and receive +credit for their three pairwise distances. The exact linear optimum in +ambient dimension m is `-floor(3m/2)`. Every minimizer is classified. + +At two copies the normalized power-tariff optimum is +`min(-1, 3/2^t - 3)`, for `0 3/2`. At the linear tariff, +the normalized optimum drops from `-1` to `-3/2`. + +This is an exact gap in an abstract signed graph, with finite corroboration. +It supplies neither a physical scalar word nor a new kappa. In particular, +the three graph credits are not claimed to be independently delivered +recursive targets on arbitrary dirty inputs. + +## Proof and context + +[PROOF.md](PROOF.md) gives the dimension bound, attainment, all equality +cases and the exhaustive two-dimensional affine table. This extends the +variable-boundary question left open by Ali Romman's +[PR6171](https://github.com/CrocSwap/integer-mult-bounds/pull/6171), at +`343232cdf5273d1f77569de390f0977b46916644`. That result fixes every productive +boundary to a repeated space. This package makes those boundaries variable +and proves an exact optimum, beyond its arithmetic warning about negative +credits. It does not audit or contradict the fixed-boundary theorem. + +Base main is `3f0152a32eeebac0df11946dbd50cabe5a7f7839`, priority revision 8. +The selected `0.003125804` frontier is unchanged. The card's first selected +source-binding control passed; no predecessor scientific replay was run. +The source PR is cited as conceptual context. No pending executable or Git +object is needed for the proof or replay. + +## Reproduce + +From the repository root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/signed-triangle-tensor-gap/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -O -B research/signed-triangle-tensor-gap/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/signed-triangle-tensor-gap +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/signed-triangle-tensor-gap --check-source-history +``` + +A clean `python3.12` executable can replace the local interpreter path. +The direct marker is `PASS_SIGNED_TRIANGLE_TENSOR_GAP`. +[RESULT.json](RESULT.json) records every finite domain, minimizer count and +ordered trace digest, and binds all six source files by SHA256. Replays are +read-only. To regenerate a receipt, supply `--output /absolute/scratch/result.json` +with a new output filename, then compare it with the committed receipt. + +The verifier enumerates all ordered triples over F2 in dimensions 0 through +4 and over F3 and F5 in dimension 2. A separate closure inventory checks the +binary RREF enumeration. It checks the attaining construction at widths +1 through 64 and the nine affine costs at all three relevant envelope +endpoints. Missing/spurious table rows, intersecting-plane equality and the +strict threshold have explicit controls. The written proof supplies the +unbounded all-field claim; the finite checks do not replace it. + +## Limitations + +The domain consists of canonical subspace charts. General Lagrangian charts, +a prescribed scalar contact graph and actual native phases are outside it. +A legal dirty-input circuit, independence of physical targets, restoration, +owned storage, movement, adapters, precision, compiler closure, BIT and outer +admission remain open and unpriced. No selected cold replay, Lean or Docker +run is needed for this scoped theorem. Independent human and formal +proof-kernel review are unclaimed. + +## Open next questions + +- Can a legal arbitrary-dirty-input scalar circuit realize this signed graph, + or is there a contact/path invariant that excludes it? First assign the + three productive pairs to distinct logical lifetimes and account for every + paid transition. Independent target delivery and restoration are blockers. +- What is the all-width optimum for `0 pivots[i]] + for values in itertools.product(range(prime), repeat=len(cells)): + rows = [[int(j == pivots[i]) for j in range(dimension)] + for i in range(rank)] + for (i, j), value in zip(cells, values): + rows[i][j] = value + spaces.append((rank, span_mask(rows, prime, dimension))) + need(len({mask for _, mask in spaces}) == len(spaces), "Duplicate space") + return spaces + + +def closure_oracle(dimension): + """Independent F2 enumeration by repeated adjoining of a vector.""" + known = {1} + for _ in range(dimension): + previous = tuple(known) + for mask in previous: + members = [x for x in range(1 << dimension) if (mask >> x) & 1] + for added in range(1 << dimension): + enlarged = mask + for member in members: + enlarged |= 1 << (member ^ added) + known.add(enlarged) + return known + + +def exhaustive_case(prime, dimension): + spaces = subspaces(prime, dimension) + if prime == 2: + need({mask for _, mask in spaces} == closure_oracle(dimension), + "RREF and closure enumerations disagree") + sizes = {prime ** k: k for k in range(dimension + 1)} + intersections = [[sizes[(a & b).bit_count()] for _, b in spaces] + for _, a in spaces] + distances = [[ra + rb - intersections[i][j] * 2 + for j, (rb, _) in enumerate(spaces)] + for i, (ra, _) in enumerate(spaces)] + expected = -(3 * dimension // 2) + minimum = None + minimizers = 0 + coefficients = set() + digest = hashlib.sha256() + for indices in itertools.product(range(len(spaces)), repeat=3): + ranks = [spaces[i][0] for i in indices] + credits = [distances[indices[i]][indices[j]] for i, j in PAIRS] + value = sum(ranks) - sum(credits) + pairwise_disjoint = all(intersections[indices[i]][indices[j]] == 0 + for i, j in PAIRS) + balanced = sorted(ranks) == [dimension // 2, dimension // 2, + (dimension + 1) // 2] + need(value >= expected, "Linear floor violated") + need((value == expected) == (pairwise_disjoint and balanced), + "Equality classification violated") + if minimum is None or value < minimum: + minimum = value + minimizers += int(value == expected) + if dimension == 2: + coefficients.add((ranks.count(1) - credits.count(1), + ranks.count(2) - credits.count(2))) + digest.update(f"{indices}:{value}\n".encode()) + need(minimum == expected and minimizers > 0, "Floor not attained") + if dimension == 2: + need(tuple(sorted(coefficients)) == COEFFICIENTS, "Power table changed") + return {"prime": prime, "dimension": dimension, "spaces": len(spaces), + "ordered_triples": len(spaces) ** 3, "linear_minimum": minimum, + "minimizers": minimizers, "trace_sha256": digest.hexdigest()} + + +def attaining_spaces(dimension): + half = dimension // 2 + first = tuple(1 << j for j in range(half)) + second = tuple(1 << j for j in range(half, dimension)) + third = tuple((1 << j) | (1 << (half + j)) for j in range(half)) + return first, second, third + + +def binary_rank(rows, dimension): + basis = [0] * dimension + rank = 0 + for row in rows: + value = row + for pivot in range(dimension - 1, -1, -1): + if (value >> pivot) & 1: + if basis[pivot]: + value ^= basis[pivot] + else: + basis[pivot] = value + rank += 1 + break + return rank + + +def construction_checks(): + for dimension in range(1, 65): + spaces = attaining_spaces(dimension) + ranks = [binary_rank(rows, dimension) for rows in spaces] + distances = [] + for i, j in PAIRS: + union_rank = binary_rank(spaces[i] + spaces[j], dimension) + need(union_rank == ranks[i] + ranks[j], "Nonzero intersection") + distances.append(2 * union_rank - ranks[i] - ranks[j]) + need(sum(ranks) - sum(distances) == -(3 * dimension // 2), + "Construction misses floor") + return 64 + + +def power_checks(coefficients): + need(tuple(sorted(coefficients)) == COEFFICIENTS, "Incomplete power table") + checks = 0 + for constant, slope in coefficients: + for a in (Fraction(1), Fraction(3, 2), Fraction(2)): + need(constant + slope * a >= min(-a, 3 - 3 * a), + "Power-envelope endpoint violated") + checks += 1 + need(2 ** 3 > Fraction(3, 2) ** 4, "Threshold certificate failed") + return checks + + +def run_checks(): + cases = [exhaustive_case(prime, dimension) for prime, dimension in LAYOUTS] + controls = [] + for changed in (COEFFICIENTS[:-1], COEFFICIENTS + ((-9, 0),)): + try: + power_checks(changed) + except ValueError: + controls.append("omitted_table_row" if len(changed) == 8 + else "spurious_table_row") + else: + raise ValueError("Changed power table accepted") + # Merely different subspaces need not have zero intersection. + planes = ((1, 2), (1, 4), (2, 4)) + ranks = [binary_rank(rows, 3) for rows in planes] + distances = [2 * binary_rank(planes[i] + planes[j], 3) - ranks[i] - ranks[j] + for i, j in PAIRS] + need(sum(ranks) - sum(distances) == 0 > -4, + "Distinct intersecting planes must not attain the dimension-three floor") + controls.append("distinct_is_not_disjoint") + need(Fraction(3, 2) - 3 < -1, "Normalized two-copy advantage missing") + need(Fraction(3, 1) / Fraction(3, 2) - 3 == -1, + "Equality at power threshold missing") + controls.append("strict_threshold") + local = Path(__file__).resolve().parent + source_hashes = {name: hashlib.sha256((local / name).read_bytes()).hexdigest() + for name in ("README.md", "PROOF.md", "TASK.json", + "SOURCES.json", "VERIFY.json", "verify.py")} + return {"schema_version": 1, "claim_type": "scoped proof with finite corroboration", + "linear_optimum": "-floor(3m/2)", + "two_copy_normalized_power_optimum": "min(-1,3/2^t-3), 0