[MCA] Cut common-core shortening staircase

[scottdhughes]

Stack and review boundary

This is a ready scoped MCA v4 S/A/E route-cut packet stacked on #1160 at exact head c5f4ea7a0c78828c901ae5f3428894a8b2e2806b.

Review only:

c5f4ea7a0c78828c901ae5f3428894a8b2e2806b..e26c15b2d

Upstream main remains 93fba1be3f3299b0ba4708d88715377bbb656e45; #1160 remains open. A refreshed open-PR audit found no duplicate common-core shortening staircase packet. #1161 is a symbolic rate-half Lane-T biform route cut and #1162 is a razor-bracket packet; neither overlaps this active KoalaBear common-core theorem beyond the usual experimental/agents-log.md integration seam.

Exact local theorem

For one selected non-affine family of actual support-wise bad explanation states, let C be the common intersection of their maximal agreement supports, c=|C|<k, and divide by its squarefree locator after interpolating the received pair on C.

This gives a typed reversible adapter

(n,k,m) -> (n-c,k-c,m-c)

that preserves the finite affine slope, the declared explanation/support correspondences, identical-support noncontainment, field of definition, and the invariants m-k, n-k, and n-m. It does not identify the shortened line/carrier/support with the original objects. Reverse scalar-locator owner use requires denominator nonvanishing on the deleted core, and the converse embedding requires compatible fresh field points.

Sharp KoalaBear walls

At (n,k,m)=(2097152,1048576,1116048) and B_*=274980728111395087:

• the deployed order-32 degree-18 interface survives exactly through c=4130;
• at c=4131 the exact floor drops to 17;
• the generic fixed-core compiler fits through shortened dimension s=2 and fails at s=3;
• under shortened direction separation,
  J_13=47876303026096432 < B_*, while
  J_14=743896698428332665 > B_*;
• Jo's agreement-set shortening transfer cannot bridge the first degree wall: at c=4131 its binomial multiplier alone has 3765 bits and exceeds B_*; staged shortening telescopes to the same factor.

Route cut and ledger effect

The local cancellation cannot be summed over varying local 32-tuple cores. The active v4 source still lacks a chronology-correct whole-line selector that sends each actual slope exactly once to an earlier owner, one paid fixed-core family, a shortened direction-list residual, or COMMON_CORE_SHORTENED_s_GE_14.

That selector is the first missing bridge for this staircase route; an alternative maximum-type whole-line theorem could bypass it. This packet therefore records:

U_S movement = U_A movement = U_E movement = global ledger movement = 0.

It does not claim S/A/E, KoalaBear, LIST, or universal four-rate closure.

Verification

Canonical payload:

f5aac02184e6e3c0c3acda8fc64929d37e3166ce74556e7b3d217cdc8a520b7c

Passed:

• Python verifier in normal and optimized modes;
• 16/16 hostile mutations rejected in each mode;
• Sage exact GF(17) cancellation: all five slopes and same-support noncontainment preserved under (8,4,6)->(6,2,4);
• FLINT exact integer/rational replay;
• Wolfram connector: all 17 exact checks true;
• Draft 2020-12 schema, canonical JSON, payload, and 7/7 packet hashes;
• five exact Git blob/SHA/current-byte source pins with line-range bounds;
• git diff --check.

Independent source/chronology, mathematics, and certificate/custody reviews are GREEN on the final payload. The initial source review caught two missing source pins and overbroad identity/necessity wording; those were corrected, guarded, resealed, and re-reviewed GREEN.

Maximal next attack

Construct or falsify the actual-record common-core forest compiler before thm:partial-relative: canonicalize complete realizable explanation states, partition varying tuple cores in distinct-slope units, and retain the identical original provenance through the shortening adapter. If a disjoint selector is false, preserve the smallest actual collision. If it succeeds, attack the first surviving DIRECTION_LIST_SHORTENED_s or COMMON_CORE_SHORTENED_s_GE_14 family with a same-owner maximum-type theorem.

[AllenGrahamHart]

I executed the reserve-arithmetic probe proposed for the direct S/A/E route, using the literal 2w repair from #1160 against the active B^*-31-(n-g) owner target.

