[aliromman]

This proves an all-length obstruction for the actual coded terminal family: adding distinct fresh stages cannot produce a decoder with a constant number of scalar ADDs. It also gives an exact two-path cancellation when the interface has two shared central axes. The complete kappa calculation is unchanged; no new supplier or higher kappa is claimed.

The proof, exact receipt and marker certificates contain the result and evidence.

For any fixed k >= 1, any order of distinct stages, and any nonzero integer stage powers, one common binary axis and eight private axes per stage give ADDs >= max(0, 2f - 24k). This permits cross-owner scalar mixing, arbitrary owned workspace, and coefficients and monomial maps that depend on tensor width f. The linear instruction schedule must be independent of input values. The proof separates the binary map of every owner path, then isolates one term by coordinate contractions. Owner coefficients are applied once, outside tensor powers.

Short certificates strengthen the bound to ADDs >= max(0, 2f - 6) for all sixteen negative-output banks in the saved caller, including its eighteen-stage bank. Do not add these sixteen bounds together. The previous two-stage bound retains its better constant for its two named banks.

With two shared axes, L R = (L H)(H R) gives distinct local paths with the same signed operator. The actual owner coefficients +1/4 and -1/4 then cancel at every tensor width. The proof specifies every map. This is a two-path construction, not a complete 112-owner provider. The extra central axis, remaining owners, targets and restoration still need a complete paid bill. A simple shared-axis screen on the unchanged source did not cancel the tested block; it is recorded as a bounded negative experiment.

Validation uses Python 3.12 and the standard library:

python3 -B scripts/research_package.py --package research/fresh-stage-code-separation

Expected final scientific marker:

PASS_ALL_LENGTH_FRESH_STAGE_SEPARATION_NO_NEW_KAPPA

Both registered normal/optimized checks pass: 57,344 signed normalizer entries, all 12,544 code-polynomial entries, all 12,656 two/three-stage paths, 12,654 literal killing markers, both directions of the short-marker dynamic program, all sixteen banks, and repeated-stage/two-center controls. The marker proposer reproduces the saved bytes. Committed-byte and official export checks pass; both modes also pass in a read-only Git-free export. Five optimized mutation runs reject changed source bytes, an empty marker, a repeated stage, a wrong Q orientation, and a typed receipt change. Hosted verification passed for head 256126eeb1607c0bf52996c3d90490f2b786b94a.

The unbounded theorem rests on its written induction. These checks share source data and elementary matrix code; independent human or proof-kernel acceptance is not claimed. No complete producer, native/outer/compiler admission, selected cold replay, Lean, Docker or optional full-history check was run. The checkout is shallow. Paid decoders, width-dependent scalar work, correlated saved histories, repeated stages, and changed recursive target contracts remain outside the obstruction.

Base: canonical main 1ec1119972c9aefe42525172d07b332fcff81cb4, priority 7. Only the new scoped package changes. The frozen code A and signed normalizers are copied byte-exactly. Source pins retain exact copied bytes and notices. The canonical claim separates this proof from active caller and frame work. The selected conditional kappa remains 0.0030217758.

Credit @dillona for PR #4933's physical code, signed normalizers and caller; @1337isnot1337 for PR #5065's two-stage proof and open longer-product question; and @Dugongue for PR #4929's center-free code. @intqwq (Cao Yifan), @zxv, Jacob Alan Sussman and the retained native/controller lineage remain credited in the source notice. The code spectrum and one-stage four-point formula are predecessor results. New work by @aliromman with substantial OpenAI Codex assistance; Apache-2.0.

[jwr404]

Independent review (jwr404). Base: upstream/main 1ec1119.

Replay. python3.12 -B scripts/research_package.py --package research/fresh-stage-code-separation prints PASS_ALL_LENGTH_FRESH_STAGE_SEPARATION_NO_NEW_KAPPA in both modes and then PASS_REGISTERED_RESEARCH_PACKAGE … outcome=negative-result. It takes 20 s.

Independent census of the short markers. My ~50-line script reads only inputs/CODE.json, inputs/NORMALIZERS.json and MARKERS.json. It takes G_rows as row bitmasks, inverts each map by transposing it (after checking G⁻¹G = I on samples), and checks that the 112 central images are distinct. It then brute-forces every owner path, with no DP. Each path starts at owner 0, ends at owner k mod 2, and uses nonzero-A or diagonal edges. Each saved marker input is pushed stage by stage through G_{s,j}, then G_{s,i}⁻¹:

stages	allowed paths	survivors of saved marker
2	53	1
3	1,361	1
4	72,185	1

This agrees with both of the package's DPs. Also confirmed: A₀₁ = A₁₀ = −1/2, every row of A has 52 nonzero entries, the code polynomial A² + 12A = 13I holds on sampled rows, and the §7 products are A₀₂A₂₁ = 1/4 and A₀,₉₈A₉₈,₁ = −1/4.

Proof, checked by hand. I find no gap.

• §2. In the cancellation step, write X = (F′k)⁻¹F_k = Y, where X ∈ H_k and Y lies in the group generated by H{<k}. X fixes V_{<k} pointwise and Y fixes V_k pointwise. So X is determined by X(e) ∈ (E+V_k) ∩ (E+V_{<k}) = E, which forces X(e) = e and X = I. The backward owner recovery uses distinct q_i at the last stage and then repeats.
• §3. The witness's first-stage image G_{1,1}⁻¹q₀ is neither e nor 0, so it has a V₁ component that later stages fix pointwise. The power formula A^a = α_a A + (1−α_a)I with α_a ≠ 0 also gives the DP's edge domain, supp(A) ∪ diag, for every nonzero exponent.
• §5. C_{s}^{a} = D_s⁻¹(A^a ⊗ I)D_s, with D_s = blockdiag(K_{s,i}^{⊗f}), so J_f really is Σ_p c_p N_p^{⊗f} in a fixed owner block. The orthogonal-complement argument for e, and the 2^m row / 2+2 index bookkeeping of ℓ_l, give S ≥ 2^{2f−3m}. S ≤ 2^g holds for binary ADDs, and SCALE, COPY, CLEAR and monomial maps preserve the maximum support. Dirty workspace only adds input columns, so it cannot help.
• §6. bank_checks confirms that the certificates' selected path is the §3 alternating path. Its coefficient ∏ α(a_s)·A₀₁ is nonzero for each actual bank.

Two small presentation notes (non-blocking).

1. The bound already holds for implementing a single (input-owner, output-owner) block of J_f, not just all of J_f. The proof only uses one block, so saying so in §1 would make the statement slightly stronger and easier to apply.
2. In §6, "Every bank length in the source endpoint has a certificate with m ≤ 2" gives g ≥ 2f − 6. This deserves a written warning against summing the sixteen bank bounds. The PR body gives that warning, but neither PROOF.md nor README.md does.

Verdict: correct as a scoped all-length obstruction. The §7 two-axis cancellation is a correct explicit example, not a provider. No κ is claimed and none is affected.