[petalas]

Summary

Scoped proof: every formal UT4 central-target word needs at least 4w middle b calls, with arbitrary finite restored dirty workspace and free scalar mixing. The new bound is n_b >= 2w + rank(X_b) + rank(Y_b).

U = [U_A; U_C],  V = [V_A V_C]
XY = UY = XV = 0
UV = [[0,P],[P,0]],  rank(UV) = 2w
2w <= dim(ker X / im Y) = n_b - rank X - rank Y

With ToikY's credited outer floors and direct word, the exact complete tariff is 2w alpha + 4w beta + 2w gamma for all nonnegative uniform letter prices. The unit minimum is 8w. This settles both remaining seven-b mixed-rank cases in Victor Li's #3938 and the pure-central weighted question in Josie Elliston's #1816. No new kappa is claimed.

Evidence

Before, #3938 excludes middle ranks (2,2) and leaves (2,3)/(3,2) open. After, the paired middle quotient excludes all n_b<4w algebraically, for every finite role count and word length.

The standalone verifier passes 20,632 new paired-coefficient word fixtures, 42 complete full-group endpoint fixtures, 80 omitted-call controls and ten additional rejection controls. Both warning-strict normal and optimized checks produce identical generated file-hash receipts. They took 0.523 and 0.518 seconds locally; the complete registered replay took 1.365 seconds. These are check durations, not performance gains.

Reproduce from the repository root with CPython 3.12 and the standard library:

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

Other machines may substitute their CPython 3.12 path. Metadata/pins, committed-byte/source-history preflight, AST/in-memory compile, committed export integrity and a Git-free optimized replay pass. No predecessor verifier or census is imported, audited or replayed. The universal claim is the written factorization and dimension argument; finite fixtures corroborate its implementation.

Credit ToikY #1662 for the model, quotient homomorphism, span floors and direct upper word; Victor Li #3938/#3887 for the open mixed-rank gate; Josie Elliston #1816 for two-target unit optimality and the weighted question; Aaron Wang #1690 and the retained #1680/#1573/#1589/#1607 lineage. Exact source provenance is pinned. The advance claim targets seven middle calls; the same argument yields the uniform tariff directly.

Limitations

This is a scoped formal-model proof. It does not supply a native BIT mechanism, rational-frame identity, supplier admission or a complete multiplication theorem. Role-dependent prices, extra free address operations, clean allocation, physical/native implementation, compiler/hosting, stock, precision, tape and analytic recovery are outside scope. The five selected framework assumptions remain. Human review, proof-kernel formalization, selected supplier cold replay, Lean and Docker are unrun.

Open next questions

Can an additional paid address letter escape the paired coefficient equations? Begin with its exact quotient image, identify which hypothesis changes, and price one complete arbitrary-dirty word. No such changed-alphabet construction is supplied here.

Related open work

The completion refresh inspected all eleven other account open PRs created after the advance CLAIM. No additional pure-central UT4 tariff or shared numerical endpoint was found. Adjacent call-cost work is listed below; no additional computations were run to compare it.

• PR6408 gives vector-cocycle floors for formal rank-one register words. This PR uses paired cubic coefficients for a central UT4 endpoint; the cocycle package computes no central UT4 tariff.
• PR6407 prices four pure shear stages for a two-bank swap. Its stage-rank tariff has a different endpoint and operation alphabet from the paid-letter tariff here.
• PR6411 prices source injections for completed partial echoes over characteristic-zero fields. Its observation contract and indivisible child operations differ from the full formal UT4 endpoint here.

The closest same-object predecessors #1662, #1816, #3887 and #3938 are merged. Unpublished work remains outside this coverage.

CI notes

Both hosted checks passed at exact head 2acaf42e1f8a17c13951c5f706decfa4e325bac3 in run 41528426188: plan and replay (research/ut4-hyperbolic-middle-floor). The completed checks were read once; run metadata confirms completed success at the matching head.

Hosted replay confirms execution of the registered normal and optimized finite checks and package metadata validation. The universal written proof remains outside a formal kernel. All recorded local checks, committed-byte/source-history preflight, export integrity and Git-free replay also passed. Native, physical and supplier obligations remain outside scope.

Merge Danger

Door: two-way. Blast Radius: package. The change adds six isolated research files and its opt-in replay manifest.