Verdict: SURVIVES_WITH_EXPLICIT_PRICE. The near-rational stratum cannot be absorbed into the same exception set bounded by 31, since 2w=134944 on KoalaBear and 134896 on Mersenne-31. If it is placed in a separate earlier first-match owner, the exact large-owner target becomes

B_owner^(2w)(g) <= B^*-(2w+31)-(n-g).

Exact endpoint replay:

row          target at g_min            target at g=n   floor(target/avg-ceil)
KoalaBear    274980728110346481          274980728111260112      4807520
Mersenne-31          15728609                   16642288                9

All affine and smaller-owner branches retain positive margins. In the large-owner branch, 2w+31+(n-g)+target = B^* identically. So integer arithmetic does not kill the direct route, but every retained source interface must tighten the large-owner target by exactly 2w.

This does not prove the revised large-owner bound, exception routing, the whole-line selector, or either safe row. The proof packet, source/blob pins, primary verifier (8/8 mutations), and independent audit (3/3) are at AllenGrahamHart/rs-mca-prize-dag@2607c6fa7.

Before packaging this as a small stacked threshold-note PR on the #1160/#1163 lineage, please signal if that would collide with an in-progress source regeneration.

[AllenGrahamHart]

Follow-up on the shared d1=67473 K-adapter probe: the mutation control (u,v)=(1_E,X^k) yields an exact hostile regression for unguarded source-dimension transport.

On the deployed KoalaBear row, let D=<zeta> have order n=2^21, let e=67473, let E be the first e subgroup powers, and let S be the next m=1116048 powers. At slope zero:

• for RS[F,D,k], u=1_E is explained by zero on S, while no degree-<k polynomial agrees with v=X^k on m>k points, so the witness is support-wise MCA-bad;
• for RS[F,D,k+1], the pair (0,X^k) simultaneously explains the same received pair on the same support.

Thus badness / first-owner semantics cannot be transported silently from K=k+1 to the actual degree-<k problem, even when a numerical prefix profile lines up. This does not refute a guarded adapter: retaining K=k, or explicitly carrying and rechecking the original degree and pair-noncontainment guards, remains open.

Proof packet, exact Pocklington/subgroup reconstruction, eight mutation controls, and an independent audit are in commit 80d430a68. Both verifiers pass. The source contract pins this PR head e26c15b2d2c2f98ae12dda17b97c40981f76e1ff and the #1159 note/verifier blobs. No row closure or Q/BC owner assignment is claimed.

[AllenGrahamHart]

The third shared route-comparison probe also has an exact answer: the deployed #1160 line is rejected by the necessary balanced-profile guard of the cycle-19 candidate P_BC contract.

For each of the 67,472 displayed bad slopes gamma_i, the word U_i=u+gamma_i v is supported exactly on E\{e_i}, of size 67,471. If W_i is that support locator, then (W_i,0) lies in the received-word lattice, so its effective shifted degree is 67,471. Therefore d1(U_i)<=67471, while the candidate BC contract requires d1>=67472. All 67,472 displayed slopes are rejected. This is symbolic support-locator arithmetic; no field enumeration or reduced-basis computation is needed.

The three pre-registered shared probes now read:

1. reserve repricing: survives, but the owner target must pay the explicit 2w charge;
2. silent K=k+1 badness transport: refuted; the original degree and pair-noncontainment guards must be retained;
3. [MCA] Repair support-wise near-rational reduction by 2w #1160-line BC rejection: passes at necessary-guard level.

Proof packet, source pins, eight mutations, and independent audit: commit d797d8ffd.

Scope caveat: this does not prove that the cycle-19 candidate relation is executable or equivalent to the independently frozen BC owner. The next shared-spine obligation is a typed P_BC soundness contract together with the original-degree guarded K adapter, not another profile-only substitution.

[AllenGrahamHart]

The K=k+1 mutation has an exact general repair at the lattice-to-witness layer.

For the same received-word lattice, define

s_k(W,N)   = max(deg W, deg N-(k-1))
s_k+1(W,N) = max(deg W, deg N-k).

