Finite construction: exact two-helper k8 gauges save 576 scalar primitives

research/k8-pair-dyadic-seed25/CLAIM.json

@@ -0,0 +1,59 @@
+{
+  "track": "complex supplier",
+  "seed": 25,
+  "seed_source": "secrets.randbelow(100), OS randomness",
+  "started_utc": "2026-10-13T19:56:01Z",
+  "expected_finish_utc": "2026-10-13T20:36:01Z",
+  "base_commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe",
+  "candidates": [
+    {
+      "object": "P112 masked decoder with rank-one odd-support correction",
+      "decision": "deferred; requires a new realization contract and broader synthesis"
+    },
+    {
+      "object": "P104 term delivery with paid downward frame moves",
+      "decision": "not selected; PR1125 already covers this mechanism"
+    },
+    {
+      "object": "PR1094 k8 two interacting helper diagonal scaling",
+      "decision": "selected; PR1161 covers single helpers; PR1170 consolidates existing stage scales"
+    }
+  ],
+  "scope": "Every unordered pair of non-center helpers joined by an ADD, each exponent in {-2,-1,1,2}; exact primitive costs and full maps for the best witness. Seed selects radius 1+seed%3=2. Existing SCALE and non-scalar events retained; entry/exit scales paid.",
+  "predecessor": {
+    "pr": 1161,
+    "head": "d210969d3158a1e6c505e41f67dd84e555c88564"
+  },
+  "changed_hypothesis": "Two helper coordinates may change simultaneously, including their connecting ADD coefficients.",
+  "optimistic_budget": "Recursive profile stays fixed; only a strictly reduced fully paid scalar primitive count is an acceptable local construction result. No kappa claim.",
+  "stopping_rule": "Complete finite adjacent-pair census; one winning exact scalar replay; stop new experiments by 20:26:01 UTC.",
+  "coordination": "No pinned issue returned by GraphQL; local claim, discussion board and 808 open PRs inspected.",
+  "deliverable": "One research package: exact finite search receipt, reproducible checker, witness, controls, pins and attribution.",
+  "attribution": "Hanson Sun with substantial OpenAI Codex assistance; credit PR1161 and its predecessor lineage; Apache-2.0.",
+  "pivot": {
+    "reason": "The bounded connected winner has zero interaction gain; the two best separate helpers nominate a stronger witness. Affine-cell geometry permits finite certification over all integer exponents.",
+    "domain": "All unordered pairs among the 237 cold-to-FULL, unwrapped, non-center helpers with no COPY/clear incidence; integer exponents including zero; same original ADD topology and all existing SCALEs fixed.",
+    "method": "Exact line-arrangement vertices; independent rectangular integer enumeration on interacting pairs and separable single-coordinate enumeration elsewhere.",
+    "coverage_goal": "27966 unordered helper pairs per orientation; no arbitrary exponent cutoff."
+  },
+  "result": {
+    "status": "verified finite scalar contribution",
+    "helpers": [
+      251,
+      427
+    ],
+    "forward_exponents": [
+      -2,
+      -2
+    ],
+    "backward_exponents": [
+      2,
+      2
+    ],
+    "saving_complex_primitives_per_orientation": 576,
+    "pairs_per_orientation": 27966,
+    "exponents": "all integers",
+    "new_kappa": false,
+    "artifact_url": "https://github.com/bbMisk/integer-mult-bounds/tree/hanson/complex-pair-scaling-seed25/research/k8-pair-dyadic-seed25"
+  }
+}

research/k8-pair-dyadic-seed25/CONTEXT.json

