From d297eb399c5b2457b2028130c0752234fad9ccba Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 29 Oct 2026 16:23:40 +0000 Subject: [PATCH] feat(research): prove strict projection-cut local traps --- research/projection-local-trap/PROOF.md | 109 +++++++++ research/projection-local-trap/README.md | 134 +++++++++++ research/projection-local-trap/RESULT.json | 92 ++++++++ research/projection-local-trap/SOURCES.json | 24 ++ research/projection-local-trap/TASK.json | 81 +++++++ research/projection-local-trap/VERIFY.json | 34 +++ research/projection-local-trap/verify.py | 242 ++++++++++++++++++++ 7 files changed, 716 insertions(+) create mode 100644 research/projection-local-trap/PROOF.md create mode 100644 research/projection-local-trap/README.md create mode 100644 research/projection-local-trap/RESULT.json create mode 100644 research/projection-local-trap/SOURCES.json create mode 100644 research/projection-local-trap/TASK.json create mode 100644 research/projection-local-trap/VERIFY.json create mode 100644 research/projection-local-trap/verify.py diff --git a/research/projection-local-trap/PROOF.md b/research/projection-local-trap/PROOF.md new file mode 100644 index 0000000000..342fd77c86 --- /dev/null +++ b/research/projection-local-trap/PROOF.md @@ -0,0 +1,109 @@ +# A strict local trap for projection cuts + +Let K be any field, V=K^2, and 0 S and b parallel edges S -> V, where a,b are positive integers. +Every edge is charged its dimension gap to power t, with 0^t=0. +Every subspace S is legal. Boundaries stay fixed during a projection move. + +The complete objective of this graph is + + E(S) = a (dim S)^t + b (2-dim S)^t. + +There are precisely three possible objective values: + + E(V)=a h, E(line)=a+b, E(0)=b h. + +These formulas retain every edge, including parallel multiplicity. There +are no productive credits or unpriced terms in this abstract objective. + +## Strict local trap and joint escape + +By a rank-one projection move we mean the choice, at each free vertex, +between its current frame F and P(F), for one linear idempotent P whose +kernel has dimension one. This is the move in Dugongue's PR556. In this +two-dimensional space, P has rank one and maps V to a line. There is only +one free vertex, so optimizing all subsets for any such P compares just +E(V) and E(line). + +The initial frame V is strictly worse than the zero frame and strictly +better than every changed single-projection frame if and only if + + a>b and a+b>a h. (1) + +Under (1), every nontrivial rank-one projection move increases the entire +objective. Exhaustively optimizing each binary move therefore retains V. +This remains true under any sequence that accepts only nonincreasing +objectives. It is a strict local minimum with respect to these moves. + +Take P(x,y)=(0,y) and Q(x,y)=(x,0). They are idempotent, have one-dimensional +kernels, commute, and PQ=QP=0. Their joint action sends the free frame to 0. +Every intermediate frame remains between the fixed boundary frames, hence +legal. The joint objective decreases by exactly (a-b)h. The first step +must increase the objective; that is the obstruction to monotone descent. +Since a+b>a h>b h, the zero frame is also the global optimum over all S. + +This proves existence over every field. It does not use a finite-field +extrapolation or the correctness of a predecessor's implementation. + +## Sharp number of edges in this class + +Set delta=2-h, with 0d. + +For a fixed d the least possible a is floor(d/delta)+1. This choice has +b=a-d>=1 because delta<1. Therefore the least edge count at that d is + + N_d = 2 floor(d/delta)+2-d. + +As 1/delta>1, increasing d by one increases floor(d/delta) by at least one. +Thus N_(d+1)-N_d>=1. The global minimum occurs at d=1 and is exactly + + N_min(t) = 2 floor(1/(2-2^t))+1. (2) + +It is attained by a=floor(1/(2-2^t))+1 and b=a-1. The strict inequality +matters when the reciprocal is an integer. A tie at a smaller a is not a +strict trap. This is a minimum only within the specified three-vertex, +two-boundary, positive-parallel-multiplicity class. It is not a minimum +over arbitrary frame graphs or physical scalar programs. + +## An exact 481-edge example + +At t=997/1000, the following strict integer inequalities hold: + + 2^997 * 240^1000 > 479^1000, + 2^997 * 241^1000 < 481^1000. + +Taking positive thousandth roots gives + + 479/240 < h < 481/241. + +It follows that 240 < 1/(2-h) < 241. Formula (2) gives N_min=481, +attained by a=241 and b=240. Its profiles are + + initial V: 241 rank-two edges, 240 rank-zero edges; + any line: 481 rank-one edges; + final 0: 240 rank-two edges, 241 rank-zero edges. + +For every 0241h persists, while 241h>240h. The 481-edge minimality is asserted +only at t=997/1000. At the linear tariff t=1 there is no trap in this +class: a+b>2a would require b>a, contradicting the cheaper-zero condition. + +The pinned selected complex supplier uses C=10940329/3500000000, so its +power exponent t=1-C lies in this interval. This arithmetic comparison +only locates the abstract example in a relevant power range. It does not +embed these parallel edges in the selected supplier, transfer its caller +contract, change its signed invoice or establish a kappa gain. + +## What changes for the next search + +The binary optimum for one projection can be exact and still provide no +certificate of a joint optimum. To escape this example, a search must +allow a simultaneous corank-two image or temporarily accept a worse +intermediate frame. A richer move must still retain fixed observations, +productive targets, dirty restoration and every physical cost. No such +supplier implementation is established here. diff --git a/research/projection-local-trap/README.md b/research/projection-local-trap/README.md new file mode 100644 index 0000000000..68441a4c56 --- /dev/null +++ b/research/projection-local-trap/README.md @@ -0,0 +1,134 @@ +# Exact projection cuts can stop at a strict local minimum + +Scoped proof with exact finite corroboration. For every field K and every +power tariff f(r)=r^t, 0 initial > final + predicted = a > b and a * (2 - h) > a - b + require(literal == predicted, "strict-trap predicate") + cases += 1 + ties += int(middle == initial and initial > final) + if literal: + traps += 1 + best = a + b if best is None else min(best, a + b) + optimum = minimum_edges(h) + require(best == optimum, "bounded grid minimum") + for total in range(2, optimum): + for a in range(1, total): + b = total - a + require(not (a + b > a * h > b * h), "smaller graph") + smaller += 1 + a = (optimum + 1) // 2 + require(a + a - 1 > a * h > (a - 1) * h, "attaining graph") + return {"tariffs": len(tariffs), "pairs": cases, "strict_traps": traps, + "ties_with_cheaper_zero": ties, "smaller_graph_pairs": smaller} + + +def multiply(a, b, p): + return tuple(sum(a[2 * i + k] * b[2 * k + j] for k in range(2)) % p + for i in range(2) for j in range(2)) + + +def image(a, vectors, p): + return frozenset(((a[0] * x + a[1] * y) % p, + (a[2] * x + a[3] * y) % p) for x, y in vectors) + + +def projector(a, p): + return (any(a) and (a[0] * a[3] - a[1] * a[2]) % p == 0 + and multiply(a, a, p) == a) + + +def profile(space, vectors, p, a=241, b=240): + parameters(Fraction(3, 2), a, b) + require(space <= frozenset(vectors) and (0, 0) in space, "bad frame") + dimension = {1: 0, p: 1, p * p: 2}[len(space)] + ranks = [] + for _ in range(a): + ranks.append(dimension) + for _ in range(b): + ranks.append(2 - dimension) + counts = Counter(ranks) + require(sum(counts.values()) == a + b, "lost parallel edge") + return tuple(counts[r] for r in range(3)) + + +def field_checks(p): + require(p in FIELDS, "unsupported field") + vectors = tuple(product(range(p), repeat=2)) + lines = {frozenset(((k * x) % p, (k * y) % p) for k in range(p)) + for x, y in vectors if (x, y) != (0, 0)} + require(len(lines) == p + 1, "projective line inventory") + zero, full = frozenset({(0, 0)}), frozenset(vectors) + frames = lines | {zero, full} + profiles = {s: profile(s, vectors, p) for s in frames} + require(profiles[zero] == (241, 0, 240), "zero profile") + require(profiles[full] == (240, 0, 241), "full profile") + require(all(profiles[s] == (0, 481, 0) for s in lines), "line profile") + projectors = [] + matrices = 0 + for matrix in product(range(p), repeat=4): + matrices += 1 + if projector(matrix, p): + projectors.append(matrix) + require(image(matrix, vectors, p) in lines, "projector image") + require(len(projectors) == p * (p + 1), "projector inventory") + zero_matrix = (0, 0, 0, 0) + identity = (1, 0, 0, 1) + orthogonal_pairs = 0 + pairs = 0 + for left in projectors: + for right in projectors: + pairs += 1 + lr, rl = multiply(left, right, p), multiply(right, left, p) + if lr == zero_matrix and rl == zero_matrix: + orthogonal_pairs += 1 + require(tuple((left[i] + right[i]) % p for i in range(4)) + == identity, "complementary projectors") + require(image(lr, vectors, p) == zero, "joint image") + require(orthogonal_pairs == p * (p + 1), "joint escape inventory") + return {"p": p, "frames": len(frames), "matrices": matrices, + "projectors": len(projectors), "pairs": pairs, + "joint_escapes": orthogonal_pairs, + "literal_edges": 481 * len(frames)} + + +def power_sign(constant, coefficient, numerator, denominator): + """Sign of constant+coefficient*2^(numerator/denominator), exactly.""" + require(type(numerator) is int and type(denominator) is int + and 1 <= numerator <= denominator <= 1000, "bad power") + require(type(constant) is int and type(coefficient) is int + and abs(constant) <= 10000 and abs(coefficient) <= 10000, + "bad linear power expression") + if coefficient == 0: + return (constant > 0) - (constant < 0) + if constant == 0 or constant * coefficient > 0: + return (coefficient > 0) - (coefficient < 0) + difference = (2 ** numerator * abs(coefficient) ** denominator + - abs(constant) ** denominator) + return ((coefficient > 0) - (coefficient < 0)) * ( + (difference > 0) - (difference < 0)) + + +def power_checks(): + require(power_sign(479, -240, 997, 1000) == -1, "240 is too small") + require(power_sign(481, -241, 997, 1000) == 1, "241 attains trap") + require(power_sign(0, 1, 997, 1000) == 1, "joint improvement") + small = 0 + for a in range(1, 241): + for b in range(1, a): + require(power_sign(a + b, -a, 997, 1000) < 0, + "smaller incoming multiplicity") + small += 1 + require(Fraction(10940329, 3500000000) > Fraction(3, 1000), + "pinned complex power is outside covered interval") + require(power_sign(481, -241, 1, 1) == -1, "linear-tariff control") + return {"exponent": "997/1000", "minimum_edges": 481, + "a": 241, "b": 240, "smaller_a_pairs": small, + "current_complex_C_provenance": "10940329/3500000000"} + + +def must_reject(kind, args): + try: + if kind == "parameters": + parameters(*args) + elif kind == "power": + power_sign(*args) + elif kind == "receipt": + validate_receipt(*args) + else: + raise RuntimeError("unknown rejection control") + except ValueError: + return + raise ValueError("control was accepted") + + +def validate_receipt(expected, actual): + require(type(expected) is dict and expected == actual, "receipt mismatch") + + +def controls(): + names = [] + for bad in (Fraction(1), Fraction(2), Fraction(0), Fraction(3)): + must_reject("parameters", (bad, 2, 1)) + names.append("invalid tariff " + str(bad)) + for a, b in ((0, 1), (1, 0), (1001, 1), (True, 1)): + must_reject("parameters", (Fraction(3, 2), a, b)) + names.append("invalid multiplicity " + str((a, b))) + require(not (3 > 2 * Fraction(3, 2) > Fraction(3, 2)), "tie is strict") + names.append("non-strict boundary") + require(minimum_edges(Fraction(3, 2)) == 5, "strict rounding control") + names.append("integer reciprocal boundary") + require(not projector((0, 1, 0, 0), 2), "nilpotent is a projection") + names.append("non-idempotent rank-one map") + require(multiply((1, 0, 0, 0), (1, 1, 0, 0), 2) != (0, 0, 0, 0), + "noncomplementary pair is an escape") + names.append("noncomplementary pair") + must_reject("power", (1, -1, 1001, 1000)) + names.append("invalid power") + must_reject("receipt", ({"count": 1}, {"count": 2})) + names.append("changed receipt count") + must_reject("receipt", ({"hash": "bad"}, {"hash": "good"})) + names.append("changed receipt hash") + return names + + +def receipt(): + return { + "status": "PASS_PROJECTION_LOCAL_TRAP", + "claim_type": "scoped proof with exact finite corroboration", + "scalar_grid": scalar_grid(), + "fields": [field_checks(p) for p in FIELDS], + "power": power_checks(), + "controls": controls(), + "sha256": {name: sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in BOUND_FILES}, + "new_kappa": False, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--generate", action="store_true", + help="emit a new receipt without comparing RESULT.json") + args = parser.parse_args() + actual = receipt() + if not args.generate: + expected = json.loads((PACKAGE / "RESULT.json").read_text()) + validate_receipt(expected, actual) + print(json.dumps(actual, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()