Every vector satisfies s_k+1 <= s_k <= s_k+1+1, and the two minima satisfy the same inequalities. For a monic split complement locator W of degree omega=n-m with W|N, the effective K=k+1 support envelope permits deg(N/W)<=k. It represents an actual degree-<k explanation on the identical support exactly when

deg(N/W)<k
<=> deg N<=omega+k-1
<=> s_k(W,N)<=omega.

Conversely every actual degree-<k explanation on an exact size-m support produces one unique guarded pair. Same-support pair noncontainment is executable too: interpolate u|T and v|T to degree <m; simultaneous code explanation holds iff both interpolants have degree <k.

This resolves SEM-QBC soundness at the lattice-to-witness layer and the algebraic degree guard in condition 4, including boundary records. It deliberately does not claim that a numerical profile determines Q/BC ownership, preserve chronology across shifts, prove slope-global Q exclusion, or cover the frozen BC cell.

Proof and two checkers: commit 3f626c84d. The primary checker exhausts all 15*7^4=36015 exact-support records on a GF(7) row and verifies exactly 7^3 actual-code records per support; the independent checker verifies the official one-coefficient gap and same-support contained/noncontained controls. No Modal computation was used.

[AllenGrahamHart]

Independent replay/import report for the #1159 actual pole-line certificate:

• Replaying the primary checker at the exact [K3] Audit actual-record dimension shift before Rec_2_4 #1159 head e603e0cedc5220ec2f29bd53836e732e3ec14934, with the public DAG supplied for external pins, passes the actual-record check plus all 62 semantic and 3 parser mutations.
• Replaying from the later [MCA] Cut common-core shortening staircase #1163 stack correctly fails the source-drift gate because intervening [MCA] Repair support-wise near-rational reduction by 2w #1160/[MCA] Cut common-core shortening staircase #1163 changes modify a pinned manuscript. The exact-head result is the valid provenance replay.
• Two new independent local checkers reconstruct primality, the order-2^21 carrier, irreducibility of X^6+X+6, the exact support, pole-line cancellation, same-support noncontainment, and d1=67473 under both shifts.

The record also passes the new guarded adapter: the size-m support-complement locator with numerator zero has quotient degree -infinity<k, so it reconstructs the identical degree-<k explanation. This concretely closes the parser/witness-soundness gap for one deployed record.

The owner remains explicitly UNASSIGNED: boundary under K=k and first-interior under K=k+1 are numerical profile labels only. No Q, BC, or U_new membership is inferred.

Compact import and independent verifiers: commit d888aff32.

[AllenGrahamHart]

Follow-up route-cut audit from the prize DAG, after independently banking the common-core cancellation theorem in this PR.

A tiny exact search found the preferred local-selector collision from section 7. Over RS[GF(11), GF(11)^*, 5] at agreement m=7, the relative critical order is 6. One received line has seven displayed support-wise MCA-bad slopes, each with a unique degree-<5 explanation on its exact seven-point maximal support. The two non-global-affine records are:

R1 = {0,2,3,5,6,8},   C(R1) = {8,10}
R2 = {0,2,3,5,6,9},   C(R2) = {10}

They share slope 0. Therefore the record-local intersection C(R) is not a slope invariant: assigning each local record directly to its fixed-core family does not itself produce disjoint slope ownership.

Scope: this does not refute the cancellation adapter, and it is not a deployed-row or first-match counterexample. It cuts only the naive record-local owner. A successful forest compiler still needs a genuinely line-global priority with controlled projection/add-back fibers, or the same-owner maximum-type bypass already allowed in section 5.

Primary verifier: 840 support-first interpolation checks, 6/6 mutations. Independent audit: exhaustive 7 * 11^5 = 1,127,357 codewords, separate modular interpolation, 3/3 controls.

• statement and exact payload
• cycle note and route consequence

[AllenGrahamHart]

A proved repair to the local-core collision is now banked: take the intersection over the entire declared selected residual slope set once per received line, rather than per critical record.

For a finite selected family with at least two slopes, either all explanations are globally affine, or the line-global core C_* has size below k. The common-core cancellation theorem then applies simultaneously to every selected slope. The slope map is literally the identity, has fiber one, and preserves actual same-support badness plus (m-k,n-k,n-m). This eliminates the core-choice sum and record-local ownership collision.

