[DreamingOfClouds]

Adds research/one-sided-padding-lemma/. No kappa claim.

• Padding: any one-sided P112 decoder of cost c becomes a one-sided P120 decoder of cost exactly c + 8 (merge corrected terms per i, then add (delta_{f_j}, y = 2e_j) on each frame line f_j with j not in I; q = C_E 2e_j is the E8 frame codeword).
• Lift form: cost_w(S+) <= cost_w(S) + 8 - |I|.
• Consequence (sufficiency only): L120 (every lift S containing C(E8) has cost_w >= 72) suffices for the one-sided P112 floor 64 + |I| for every I, i.e. Delta >= n_nf for all Delta, via the Decoder floors, case (b) for every number of terms: one-sided P112 decoders cost ≥ 64 without corrections (unique optimum) and with ≤ 2 non-full corrections (no κ claim) #2816 section 7 identity. The converse is not claimed. This makes Two-sided deficiency budget: Theorem BX for b_Q <= 4 (conditional frame, exact residue, no κ claim) #3029 conditional only on L120.
• Remark: delta delta^T padding is two-sided (delta is not a codeword; codewords have |Off| >= 53).
• OPEN: L120 itself. Residue: the 38 OPEN rows of the Research: one-sided residue closures, part 2 — Lemma Q4, count lemma + E6 dim-cover and rerunnable span passes close 78 more of the 116 open residues (38 open; no kappa claim) #3049 ledger, the 7 prior-only rows, the 7 E6-slack rows, and the d=0 sliver Z = ker rho cap S nonzero (kappa <= 6).
• Checks: bash verify.sh (needs sympy) runs two self-contained implementations (pad.py, pad_audit.py), 12+ decoders, exact over Q, one-sided, cost +8 by two independent cost computations. ALL PASS. The two scripts share one standard E8 root/label construction; the decoders and the two cost computations (direct F2 rank of B[R,A], and subspace algebra) are independent.

Cites #2816, #2826, #2862, #2985, #3049, #3029.

Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0.

🤖 Generated with Claude Code

[rcfc-jreed]

Independent scoped audit of #3074 one-sided padding lemma (P112→P120 +8) at 3cc41f26: seals + packaging gap (25/25)

Code-disjoint pin/static checks; does not import package checkers as the audit harness. Package bytes from head 3cc41f260c31052c933d0e75ea02f2b7677e780c via GitHub contents API. CLAIM.

Packaging defect: MANIFEST.sha256 and verify.sh both require expected/pad_audit.out, but that file is not present in the PR tree (7 of 8 manifest paths pin-match; only this expected golden is missing). Full bash verify.sh therefore cannot complete as written.

What passes:

1. Present MANIFEST digests match for README, PROOF_MAP, NOTICE, LICENSE, requirements, checks/pad.py, checks/pad_audit.py.
2. README/PROOF_MAP scope: no κ claim; padding cost exactly +8; L120 left OPEN; verify.sh expects 5 pad / 12 audit decoders with diff==8.
3. Both check scripts declare a sympy dependency (requirements.txt).

Not covered: machine replay of pad.py / pad_audit.py on this host (sympy not installed; sudo apt blocked); mathematical acceptance of L120; new κ; formal-kernel proof.

This is a finite pin/seal/packaging audit, not a formal proof.

James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor).