Research: JP8 additive coefficient routes save 2,784 beyond rescaling (no new kappa)

research/jp8-additive-coefficient-routes/CLAIM.md

@@ -0,0 +1,62 @@
+# Local sprint claim
+
+- Track: complex supplier; fresh OS-random assignment seed **31**, generated
+  with Python `secrets.randbelow(100)` on 2026-10-13.
+- Exact base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`.
+- Object: consecutive same-source additions in the selected #626 JP8
+  `full_frame_cleanup`, keeping the existing operation order and frame 1.
+- Hypothesis: between different odd numerators, a positive unit source read
+  bracketed by dyadic shifts can cost less than clearing and rebuilding the
+  existing private coefficient stream.
+- Method: enumerate routes `w *= 2^u; w += x; w *= 2^v`,
+  `-16 <= u,v <= 16`, alongside existing power-of-two reuse; charge every
+  source read, shift, accumulation and boundary clear. Admit only routes
+  within the original positive prefix envelope and strictly cheaper than
+  reset. Stop after this finite route class and the exact replay.
+- Deliverable: executable finite construction, exact full scalar-projection
+  replay, source pins, cost certificate, negative controls and scoped note.
+- Expected finish: 2026-10-13 06:40 UTC; hard handoff before 06:54 UTC.
+
+Three narrow candidates were considered: (0) CK cleanup additive transitions,
+(1) JP8 cleanup additive transitions, and (2) private-center quarter-coefficient
+factoring. Seed `31 % 3 = 1` selected JP8; #786 already covers candidate 2
+and reports a larger conservative local invoice. The additive transition
+class differs from #739's power-of-two-only reuse and its explicitly excluded
+odd-numerator transitions. #769 covers CK power-of-two ladders; #793 instead
+permutes commuting frame-zero compensation. #722, #734, #751, #755 and #787
+cover equal-magnitude reuse, individual signed Horner circuits, target fan-in,
+other phases, or composition. None of their implementations is imported.
+
+Before claiming, read the selected record, construction/review, contribution
+instructions, review ledger and preserved-research index. Checked open PR
+metadata through #799 at 05:53 UTC. GitHub returned no pinned coordination
+issue; the only open issue was #650 about Discussions. This file records the
+claim under the requested fallback. No separate reservation issue is opened.
+
+Contributor: Ryan Haines (@Ryan-Haines), with substantial OpenAI Codex
+assistance. New material is Apache-2.0. Result and handoff will be recorded
+once after verification.
+
+## Result and handoff
+
+Completed: [PR #811](https://github.com/CrocSwap/integer-mult-bounds/pull/811).
+The 269 positive one-read transitions save 2,784 real primitives beyond the
+power-only comparator; total forward saving is 32,810 (257,232 to 224,422).
+Both orientations pass literal replay on 725 arbitrary columns. Independent
+integer enumeration covers 849,420 exponent pairs and 6,776 block input
+columns. Windows and Linux, optimized/relocated/recompressed replay, 12+4+25
+mutation controls, four packaging tests, Ruff and selected-record integrity
+pass. The unchanged backward maximum leaves the local invoice unchanged;
+no new kappa is claimed. README.md gives the reproduction command and limits.
+
+Final overlap refresh: 629 open PRs through #810 at 06:08 UTC, plus renewed
+confirmation of no pinned issue and unchanged `origin/main`. New #807
+changes CK helper bases; #809 changes a historical center basis. Neither
+examines fixed-order JP8 cleanup numerator transitions. Source/comparison
+heads for #739 and #793 are pinned; no pending implementation is imported.
+
+The initial research commit is `e80c08f`; this final claim update records the
+result once. A clean patch and short handoff are also retained in the local
+workspace as `jp8-additive-s31.patch` and `jp8-additive-HANDOFF.txt`, including
+the final commit and verification command. This local claim is the requested
+coordination fallback because no pinned sprint issue exists.

research/jp8-additive-coefficient-routes/EXPECTED.json

@@ -0,0 +1,74 @@
+{
+  "schema": "jp8-positive-one-read-replay/1",
+  "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60",
+  "negative_controls": [
+    "missing_initial_clear",
+    "missing_final_clear",
+    "wrong_target_sign",
+    "wrong_transition_source",
+    "endpoint_neutral_prefix_excursion",
+    "source_alias",
+    "changed_source",
+    "frame_crossing",
+    "phase_crossing",
+    "wrong_shift_equation",
+    "prefix_route_exclusion",
+    "planner_phase_boundary"
+  ],
+  "orientations": {
+    "forward": {
+      "columns": 725,
+      "live_columns": 716,
+      "arbitrary_private_columns": 9,
+      "real_primitives": 224422,
+      "prefix_l1": "4536094588619580433782972610869617/281474976710656",
+      "paid_profile": {
+        "1": 2512,
+        "2": 400,
+        "3": 448,
+        "4": 160,
+        "5": 70,
+        "6": 8,
+        "8": 8
+      },
+      "non_scalar_events_sha256": "1fcf711555d365968ff8b64172090960cf98559865bd858c521c2adc7b12f792",
+      "original_real_primitives": 257232,
+      "power_only_real_primitives": 227206,
+      "additional_real_saved": 2784,
+      "one_read_transitions": 269,
+      "blocks": 1091
+    },
+    "backward": {
+      "columns": 725,
+      "live_columns": 716,
+      "arbitrary_private_columns": 9,
+      "real_primitives": 257280,
+      "prefix_l1": "16753412757380464429924108070201913461/8388608",
+      "paid_profile": {
+        "1": 2512,
+        "2": 400,
+        "3": 448,
+        "4": 160,
+        "5": 70,
+        "6": 8,
+        "8": 8
+      },
+      "non_scalar_events_sha256": "299442a1d68206eb7f49f0c9789cc8fa410a0615cff9c1900c54b064e901aa21",
+      "original_real_primitives": 257280,
+      "power_only_real_primitives": 257280,
+      "additional_real_saved": 0,
+      "one_read_transitions": 0,
+      "blocks": 0
+    }
+  },
+  "certificate_sha256": "973c3a108d6c3d4c78455c2fed95baf0440bc99a39dfb515976d9e2f41ef928c",
+  "unintegrated_budget": {
+    "unchanged_local_adapters": 437040,
+    "unchanged_compiler_charge": 25934336,
+    "max_orientation_primitives": 257280,
+    "binding_orientation": "backward",
+    "original_local_primitive_bound": 11334342462720,
+    "optimistic_local_primitive_bound": 11334342462720,
+    "new_kappa_claimed": false
+  }
+}

research/jp8-additive-coefficient-routes/INDEPENDENT.json

@@ -0,0 +1,27 @@
+{
+  "method": "integer-grid exhaustive square plus dirty-input block matrices",
+  "certificate_sha256": "973c3a108d6c3d4c78455c2fed95baf0440bc99a39dfb515976d9e2f41ef928c",
+  "orientations": {
+    "forward": {
+      "distinct_pairs": 780,
+      "exponent_pairs_checked": 849420,
+      "blocks": 1091,
+      "block_input_columns": 6776,
+      "real_primitives_saved": 32810,
+      "negative_controls": [
+        "initial_clear",
+        "final_clear",
+        "target_sign",
+        "endpoint_neutral_growth"
+      ]
+    },
+    "backward": {
+      "distinct_pairs": 0,
+      "exponent_pairs_checked": 0,
+      "blocks": 0,
+      "block_input_columns": 0,
+      "real_primitives_saved": 0,
+      "negative_controls": []
+    }
+  }
+}

research/jp8-additive-coefficient-routes/NATIVE.json

@@ -0,0 +1,71 @@
+{
+  "status": "PASS_INDEPENDENT_LOCAL_SCALAR_FRAME_AND_WRAPPER_REPLAY",
+  "v": 112,
+  "helpers": 492,
+  "local": {
+    "forward": {
+      "all_exact_columns": 716,
+      "prefix_l1_upper": "4536094588619580433782972610869617/281474976710656",
+      "prefix_bits_upper": 64,
+      "charged_payload_bits": 192,
+      "private_work_erased": true
+    },
+    "backward": {
+      "all_exact_columns": 716,
+      "prefix_l1_upper": "16753412757380464429924108070201913461/8388608",
+      "prefix_bits_upper": 101,
+      "charged_payload_bits": 192,
+      "private_work_erased": true
+    }
+  },
+  "paid_profiles": {
+    "forward": {
+      "1": 2512,
+      "4": 160,
+      "8": 8,
+      "3": 448,
+      "2": 400,
+      "5": 70,
+      "6": 8
+    },
+    "backward": {
+      "1": 2512,
+      "4": 160,
+      "8": 8,
+      "3": 448,
+      "2": 400,
+      "5": 70,
+      "6": 8
+    }
+  },
+  "entering_helpers": 204,
+  "cold_hyperplane_ended_helpers": 22,
+  "negative_controls_rejected": [
+    "wrong_scale",
+    "missing_center",
+    "wrong_common_frame",
+    "wrong_child_rank",
+    "missing_pre_wrapper",
+    "missing_post_wrapper",
+    "wrapper_with_wrong_frame",
+    "wrapper_in_wrong_phase",
+    "wrapper_on_a_data_register",
+    "wrapper_on_a_target_register",
+    "wrapper_on_a_centre_register",
+    "hpe_pre_wrapper_resolved_to_full_recipe",
+    "hpe_post_wrapper_without_terminal_frame",
+    "hpe_post_wrapper_wrong_terminal_frame",
+    "hpe_tail_gate_at_full_frame",
+    "hpe_tail_climb_dropped",
+    "hpe_helper_exit_adapter_to_full",
+    "hpe_tail_gate_moved_into_full_cleanup",
+    "cold_hpe_pre_wrapper_replaced_by_identity_entry_adapter",
+    "cold_hpe_pre_wrapper_dropped",
+    "cold_hpe_post_wrapper_replaced_by_exit_adapter",
+    "cold_hpe_pre_wrapper_resolved_to_cold_full_convention",
+    "cold_hpe_wrapper_with_nonzero_entrance",
+    "cold_hpe_post_wrapper_wrong_terminal_frame",
+    "cold_hpe_premix_gate_before_pre_wrapper"
+  ],
+  "scope": "Literal forward and inverse-transpose replay on every arbitrary data/helper column, physical frame incidence, ordered paid wrappers, cleared private work and prefix coefficients. Global hosting and outer exponent are separate."
+}

research/jp8-additive-coefficient-routes/PROOF.md

@@ -0,0 +1,114 @@
+# Fixed-order positive one-read substitution
+
+## Local identity and legality
+
+Consider a consecutive block of scalar additions `t_j += q_j x`. All
+registers are at the same full frame; `x` is never a target. The block
+contains no scale, frame change, child, adapter, wrapper or center event.
+Each target retains its original position and signed coefficient. The
+existing private coefficient stream `w` is cleared initially and finally.
+
+Write `a_j = abs(q_j)`. Binary Horner preparation constructs `w = a_0 x`
+after erasing an arbitrary incoming `w`. At every target update, the stream
+holds `a_j x`, so adding/subtracting it realizes the required signed update.
+The permitted transitions are either `w *= 2^k`, when `a_j/a_(j-1)=2^k`, or
+
+```text
+w *= 2^u
+w += x
+w *= 2^v
+```
+
+with `(a_(j-1)*2^u + 1)*2^v = a_j`. This identity is over exact complex
+values, component by component; no division of the live source is needed.
+All halvings are inherited exact dyadic scalar primitives. Induction over
+the target updates proves the same live-register map for arbitrary dirty
+inputs, with no incoming private-work dependence and zero outgoing work.
+There is no new helper or recursive child. Existing source access is paid
+once for each `w += x`.
+
+For example, a real source coefficient changes from `1/2` to `3/2` with
+the single operation `w += x`. Clearing and rebuilding the latter costs six
+real-component primitives before its target update. The transition saves
+five in that component, or ten across real and imaginary components.
+
+## Complete cost in this class
+
+For a positive reduced dyadic `a = A / 2^d`, the selected binary-Horner
+preparation costs
+
+```text
+P(a) = 1 + (bit_length(A)-1) + popcount(A) + d
+```
+
+including its initial clear. A standalone addition costs `P(a)+2`, adding
+one target accumulation and one final clear. A block of `m` additions costs
+
+```text
+P(a_0) + m + sum(transition_cost_j) + 1.
+```
+
+A pure shift costs `abs(k)`. A one-read transition costs
+`abs(u)+1+abs(v)`. The alternative cut between consecutive additions costs
+`1+P(a_j)` (previous final clear plus next preparation). A transition is
+selected only if strictly cheaper than that cut. Since its endpoint
+coefficient is fixed, the saving for each admissible adjacent edge is
+independent of all other edges. Taking each strict minimum and splitting
+at all other edges therefore minimizes cost in the specified fixed-order
+class. Ties prefer reset, then pure shifts, then lexicographically ordered
+`(cost,u,v)`. This claim includes the fixed binary-Horner preparation and
+does not assert unrestricted circuit optimality.
+
+The constructor enumerates 33 values of `u`; the equation uniquely
+determines `v`, if it is an integer. The independent implementation
+enumerates all 1,089 pairs directly using exact integers. Thus the omitted
+`v` loop in the constructor does not reduce the claimed finite coverage.
+All 780 distinct magnitude pairs and all 4,298 occurrences are accounted
+for, including unprofitable/infeasible cases. All 269 selected one-read
+transitions have unequal odd numerators.
+
+The full-program recount pays unchanged macro lowering outside the blocks.
+It counts all target updates, boundary clears and work preparation inside
+them. Non-scalar events are unchanged and their hashes and paid recursive
+profiles are recorded. The finite forward count is 224,422; the backward
+count remains 257,280. With the existing adapter/compiler allowances the
+orientation maximum, and hence the conservative local invoice, is unchanged.
+
+## Prefix envelope
+
+Let `N_x` be the positive L1 envelope of the fixed live source. The work
+stream has envelope exactly `a N_x`: preparation, shifts and the new source
+read use positive coefficients. They introduce no cancellation in the
+envelope. In the one-read route its maximum coefficient is
+
+```text
+max(a, a*2^u + 1, b).
+```
+
+The pre-read value `a*2^u` is smaller than the middle value and the shifts
+are monotone between endpoints. Require this maximum to be at most
+`max(a, numerator(b))`. The old execution has already reached `a N_x`
+and its binary-Horner preparation for `b` reaches
+`numerator(b) N_x`. The replacement therefore never exceeds the old
+prefix envelope. Pure shifts are monotone between `a` and `b` and satisfy
+the same comparison. Original target updates and all their positive
+envelopes are unchanged. This argument allows unequal incoming target and
+source envelopes and composes across every block.
+
+The literal full-program replay independently measures the exact positive
+envelope. It agrees with both selected SPEC values, not merely the 192-bit
+cap. The integer implementation checks each block's dirty-input matrix and
+local envelope with a common scale of `2^(D+32)`, where `D` is the maximum
+input-coefficient denominator exponent. Two shifts of at most 16 cannot
+exhaust that grid; divisibility is checked before every right shift.
+
+## Scope of evidence
+
+The algebraic block argument explains substitution in the inherited scalar
+model. Exhaustive enumeration certifies only the stated finite route class.
+The all-column literal replay checks finite endpoints, clearing, accounting
+and positive envelopes. The unchanged native replay checks the original
+macro frame/wrapper obligations. These checks do not independently prove
+the all-size multiplication theorem or integrate a new production private-
+work contract. In particular, no exponent improvement follows from the
+unchanged maximum local invoice.