The price is explicit: the global core can be smaller than every useful local core. At the KoalaBear staircase, the one global family is paid only for s<=2 or direction-separated 3<=s<=13; otherwise it emits one honest direction-list or s>=14 residual. In the exact GF(11) collision control, C_*={10} shortens (10,5,7) to (9,4,6), preserves all seven slopes, and fails direction separation at equality, so it correctly lands in the direction residual rather than claiming payment.

• proved theorem, proof, and two verifiers
• cycle note

This does not close S/A/E, but it separates the ownership issue from the remaining mathematical issue: direction-list control for 3<=s<=13, then the large-global-dimension residual.

[AllenGrahamHart]

Follow-up: the direction-separation hypothesis in thm:affine-span-mca can be removed for the support-wise MCA application.

Fix a selected slope gamma, an exact size-m agreement support S_gamma, and a basis c_1,...,c_s for the affine explanation direction. If the incident normals fail to span F^(s+1), there is a nonzero relation

delta r_1 - sum_i mu_i c_i = 0 on S_gamma.

• If delta=0, basis independence gives a nonzero degree-<K codeword with m=K+w>K roots, impossible.
• If delta!=0, r_1 agrees on S_gamma with b=delta^(-1) sum_i mu_i c_i. Since r_gamma agrees there with c_gamma, the base word r_0 agrees on the same support with c_gamma-gamma b. This contradicts exact same-support pair noncontainment.

Thus the full-rank input needed by the existing incidence proof follows locally from pair noncontainment; no global condition max_c agr(r_1,c)<m is needed. The rest of the proof and its bound are unchanged.

For the whole-line shortened family (K=s, n=R+s, m=d+s) this gives

J_s = floor(prod_{i=0}^s (R+i)/(d+i)).

At the two deployed rows:

KoalaBear:   J_13=47876303026096432 <= B*=274980728111395087
             < J_14=743896698428332665
Mersenne-31: J_5=14115447 <= B*=16777215 < J_6=219426634.

So the direction-list branch disappears throughout the numerically paid range. The remaining whole-line global-core residual starts at s>=14 (KoalaBear) and s>=6 (Mersenne-31).

Proof packet, exact contracts, hostile GF(11) control, and two independent verifiers: AllenGrahamHart/rs-mca-prize-dag@3a13f2dcd

The control is intentionally outside the old direction-separation hypothesis (agr(r_1,C)=m) but has rank five at all seven selected slopes; the exhaustive audit checks all 7*11^5=1,127,357 candidate normal relations.

[AllenGrahamHart]

A second composition substantially narrows the large-s residual left by common-core shortening.

After whole-line cancellation, write the shortened row as

(N,K,m)=(R+s,s,d+s),  t=R-d.

Let d_U(y_1) be the minimum weight of a lift of the shortened line-direction syndrome and put j=R-d_U(y_1). Pair noncontainment forces y_1!=0. Applying the existing direction-distance ray theorem on the full shortened domain gives

|Z| <= floor((R+s)(d-j) /
             (d^2-(R-2d)s-(R+s)j))

whenever the denominator is positive. This is one whole-line family, so there is no union/core multiplicity.

Solving the denominator and exact floor inequalities against the deployed budgets gives:

KoalaBear:   all j paid for s<=13 by the support-wise affine-span result;
             0<=j<=J_B(s) paid for 14<=s<=4982.
Mersenne-31: all j paid for s<=5;
             0<=j<=J_B(s) paid for 6<=s<=4979.

On KoalaBear the budget never cuts before denominator positivity; the maximum paid value over the whole range is 168818566 at (s,j)=(1356,3156), far below B*=274980728111395087.

On Mersenne-31 the maximum paid value is 16131678 at (1970,2617), below B*=16777215. There are exactly thirteen dimensions where the last positive-denominator defect is over budget and J_B(s) is one smaller; the packet pins all thirteen.

Thus the remaining common-core branch is no longer opaque “large dimension.” It is the explicit low-direction-distance cell

s>=4983 or j>J_B(s)  (KoalaBear),
s>=4980 or j>J_B(s)  (Mersenne-31).

