From 4ee826b9cdfa2587ec96a00ba0cf80faa2173d12 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 29 Oct 2026 16:31:07 +0000 Subject: [PATCH] feat(research): reduce coordinate cache trees to coordinate charts --- research/coordinate-cache-retraction/PROOF.md | 157 +++++++++++++ .../coordinate-cache-retraction/README.md | 105 +++++++++ .../coordinate-cache-retraction/SOURCES.json | 30 +++ .../coordinate-cache-retraction/TASK.json | 87 +++++++ .../coordinate-cache-retraction/VERIFY.json | 34 +++ .../coordinate-cache-retraction/verify.py | 215 ++++++++++++++++++ 6 files changed, 628 insertions(+) create mode 100644 research/coordinate-cache-retraction/PROOF.md create mode 100644 research/coordinate-cache-retraction/README.md create mode 100644 research/coordinate-cache-retraction/SOURCES.json create mode 100644 research/coordinate-cache-retraction/TASK.json create mode 100644 research/coordinate-cache-retraction/VERIFY.json create mode 100644 research/coordinate-cache-retraction/verify.py diff --git a/research/coordinate-cache-retraction/PROOF.md b/research/coordinate-cache-retraction/PROOF.md new file mode 100644 index 0000000000..32add4e96f --- /dev/null +++ b/research/coordinate-cache-retraction/PROOF.md @@ -0,0 +1,157 @@ +# Coordinate reduction of a cache tree + +This proof and its finite checker were produced by Nick Petalas. + +## Contract and result + +Let K be any field, including characteristic two. Let V=K^(2n), n>=1, +with symplectic basis e_1,...,e_n,f_1,...,f_n and alternating form +=delta_ij. A chart is an n-dimensional isotropic subspace. +Its paid rank distance is + + d(L,M) = n - dim(L intersect M). + +The use of this distance for binary Clifford transports, and the typed-copy +contract distributing one unchanged logical snapshot, are cited from zxv's +PR5283. This proof does not re-establish its native compiler or physical +contract. The all-field statement below is linear algebra; its direct +Clifford application is over F2. + +A coordinate chart chooses one vector from each pair {e_i,f_i}. Write A for +the set of these 2^n charts. There is an explicit map R from every chart to A +such that + + R(A) = A for every A in the coordinate set, + d(R(L),R(M)) <= d(L,M) for every pair of charts. + +Consequently a finite tree with fixed coordinate terminal charts and arbitrary +intermediate charts has a coordinate-labeled replacement with the same tree +and no larger paid cost, for any nonnegative nondecreasing tariff on each +edge. Tariffs may differ between edges. This includes r^s for every s>0, +with 0^s=0. Concavity is not required. + +The contribution is this search reduction for the cache contract. Echelon +pivots and initial-subspace arguments are elementary linear algebra. No claim +of priority for those general ideas or for building retractions is made. + +## 1. The pivot map + +Order coordinates as + + c_1,...,c_(2n) = e_1,...,e_n,f_n,...,f_1. + +The reversed order of the f coordinates matters. The only nonzero coordinate +pairings have indices summing to 2n+1, and their values are units 1 or -1. + +For any subspace W, take a row-reduced echelon basis in this order. Let P(W) +be its pivot positions, and define + + I(W) = span{c_j : j in P(W)}. + +A nonzero linear combination of echelon rows has its first nonzero coordinate +at the first pivot whose row has nonzero coefficient. Therefore P(W) is exactly +the set of possible first nonzero positions of nonzero vectors in W. It +follows that |P(W)|=dim W and, whenever W is contained in U, + + P(W) is contained in P(U). + +In particular + + P(U intersect W) is contained in P(U) intersect P(W), + dim(U intersect W) <= dim(I(U) intersect I(W)). (1) + +A coordinate subspace is fixed by I. + +## 2. Isotropic spaces stay isotropic + +Suppose an isotropic W had complementary pivots i,j with i+j=2n+1. +Choose their echelon rows u,v, normalized to have leading coefficient one. +Every supported coordinate of u has index at least i; every supported +coordinate of v has index at least j. A nonzero term of requires the +two coordinate indices to sum to 2n+1. Since i+j already has that value, +the only possible term is the leading pair i,j. Its coefficient is 1 or -1, +which is nonzero in every field. This contradicts isotropy. + +Thus P(W) contains no complementary pair. For an n-dimensional chart L, +there are n pivots among n pairs, so exactly one position in each pair is +chosen. Hence I(L) is a coordinate chart. Define R(L)=I(L). Equation (1) +proves the distance inequality. Since coordinate charts are fixed, R is a +retraction. Its Lipschitz constant one is sharp: opposite coordinate charts +remain at distance n. + +This argument proves every field and dimension directly. The finite census +is corroboration, not an extrapolation to those quantifiers. + +## 3. Retraction of an entire tree + +Fix any finite tree T and any assignment L_v of charts to its vertices. +Every prescribed terminal must lie in the same coordinate set A. Replace +L_v by R(L_v) at every vertex. Terminals are fixed, and each edge uv obeys + + phi_uv(d(R(L_u),R(L_v))) <= phi_uv(d(L_u,L_v)). + +Sum over edges. The tree, its vertex count, and its terminal assignments +are unchanged; internal vertices or zero-rank edges need not be deleted. +For each fixed topology the two exact minimum costs agree, because every +unrestricted assignment retracts and every coordinate assignment was already +allowed. Over all finite topologies their infima also agree. Existence of a +global optimizer is not needed for the replacement claim. + +In the abstract typed-copy contract, each vertex still represents the same +snapshot in its newly chosen chart. Implementing the changed transports +requires the predecessor's exact phase and ordinary-operation contracts. +The inequality prices only the rank-dependent edges. It does not bound +ordinary monomial work or certify an emitted physical word. + +Fixed productive credits depending only on unchanged terminals can be +subtracted from both sides. A negative term depending on a variable internal +edge, such as -d^s, reverses monotonicity and is not covered. Nor are additional +restrictions on intermediate charts unless the map preserves them. + +## 4. Connection to canonical coordinate-subspace frames + +PR5283 gives the canonical binary chart + + Lambda(U) = {(x,x+z) : x in U, z in U-perp}. + +If every required U is spanned by a subset of one standard coordinate basis, +these charts choose between (e_i,e_i) and (0,e_i) independently for each i. +Those are paired vectors of a common symplectic basis. They satisfy the +hypothesis above. Arbitrary subspaces U, or arbitrary terminal charts, need +not share such a basis. No claim that a selected caller has this property +is made here. + +## 5. Finite evidence and failure boundaries + +The checker enumerates row-reduced bases rather than sampling charts. +Distances are independently computed by enumerating vector spans and counting +their literal intersections. It checks the intersection-leading inclusion, +all ordered chart pairs in the registered domains, retraction idempotence, +and the complete coordinate image. Finite monotone tariff tables and a +four-terminal tree census corroborate the cost consequence. + +The self-dual coordinate order cannot be discarded. In interleaved order +(e_1,f_1,e_2,f_2), the isotropic plane spanned over F3 by +(1,0,1,0),(0,1,0,-1) has pivots e_1,f_1. Their coordinate span is not +isotropic. Reordering to the stated self-dual order repairs this example. + +Two distinct lines span(e_1) and span(e_1+f_1) over F2 have distance one +and retract to the same line. Thus a decreasing tariff or a negative +internal-edge credit can increase. The second line also shows that a +non-coordinate terminal need not remain fixed. These are explicit scope +controls, not a universal obstruction to changed contracts. + +Physical movement, dirty restoration, ownership, source-row lifetimes, +precision, native phases, compiler closure and the complete signed supplier +invoice remain separate obligations. No new kappa or complete multiplication +theorem follows from this rank-only reduction. + +## Credit + +Credit zxv for PR5283's snapshot tree, paid Lagrangian metric and cache cost +interface; Matarener for PR5060's preceding center-intersection argument; +Dugongue for PR4534's owned-center retiming contract; and the native, helper, +compiler and supplier contributors retained in PR5283's source notices. +The predecessor files are cited as immutable provenance, not imported or +replayed. Independent human and formal proof-kernel review are unclaimed. +Apache-2.0. diff --git a/research/coordinate-cache-retraction/README.md b/research/coordinate-cache-retraction/README.md new file mode 100644 index 0000000000..3c7f05f078 --- /dev/null +++ b/research/coordinate-cache-retraction/README.md @@ -0,0 +1,105 @@ +# Coordinate charts suffice for coordinate-terminal cache trees + +This contribution was produced by Nick Petalas. Claim type: scoped proof +with exact finite corroboration. No new kappa is claimed. + +If every required terminal chart selects one coordinate from each symplectic +pair in a common basis, arbitrary intermediate Clifford charts cannot lower +the rank-only cache-tree cost. Echelon pivots in a self-dual coordinate order +give an explicit retraction onto the 2^n coordinate charts that fixes every +terminal and never increases any edge rank. + +The [proof](PROOF.md) covers every field and dimension. Any nonnegative +nondecreasing edge tariffs are allowed, including r^(1-kappa) for 0 pivots[i]) + patterns.append((pivots, free)) + require(sum(prime ** len(free) for _, free in patterns) <= 4096, + "census capacity exceeded") + for pivots, free in patterns: + for entries in itertools.product(range(prime), repeat=len(free)): + rows = [[0] * (2*n) for _ in range(n)] + for i, column in enumerate(pivots): + rows[i][column] = 1 + for (i, j), value in zip(free, entries): + rows[i][j] = value + yield tuple(tuple(row) for row in rows) + + +def literal_span(rows, prime, width): + require(prime ** len(rows) <= 125, "span capacity exceeded") + return frozenset(tuple(sum(c * row[j] for c, row in zip(coefficients, rows)) + % prime for j in range(width)) + for coefficients in itertools.product(range(prime), repeat=len(rows))) + + +def chart_domain(prime, n, expected): + planes = tuple(all_rref_planes(prime, n)) + charts = tuple(rows for rows in planes + if all(pairing(a, b) % prime == 0 for a in rows for b in rows)) + require(len(charts) == expected and len(charts) <= 256, "chart census mismatch") + spans = tuple(literal_span(rows, prime, 2*n) for rows in charts) + masks = tuple(retract(rows, prime, n) for rows in charts) + for rows, span, mask in zip(charts, spans, masks): + require(len(span) == prime**n, "dependent census basis") + leading = {next(i for i, x in enumerate(v) if x) for v in span if any(v)} + require(mask == sum(1 << i for i in leading), "literal leading positions disagree") + require(retract(coordinate_rows(mask, 2*n), prime, n) == mask, + "retraction is not idempotent") + require(len(set(masks)) == 2**n, "coordinate image incomplete") + return planes, charts, spans, masks + + +def check_domain(prime, n, expected): + planes, charts, spans, masks = chart_domain(prime, n, expected) + dimensions = {prime**i: i for i in range(n+1)} + attained = set() + strict = 0 + for i in range(len(charts)): + for j in range(len(charts)): + common = spans[i] & spans[j] + distance = n - dimensions[len(common)] + projected = n - (masks[i] & masks[j]).bit_count() + require(projected <= distance, "distance increased") + common_leads = {next(k for k, x in enumerate(v) if x) + for v in common if any(v)} + require(all((masks[i] & masks[j]) & (1 << k) for k in common_leads), + "intersection-leading inclusion failed") + attained.add((distance, projected)) + strict += projected < distance + tariffs = tuple((0,) + values for values in + itertools.combinations_with_replacement(range(4), n)) + for tariff in tariffs: + for distance, projected in attained: + require(tariff[projected] <= tariff[distance], "monotone price increased") + return {"field": prime, "n": n, "all_planes": len(planes), "charts": len(charts), + "coordinate_charts": len(set(masks)), "ordered_pairs": len(charts)**2, + "strict_contractions": strict, "tariff_distance_checks": len(tariffs)*len(attained)} + + +def fixed_tree_check(): + _, charts, spans, masks = chart_domain(2, 2, 15) + lookup = {rows: i for i, rows in enumerate(charts)} + terminals = tuple(lookup[coordinate_rows(mask, 4)] for mask in sorted(set(masks))) + dims = {1: 0, 2: 1, 4: 2} + price = (0, 2, 3) + costs = tuple(tuple(price[2-dims[len(a & b)]] for b in spans) for a in spans) + projected = tuple(lookup[coordinate_rows(mask, 4)] for mask in masks) + count = 0 + minima = [] + # All three four-leaf binary topologies, retaining zero-length edges. + for split in ((0, 1, 2, 3), (0, 2, 1, 3), (0, 3, 1, 2)): + a, b, c, d = (terminals[i] for i in split) + full, restricted = [], [] + for u, v in itertools.product(range(len(charts)), repeat=2): + value = costs[a][u]+costs[b][u]+costs[u][v]+costs[v][c]+costs[v][d] + pu, pv = projected[u], projected[v] + after = costs[a][pu]+costs[b][pu]+costs[pu][pv]+costs[pv][c]+costs[pv][d] + require(after <= value, "whole tree price increased") + full.append(value) + if u in terminals and v in terminals: + restricted.append(value) + count += 1 + require(min(full) == min(restricted), "restricted tree minimum changed") + minima.append(min(full)) + return {"labeled_trees": count, "minimum_prices_in_half_units": minima} + + +def expect_rejection(rows, prime, n): + try: + retract(rows, prime, n) + except ValueError: + return + raise ValueError("malformed chart accepted") + + +def controls(): + for rows, prime, n in (((), 2, 1), (((1, 0),), 4, 1), + (((1, 0, 0),), 2, 1), (((1.0, 0),), 2, 1), + (((1, 0, 0, 0), (1, 0, 0, 0)), 2, 2), + (((1, 0, 0, 0), (0, 0, 0, 1)), 2, 2), + (((1, 0),), 2, 4)): + expect_rejection(rows, prime, n) + left, right = ((1, 0),), ((1, 1),) + require(retract(left, 2, 1) == retract(right, 2, 1), "strict witness lost") + require(literal_span(left, 2, 2) & literal_span(right, 2, 2) == {(0, 0)}, + "strict witness not distinct") + before, after = 1, 0 + require(-after > -before, "negative-edge control failed") + decreasing = (1, 0) + require(decreasing[after] > decreasing[before], "decreasing tariff control failed") + # An interleaved order e1,f1,e2,f2 makes naive pivots nonisotropic. + interleaved = ((1, 0, 1, 0), (0, 1, 0, 2)) + _, bad_pivots = echelon(interleaved, 3, 4) + require(bad_pivots == (0, 1), "bad-order control lost") + a, b = interleaved + require((a[0]*b[1]-a[1]*b[0]+a[2]*b[3]-a[3]*b[2]) % 3 == 0, + "original interleaved plane not isotropic") + require(retract(((1, 1, 0, 0), (0, 0, 2, 1)), 3, 2) == 5, + "self-dual order correction failed") + projected_rows = coordinate_rows(retract(right, 2, 1), 2) + require(projected_rows != right, "noncoordinate terminal was fixed") + return {"invalid_charts_rejected": 7, "scope_controls": 4} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-result", action="store_true", help="print a generated hash-bound record") + args = parser.parse_args() + domains = [check_domain(p, n, expected) for p, n, expected in + ((2, 1, 3), (3, 1, 4), (5, 1, 6), (2, 2, 15), + (3, 2, 40), (5, 2, 156), (2, 3, 135))] + result = {"status": "PASS_COORDINATE_CACHE_RETRACTION", "domains": domains, + "tree": fixed_tree_check(), "controls": controls()} + if args.emit_result: + package = Path(__file__).resolve().parent + result["sha256"] = {name: hashlib.sha256((package/name).read_bytes()).hexdigest() + for name in ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py")} + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()