Review the encoded many-axis production_axis guard.

research/many-axis-encoded-axis-guard/PROOF.md

@@ -0,0 +1,94 @@
+# Encoded axis guard for the many-axis prime band
+
+The source under review is `TensorPlan` from PR #3935, as vendored by PR #4029
+at `726c9a3a1dc58d2b1223dd681eb712255be407c1` and pinned here by SHA-256
+`474730f42fcd2bd24720af4e08c71fb51cc374c3e16b8b6d7e565900f1a9e7c3`.
+PR #4029's prime-supply prose is the claim being checked. This note does not
+reprove Fiori–Kadiri–Swidinsky and does not run an encoded Count machine.
+
+## What the encoded method is
+
+`TensorPlan.production_axis(self, s, t)` is a predicate on two live Counts.
+Its only `self` fields are `d`, `target_halo` and `w`. In source order its
+four `multiply_small` constants are `4`, `2`, `2`, `2`, and its three `need`
+messages are the lower ratio, the upper ratio and the period. The body names
+no tape operation: no `rewind`, `read_fixed`, `write_fixed`, `read`, `write`,
+`append` or `clear`.
+
+`TensorPlan.__init__` loads each source word with `read_fixed` before the
+single `self.production_axis(s, t)` call, and a `rewind` occurs at a later
+line. Oddness (`s.read() == 1`) and the near-one test `s < t < 2s` are gates
+in `__init__`, not in `production_axis`.
+
+So this method does not lower a sequential prime queue onto a tape. A producer
+meets it only by placing an already-loaded odd Count `s` next to its target
+`t`. Head return of the sources, flags and axis-row tapes is an `__init__`
+obligation after the guard returns.
+
+## The three predicates
+
+Write `g = t - s`, with `t > s`, and write `d`, `H` and `w` for the three
+fields. The constants above are exactly
+
+```
+4 d g > s,     (2d - 1) g < s,     s > 2 (H + 2 w).
+```
+
+The first two are equivalent to `t / (4d + 1) < g < t / (2d)`.
+
+## The prime band sits inside the ratio and near-one gates
+
+PR #4029 uses, for each target scale,
+
+```
+I(t, d) = (t (1 - 1/(3d)), t (1 - 1/(4d))].
+```
+
+For every integer `d >= 1` and every real `s` in that interval,
+`t/(4d) <= g < t/(3d)`. Both comparisons are strict against the encoded
+thresholds because `1/(4d) > 1/(4d+1)` and `1/(3d) < 1/(2d)`. At the closed
+endpoint `g = t/(4d)`, one still has `4 d g = t > s`. Thus every such `s`
+satisfies both ratio predicates. Since `s <= t (1 - 1/(4d)) < t` and, for
+`d >= 2`, `s > t (1 - 1/(3d)) >= (5/6) t > t/2`, the near-one gate
+`s < t < 2s` holds as well.
+
+The band alone does not imply oddness. For `t = 16` and `d = 2` the integer
+`s = 14` lies in `I(16, 2)`, passes both ratios and near-one, and is even, so
+`__init__` rejects it before `production_axis`.
+
+## Period, and why the factor 2 is necessary
+
+Assume `d >= 2`, `ell >= 2`, `t` is `2^ell` or `2^(ell-1)`, and
+`K = H + 2w <= 2^(ell-3)`. Every integer `s` in `I(t, d)` satisfies
+
+```
+s > t (3d-1)/(3d) >= 2^(ell-1) * 5/6 = 2^(ell-2) * 10/6 > 2^(ell-2) >= 2K.
+```
+
+The coefficient `5/6` is the `d = 2` case; larger `d` only raises it. The
+inequality is strict, so the integer `s` is at least `2^(ell-2) + 1` when
+`2K` equals that power of two. Prime abundance is not used.
+
+The final encoded doubling is not optional. For `t = 1024`, `d = 4` and
+`s = 939`, the point lies in the band and passes both ratios, and `s > 470`,
+but `s > 2 * 470` fails. A lowering that keeps only `s > H + 2w` accepts a
+source the method rejects.
+
+## Product room, after the band
+
+Let `D = d - 1`, matching PR #4029's reading that the internal `d` is one more
+than the resampled axis count. For `x = 1/(3d)` and every integer `D >= 1`,
+
+```
+(1 - x)^D >= 1 - D x = (2D + 3) / (3D + 3) > 2/3,
+```
+
+so a product of `D` band ratios is strictly above `2/3` and the reciprocal
+target/source product is strictly below `3/2`. This is the algebraic step only.
+It does not count primes.
+
+## What remains outside the method
+
+`production_common` still carries the Gaussian policy, separation and restored
+error margin, and it is invoked only after every axis guard returns. The
+imported prime-count cutoff is untouched. No encoded tape scheduler is run.