Proof packet and two exact verifiers: AllenGrahamHart/rs-mca-prize-dag@d21366a88

The primary verifier scans 9,943 dimensions. The independent audit directly enumerates 21,505,828 positive defect candidates and reproduces the maxima and thirteen Mersenne spike cells.

[AllenGrahamHart]

The low-direction cell also supports an exact recursive shortening theorem.

In a shortened row (R+s,s,d+s), choose a minimum lift of the nonzero line-direction syndrome:

q=r_1-b,  wt(q)=R-j,  E=supp(q),  0<=j<d.

Every size-(d+s) pair-noncontained witness meets E in at least

(d+s)-(s+j)=d-j

coordinates. For each x in E, condition on witness agreement at x and cancel that coordinate. This injects the corresponding slopes into a support-wise MCA-bad child in row (R+s-1,s-1,d+s-1).

The child's direction defect cannot increase: any child direction residual lifts to an original degree-<s direction residual of the same weight, while q was globally minimum. Hence j_x<=j.

Double-counting (slope,x) incidences gives the field-general recurrence

M_s(j) <= floor((R-j) M_(s-1)(j)/(d-j)),  0<=j<d.

Composing this with the direct direction-distance bound and the last all-defect affine-span payment yields:

KoalaBear:   j<=4330 at s=14 and through s=22;
             j<=9 at s=4982; j<=8 at s=4983;
             rank-regular j=0 through s=4992.
Mersenne-31: j<=4334 at s=6; j<=4333 at s=7;
             j<=1 at s=4978; j=0 at s=4979.

Relative to the direct router, this extends 4,331 KoalaBear defects by up to ten dimensions and 4,335 Mersenne defects by one dimension.

Proof packet and independent defect-major/dimension-major exact replays: AllenGrahamHart/rs-mca-prize-dag@3dec7412c

The residual remains explicit: j>=d or the complement of the certified recursive envelope. No full row payment is claimed.

[AllenGrahamHart]

Complementary high-defect payment: sparse directions reduce to punctured ordinary lists.

In shortened row (R+s,s,d+s), suppose

r_1=b+q,  b in C,  E=supp(q),  |E|=e<d.

For a selected slope with explanation c_gamma, put a_gamma=c_gamma-gamma b. Outside E, a_gamma agrees with r_0 on at least d+s-e coordinates. Puncturing E and applying the complete-code affine-span list theorem gives at most

floor(C(R-e+s,s)/C(d-e+s,s))

distinct base explanations.

Every pair-noncontained witness must meet E; otherwise (a_gamma,b) explains the received pair on that witness. For fixed punctured explanation a and x in E, the equation

a(x)-r_0(x)=gamma q(x)

determines one slope. Therefore

|Z| <= e*floor(C(R-e+s,s)/C(d-e+s,s)).

At the first all-direction-unpaid dimensions:

KoalaBear, s=14: e=5 -> 239567470186217925 <= B*;
                  e=6 -> 287536780021025682 > B*.
Mersenne, s=6:   e=1 -> 14115447 <= B*;
                  e=2 -> 28233244 > B*.

So these cells also pay the extreme high-defect tails j=R-e>=1048571 and j>=1048575.

Proof packet and independent exact-binomial/product scans: AllenGrahamHart/rs-mca-prize-dag@c25e21360

This is disjoint in mechanism from the recursive low-defect payment. The middle defect interval remains explicit and open.

[AllenGrahamHart]

A codeword-direction gauge gives an additional rank router on every shortened MCA family.

For any b in C, apply

(r_0,r_1,c_gamma) -> (r_0,r_1-b,c_gamma-gamma b).

This preserves slopes and every exact agreement support. Pair containment is equivalent via (p_0,p_1)<->(p_0,p_1-b), so support-wise MCA badness is preserved in both directions.

If r_c and r_b are the affine ranks of the original and transformed explanation families, their difference spaces are related by a rank-one update:

(c_gamma-c_0) -> (c_gamma-c_0)-(gamma-gamma_0)b

hence |r_c-r_b|<=1.

In shortened row (R+K,K,d+K), applying the support-wise affine-span theorem to transformed rank r gives

