[JoyboyBrian]

The existing full-Toeplitz physical-cut audit leaves its numerical contract at a proper subset of a matching layer open. This adds a four-way source-bound interpolation theorem: prefix, suffix and both inverse operators obey sqrt(a²+b²) from adjacent complete-boundary bounds. The generic sqrt(2) loss is sharp even when all four complete-boundary contracts hold together. The proof binds the coordinate projections to the actual retained rational FFT and dirty Toeplitz-shear matching gates.

The resulting child/Full implication retains the original complete-layer bounds as premises: sublayer fragments use sqrt(2) H (safe rational 2H), physical cuts use sqrt(2) K, and arbitrary segments use 2K². One extra data bit funds the doubled suffix envelope only when the original rounding-event count is retained. Gate-internal arithmetic, overlapping/asynchronous operations, physical delivery and full supplier admission remain separate. No selected κ changes.

Validation: registered warning-strict CPython 3.12 normal/optimized replay passes 97 cuts, 52 proper sublayer cuts, 388 exact interpolation identities and 388 partial-cut spectral certificates. Six controls cover the missing loss, projection side, overlap and complex-adjoint boundaries. Committed-byte/source-history and official 13-file export integrity pass. Git-free normal/optimized replays with PATH=/nonexistent pass (0.743/0.673 s locally); all exported bytes remain unchanged. Source-byte corruption and a wrong-projection implementation mutant reject. Hosted CI has not yet been verified.

This PR has three substantive commits: quantified theorem/matrix oracle; actual-source replay and discriminating controls; finalized contracts and independent PSD-certified neighboring spectral envelopes. Canonical investigation: #4202 (comment) . Base b91956876e5b4122fd89179f1b57557ff8378f15, priority revision 7. Entry overlap covered 317 open PRs, 4,064 discussion records and 6,636 current-base notes; no exhaustive novelty claim.

Credit Jose Manuel/jmbarrancoml for rational FFT/Full and numerical fragment contracts, Vlado Vojdanovski/PR1673 for the matching scheduler, Chafik Boukhalfa/PR628 for certified phases, and Brian/JoyboyBrian's physical-cut trace audit. Prepared by JoyboyBrian with substantial OpenAI Codex assistance. The written proof establishes the quantified implication; finite checks and author-process review do not constitute independent human or proof-kernel acceptance. Open next questions are in the package.

Submission checkpoint: fresh official main at 04:59 UTC remains b91956876e5b4122fd89179f1b57557ff8378f15, with unchanged guidance and affected source inputs. Complete submission overlap covers 318 open PRs (04:59:29 UTC), 4,077 discussion records (05:00:22 UTC), and all 6,636 current-base notes. Scoped matching/sublayer and downset/allocation queries identify the credited explicit predecessor obligations and this round's claims; no exhaustive novelty assertion is made. Coordinating Codex review independently read the full four-way proof, sharpness construction and exact source cut oracle, with no blocker.

[jwr404]

Independent review at head 8a7e0e9b4a085f4fb47a76700dfe135412b9c4ef

Identities: all correct. With G block-diagonal on disjoint supports and E the projection onto the selected gates' supports, EG = GE and H = EG + (I−E). Then:

• P = HP₀ = EP₁ + (I−E)P₀
• P⁻¹ = P₀⁻¹H⁻¹ = P₀⁻¹G⁻¹E + P₀⁻¹(I−E) = P₁⁻¹E + P₀⁻¹(I−E), using EG⁻¹ = G⁻¹E
• S = S₁GH⁻¹ = S₁E + S₀(I−E), since GH⁻¹ = E + G(I−E)
• S⁻¹ = HG⁻¹S₁⁻¹ = ES₁⁻¹ + (I−E)S₀⁻¹

The order of factors is as stated.

Norm bound: correct. For P and S⁻¹ the projections sit on the output side, so squared norms add. For P⁻¹ and S they sit on the input side, so a‖Ex‖ + b‖(I−E)x‖ ≤ √(a²+b²)‖x‖ by Cauchy–Schwarz. Neither step depends on dimension, and both hold over ℂ.

Sharpness witness: correct. P₁ = GP₀ = [[1,0],[m,1]], and P₀⁻¹ = [[1/m,0],[−1,m]] since det P₀ = 1. Every complete-boundary operator (P₀, P₁, their inverses, G and G⁻¹) has Frobenius norm at most m+2. The cut HP₀ sends e₀ to (m,m), which has norm √2·m:

m	max boundary Frobenius	√2·m	√2·m > m+2
4	4.24	5.66	no
5	5.20	7.07	yes
10	10.10	14.14	yes
100	100.01	141.42	yes

This confirms both the m ≥ 5 threshold and the ratio tending to √2.

The registered replay passes locally on Linux with CPython 3.12.14: PASS_MATCHING_SUBLAYER_NORM four_way_exact_bounds no_new_kappa.

Scope. As stated, the result needs the actual complete-layer bounds (GENERATOR-PROOF.md, FULL-PROOF.md (14)) as premises. It does not cover rounding inside a gate or overlapping gates.

This is an author-independent check, not maintainer acceptance. κ is unchanged.

Reviewed by James Reed with substantial Anthropic Claude (Claude Code) assistance.