research/many-axis-encoded-axis-guard/README.md

@@ -0,0 +1,58 @@
+# Encoded axis guard for the many-axis prime band
+
+Independent review of the encoded `TensorPlan.production_axis` contract that
+PR #4029 asks to be lowered onto the actual caller. No new κ and no
+selected-frontier change. Selected κ stays `0.001672660197076918`.
+
+The guard is three strict predicates on Counts that `__init__` has already
+loaded. It does not read, write or rewind a prime-queue tape. On PR #4029's
+band `I(t,d) = (t(1-1/(3d)), t(1-1/(4d))]`, every real point satisfies both
+ratio predicates, and for `d >= 2` it also satisfies the near-one gate
+`s < t < 2s`. Oddness is separate: `s = 14`, `t = 16`, `d = 2` is in the band
+and even. If `K = target_halo + 2w <= 2^(ell-3)`, every band integer beats the
+encoded period `s > 2K`. The witness `s = 939`, `t = 1024`, `d = 4`,
+`target_halo = 470` passes `s > K` and fails `s > 2K`.
+
+The argument is in [PROOF.md](PROOF.md). The imported prime-number estimate is
+not reproved. `production_common`, numerical recovery and a literal encoded
+tape scheduler stay open.
+
+## Reproduce
+
+Python 3.12, standard library, from the repository root:
+
+```sh
+python3.12 -B research/many-axis-encoded-axis-guard/verify.py
+python3.12 -B scripts/research_package.py --package research/many-axis-encoded-axis-guard
+```
+
+`verify.py` checks the vendored plan's SHA-256, the AST contract, the rational
+endpoint and Bernoulli identities, every band integer for `ell = 3..12` and
+`d = 2..8` on both target scales, and the even and factor-2 witnesses.
+`-O` runs the same checks. Expected first line:
+
+```text
+PASS_MANY_AXIS_ENCODED_AXIS_GUARD
+```
+
+## Open next questions
+
+1. Can the prime queue be written as the odd `read_fixed` source tape that
+   `__init__` loads before `production_axis`, with head return included?
+   The predicate review does not supply that scheduler. The blocker is an
+   encoded Count runtime, which this package does not execute.
+2. Does the imported prime-count cutoff still leave at least `D` primes in
+   each band after the oddness gate removes composite and even integers?
+   PR #4029 treats odd primes as the selection. A band integer need not be an
+   odd prime, as `14` shows. The blocker is the analytic estimate, which is
+   not reproved here.
+
+## Credit
+
+The tensor plan is Jose Manuel's PR #3935. The prime-band statement, the
+`d = D+1` reading and the period premise are ToikY's PR #4029, following
+PR #4024 and the source08 prime-interval lineage named there. This package
+re-derives the encoded predicates and the band inclusions from that vendored
+file and does not import PR #4029's checker.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.

research/many-axis-encoded-axis-guard/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    }
+  ]
+}

research/many-axis-encoded-axis-guard/TASK.json