@@ -0,0 +1,48 @@
+{
+  "selected_at_base": {
+    "kappa": "836330098538459/500000000000000000",
+    "binding_supplier": "complex",
+    "reference": "research/community-frontier1094-audit/ASSEMBLY.json"
+  },
+  "source_authors": [
+    "woklerx / PR1161",
+    "Sagar Thakrar / PR696",
+    "Rohan Arun / PR1094",
+    "Jeremy Kothe / PR1042 and k8/T16 lineage",
+    "icekylinx / PR425, PR433, PR531, gauge44",
+    "Douglas Colkitt / retained source-bound review"
+  ],
+  "new_contributor": "Hanson Sun / bbMisk",
+  "assistance": "Substantial OpenAI Codex assistance: research, implementation, verification, documentation",
+  "license": "Apache-2.0",
+  "overlap": [
+    {
+      "pr": 1161,
+      "head": "d210969d3158a1e6c505e41f67dd84e555c88564",
+      "scope": "one non-center helper, all integer exponents",
+      "delta": "two helper coordinates, shared-edge interaction, exact pair census; byte-for-byte retained engine functions credited"
+    },
+    {
+      "pr": 1170,
+      "head": "df273e3cb1e62c1bfdf6599160b538e7a4b879d7",
+      "scope": "existing A/B SCALE consolidation",
+      "delta": "existing SCALE operations fixed; no composition claim"
+    },
+    {
+      "pr": 1064,
+      "head": "b0181971c2364744d1dd9b0c2d4ee1ea532b8bb6",
+      "scope": "local eight-register factory source scaling",
+      "delta": "whole selected finite scalar provider; all pairs within restricted boundary interface"
+    }
+  ],
+  "new_kappa": false,
+  "native_admission": false,
+  "global_hosted_invoice": false,
+  "formal_Lean_multiplication_theorem": false,
+  "final_overlap": {
+    "open_prs": 820,
+    "highest_observed_pr": 1211,
+    "specific_predecessor_head_unchanged": true,
+    "duplicates_found": false
+  }
+}

research/k8-pair-dyadic-seed25/README.md