A_(K,r)=floor(max(
  (R+K)^(falling r+1)/((d+K)d^(rising r)),
  (R+r)^(falling r+1)/d^(rising r+1))).

The exact deployed ambient walls are:

KoalaBear:   r<=11 for all K<=1048576;
             r=12 through K=745260;
             r=13 through K=289603;
             r>=14 not uniformly paid.
Mersenne-31: r<=4 for all K<=1048576;
             r=5 through K=482472;
             r>=6 not uniformly paid.

Adjacent boundaries:

KB r=12: 274980259855184513 <= B* < 274981914318597687
KB r=13: 274980152556476265 <= B* < 274982259324238595
M31 r=5: 16777192 <= B* < 16777228

For fixed r, the first term has one turn because the sign of its successive difference is the sign of rK+(r+1)d-R+r; the interval certification is therefore exact.

Proof packet and exhaustive/independent arithmetic checks: AllenGrahamHart/rs-mca-prize-dag@60db12dc5

Choosing the nearest codeword b from the direction-distance route means every surviving cell now carries both a direction-defect condition and a transformed affine-rank floor. No rank drop is assumed.

[AllenGrahamHart]

Rank refinement of the sparse-direction payment: the punctured-list bound depends on transformed explanation rank, not ambient shortened dimension.

Use the gauge from the preceding comment and write

q=r_1-b,  e=|supp(q)|<d,
a_gamma=c_gamma-gamma b,
r=rank_aff{a_gamma}.

After puncturing supp(q), the selected a_gamma lie in an affine rank-r flat in row

