From e384ae7181f085f92d21e3578976e3231c76e26d Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Mon, 2 Nov 2026 19:38:51 +0000 Subject: [PATCH] feat(research): prove exact signed idle completion --- .../signed-overlap-idle-completion/PROOF.md | 110 ++++++++++++ .../signed-overlap-idle-completion/README.md | 119 +++++++++++++ .../RESULT.json | 167 ++++++++++++++++++ .../SOURCES.json | 24 +++ .../signed-overlap-idle-completion/TASK.json | 90 ++++++++++ .../VERIFY.json | 32 ++++ .../signed-overlap-idle-completion/verify.py | 164 +++++++++++++++++ 7 files changed, 706 insertions(+) create mode 100644 research/signed-overlap-idle-completion/PROOF.md create mode 100644 research/signed-overlap-idle-completion/README.md create mode 100644 research/signed-overlap-idle-completion/RESULT.json create mode 100644 research/signed-overlap-idle-completion/SOURCES.json create mode 100644 research/signed-overlap-idle-completion/TASK.json create mode 100644 research/signed-overlap-idle-completion/VERIFY.json create mode 100644 research/signed-overlap-idle-completion/verify.py diff --git a/research/signed-overlap-idle-completion/PROOF.md b/research/signed-overlap-idle-completion/PROOF.md new file mode 100644 index 0000000000..73bfced6e2 --- /dev/null +++ b/research/signed-overlap-idle-completion/PROOF.md @@ -0,0 +1,110 @@ +# Signed whole-idle completion of an overlapping stage demand + +This scoped proof about a determinant relaxation was produced by Nick Petalas. +It is not a construction of the proposed caller. + +## Formal contract + +Work over K = Q(q,A,B,C), with algebraically independent stage variables +A,B,C. There are six arbitrary independent main fields. Helpers are autonomous +outputs outside these six fields and cannot be mixed into them. Use each of +three full calls exactly once. The A call is A times a determinant one query +on a two-dimensional subspace, and identity on its complement. Define the B +and C calls likewise. Query orientations and chronology are unrestricted. + +Any number of invertible maps over Q(q) are free in this relaxation, including +constant field mixing and determinant one thin queries. Their physical costs +are not declared zero. A paid whole-idle atom chooses a nonempty subset S of +{A,B,C}, a sign epsilon in {-1,+1}, and one field line. It multiplies that line +by (product of the stages in S)^epsilon. Constant conjugation is allowed. +Each stage has eight fresh axes. An atom costs H(8|S|), including an inverse +atom. There are no other stage-dependent operations. Every word is finite. + +The desired stage multiset has two ABC outputs, two AB outputs and two BC +outputs. Central query factors may remain on the first pair, with +stage-independent determinant. The target determinant has stage degrees +(4,6,4). The three full calls have degrees (2,2,2). Each atom contributes +epsilon times the indicator of S. Constant mixing cannot change these degrees. +Every exact word therefore requires the signed idle balance + + sum_atoms epsilon * 1_S = (2,4,2). (1) + +This necessary condition does not assert that every satisfying inventory +has a legal query endpoint. + +## Exact completion theorem + +Let H(0)=0, with H positive on (0,24], nondecreasing and concave on [0,24]. Among all +finite signed inventories satisfying (1), the minimum cost is + + 2 H(24) + 2 H(8). (2) + +Two positive ABC atoms and two positive B atoms attain this value in the +inventory relaxation. If H is strictly concave, this is the unique minimizing +signed subset multiset. Positions and conjugating maps are not classified. + +Write a=H(8), b=H(16), c=H(24). Give the coordinates dual weights + + y_A = y_C = (c-a)/2, y_B = a. + +These are nonnegative. Each nonempty subset S satisfies y(S)<=H(8|S|). +For B this is equality. For A or C, c<=3a gives (c-a)/2<=a. +For AB or BC, midpoint concavity gives (a+c)/2<=b. For AC use c-a<=b: +the increment on [16,24] is at most the increment on [0,8], so c<=a+b. +For ABC there is equality at c. + +A positive atom costs at least y(S). A negative atom costs at least -y(S), +since its cost is positive and y(S)>=0. Summing and using (1) gives +cost >= 2y_A+4y_B+2y_C = 2c+2a. The stated inventory attains this bound. +This proves (2) for arbitrary word length and arbitrary inverse calls. + +Strict concavity gives c<3a, (a+c)/2 0. (3) + +For an explicit proof, start with (8,8,25,25,25,25). Twice replace a pair +(8,25) by (16,17), then twice replace (16,25) by (17,24). The result is +(17,17,17,17,24,24). Every replacement preserves the sum and strictly +increases the sum of H by strict concavity. Both lists sum to 116. +For a linear tariff the rewards agree. + +The comparison cancels identical full-call/helper and other charges between +two hypothetical contracts. It does not assume equal thin-query, ordinary, +storage or compiler costs. Any difference must be subtracted separately. +Neither six-field comparator is supplied as an operator word here. Equation +(3) is an improved optimistic budget, not a larger kappa or feasible supplier. + +## Applicability and remaining obligations + +The formal Laurent stage identity is an explicit hypothesis. A finite-order +Gaussian may satisfy additional relations. This degree condition is not an +impossibility theorem for every specialized native implementation. +Stage-dependent free maps, helper feedback, another rank/support relation, +changed native multiplicities or changed output contracts need new arguments. + +An attaining inventory need not be placeable at legal chronological cuts. +The exact query coefficients, independent output map, native frames and +absolute phases, arbitrary helper preservation, owned erasure, thin-query +count, precision, stock, tape movement, compiler and outer costs remain open. +No selected-frontier or complete multiplication theorem follows. diff --git a/research/signed-overlap-idle-completion/README.md b/research/signed-overlap-idle-completion/README.md new file mode 100644 index 0000000000..99f1b050eb --- /dev/null +++ b/research/signed-overlap-idle-completion/README.md @@ -0,0 +1,119 @@ +# Exact signed-idle bill for an overlapping stage contract + +Scoped proof with exact finite corroboration. No new kappa is claimed. +This contribution was produced by Nick Petalas. + +For six independent main fields with stage sets ABC, ABC, AB, AB, BC, BC, +and one native query-pair use of each stage, the determinant deficit is +(2,4,2). Allow arbitrary constant invertible mixing and forward or inverse +whole-idle calls on any nonempty stage subset. The exact idle-inventory +minimum, for every nondecreasing concave tariff H with H(0)=0, is + + 2H(24) + 2H(8). + +For a strictly concave tariff the unique optimal signed subset multiset has +two positive ABC calls and two positive B calls. The proof covers all finite +inventories, with no search cutoff. It does not construct a chronological +caller with that inventory. + +The corresponding target-minus-idle reward strictly exceeds the uniform +six-ABC completion reward for every power tariff H(r)=r^s, 0= sum(min(x, hinge) for x in old), "concave transfer") + checks += 1 + need(sorted(ranks) == [17, 17, 17, 17, 24, 24], "final reward ranks") + return checks + + +def rejects(function, *args): + try: + function(*args) + except (ValueError, TypeError): + return + raise ValueError("negative control was accepted") + + +def verify(): + tariffs = ((0, 1, 1, 1), (0, 1, 2, 2), (0, 1, 2, 3), + (0, 4, 6, 7), (0, 8, 11, 13)) + witness = [(1, (1, 1, 1))]*2 + [(1, (0, 1, 0))]*2 + finite = [] + for raw in tariffs: + tariff = tuple(map(Fraction, raw)) + expected = 2*tariff[3] + 2*tariff[1] + need(inventory_balance(witness, (2, 4, 2), tariff) == expected, + "attaining inventory cost") + for target, optimum in (((2, 4, 2), expected), + ((4, 4, 4), 4*tariff[3])): + distance, settled = shortest_inventory(target, tariff) + need(distance == optimum, "independent finite shortest path") + finite.append({"tariff": list(raw), "target": list(target), + "optimum": str(distance), "settled": settled}) + tariff = tuple(map(Fraction, tariffs[-1])) + rejects(inventory_balance, witness[:-1], (2, 4, 2), tariff) + rejects(inventory_balance, [(-1, witness[0][1])]+witness[1:], (2, 4, 2), tariff) + rejects(inventory_balance, [(1, (0, 0, 0))], (0, 0, 0), tariff) + rejects(inventory_balance, [(2, (1, 1, 1))], (2, 2, 2), tariff) + rejects(inventory_balance, [(1, (1, 2, 0))], (1, 2, 0), tariff) + rejects(inventory_balance, witness*9, (18, 36, 18), tariff) + targets = ((1, 1, 1),)*2 + ((1, 1, 0),)*2 + ((0, 1, 1),)*2 + degrees = tuple(sum(row[i] for row in targets) for i in range(3)) + need(tuple(x-2 for x in degrees) == (2, 4, 2), "native determinant debit") + return {"status": "PASS_SIGNED_OVERLAP_IDLE_COMPLETION", + "signed_dual_inequalities": dual_checks(), + "concave_transfer_checks": check_transfers(), + "finite_shortest_paths": finite, "rejecting_controls": 6, + "scope": "Scoped proof and finite corroboration; determinant relaxation only."} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-receipt", type=Path) + args = parser.parse_args() + report = verify() + report["source_sha256"] = { + name: sha256((ROOT/name).read_bytes()).hexdigest() + for name in ("verify.py", "PROOF.md", "README.md", "TASK.json", + "SOURCES.json", "VERIFY.json")} + payload = json.dumps(report, indent=2, sort_keys=True)+"\n" + if args.write_receipt: + with args.write_receipt.open("x") as destination: + need(destination.write(payload) == len(payload), "short receipt write") + else: + receipt = json.loads((ROOT/"RESULT.json").read_text()) + need(report == receipt, "receipt differs from current proof/source replay") + print(payload, end="") + + +if __name__ == "__main__": + main()