@@ -0,0 +1,85 @@
+# Exact two-helper dyadic scaling of the k8 scalar provider
+
+Scaling L251 and L427 saves 576 scalar primitives per complex invocation in each orientation. This is optimal among dyadic gauges on at most two of the 237 eligible helpers, with ADD topology and existing SCALEs fixed. Each pair's cost is affine between vertical, horizontal and diagonal break lines. Boundary charges make it coercive; unit discounts lower boundary values. A minimum therefore occurs at an integral intersection. Independent integer-grid enumeration confirms every pair minimum. Exact replay checks all 712 input columns. Native hosting remains unchecked; no new kappa is claimed. Hanson Sun, with substantial OpenAI Codex assistance, credits @woklerx's PR1161, Sagar Thakrar's lowerer and the retained supplier lineage.
+
+| Orientation | Gauges on L251, L427 | Baseline | Candidate | Scalar saving |
+|---|---|---:|---:|---:|
+| Forward | 1/4, 1/4 | 149002 | 148426 | 576 |
+| Backward | 4, 4 | 149018 | 148442 | 576 |
+
+| Scope / evidence | Value |
+|---|---|
+| Status | Finite scalar construction; scoped optimization proof |
+| Base | `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe` |
+| Predecessor | [PR1161](https://github.com/CrocSwap/integer-mult-bounds/pull/1161), `d210969d3158a1e6c505e41f67dd84e555c88564` |
+| Scalar compiler | Sagar Thakrar, [PR696 lowering](../complex-dyadic-lowering/lower.py) |
+| Pair domain | 237 non-center, no-COPY/clear, unwrapped helpers; entry frame 0, exit FULL |
+| Exponents | All of `Z²`, including zero |
+| Topology | Original ADD operands/order; original SCALE/COPY/clear operations fixed |
+| Pair count / orientation | 27966 = 2414 interacting + 25552 separable |
+| Vertex evaluations / orientation | 735975 |
+| Independent integer-grid evaluations | 19162332, plus separable single-coordinate enumeration |
+| Original Horner saving | 416 scalar primitives / complex invocation / orientation |
+| Added boundary charges | 8 real shifts = 16 scalar primitives / complex invocation |
+| New helpers / frame moves / recursive children | 0 / 0 / 0 |
+| Paid profile | Exact equality in both orientations |
+| Positive prefix bounds | 52 / 68 bits; retained local charge 192 bits |
+| Independent literal inputs | 6 exact dirty-state cases, including coefficient workspace |
+| Rejection controls | 16 |
+| Excluded | Other helper interfaces; 3+ simultaneous gauges; negative signs; changing existing SCALEs; coefficient-work persistence; native/global invoice admission |
+| Inherited | All-size compiler, common-label/mutable-source realization, whole-call hosting, precision/tape, analytic transfer, bit H1–H5 |
+| Concurrent comparator | [PR1170](https://github.com/CrocSwap/integer-mult-bounds/pull/1170): stage SCALE consolidation; composition untested |
+| License | Apache-2.0 |
+
+```sh
+python3 -I -B research/k8-pair-dyadic-seed25/verify.py
+python3 -I -B research/k8-pair-dyadic-seed25/independent.py
+python3 -I -O -B research/k8-pair-dyadic-seed25/test_package.py
+```
+
+```text
+PASS_K8_PAIR_DYADIC_CENSUS
+PASS_INDEPENDENT_PAIR_GRID_AND_PRIMITIVES
+PASS_PAIR_REJECTION_CONTROLS
+```
+
+## Exact algebra and finite reduction
+
+```text
+h,j in eligible_helpers; (k,l) in Z²
+k_h = k, k_j = l, all other k_r = 0
+D = diag(2^k_r)
+ADD(t,s,q) -> ADD(t,s,q * 2^(k_t-k_s))
+D^-1 (D A_m D^-1) ... (D A_1 D^-1) D = A_m ... A_1
+
+|q_g| = p_g * 2^e_g, p_g positive odd
+c(p,e) = 2 + floor(log2(p)) + popcount(p) + |e| - [p=1 and e=0]
+f_g(x) = |x| - [p_g=1 and x=0]
+Delta(k,l) = 2|k| + 2|l|
+             + sum_g (f_g(e_g + sigma_g*k + tau_g*l) - f_g(e_g))
+(sigma_g,tau_g) in {(0,0),(1,0),(-1,0),(0,1),(0,-1),(1,-1),(-1,1)}
+Delta(k,l) >= 2|k| + 2|l| - sum_g f_g(e_g) - number_of_ADDs
+
+V = {0} union {-sigma_g*e_g : tau_g=0, sigma_g!=0}
+H = {0} union {-tau_g*e_g : sigma_g=0, tau_g!=0}
+D_break = {-sigma_g*e_g : sigma_g=-tau_g!=0}
+Vertices = {(v,h): v in V, h in H}
+           union {(v,v-d): v in V, d in D_break}
+           union {(h+d,h): h in H, d in D_break}
+
+Delta: lower semicontinuous, coercive, affine on each relative face interior
+face boundary discounts <= adjacent affine limits
+all nonparallel line-pair determinants = +/-1
+min_(Z²) Delta = min_(R²) Delta = min_Vertices Delta
+
+M = max_g |e_g| = 15
+Vertices subset [-2M,2M]²
+Independent interacting-pair grid = {-31,...,31}²
+Separable pairs: min Delta = min Delta_h + min Delta_j
+```
+
+[Certificate](CERTIFICATE.json) · [Full pair census](PAIR-CENSUS.json.gz) ·
+[Candidate programs](PROGRAMS.json.gz) · [Task card](CLAIM.json) ·
+[Sources](SOURCES.json) · [Validation](VALIDATION.json) ·
+[Retained predecessor proof](vendor/pr1161/PROOF.md) ·
+[Retained attribution](vendor/pr1161/PROVENANCE.md)

research/k8-pair-dyadic-seed25/SOURCES.json

@@ -0,0 +1,11 @@
+{
+  "base": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe",
+  "pr1161_head": "d210969d3158a1e6c505e41f67dd84e555c88564",
+  "vendor": {
+    "engine.py": "997b34533aea200c339263a96dd6f76facf21bf54b1627ab244e2ae72d348400",
+    "SOURCES.json": "45f24dbd27239e499600e497e3d86cf812f3b45122088ad083a836e8d646b320",
+    "BASE-SELECTED.json": "c49e308d209dfbaba184a0d41dbc03cb424663f7ad8136d56aba088bba7f5723",
+    "PROVENANCE.md": "76dca2049e8c008da0398fd722745e421be92c66dac876cf8463295f6cb18518",
+    "PROOF.md": "89cbba31b4d95b9c7c69e3bbccd9858e45cd43e1968c39472af7e03fea0e3e54"
+  }
+}

research/k8-pair-dyadic-seed25/VALIDATION.json

@@ -0,0 +1,132 @@
+{
+  "status": "PASS_SCOPED_FINITE_SCALAR_PACKAGE",
+  "verified_utc": "2026-10-13T20:14:26.147547+00:00",
+  "python": "3.14.6 (main, Jun 10 2026, 10:03:53) [Clang 21.0.0 (clang-2100.0.123.102)]",
+  "platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O",
+  "base": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe",
+  "checks": [
+    {
+      "command": "python3 -I -B research/k8-pair-dyadic-seed25/verify.py --write",
+      "exit_code": 0
+    },
+    {
+      "command": "python3 -I -O -B research/k8-pair-dyadic-seed25/verify.py",
+      "exit_code": 0,
+      "output": "PASS_K8_PAIR_DYADIC_CENSUS\nbackward pairs 27966 vertices 735975 winner {'helpers': [251, 427], 'exponents': [2, 2], 'delta_real': -288, 'separate_single_delta_real': -288, 'interaction_delta_real': 0} saving_complex 576\nforward pairs 27966 vertices 735975 winner {'helpers': [251, 427], 'exponents': [-2, -2], 'delta_real': -288, 'separate_single_delta_real': -288, 'interaction_delta_real': 0} saving_complex 576"
+    },
+    {
+      "command": "python3 -I -O -B research/k8-pair-dyadic-seed25/independent.py",
+      "exit_code": 0,
+      "result": {
+        "orientations": {
+          "backward": {
+            "baseline_real_primitives": 74509,
+            "candidate_real_primitives": 74221,
+            "exact_dirty_cases": 3,
+            "grid_evaluations": 9581166,
+            "grid_radius": 31,
+            "interacting_pairs": 2414,
+            "pairs": 27966,
+            "valuation_bound": 15
+          },
+          "forward": {
+            "baseline_real_primitives": 74501,
+            "candidate_real_primitives": 74213,
+            "exact_dirty_cases": 3,
+            "grid_evaluations": 9581166,
+            "grid_radius": 31,
+            "interacting_pairs": 2414,
+            "pairs": 27966,
+            "valuation_bound": 15
+          }
+        },
+        "status": "PASS_INDEPENDENT_PAIR_GRID_AND_PRIMITIVES"
+      }
+    },
+    {
+      "command": "python3 -I -O -B research/k8-pair-dyadic-seed25/test_package.py",
+      "exit_code": 0,
+      "result": {
+        "positive_fixtures": [
+          "shared_unit_edge",
+          "unit_discount_off_zero"
+        ],
+        "rejected": [
+          "first_entry_omitted",
+          "second_entry_omitted",
+          "first_exit_omitted",
+          "second_exit_omitted",
+          "backward_boundary_sign_reversed",
+          "incident_coefficient_not_conjugated",
+          "candidate_digest_changed",
+          "data_register_scaled",
+          "center_carrier_scaled",
+          "unit_discount_omitted",
+          "boundary_scales_unpaid",
+          "missing_vendor_pin",
+          "changed_vendor_pin",
+          "missing_original_source_pin",
+          "shared_edge_treated_as_two_independent_edges",
+          "paid_rank_changed"
+        ],
+        "status": "PASS_PAIR_REJECTION_CONTROLS"
+      }
+    },
+    {
+      "command": "python3 -B scripts/verify_selected_result.py",
+      "exit_code": 0,
+      "scope": "selected record/source integrity only"
+    },
+    {
+      "command": "ruff check research/k8-pair-dyadic-seed25/verify.py research/k8-pair-dyadic-seed25/independent.py research/k8-pair-dyadic-seed25/test_package.py",
+      "exit_code": 0
+    }
+  ],
+  "package_mutations": [
+    {
+      "label": "optimized_offline_relocation",
+      "exit_code": 0,
+      "wall_seconds": 4.384,
+      "output": "PASS_K8_PAIR_DYADIC_CENSUS\nbackward pairs 27966 vertices 735975 winner {'helpers': [251, 427], 'exponents': [2, 2], 'delta_real': -288, 'separate_single_delta_real': -288, 'interaction_delta_real': 0} saving_complex 576\nforward pairs 27966 vertices 735975 winner {'helpers': [251, 427], 'exponents': [-2, -2], 'delta_real': -288, 'separate_single_delta_real': -288, 'interaction_delta_real': 0} saving_complex 576"
+    },
+    {
+      "label": "gzip_header_variation_preserves_payload",
+      "exit_code": 0,
+      "wall_seconds": 4.329,
+      "output": "PASS_K8_PAIR_DYADIC_CENSUS\nbackward pairs 27966 vertices 735975 winner {'helpers': [251, 427], 'exponents': [2, 2], 'delta_real': -288, 'separate_single_delta_real': -288, 'interaction_delta_real': 0} saving_complex 576\nforward pairs 27966 vertices 735975 winner {'helpers': [251, 427], 'exponents': [-2, -2], 'delta_real': -288, 'separate_single_delta_real': -288, 'interaction_delta_real': 0} saving_complex 576"
+    },
+    {
+      "label": "actual_candidate_coefficient_corruption",
+      "exit_code": 1,
+      "wall_seconds": 4.338,
+      "output": "Traceback (most recent call last):\n  File \"<relocated-root>/research/k8-pair-dyadic-seed25/verify.py\", line 255, in <module>\n    main()\n    ~~~~^^\n  File \"<relocated-root>/research/k8-pair-dyadic-seed25/verify.py\", line 244, in main\n    need(canonical(programs) == canonical(json.loads(gzip.decompress((HERE / 'PROGRAMS.json.gz').read_bytes()))),\n    ~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n         'complete candidate program mismatch')\n         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n  File \"<relocated-root>/research/k8-pair-dyadic-seed25/verify.py\", line 24, in need\n    raise ValueError(message)\nValueError: complete candidate program mismatch"
+    },
+    {
+      "label": "actual_pinned_source_corruption",
+      "exit_code": 1,
+      "wall_seconds": 0.203,
+      "output": "Traceback (most recent call last):\n  File \"<relocated-root>/research/k8-pair-dyadic-seed25/verify.py\", line 255, in <module>\n    main()\n    ~~~~^^\n  File \"<relocated-root>/research/k8-pair-dyadic-seed25/verify.py\", line 233, in main\n    result, programs = compute()\n                       ~~~~~~~^^\n  File \"<relocated-root>/research/k8-pair-dyadic-seed25/verify.py\", line 198, in compute\n    lib = predecessor()\n  File \"<relocated-root>/research/k8-pair-dyadic-seed25/verify.py\", line 42, in predecessor\n    need(sha((folder / name).read_bytes()) == digest, 'vendor hash: ' + name)\n    ~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n  File \"<relocated-root>/research/k8-pair-dyadic-seed25/verify.py\", line 24, in need\n    raise ValueError(message)\nValueError: vendor hash: engine.py"
+    },
+    {
+      "label": "actual_certificate_corruption",
+      "exit_code": 1,
+      "wall_seconds": 4.121,
+      "output": "Traceback (most recent call last):\n  File \"<relocated-root>/research/k8-pair-dyadic-seed25/verify.py\", line 255, in <module>\n    main()\n    ~~~~^^\n  File \"<relocated-root>/research/k8-pair-dyadic-seed25/verify.py\", line 242, in main\n    need(canonical(result) == canonical(json.loads((HERE / 'CERTIFICATE.json').read_bytes())),\n    ~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n         'complete certificate mismatch')\n         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n  File \"<relocated-root>/research/k8-pair-dyadic-seed25/verify.py\", line 24, in need\n    raise ValueError(message)\nValueError: complete certificate mismatch"
+    }
+  ],
+  "not_run": [
+    "full native admission",
+    "global hosted invoice",
+    "full selected cold replay",
+    "repository-wide historical suites",
+    "hosted CI",
+    "Lean theorem"
+  ],
+  "compressed_output_equality": "canonical JSON payload; gzip header variation tested",
+  "upstream_changes": false,
+  "selected_frontier_changes": false,
+  "prose_style_pass": {
+    "status": "skipped_by_explicit_user_authorization",
+    "authorization": "Skip Emulate and submit PR"
+  }
+}