(n',K',m')=(R+K-e,K,d+K-e),  w'=d-e.

The ordinary affine-span list theorem gives at most

floor(C(R-e+r,r)/C(d-e+r,r))

distinct transformed explanations. Pair noncontainment gives slope fiber at most e, exactly as in the full-code special case. Hence

|Z| <= e*floor(C(R-e+r,r)/C(d-e+r,r)),

independent of ambient K.

Exact rank/support walls:

KoalaBear:   r=12 -> e<=1144; r=13 -> e<=87;
             r=14 -> e<=5;    r=15 -> no e>=1.
Mersenne-31: r=4  -> e<=282;  r=5  -> e<=18;
             r=6  -> e<=1;    r=7  -> no e>=1.

Representative adjacent checks:

KB r=13: 272256895343216442 <= B* < 275435997743171320
M31 r=5: 16363584 <= B* < 17273869

Proof packet and independent exact-binomial/gcd-product scans: AllenGrahamHart/rs-mca-prize-dag@a62dfeb19

Combined with the gauge-rank router, the surviving common-core cell is now explicitly joint: transformed rank beyond its ambient wall and direction support beyond the corresponding table entry. No joint interaction theorem is assumed.

[AllenGrahamHart]

A further proved refinement of the shortened sparse-direction branch is now available at AllenGrahamHart/rs-mca-prize-dag@4d2c9d3a5.

After a codeword gauge, write q=r_1-b, E=supp(q), |E|=e<d, and let the transformed selected explanations have affine rank at most r. For one distinct explanation a, define its outside-agreement deficit

h_a = m - |{x outside E : a(x)=r_0(x)}|.

Same-support pair noncontainment gives 1 <= h_a <= e. Every slope owned by a is a fiber of (a-r_0)/q on E with at least h_a points, so a owns at most floor(e/h_a) slopes.

Applying the affine-span list theorem cumulatively to explanations with deficit at most h gives

B_h = floor(C(R-e+r,r)/C(d-h+r,r)).

Hence the selected slope count obeys the field-general, ambient-dimension-independent bound

|Z| <= sum_(h=1)^e (B_h-B_(h-1))*floor(e/h),   B_0=0.

Exact paid prefixes:

KoalaBear:   r=12: e<=1407; r=13: e<=89; r=14: e<=5; r=15: none.
Mersenne-31: r=4:  e<=287;  r=5:  e<=18; r=6:  e<=1; r=7:  none.

For comparison, the previous scalar e * B_e prefixes were KB 1144,87,5 and M31 282,18,1.

The node has exact adjacent-boundary checks, an independent gcd-product implementation, and a brute-force audit of 125 small cumulative-cap allocation problems. Repository-wide verifier, DAG, orbit, and critical-document checks pass.

Scope: this is a proved local K4 route cut, not a first-match owner, bankable U_new, or KoalaBear row payment. Ledger movement remains zero. The remaining branch must jointly evade the support, transformed-rank, and weighted deficit-profile walls.

[AllenGrahamHart]

A stronger, support-sensitive incidence theorem is now proved at AllenGrahamHart/rs-mca-prize-dag@99d52e857. It uses the same minimum-lift gauge and support-wise affine-span setup as the preceding comments, but unlike punctured-list payment it remains valid when e >= d.

Let q=r_1-b, E=supp(q), |E|=e<=R, and place the transformed selected explanations in an affine codeword flat of dimension at most r. In the affine-incidence parameter space,

v_x=(q(x),-c_1(x),...,-c_r(x)).

If z normals are zero, every one is outside E. Among the n-z active coordinates, exactly n-e-z are outside E, and all of their normals have zero slope component. Therefore no full (r+1)-normal basis lies wholly outside E, and the candidate ordered-basis numerator sharpens from

(n-z)_fall_(r+1)

to

(n-z)_fall_(r+1) - (n-e-z)_fall_(r+1).

Combining this exact subtraction with the existing two-endpoint affine-span envelope gives

|Z| <= floor(P(R,r,e) M(K,r)),

P(R,r,e)
 = 1 - (R+r-e)_fall_(r+1)/(R+r)_fall_(r+1),

M(K,r)
 = max(
     (R+K)_fall_(r+1)/((d+K)d_rise_r),
     (R+r)_fall_(r+1)/d_rise_(r+1)).

The support factor is increasing. The proved one-turn dimension calculation reduces a uniform r<=K<=R certificate to the K=R endpoint for all displayed ranks.

Exact uniform walls:

KoalaBear:
  r=11: every e<=R
  r=12: e<=15903
  r=13: e<=435
  r=14: e<=13
  r=15: no e>=1

Mersenne-31:
  r=4: every e<=R
  r=5: e<=62235
  r=6: e<=1486
  r=7: e<=41
  r=8: e<=1
  r=9: no e>=1

The node passes exact rational endpoint and adjacent-wall checks, four hostile mutations, an independent recurrence/gcd implementation, exhaustive tuple subtraction in 239 small models, and 189 support-monotonicity checks. All repository-wide DAG/orbit/protocol checks pass.

Scope: proved local K4 route cut, no first-match owner and no bankable U_new; row-ledger movement remains zero. The surviving shortened family now has explicit joint lower walls on transformed rank and minimum-lift direction support, including part of the former middle-support region.

[AllenGrahamHart]

Exact common-zero optimization of the support-sensitive theorem is now proved at AllenGrahamHart/rs-mca-prize-dag@5d724af27.

Retain the notation of the preceding comment and write the zero-normal split as z=g+c. The subtracted-basis proof gives

|Z| <= ((n-z)_fall_(r+1)-(n-e-z)_fall_(r+1))
       /((m-g)(d+c)_rise_r).

For fixed z, the numerator is fixed while

(m-z+c)(d+c)_rise_r

strictly increases with c. Thus c=0,g=z is the worst split. Setting x=R+K-z yields the exact one-dimensional envelope

|Z| <= floor(max_(x=R+r..R+K)
  ((x)_fall_(r+1)-(x-e)_fall_(r+1))
  /((x-R+d)d_rise_r)).

Using x<=2R gives one certificate uniform over every shortened dimension r<=K<=R.

Exhaustive exact official walls:

KoalaBear:   r=12 e<=31806; r=13 e<=870; r=14 e<=26; r=15 none.
Mersenne-31: r=5 e<=124471; r=6 e<=2973; r=7 e<=83;
             r=8 e<=2; r=9 none.

Every last-paid and adjacent first-unpaid maximum is attained at x=2R=2097152. Two independent constant-memory implementations each exhaust 16,777,078 integer cells and recover all nine boundaries; the second uses falling-product recurrences and separately checks 140 fixed-z denominator cells.

The notable route effect is Mersenne transformed rank five: a survivor now needs e>=124472>d=67448, so this theorem cuts into the middle-support region rather than stopping at the sparse puncturing boundary. This remains a proved local K4 route cut with zero row-ledger movement and no first-match-owner claim.

[AllenGrahamHart]

Follow-up composition theorem from the public Prize DAG: AllenGrahamHart/rs-mca-prize-dag@fc74e16cd (rate_half_mca_global_core_rank_support_distance_router).

This combines the PRs whole-line common-core shortening with three already-proved bounds on the same shortened selected slope family: the codeword-gauge rank envelope, the exact direction-support/common-zero affine-basis envelope, and recursive direction-distance shortening. No budgets are added.

The exact KoalaBear consequence sharpens the route-cut residue. At the first legal residual dimension s=14, transformed rank satisfies r<=s; ranks <=13 are already paid, hence a survivor has exactly r=14. Exact integer maximization pays e<=31,768, while recursive direction distance pays e>=1,044,246. Thus the sole surviving first cell is

s=14, r=14, 31,769 <= e <= 1,044,245.

Uniform low-support walls through s=4992 are e<=31,768, 1,576, 94, 5 at ranks 14,15,16,17; each is paired with the recursive high-support suffix at its own legal dimension. The analogous Mersenne first cell is s=r=6, 11,848<=e<=1,044,241.

Two independent constant-memory exact checkers replay 99,490 support cells, 9,953 rank cells, 22 recursive frontiers, ten legal-rank residual intervals, 96 small monotonicity models, and 7 hostile controls. DAG/protocol/orbit validation is green. Scope is deliberately a route localization only: it does not pay the middle interval, supply the active K3 first-match atlas, allocate U_K3, or close a row.

[AllenGrahamHart]

Correction to my earlier affine-span comment in this thread: draft PR #1165 gives an exact GF(1009) counterexample to thm:affine-span-mca. It has 31 selected slopes versus the claimed bound 23, satisfies direction separation, and every selected support is same-support pair-noncontained. Pair noncontainment forces local full incident rank but does not justify the proof's proper-subspace occupancy estimate.

Please treat my earlier claim that pair noncontainment preserves the incidence proof, and the resulting direction-separated fixed-core payments through s=13, as retracted. The common-core cancellation theorem itself is unaffected.

[AllenGrahamHart]

Follow-up: #1165 now includes a proved replacement theorem, not only the retraction. For selected explanation affine rank q, the valid final extension factor is L=max(1,e-(N-m)), giving floor(max(A_q,B_q)/L).

At the first KoalaBear shortened row this fully pays every family of actual affine rank q<=9; ranks q=10,11,12,13 are paid from e>=981108,981153,981861,992852, respectively. Rank 14 remains unpaid by this compiler. Thus the fixed-core staircase can be repaired through shortened dimension 9, but dimensions 10-13 need the printed direction-support guards rather than the former unconditional payment. The exact verifier includes all eight adjacent wall failures and an exhaustive GF(3) control.

[AllenGrahamHart]

Further correction/narrowing from #1165: the previously opaque top explanation-rank cell now has an exact two-branch decomposition.

For full explanation affine rank q=K, anchor one slope and set

V=span{(gamma-gamma_0,c_gamma-c_gamma0)} <= F direct_sum C.

Then h=dim(V) is K or K+1. If h=K, V is the graph of a nonzero functional and exactly an affine hyperplane of codeword gauges drops explanation rank to K-1; if h=K+1, no gauge drops rank. Pair noncontainment forces r_1 notin C, so h is also the error-vector affine rank.

Consequently, at the first KoalaBear shortened row the q=14,h=14 branch now inherits the rank-13 corrected occupancy suffix e>=992852; only the full-lift q=14,h=15 branch retains the older high-support threshold e>=1044239. Together with the low-support gate, the exact split is

h=14: e<=5 or e>=992852
h=15: e<=5 or e>=1044239.

The analogous Mersenne split is h=6: e<=1 or e>=1037876 versus h=7: e<=1 or e>=1044242. This is a proved route narrowing, not a row payment; both displayed middle intervals remain open. #1165 includes the proof and an exhaustive small-field gauge audit.