[petalas]

Summary

Scoped proof with exact finite corroboration. Bounded approximate decoder rows retain the acyclic rank obstruction from DreamingOfClouds's PR5559. The sharp universal triangular-envelope cutoff is

a_n(L) = first positive root of e * sum_{k=0}^{n-1}(1+L-e)^k = 1
error < a_n(L), selected free-entry magnitude <= L  =>  full rank n
a_n(L) * L^(n-1) -> 1 for fixed n

An explicit real matrix attains rank n-1 at the cutoff. Rational boundary witnesses exist in every dimension; n=8 gives error 1/255 and L=256/255. At L=1 the eight-row cutoff lies strictly between 1/256 and 1/250. A deficient row at error <=2^-p and L<=2^b requires p<n+(n-1)b.

The result adds the approximate paid-subtotal contract and coefficient-growth consequence. The predecessor's exact floors are cited, not audited or replayed. Classical interval-matrix comparison and scaled diagonal dominance retain their credit. This contribution was produced by Nick Petalas. Advance claim.

Evidence

Before, the cited decoder package explicitly left approximate border cost outside its exact acyclic rank argument. The new written proof supplies a quantitative persistence threshold and an attaining family. The standalone exact verifier passes 75 determinant identities, all 1,056 real sign vertices in four stated boxes, 60 rational rank-deficient witnesses, 60 wrap-omission controls and 15 named domain or semantic controls. An exact cancellation example shows why the magnitude bound must apply to the paid subtotal rather than the final output.

From the repository root, CPython 3.12 standard library only:

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

Substitute another CPython 3.12 path elsewhere. All commands passed locally on Python 3.12.15. Each registered normal/optimized command took about 0.14 seconds; the complete package runner took about 0.54 seconds. These are timeout-budget measurements, not performance-improvement claims. The assignment and coordination suites passed 16 and nine tests. The generated stdout receipt binds all seven package files. Committed bytes, modes and provenance history pass at ab1317b6feef935da8286fafee0f361c863125ba.

Limitations

Sharpness is for the directed triangular envelope, not a P112 attaining decoder or a sharp fixed-mask cutoff. The transfer covers acyclic rank rows and independently valid support inequalities. Exact-only cover and coefficient-ratio clauses do not automatically transfer. Ranks in the transfer are over the coefficient field, not F2. Unbounded coefficients can escape the magnitude hypothesis.

There is no unrestricted border-cost floor, COPY64 theorem, physical coefficient or precision cost, complete invoice, native supplier, selected-frontier change or new kappa. The five selected framework assumptions remain. The written all-dimension proof is not proof-kernel verification; human and formal proof-kernel review are unclaimed. No predecessor scientific replay, selected cold replay, Lean or Docker run was performed.

Open next questions

• Derive the sharper cutoff for one actual P112 selector with its exact zero cells. Begin with its comparison matrix; an actual paid-subtotal magnitude contract remains necessary.
• Price a complete approximate decoder after the required factor growth, including coefficient delivery, rounding and restoration.

Related open work

• Decoder floors: universality, projection transfer and batching reductions; C(P112) ≥ 64 reduced to named conjectures, C(P120) ≥ 72 restated on N₀ (no κ claim) #2832 studies exact decoder-floor reductions; this adds a bounded approximate rank-row contract.

• C(P112) >= 64: complete reduction to stated conjectures #3154 reduces the exact P112 floor to named conjectures; none is settled or replayed here.

• Checkpoint symmetric two-star P112 supports and inconclusive COPY63 search #5088 searches exact P112 support dictionaries; this supplies no new dictionary or COPY63 witness.

• Checkpoint eight masked-decoder basis searches (exploratory; no new K) #5064 searches exact corrected decoder bases; this instead bounds an approximate interface under explicit magnitudes.

• Non-dense fitting B: every E8 term with x·y ≠ 0 has rank ≥ 9; square root-code floors E8 ≥ 72, P112 ≥ 64, P104 ≥ 56, D4 ≥ 12 for any fitting B (no κ claim) #3045 studies exact square root-code floors for fitting pairings; this neither changes that model nor transfers its F2 prices automatically.

• One-sided padding lemma: P112 to P120 at cost exactly +8 (L120 suffices for Delta >= n_nf) #3074 gives exact one-sided padding; this does not construct or reprice a padded decoder.

• Two-sided deficiency budget: Theorem BX for b_Q <= 4 (conditional frame, exact residue, no κ claim) #3029 studies exact two-sided deficiency budgets; its numerical and combinatorial claims are not recomputed.

• Research: one-sided residue closures — Circuit Lemma, relative root counting and plane lemma close 480 of the 603 d>=4 residues (116 open; no kappa claim) #2985 closes exact one-sided residue cases; this does not classify those residues.

• Bind P112 tetrad decoder to selected ports; no kappa change #3566 binds a tetrad decoder to selected ports; physical port binding remains outside this result.

• Screen P112 tetrad coefficient fusion under relaxed rank ceilings #3604 studies tetrad coefficient fusion; this gives a magnitude obligation without a fusion schedule or tariff.

• Add exact dirty-input coefficient audit for P112 tetrad block #3916 audits a tetrad's exact dirty-input coefficients; this contributes a new approximate obstruction rather than an audit.

• Reduce complete rank-eight replay time by 32.78% (no κ) #6598 accelerates the existing rank-eight decoder replay; this imports none of that engine or its scientific counts.

• Prove exactly three shared A2 rank-six equality fibers (no κ) #6582 classifies root-capacity equality fibers; this does not classify or price those supports.

• Prove the sharp inverse envelope under a column cap (no κ) #6788 studies the exact inverse 1-norm envelope under simultaneous row and column caps. This result instead bounds singularity under entrywise triangular limits and transfers acyclic decoder rank rows; no common numerical quantity is compared.

The completion refresh read the nine other open account PRs created since the advance claim: #6785, #6786, #6787, #6788, #6789, #6791, #6792, #6793 and #6794. None computes a competing acyclic-selector error cutoff. No additional mathematical computations were run to check those contributions.

CI notes

Both hosted checks passed at exact head ab1317b6feef935da8286fafee0f361c863125ba in run 42223528815: plan and replay (research/acyclic-border-error). The completed checks were read once and both report pass. Hosted replay certifies execution of the registered normal and optimized finite checks and repository checks at this commit. It does not constitute independent human or proof-kernel acceptance of the universal written proof. All listed local checks also passed.

Merge Danger

Door: two-way.

Blast Radius: research.

Only seven files in the new isolated package are added. Shared code, frozen evidence, predecessor credit and the selected frontier are unchanged.