@@ -0,0 +1,72 @@
+{
+  "schema_version": 1,
+  "task_id": "supplier-boundary-audit",
+  "priority_revision": 6,
+  "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f",
+  "original_card": {
+    "id": "supplier-boundary-audit",
+    "question": "Does one selected supplier obligation follow from its actual source-bound checks?",
+    "starting_points": [
+      "certificates/selected-result.json",
+      "research/owner-boundary-audit/README.md",
+      "research/scatter-export-parity-audit/README.md"
+    ],
+    "methods": [
+      "Trace one hypothesis through the source, checker and complete caller.",
+      "Construct one semantically invalid but superficially well-formed fixture and test rejection."
+    ],
+    "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read #2977 reported duplicate-scatter counterexample and its opt-in repair. The archive is not a production fix or an independently validated selected-result failure; the selected generator emits unique rows.",
+      "scope": "Source-binding orientation only; does not replay or validate the reported bug."
+    },
+    "first_experiment": "First check whether the scatter repair has been adopted. If still open, independently reproduce #2977 symbolic-versus-exported parity on the tiny duplicate fixture, compare the selected unique-row positive control, and define either enforced uniqueness or consistent multiplicity semantics. A bounded guard-adoption patch must preserve valid inputs and test the actual exported action. Stop after this obligation; no full historical replay or frontier change follows from the mutant alone.",
+    "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.",
+    "allowed_variations": [
+      "Audit one named current condition using a new semantic counterexample."
+    ],
+    "scope_change_triggers": [
+      "Reporting the historical timing-only diagnostic as a new current acceptance bug.",
+      "Calling a malformed mutant a failure of the selected construction, or importing an opt-in repair without testing the exporter boundary."
+    ],
+    "overlap_terms": [
+      "owner boundary",
+      "bridge omission",
+      "hosting",
+      "2977",
+      "scatter export",
+      "duplicate index",
+      "parity semantics"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Review PR #4029's many-axis prime producer at the encoded TensorPlan.production_axis boundary: which predicates the method enforces, which tape operations it does not perform, and whether the stated prime band meets those predicates.",
+  "scope_change_reason": "Discussion #1166 comment 19037887 asks for a review of the many-axis prime producer at the actual encoded caller boundary. The catalogue card's scatter/export example is a different obligation. This package audits the vendored PR #3935 guard instead of reproducing the #2977 duplicate-scatter mutant.",
+  "bottleneck_link": "A prime-length producer changes a supplier only if it meets the encoded axis guard, including the factor-of-two period test and the odd-source gate. Knowing that production_axis is not itself a tape scheduler stops a lowering that would drop that factor or skip head return.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the production_axis contract, the band inclusions and the two witnesses. Do not reprove the prime-number estimate or build an encoded tape runtime.",
+  "outcome": "completed",
+  "evidence": "verify.py prints PASS_MANY_AXIS_ENCODED_AXIS_GUARD. It checks fixture SHA-256 474730f42fcd2bd24720af4e08c71fb51cc374c3e16b8b6d7e565900f1a9e7c3, the AST contract, 1783 band integers, and the even and factor-2 controls.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Substantial Cursor Grok assistance for the proof writeup, AST checker and witnesses.",
+  "open_questions": [
+    {
+      "question": "Can the prime queue be written as the odd read_fixed source tape that TensorPlan.__init__ loads before production_axis, including head return?",
+      "why_it_matters": "production_axis only tests Counts that are already loaded, so the predicate review does not admit a producer.",
+      "first_step": "Emit one odd fixed-width source word, run the authenticated guard on those Counts, and rewind the sources, flags and axis-row tapes.",
+      "blocked_by": "No encoded Count runtime is executed in this package."
+    },
+    {
+      "question": "After the oddness gate deletes even and composite band integers, does the imported prime-count cutoff still leave D primes in each band?",
+      "why_it_matters": "The band contains even integers, such as 14 at t=16 and d=2, which __init__ rejects before the axis guard.",
+      "first_step": "Apply the oddness predicate inside the PR #4029 prime-count estimate and restate the cutoff.",
+      "blocked_by": "The Fiori\u2013Kadiri\u2013Swidinsky input is not reproved here."
+    }
+  ]
+}

research/many-axis-encoded-axis-guard/VERIFY.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "AST contract of production_axis, rational band inclusions, 1783 band integers, even-source witness and factor-2 period witness"
+    }
+  ]
+}