From 06fc8ef80235f02c67295e474d7766f843f1eaa0 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 30 Oct 2026 11:29:43 +0000 Subject: [PATCH] feat(research): prove the single-merge cache cost floor --- .../p104-single-merge-cache-floor/PROOF.md | 142 +++++++++++ .../p104-single-merge-cache-floor/README.md | 119 ++++++++++ .../SOURCES.json | 24 ++ .../p104-single-merge-cache-floor/TASK.json | 91 +++++++ .../VALIDATION.md | 55 +++++ .../p104-single-merge-cache-floor/VERIFY.json | 34 +++ .../p104-single-merge-cache-floor/verify.py | 223 ++++++++++++++++++ 7 files changed, 688 insertions(+) create mode 100644 research/p104-single-merge-cache-floor/PROOF.md create mode 100644 research/p104-single-merge-cache-floor/README.md create mode 100644 research/p104-single-merge-cache-floor/SOURCES.json create mode 100644 research/p104-single-merge-cache-floor/TASK.json create mode 100644 research/p104-single-merge-cache-floor/VALIDATION.md create mode 100644 research/p104-single-merge-cache-floor/VERIFY.json create mode 100644 research/p104-single-merge-cache-floor/verify.py diff --git a/research/p104-single-merge-cache-floor/PROOF.md b/research/p104-single-merge-cache-floor/PROOF.md new file mode 100644 index 0000000000..413696a819 --- /dev/null +++ b/research/p104-single-merge-cache-floor/PROOF.md @@ -0,0 +1,142 @@ +# Exact tariff for a single merged operand cache + +This scoped proof is produced by Nick Petalas. Apache-2.0. + +## Model + +Let the frame spaces be over any field. Write S,U,H,L,R for subspaces with + + dim S=s, dim U=u, dim H=dim R=u+1, dim L=1, + 1 <= s < u, H intersection R=U, S,L <= U, L not contained in S. + +The field quantifier concerns frame geometry. Every nested MOVE is granted +as an available operation in the relaxation; native availability over an +arbitrary field is not asserted. The separate scalar payload check uses rational numbers. + +The reader ascends from zero to R. The root descends from H to L and is read +once at F. Two independent operands V and B are captured at S and U. Each +owned cache descends to one common merge frame M; one cache forms V+B there. +The sum cache then descends to A and is delivered once to the reader. The +reader also receives -4Q from the root at F. The required logical endpoint is +A_in+V+B-4Q, with all public sources unchanged. Coefficients are scalar and +fixed. The argument does not require independence in the actual source word. +Independence defines this local replacement contract. + +Every nested native MOVE of rank r costs phi(r). Here phi(0)=0 and phi is +nonnegative, increasing and concave on nonnegative integer ranks. All native +cache transport is charged. Waiting, clean owned storage, capture, the merge, +disposal and ordinary control are free in this deliberately favorable model. +Disposal can discard arbitrary cache contents. This is a tariff relaxation, +not a physical erasure or native implementation claim. + +There is exactly one merge and one subsequent sum delivery. There are no +additional reads, split deliveries, public ascending caches, cloned roots, +changed productive targets or coordinated removal of other work. Intermediate +stops on each monotone path are unrestricted. Scalar logical payload checks +do not establish the native meaning of those paths. + +Jerry Chen / CubeJerry's PR6248 supplies the question of mixed operands and +the inherited reader-497 geometry. Its separate-cache theorem is not replayed +or reproved here. The new model merges the sources before delivery. + +## Reduction to three dimensions + +Both pre-merge caches descend, so M<=S<=U. The sum descends to A<=M. Since +L<=F<=H and F lies on the reader path to R, L<=F<=U. Reader contacts A,F +are comparable. F cannot be below or equal to A: that would give L<=S. +Thus A= phi(s), + phi(u-m) >= phi(u-s). + +The remaining terms are phi(1)+2phi(u). Therefore C>=C_low. Equality is +attained at (a,m,f)=(0,s,1), with M=S, A=0 and F=L. + +If f>=2, both root segment ranks lie between 1 and u-1 and sum to u. +Concavity minimizes their sum at the two extreme ranks: + + phi(u+1-f)+phi(f-1) >= phi(1)+phi(u-1). + +Group the other terms as follows: + + phi(a)+phi(s-m)+phi(m-a) >= phi(s), + phi(f-a)+phi(u+1-f) >= phi(1)+phi(u-a), + phi(u-a) >= phi(u-s), + phi(u-m) >= phi(u-s). + +For the second inequality, its two arguments are at least one and sum to +u+1-a. Concavity again places the minimum at the extremes 1,u-a. Adding +the inequalities gives C>=C_high. Equality is attained at +(a,m,f)=(s,s,u), with A=M=S and F=U. This proves the claimed exact minimum +without enumerating fields, subspaces or path lengths. + +The excess over the unchanged schedule is exactly + + min(2phi(u)-phi(1)-phi(u-1), phi(u-s)). + +Both terms are nonnegative for increasing phi. For phi(r)=r^t, 01, and u-s>=1. Thus no itinerary in this +single-merge class improves the complete signed moment when other work and +productive targets stay fixed. Any additional nonnegative physical charge +only increases this obstruction. + +## Reader 497 and finite evidence + +PR6248 identifies s=3,u=6 for frames S=519,U=520,H=529,L=595,R=914 in +Ali Romman's PR6167. These source identities and inclusions are inherited +premises, not a new audit of the word. The new exact minimum is + + min(H1+2H3+2H6, 2H1+3H3+H5), + +whereas C0=2H1+2H3+H5. The excess is + + min(2H6-H1-H5, H3) > 0, for H_r=r^t and 0=2 endpoint. Since every increasing +concave tariff is a nonnegative combination of min(r,k) on a bounded integer +domain, these integer certificates corroborate the complete tariff comparison. +The same finite check covers 2<=u<=14 and 1<=s 0. + +This closes one mixed-cache route explicitly left outside Jerry Chen / +CubeJerry's [PR6248](https://github.com/CrocSwap/integer-mult-bounds/pull/6248). +That result keeps the two caches separate. Here they descend to a common +frame, form V+B once, and deliver that sum to the ascending reader. Every +native cache MOVE is charged. This is a new representation and tariff proof, +not a replay of the predecessor's numbers. + +## General result and scope + +Let S,U,H,L,R have dimensions s,u,u+1,1,u+1, with 1<=s= 0, "capped-sum floor") + return differences + + +def check_dimensions(): + actual, pair_count, recipe_count = [], 0, 0 + for u in range(2, MAX_DIMENSION+1): + for s in range(1, u): + pair_count += 1 + low, high = endpoints(s, u) + require(formula(s, u, 0, s, 1) == low, "low endpoint attainment") + require(formula(s, u, s, s, u) == high, "high endpoint attainment") + for m in range(s+1): + for a in range(m+1): + for f in range(a+1, u+1): + profile = geometric_profile(s, u, a, m, f) + require(profile == formula(s, u, a, m, f), "independent geometric invoice") + differences = certify(profile, low if f == 1 else high, u) + recipe_count += 1 + if (s, u) == (3, 6): + actual.append({"a": a, "m": m, "f": f, + "paid_ranks": profile, "cap_gaps": differences}) + require(len(actual) == 50, "reader-497 recipe coverage") + require(pair_count == 91 and recipe_count == 20_839, "general finite coverage") + return pair_count, recipe_count, actual + + +def payload_word(): + # Rows are A,V,B,Q,C_V,C_B. Disposal is explicitly free in this relaxation. + return (("copy", 4, 1, 1), ("copy", 5, 2, 1), ("add", 4, 5, 1), + ("clear", 5, 0, 0), ("add", 0, 4, 1), ("clear", 4, 0, 0), + ("add", 0, 3, -4)) + + +def execute(word, public): + require(len(word) <= 8 and len(public) == 4, "payload bounds") + rows = [*public, Fraction(0), Fraction(0)] + for operation, destination, source, coefficient in word: + require(0 <= destination < 6 and 0 <= source < 6, "row bounds") + if operation == "copy": + require(rows[destination] == 0, "copy into empty owned row") + rows[destination] = coefficient*rows[source] + elif operation == "add": + rows[destination] += coefficient*rows[source] + elif operation == "clear": + rows[destination] = Fraction(0) + else: + raise ValueError("unknown payload operation") + return tuple(rows) + + +def expected(public): + a, v, b, q = public + return (a+v+b-4*q, v, b, q, Fraction(0), Fraction(0)) + + +def check_payload(): + basis = [tuple(Fraction(i == j) for i in range(4)) for j in range(4)] + samples = [tuple(Fraction(x, 3) for x in row) for row in product(range(-1, 2), repeat=4)] + for public in [*basis, *samples]: + require(execute(payload_word(), public) == expected(public), "dirty payload endpoint") + return basis, len(basis)+len(samples) + + +def check_controls(basis): + invalid = ((3, 6, 1, 0, 2), (3, 6, 1, 1, 1), (3, 6, 0, 4, 6), + (3, 6, 0, 0, 7), (0, 6, 0, 0, 1), (3, 6, True, 1, 2)) + for arguments in invalid: + reason = ("integer dimensions" if type(arguments[2]) is bool else + "dimension range" if arguments[0] == 0 else "contact incidence") + try: + formula(*arguments) + except ValueError as error: + require(str(error) == reason, "wrong recipe rejection") + else: + raise ValueError("invalid recipe accepted") + # Omitting B's cache transport turns the high endpoint into the old bill. + baseline = (1, 1, 3, 3, 5) + try: + certify(baseline, endpoints(3, 6)[1], 6) + except ValueError as error: + require(str(error) == "capped-sum floor", "wrong unpaid-MOVE rejection") + else: + raise ValueError("unpaid B transport accepted") + # Removing every cache MOVE produces a false optimistic improvement in call count. + require(caps((1, 6, 6), 6)[0] < caps(baseline, 6)[0], "unpaid-cache control") + changes = ((0, ("copy", 4, 2, 1)), (2, ("add", 4, 5, 0)), + (4, ("copy", 0, 4, 1)), (5, ("add", 4, 5, 0)), + (6, ("add", 0, 3, 0))) + for index, gate in changes: + word = list(payload_word()) + word[index] = gate + rejects = 0 + for public in basis: + try: + rejects += execute(word, public) != expected(public) + except ValueError: + rejects += 1 + require(rejects > 0, "payload mutation escaped") + return len(invalid)+2+len(changes) + + +def package_hashes(): + files = sorted(PACKAGE.iterdir()) + names = {"README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "VALIDATION.md", "verify.py"} + require({path.name for path in files} == names, "package file inventory") + hashes = {} + for path in files: + require(path.is_file() and not path.is_symlink(), "regular package files") + require(path.stat().st_size <= 1_048_576, "package byte bound") + data = path.read_bytes() + require(len(data) <= 1_048_576, "package byte bound") + hashes[path.name] = hashlib.sha256(data).hexdigest() + return hashes + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="write a generated receipt outside the checkout") + args = parser.parse_args() + pairs, recipes, actual = check_dimensions() + basis, payload_cases = check_payload() + controls = check_controls(basis) + result = {"status": "PASS_SINGLE_MERGE_CACHE_FLOOR", "dimension_pairs": pairs, + "dimension_recipes": recipes, "reader497_recipes": len(actual), + "payload_cases": payload_cases, "controls": controls, + "python": platform.python_version(), "package_sha256": package_hashes(), + "reader497_certificate": actual} + if args.receipt: + target = args.receipt.resolve() + require(not target.is_relative_to(PACKAGE.parents[1]), "receipt must be outside checkout") + encoded = json.dumps(result, indent=2)+"\n" + require(target.write_text(encoded, encoding="utf-8") == len(encoded), "receipt write") + summary = {key: result[key] for key in ("status", "dimension_pairs", "dimension_recipes", + "reader497_recipes", "payload_cases", "controls")} + print(json.dumps(summary, sort_keys=True)) + + +if __name__ == "__main__": + main()