From b66de876c724361b49f9dfe5ef70016862caab09 Mon Sep 17 00:00:00 2001 From: flyingviper <44173173+flyingviper@users.noreply.github.com> Date: Mon, 26 Oct 2026 17:40:32 +0100 Subject: [PATCH] Bound fixed rank-one active repair by 101 channels --- research/active-rank1-controller/README.md | 90 ++ research/active-rank1-controller/SOURCES.json | 36 + research/active-rank1-controller/TASK.json | 90 ++ research/active-rank1-controller/VERIFY.json | 30 + research/active-rank1-controller/Y-CLEANUP.md | 38 + .../rank1-controller.json | 1106 +++++++++++++++++ .../rank1_controller.py | 281 +++++ research/active-rank1-controller/verify.py | 34 + .../active-rank1-controller/y-cleanup.json | 142 +++ research/active-rank1-controller/y_cleanup.py | 96 ++ 10 files changed, 1943 insertions(+) create mode 100644 research/active-rank1-controller/README.md create mode 100644 research/active-rank1-controller/SOURCES.json create mode 100644 research/active-rank1-controller/TASK.json create mode 100644 research/active-rank1-controller/VERIFY.json create mode 100644 research/active-rank1-controller/Y-CLEANUP.md create mode 100644 research/active-rank1-controller/rank1-controller.json create mode 100644 research/active-rank1-controller/rank1_controller.py create mode 100644 research/active-rank1-controller/verify.py create mode 100644 research/active-rank1-controller/y-cleanup.json create mode 100644 research/active-rank1-controller/y_cleanup.py diff --git a/research/active-rank1-controller/README.md b/research/active-rank1-controller/README.md new file mode 100644 index 0000000000..d70220ba19 --- /dev/null +++ b/research/active-rank1-controller/README.md @@ -0,0 +1,90 @@ +# Fixed rank-one channels cannot cheaply repair the retained modes + +This source-bound necessary-quotient result restricts the rank-one-only part of +[Ali Romman's PR5745](https://github.com/CrocSwap/integer-mult-bounds/pull/5745) +open question about nine or more jointly noisy channels. It builds on +[flyingviper's PR5720](https://github.com/CrocSwap/integer-mult-bounds/pull/5720). +No new multiplication bound or physical construction is claimed. + +## Contract + +Keep the frozen F9-SOURCE-DAG-ALL8 backward word and omit its unimplemented +physical_add tail. Each channel carries a fixed scalar combination of the eight +original captured modes, prepared in one fixed rank-one chart. It may scatter +at any number of chronological contacts in that chart. Arbitrarily many +channels and joint cancellation of their nuisance outputs are allowed. Each +channel must pay its preparation; gathering, storage and ordinary scatter costs +are optimistically ignored. Ground-helper cleanup is granted. Y must return +correctly through the stated controls: extra delivery to its final charts is +not granted for free. + +Changing the native word, recomputing a payload from changed live data, +inter-chart transport or reframing, and extra paid cleanup are outside this +contract. Native address operators use the retained common-fixed-vector +specialization. A negative necessary test is not a general feedback theorem. + +## Certificate and proof + +The retained endpoint is X-CY, Y, H, with C=I-R^T R/4. For every control form +Z=deltaX+C deltaY. If all Y outputs are restored, the desired X correction must +be supplied by Z. This allows cancellations between different channels rather +than requiring each channel to be clean independently. + +The exact census covers every response-changing interval in each actual +rank-one chart. For each chart, retain the union of possible nonzero Z output +coordinates. Assign nonnegative weights to required output coordinates such +that every chart's union has total weight at most one. Any successful set of +charts must cover every required coordinate, so its size is at least the total +weight. This argument permits arbitrary rational coefficients and cancellation; +it is not a bounded coefficient search. + +The retained certificate establishes a weight of 50 for mode5. For the full +eight-mode correction, all 112 X rows are required. The only chart reaching +multiple Z coordinates reaches twelve; give those coordinates weight 1/12 and +the other hundred weight one. Every chart has load at most one, giving a bound +of 101 distinct fixed rank-one charts and hence at least 101 channels. +For the recursive power tariff H_r=r^q H_1, 0= 0, + "invalid field owner") + _require(kind != "L" or index < PUBLIC, "public owner out of range") + return index if kind == "L" else PUBLIC + index + + +def _add(destination, source, coefficient): + # A copy also makes self-add semantics explicit. + for key, value in list(source.items()): + result = destination.get(key, ZERO) + coefficient * value + if result: + destination[key] = result + else: + destination.pop(key, None) + + +def _canonical_sha(value): + payload = json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + return hashlib.sha256(payload).hexdigest() + + +def _chart_support(rows, controls, actual): + support = {frame: set() for frame in actual} + for port, row in enumerate(rows[:PORTS]): + for control, coefficient in row.items(): + if coefficient: + support[controls[control]["frame"]].add(port) + return support + + +def _validate_weights(support, weights): + _require(weights and all(weight > 0 for weight in weights.values()), + "weights must be strictly positive on the target support") + loads = {frame: sum((weights.get(port, ZERO) for port in ports), ZERO) + for frame, ports in support.items()} + _require(loads and max(loads.values()) <= 1, + "a chart covers target weight greater than one") + return sum(weights.values(), ZERO), max(loads.values()) + + +def _cover_certificate(support, target): + # The actual source has only one nonsingleton chart. The construction is + # still checked against every chart rather than assuming this shape. + broad = set().union(*(ports & target for ports in support.values() + if len(ports) > 1)) + _require(broad, "missing nonsingleton support for the frozen certificate") + weights = {port: Fraction(1, len(broad)) if port in broad else Fraction(1) + for port in target} + total, maximum = _validate_weights(support, weights) + _require(total.denominator == 1, "nonintegral frozen cover bound") + return { + "target_ports": sorted(target), + "target_weights": {str(port): str(weight) + for port, weight in sorted(weights.items())}, + "total_weight": str(total), + "maximum_chart_weight": str(maximum), + "minimum_distinct_fixed_chart_providers": int(total), + }, weights + + +def _expect_invalid(support, weights, label): + try: + _validate_weights(support, weights) + except ValueError as error: + _require(str(error) == "a chart covers target weight greater than one", + label + ": unexpected failure") + return {"rejected": True, "reason": str(error)} + raise ValueError(label + ": invalid support certificate was accepted") + + +def run(word_path, R_path): + """Return a compact, reproducible JSON certificate; do not write files.""" + word_bytes = Path(word_path).read_bytes() + R_bytes = Path(R_path).read_bytes() + word_sha = hashlib.sha256(word_bytes).hexdigest() + R_sha = hashlib.sha256(R_bytes).hexdigest() + _require(word_sha == WORD_SHA256, "wrong frozen backward word") + _require(R_sha == R_SHA256, "wrong frozen mode matrix") + source = json.loads(gzip.decompress(word_bytes)) + R = [[Fraction(value) for value in row] for row in json.loads(R_bytes)] + _require(len(R) == MODES and all(len(row) == PORTS for row in R), + "wrong mode matrix dimensions") + gram = [[sum((R[i][j] * R[k][j] for j in range(PORTS)), ZERO) + for k in range(MODES)] for i in range(MODES)] + _require(all(gram[i][k] == (56 if i == k else 0) + for i in range(MODES) for k in range(MODES)), + "the exact source normalization is RR^T=56I") + _require(all(any(row[j] for row in R) for j in range(PORTS)), + "a full-mode target row is zero") + + events = source["programs"]["backward"] + canonical = source["canonical"] + _require(len(canonical["start"]) == PUBLIC + and len(canonical["final"]) == PUBLIC, "wrong public interface") + frame_bases = canonical["frames"] + _require(all(len(frame_bases[canonical["start"][PORTS+j]]) == 0 + and len(frame_bases[canonical["final"][PORTS+j]]) == 8 + for j in range(PORTS)), "Y boundary is not ground to rank eight") + allowed = {"scalar", "warp", "climb", "center", "phase", "adapter", + "residual_adapter", "physical_add"} + _require(all(event[0] in allowed for event in events), "unknown source opcode") + owners = [_owner(operand) for event in events if event[0] == "scalar" + for operand in event[1] if isinstance(operand, list)] + nroles = max(owners + [PUBLIC]) + 1 + frames = list(canonical["start"]) + [None] * (nroles - PUBLIC) + rank_one = {i for i, basis in enumerate(frame_bases) if len(basis) == 1} + + # A unit impulse's suffix column changes at a read of its owner, scale, + # overwrite, clear, or warp. ADD-to-owner alone has unit diagonal. Together + # with rank-one arrivals these cuts cover every chronological contact; + # duplicate response columns are harmless and no coefficient grid is used. + sites = {(0, owner, frame) for owner, frame in enumerate(frames) + if frame in rank_one} + for i, event in enumerate(events): + kind = event[0] + if kind == "scalar": + operation = event[1] + opcode, destination = operation[0], _owner(operation[1]) + _require(opcode in ("clear", "copy", "add", "scale"), + "unknown scalar opcode") + if opcode == "clear": + frames[destination] = event[2] + if opcode in ("copy", "add"): + origin = _owner(operation[2]) + if frames[origin] in rank_one: + sites.add((i+1, origin, frames[origin])) + if opcode in ("copy", "clear", "scale"): + if frames[destination] in rank_one: + sites.add((i+1, destination, frames[destination])) + elif kind in ("warp", "climb", "center"): + if kind == "warp": + destination, frame = _owner(event[1]), event[4] + elif kind == "climb": + destination, frame = event[2], event[4] + else: + destination, frame = PUBLIC + event[1], event[3] + frames[destination] = frame + if frame in rank_one: + sites.add((i+1, destination, frame)) + + controls = [{"boundary": boundary, "owner": owner, "frame": frame} + for boundary, owner, frame in sorted(sites)] + actual = {control["frame"] for control in controls} + _require(len(actual) == 115 and len(controls) == 1090, + "frozen rank-one contact census changed") + by_boundary = {} + for number, control in enumerate(controls): + by_boundary.setdefault(control["boundary"], []).append( + (control["owner"], number)) + + rows = [{} for _ in range(nroles)] + for i, event in enumerate(events): + for owner, number in by_boundary.get(i, []): + rows[owner][number] = rows[owner].get(number, ZERO) + 1 + if event[0] != "scalar": + continue # Fixed-vector, normalized ABI; omit physical_add. + operation = event[1] + opcode, destination = operation[0], _owner(operation[1]) + if opcode == "clear": + rows[destination] = {} + elif opcode == "copy": + rows[destination] = dict(rows[_owner(operation[2])]) + elif opcode == "add": + _add(rows[destination], rows[_owner(operation[2])], + Fraction(operation[3], operation[4])) + elif opcode == "scale": + coefficient = Fraction(operation[2], operation[3]) + rows[destination] = {key: value * coefficient + for key, value in rows[destination].items() + if value * coefficient} + for owner, number in by_boundary.get(len(events), []): + rows[owner][number] = rows[owner].get(number, ZERO) + 1 + raw_support = _chart_support(rows, controls, actual) + + # Source endpoint: X'=X-CY, Y'=Y, H'=H, C=I-R^T R/4. + # Initial ground Y preconditioning can cancel total final Y, but then its + # X response contributes C*deltaY. Thus Z is the necessary restored-Y + # response, including cancellations jointly across different providers. + for i in range(PORTS): + for j in range(PORTS): + coefficient = Fraction(i == j) - sum( + (R[k][i] * R[k][j] / 4 for k in range(MODES)), ZERO) + if coefficient: + _add(rows[i], rows[PORTS+j], coefficient) + support = _chart_support(rows, controls, actual) + _require(Counter(map(len, support.values())) == {0: 2, 1: 112, 12: 1}, + "unexpected restored-Y support shape") + _require(support[114] == support[115] == set() + and support[137] == {31, 33, 49, 55, 68, 74, 80, 83, 85, 88, 98, 101}, + "exceptional chart supports changed") + + one_target = {i for i, value in enumerate(R[5]) if value} + _require(len(one_target) == 56, "mode-five target support changed") + one, one_weights = _cover_certificate(support, one_target) + full, full_weights = _cover_certificate(support, set(range(PORTS))) + _require(one["minimum_distinct_fixed_chart_providers"] == 50 + and full["minimum_distinct_fixed_chart_providers"] == 101, + "unexpected fixed-chart cover bound") + + # These alter semantic boundary/coverage obligations, not numerical noise. + dropped_Y = _expect_invalid(raw_support, one_weights, + "dropped final-Y restoration") + dropped_Y["raw_chart_114_weight"] = str(sum( + (one_weights.get(port, ZERO) for port in raw_support[114]), ZERO)) + artificial = dict(support) + artificial[-1] = set(one_target) + extra_chart = _expect_invalid(artificial, one_weights, + "artificial all-target chart") + extra_chart["artificial_chart_weight"] = str(sum(one_weights.values(), ZERO)) + + return { + "schema": "active-rank1-controller-v1", + "source": {"word_sha256": word_sha, "R_sha256": R_sha, + "direction": "backward", "physical_add": "omitted"}, + "scope": { + "quotient": "common fixed vector; retained normalized adapter ABI", + "controller": "immutable payloads; one fixed rank-one chart per provider", + "contacts": "all coframed chronological additive intervals; native word unchanged", + "restoration": "final Y restored jointly; arbitrary helper cleanup granted", + "excluded": ["provider movement or reframing", "payload updates", + "additional native operations", "free final-Y cleanup"], + "claim": "necessary fixed-chart support bound, not a global feedback bound or new kappa", + }, + "census": {"public_fields": PUBLIC, "scalar_and_owned_fields": nroles, + "events": len(events), "mode_matrix_shape": [MODES, PORTS], + "mode_gram_diagonal": 56, "all_mode_columns_nonzero": True, + "rank_one_frame_inventory": len(rank_one), + "actual_rank_one_charts": len(actual), + "contact_intervals": len(controls), + "omitted_physical_add_events": sum(e[0] == "physical_add" for e in events)}, + "controls_sha256": _canonical_sha(controls), + "actual_rank_one_frame_bases": {str(frame): frame_bases[frame] + for frame in sorted(actual)}, + "output_nulling_invariant": "Z=deltaX+(I-R^T R/4)*deltaY", + "chart_Z_support": {str(frame): sorted(support[frame]) for frame in sorted(actual)}, + "one_mode_cover": one, + "full_eight_mode_cover": full, + "semantic_negative_controls": { + "dropped_final_Y_restoration": dropped_Y, + "artificial_all_target_chart": extra_chart, + }, + } diff --git a/research/active-rank1-controller/verify.py b/research/active-rank1-controller/verify.py new file mode 100644 index 0000000000..fbb54bfc4d --- /dev/null +++ b/research/active-rank1-controller/verify.py @@ -0,0 +1,34 @@ +"""Source-bound, read-only fixed-rank-one controller replay.""" +from pathlib import Path +from tempfile import TemporaryDirectory +from hashlib import sha256 +import io,json,tarfile,types +HERE=Path(__file__).resolve().parent +ARCHIVE=HERE.parents[1]/'research/filtered-native-kappa004/inputs/original-packet.tar.gz' +ARCHIVE_SHA='595f988e748b1f3b25e7525a226da173966e4278a70f511b2919245cec1b45f7' +MEMBERS={ + 'word':('research/retained_state_next/F9-SOURCE-DAG-ALL8-WORD.json.gz','934fea11e51f674ce2031b7d3127b994a921a9d83317b00359292752563a1775'), + 'R':('upstream/research/involutory-producer-raw-dual/inputs/R/R.json','7b33b6dfb494c6eafe6d87a08d6a2c2e0681e56429495b2b27949040f0f63cd1')} +def need(ok,msg): + if not ok:raise ValueError(msg) +def load(name): + path=HERE/(name+'.py');m=types.ModuleType(name);m.__file__=str(path) + exec(compile(path.read_bytes(),str(path),'exec'),m.__dict__) + return m +def main(): + raw=ARCHIVE.read_bytes();need(sha256(raw).hexdigest()==ARCHIVE_SHA,'Exact source archive') + with TemporaryDirectory(prefix='active-rank1-') as temp: + paths={} + with tarfile.open(fileobj=io.BytesIO(raw),mode='r:gz') as archive: + inventory=archive.getmembers() + for key,(name,digest) in MEMBERS.items(): + matches=[m for m in inventory if m.name=='filtered_native_implementation/'+name] + need(len(matches)==1 and matches[0].isfile(),'Unique regular data member') + data=archive.extractfile(matches[0]).read();need(sha256(data).hexdigest()==digest,'Pinned data member') + paths[key]=Path(temp)/(key+'.input');paths[key].write_bytes(data) + for module,receipt in [('rank1_controller','rank1-controller.json'),('y_cleanup','y-cleanup.json')]: + actual=load(module).run(paths['word'],paths['R']) + expected=json.loads((HERE/receipt).read_bytes()) + need(actual==expected,'Complete exact certificate comparison: '+receipt) + print('PASS_FIXED_RANK1_CONTROLLER_AND_CLEANUP_GEOMETRY; no new bound claimed') +if __name__=='__main__':main() diff --git a/research/active-rank1-controller/y-cleanup.json b/research/active-rank1-controller/y-cleanup.json new file mode 100644 index 0000000000..458b040eb9 --- /dev/null +++ b/research/active-rank1-controller/y-cleanup.json @@ -0,0 +1,142 @@ +{ + "schema": 1, + "source_word_sha256": "934fea11e51f674ce2031b7d3127b994a921a9d83317b00359292752563a1775", + "R_sha256": "7b33b6dfb494c6eafe6d87a08d6a2c2e0681e56429495b2b27949040f0f63cd1", + "R_gram": "56 I8", + "C_definition": "I112 - transpose(R)*R/4", + "R_times_C": "-13 R", + "C_inverse": "I112 - transpose(R)*R/52", + "inverse_identity_checked_using_exact_R_gram": true, + "pure_Y_route_assumption": "deltaX = -C*deltaY; desired deltaX = -transpose(r5)*m", + "unique_deltaY": "-transpose(r5)*m/13", + "all112_C_times_deltaY_entries_equal_r5": true, + "deltaY_nonzero_denominators": [ + 13 + ], + "Y_initial_rank": 0, + "Y_final_rank": 8, + "mode5_support": [ + 4, + 5, + 10, + 11, + 14, + 15, + 18, + 19, + 20, + 21, + 22, + 23, + 29, + 30, + 33, + 34, + 36, + 37, + 39, + 40, + 41, + 42, + 46, + 47, + 49, + 50, + 52, + 53, + 54, + 55, + 59, + 60, + 62, + 63, + 64, + 65, + 68, + 69, + 70, + 71, + 73, + 74, + 83, + 84, + 90, + 91, + 96, + 97, + 101, + 102, + 105, + 106, + 108, + 109, + 110, + 111 + ], + "mode5_Y_target_frames": [ + 146, + 147, + 152, + 153, + 156, + 157, + 160, + 161, + 162, + 163, + 164, + 165, + 171, + 172, + 175, + 176, + 178, + 179, + 181, + 182, + 183, + 184, + 188, + 189, + 191, + 192, + 194, + 195, + 196, + 197, + 201, + 202, + 204, + 205, + 206, + 207, + 210, + 211, + 212, + 213, + 215, + 216, + 225, + 226, + 232, + 233, + 238, + 239, + 243, + 244, + 247, + 248, + 250, + 251, + 252, + 253 + ], + "distinct_rank8_targets": 56, + "all_distinct_target_pairs_join_to_rank9": true, + "rank1_chart_target_containment": { + "72": 28, + "114": 24, + "115": 24 + }, + "scope": "Conditional scalar identity and literal cleanup geometry only. No paid-native-route lower bound, dyadic compilation, or physical construction is claimed." +} diff --git a/research/active-rank1-controller/y_cleanup.py b/research/active-rank1-controller/y_cleanup.py new file mode 100644 index 0000000000..a103e8a58a --- /dev/null +++ b/research/active-rank1-controller/y_cleanup.py @@ -0,0 +1,96 @@ +"""Exact scalar inverse and literal Y-cleanup geometry; no native replay.""" +from fractions import Fraction +from hashlib import sha256 +from pathlib import Path +import gzip +import json + + +WORD_SHA256 = '934fea11e51f674ce2031b7d3127b994a921a9d83317b00359292752563a1775' +R_SHA256 = '7b33b6dfb494c6eafe6d87a08d6a2c2e0681e56429495b2b27949040f0f63cd1' + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def binary_rank(vectors): + basis = {} + for value in vectors: + while value: + pivot = value.bit_length() - 1 + if pivot in basis: + value ^= basis[pivot] + else: + basis[pivot] = value + break + return len(basis) + + +def run(word_path, R_path): + """Read the two pinned archive members and return JSON-compatible facts.""" + raw, rraw = Path(word_path).read_bytes(), Path(R_path).read_bytes() + need(sha256(raw).hexdigest() == WORD_SHA256, 'Wrong native word bytes') + need(sha256(rraw).hexdigest() == R_SHA256, 'Wrong R bytes') + word = json.loads(gzip.decompress(raw)) + rows = [[Fraction(value) for value in row] for row in json.loads(rraw)] + need(len(rows) == 8 and all(len(row) == 112 for row in rows), 'Wrong R shape') + gram = [[sum(a*b for a, b in zip(x, y)) for y in rows] for x in rows] + need(gram == [[Fraction(56 if i == j else 0) for j in range(8)] + for i in range(8)], 'R Gram matrix is not 56 I8') + # P=R^T R has P^2=56P. This is the coefficient of P in + # (I-P/4)(I-P/52), establishing the displayed inverse exactly. + inverse_coefficient = -Fraction(1, 4)-Fraction(1, 52)+Fraction(56, 208) + need(inverse_coefficient == 0, 'Claimed C inverse does not multiply to I') + mode = rows[5] + delta_y = [-x/13 for x in mode] + r_delta_y = [sum(a*b for a, b in zip(row, delta_y)) for row in rows] + c_delta_y = [delta_y[i]-sum(rows[k][i]*r_delta_y[k] for k in range(8))/4 + for i in range(112)] + need(c_delta_y == mode, 'C deltaY is not r5 on all112 entries') + + canonical = word['canonical'] + frame_rows = canonical['frames'] + need(frame_rows[0] == [], 'Ground frame is not frame0') + need(all(canonical['start'][i] == 0 for i in range(112, 224)), + 'Y does not start at ground') + need(all(len(frame_rows[canonical['final'][i]]) == 8 for i in range(112, 224)), + 'Y does not finish at rank8') + support = [i for i, value in enumerate(mode) if value] + frames = [canonical['final'][112+i] for i in support] + need(len(support) == 56 and set(mode) == {Fraction(-1), Fraction(0), Fraction(1)}, + 'Unexpected mode5 support or coefficients') + need(len(set(frames)) == 56, 'The56 Y destination frames are not distinct') + need(all(binary_rank(frame_rows[f]+frame_rows[g]) == 9 + for i, f in enumerate(frames) for g in frames[i+1:]), + 'Two distinct Y target hyperplanes fail to join to rank9') + containment = {} + for frame in (72, 114, 115): + need(len(frame_rows[frame]) == 1, 'Selected provider frame is not rank1') + containment[str(frame)] = sum(binary_rank(frame_rows[frame]+frame_rows[g]) == 8 + for g in frames) + need(containment == {'72': 28, '114': 24, '115': 24}, + 'Unexpected rank1-provider containment counts') + return { + 'schema': 1, + 'source_word_sha256': WORD_SHA256, + 'R_sha256': R_SHA256, + 'R_gram': '56 I8', + 'C_definition': 'I112 - transpose(R)*R/4', + 'R_times_C': '-13 R', + 'C_inverse': 'I112 - transpose(R)*R/52', + 'inverse_identity_checked_using_exact_R_gram': True, + 'pure_Y_route_assumption': 'deltaX = -C*deltaY; desired deltaX = -transpose(r5)*m', + 'unique_deltaY': '-transpose(r5)*m/13', + 'all112_C_times_deltaY_entries_equal_r5': True, + 'deltaY_nonzero_denominators': sorted({x.denominator for x in delta_y if x}), + 'Y_initial_rank': 0, + 'Y_final_rank': 8, + 'mode5_support': support, + 'mode5_Y_target_frames': frames, + 'distinct_rank8_targets': 56, + 'all_distinct_target_pairs_join_to_rank9': True, + 'rank1_chart_target_containment': containment, + 'scope': 'Conditional scalar identity and literal cleanup geometry only. No paid-native-route lower bound, dyadic compilation, or physical construction is claimed.', + }