[petalas]

Summary

alpha = 1/(8*13^m), R = 4^(f-1)
operator_error^2 >= alpha^2 max(0, 1 - 2^g/R)
actual inverse postdecoders: m=1, error <= 1/208 implies g >= 2(f-1)

Scoped proof with exact finite corroboration. This makes Cinna Davis's #5065 exact scalar-ADD obstruction robust to uniform Euclidean operator-norm approximation. For the actual negative-bank 0 and 8 inverse postdecoder targets in Dillon's #4933, even arbitrary width-dependent scalar coefficients cannot give error uniformly below 1/104 with a fixed ADD budget.

The new step is the sparse-row error inequality and its operator-norm/positive-tolerance consequences. The existing marker identity, physical bank labels and exact support obstruction are cited premises, not independently audited or replayed results. Only research/terminal-approximation-floor/ changes. The sparse-row inequality is sharp; a matching complete decoder or optimal whole-operator bound is unclaimed.

Evidence

• Before: Prove two-stage physical codes resist fixed scalar postdecoding (no new κ) #5065 excludes exact decoding by a fixed scalar/monomial word. After: error at most 1/208 still forces its exact 2(f-1) ADD floor.
• Exact local replay checks 65,554 support subsets, 6,561 Gaussian coefficient rows, 27 tensor truncations through width six and 119,400 corollary comparisons, plus eight rejected arguments and six discriminating controls. Registered normal and optimized commands pass, timed separately at 0.38 s and 0.37 s locally, below their 60-second limits.
• Committed-byte/source-history preflight and official export integrity pass at b39c547f11244e2a275a8ed7e5be0936fbc723bf. Read-only exported normal/optimized replays pass without Git on PATH; all ten exported files retain their bytes and modes. Three disposable semantic mutations reject for the missing error, inverse scale and marker-column factor.

Reproduce from the repository root with CPython 3.12.15, standard library only:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/terminal-approximation-floor/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/terminal-approximation-floor/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/terminal-approximation-floor
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/terminal-approximation-floor --check-source-history

A portable Python 3.12 path may replace the absolute interpreter path. Expected direct output is PASS_TERMINAL_APPROXIMATION_FLOOR.

Limitations

Linear scalar ADD/SCALE, monomial maps and owned COPY/CLEAR only, with independent dirty inputs. Nonlinear rounded execution, final composed-caller error, paid Gaussian decoder minima, changed entrances/exits or recursive job types are outside scope. Native all-column correctness, conditioning, physical storage/routing, precision/tape, compiler and outer admission remain inherited or unresolved. No full supplier/Lean/historical replay, independent human acceptance, proof-kernel validation, new kappa or selected-frontier change is claimed.

Open next questions

• Construct a complete scalar/monomial approximation with O(f) ADDs, including all owner blocks and dirty restoration; row-level sharpness alone does not supply it.
• Bind the actual entrance's least singular value and caller norm before transferring this operator floor to final Gaussian-output error.

Related open work

• Audit the centre-0 producer and reject its declared product embedding (no new κ) #5101 changes an actual-centre0 producer and tests a declared product embedding. The present theorem concerns the unchanged two-stage terminal products of Emit a phase-correct coded p16 caller removing 144 center calls (no κ) #4933/Prove two-stage physical codes resist fixed scalar postdecoding (no new κ) #5065; it neither excludes that changed producer nor validates its granted target inventory.
• Dillon's active whole-caller transport investigation changes chronological code transport and the output boundary, outside this fixed-postdecoder theorem.

CI notes

CI pending at b39c547f11244e2a275a8ed7e5be0936fbc723bf. Both registered checks passed locally. No hosted outcome is claimed yet. The historical card's first command fails with KeyError: 'complex_profile' against the changed selected schema; the current selected-source orientation passes. That orientation failure is unrelated to this package and is recorded in its README.

Merge Danger

Door: two-way.

Blast Radius: isolated.

One new research package; scientific acceptance and selected-frontier promotion are separate decisions.

Produced by Nick Petalas. Credit Cinna Davis #5065, Dillon Amburgey #4933, Dugongue/mdumitrean #4929, JoyboyBrian #5036/#5069, Cao Yifan, zxv, Jacob Alan Sussman, Ryanson Jonathan and the retained native/controller/compiler/precision lineage. Independent human and formal proof-kernel review are unclaimed.