MCA: refute and repair affine-span incidence compiler

[AllenGrahamHart]

Summary

• replace the false affine-span transverse MCA theorem with an exact
  GF(1009) counterexample and withdraw payments using its denominator;
• prove the corrected proper-subspace occupancy compiler and exact support
  walls;
• prove the full-explanation lifted-rank dichotomy and the full-lift
  near-MDS extension reduction;
• prove a field-general punctured ordinary-Johnson profile, continue it
  through centered Gram and mean-centered rungs, then use exact-layer affine
  lines to close every sparse-direction support e<d;
• add theorem notes, forty-seven deterministic verifiers, route status in
  agents.md, and a manuscript build check.

The target KoalaBear and Mersenne-31 MCA inequalities are not refuted or
claimed closed. This PR corrects one false proof route and supplies three
replacement reductions plus one large unconditional support payment.

Counterexample and root cause

The counterexample uses

C = RS[GF(1009), {0,...,99}, 1]
(n,K,m,w,s) = (100,1,21,20,1).

One received line has 31 selected pair-noncontained slopes, while the
rejected theorem claims at most 23 and
max_c agr(r_1,c)=20<m=21. Direction separation forces full incident
rank locally but does not control occupancy of a proper normal subspace:
each zero-explanation support has 20 normals on one line and one transverse
normal. It has 40 ordered bases, not the claimed m*w=420.

This retracts the direction-separated fixed-core affine-span staircase in
#1163 and the inherited copy in #1164. It does not refute common-core
cancellation, directional Johnson, gauge equivalence, the ordinary
affine-span LIST theorem, or #1164's selector-free all-LineRay
error-affine-core set-pair theorem.

Corrected occupancy theorem

For explanation affine rank s, put

e = min_(b in C) wt(r_1-b)
L = max(1,e-(n-m)).

The repaired theorem proves

|Z| <= floor((1/L) max{
  n_fall_(s+1)/(m (w+1)_rise_(s-1)),
  (n-K+s)_fall_(s+1)/(w+1)_rise_s
}).

MDS common-zero bounds control all proper incident-normal subspaces.
Pair noncontainment supplies the last transverse normal, and direction-coset
distance raises its factor to L. At the first shortened rows this pays
all KoalaBear ranks through 9 and Mersenne rank 1 for every direction
support, with exact higher-rank suffix walls.

Top-rank structure

For full explanation affine rank K, anchor one slope and define

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

The lifted rank is exactly K or K+1.

• At rank K, V is the graph of a nonzero functional; exactly the
  affine hyperplane of gauges ell(b)=1 drops explanation rank to K-1.
• At rank K+1, every codeword gauge retains explanation rank K.

Pair noncontainment gives r_1 notin C, so lifted rank equals selected
error-vector affine rank. In the full-lift branch,

W = C + span{r_1}
d_1(W) = e
d_j(W) = N-K+j-1 for 2<=j<=K+1.

Thus every higher generalized weight is already MDS-sharp. The generic
MDS-endpoint compiler still gives 743896698428332665 and 219426634,
above the two budgets, so a weight-hierarchy replay cannot close the branch.

Punctured Johnson profile

Gauge the direction as r_1=b+q, with residual support E,
|E|=e<d. A transformed explanation with outside-agreement deficit
h owns at most floor(e/h) slopes. After puncturing E, all
explanations of deficit at most h form an ordinary RS list at agreement
m-h. Pairwise agreement is at most K-1, hence

J_h = floor((N-e)(m-h-K+1)
            /((m-h)^2-(N-e)(K-1))).

|Z| <= sum_h (J_h-J_(h-1))*floor(e/h)
    <= (e-1)J_floor(e/2)+J_e.

The weakest Johnson denominator is positive through exactly:

KoalaBear K=14:
  e=63908, denominator=1218,
  bound=4607583 <= 274980728111395087.

Mersenne-31 K=6:
  e=65236, denominator=2794,
  bound=2605443 <= 16777215.

At the adjacent supports the denominators are -5924 and -1636.
Those are proof-method walls, not unsafe certificates.

Near-Johnson centered-Gram continuation

The first post-Johnson strip still has an exact rank bound. For equal-size
A-blocks in an n-set with pairwise intersections at most c, put

g=nc-A^2>=0
G=(A-c)^2-cg.

Equal row sums put the all-ones vector in the incidence column space, so
rank(BB^T-cJ)<=rank(B)<=n. Trace-rank, Cauchy incidence, and
delta^2<=c*delta give

L <= floor(n*A*(A-c)/G)       when G>0.

Combining this with the deficit split extends the low-support walls again:

KoalaBear:   e<=64037, endpoint bound 198047217.
Mersenne-31: e<=65418, endpoint bound  16759641.

At KoalaBear e=64038, G=-36911. At Mersenne e=65419, G remains
positive but the valid bound 18212004 exceeds budget 16777215.

PSD mean-centered refinement

Centering the incidence columns at their mean is stronger. The matrix

H=B(I-J/n)B^T

is PSD of rank at most n-1. For g=nc-A^2>=0, 2A^2>=nc, and
T=(n-A)^2-(n-1)g>0, the endpoint chord for off-diagonal squares and
trace-rank give

L <= floor((n-1)n^2(A-c)/(A*T)).

Combining Johnson and mean-centered raw caps through their proved suffix
minima gives the exact deficit profile. It extends the walls to:

KoalaBear:   e<=64047, endpoint profile 181731868.
Mersenne-31: e<=65454, endpoint profile  16101127.

At KoalaBear e=64048, T=-1499457466. At Mersenne e=65455, all caps
remain defined but the exact profile 17120123 exceeds budget by 342908.

Exact-layer affine-line branch closure

At exact deficit h=e-r, an assigned explanation misses at most r
exceptional agreement coordinates. If e-3r>=K, any three explanations
share at least K exceptional agreements. Restriction injectivity
synchronizes all normalized pair differences, putting the entire exact
layer on one affine codeword line. Outside-core packing gives

L_r <= floor((N-e-(K-1))/(m-e+r-(K-1)))
for 0<=r<=floor((e-K)/3).

The lower two thirds retain the positive punctured-Johnson prefix. Uniform
endpoint comparison gives J_floor(e/2)<=31 and J_H<=47. The line
sum is termwise nondecreasing in e, with endpoint calibrations

KoalaBear:   31*(67472-2)+47+9405342 = 11496959.
Mersenne-31: 31*(67448-2)+47+9405365 = 11496238.

Both fit budget, so every sparse-direction support e<d is paid. The
terminal layer is the special case r=0; before the full top-third
closure it separately moves the walls through e=64048 and e=65455.

Full-lift total-common-core continuation

For e>=d, some synchronized exact layers have at most K-1 outside
agreements, so outside zero-core packing no longer applies. On an affine
explanation line, however, a coordinate common to every parameter is a
simultaneous base/direction agreement for one codeword pair. Pair
noncontainment limits that total core to m-1; off-core agreement sets
are disjoint. Thus

Q_r = N-m+1                                      if A_r<=K-1,
Q_r = floor((N-e-(K-1))/(A_r-(K-1)))           otherwise.

Together with the Johnson prefix this extends the walls to:

KoalaBear:   e<=95943, endpoint bound 27414298.
Mersenne-31: e<=67452, endpoint bound 16266965.

KoalaBear e=95944 has prefix denominator -1037. Mersenne
e=67453 has valid bound 17248067, over budget by 470852.

Cross-layer top-third global-line synchronization

The same triple-overlap argument synchronizes explanations across different
high-deficit layers: for allowances r_i<=s=floor((e-K)/3), every three
inside agreement sets intersect in at least e-(r_1+r_2+r_3)>=K
coordinates. Restriction injectivity therefore puts the entire top-third
union on one affine explanation line. Pair noncontainment charges its total
common-core cap only once:

|Z| <= (e-1)J_floor(e/2) + J_H + (N-m+1).

Exact scans give 6336049 at the last KoalaBear support e=95943, and pay
Mersenne-31 through e=97908 with endpoint 6682339 (largest value
6683188 at e=97907). At the adjacent supports e=95944 and e=97909,
the H-prefix Johnson denominators are -1037 and -965. These are
proof-method walls, not unsafe certificates.

Full-lift mean-centered prefix continuation

The mean-centered Gram list theorem applies to the full-lift prefix once the
scope guard A_H=m-H>K-1 is stated explicitly; its ordinary set-system
proof does not require e<d. Using every cumulative cap through its suffix
minimum, rather than the coarser two-threshold estimate, gives

|Z| <= sum_(h=1)^H (B_h-B_(h-1))*floor(e/h) + (N-m+1).

Exact scans pay KoalaBear through e=96150 with endpoint 479693401, and
Mersenne-31 through e=98229 with endpoint 16488216 (largest value
16489118 at e=98228). At KoalaBear e=96151, the H=64105
mean-centered denominator is -4625043784. At Mersenne e=98230, every
cap remains legal but the profile 17415873 exceeds budget by 638658.
Neither adjacent failure is unsafe.

One-layer boundary-anchor continuation

Put q=e-K-3*floor((e-K)/3). When q>=1, split on whether the
already-synchronized top-third union has at most one or at least two
explanations. In the first case, charge the full prefix and one tail slope.
In the second, two high-union anchors synchronize the exact boundary layer,
because every mixed (s,s,s+1) triple has at least K+q-1>=K common
coordinates. This gives

|Z| <= max(P_H+1, P_(H-1)+(N-m+1)).

For Mersenne-31 at e=98230, the two case bounds are 16434745 and
16487313; the latter is below budget by 289902. At e=98231, the same
legal theorem gives 17492173, above budget by 714958. This moves the
Mersenne residual floor by one support without claiming the next support
unsafe.

Residue-two boundary-layer continuation

At e=98231, the residue is q=2. Two top anchors now synchronize both
the s+1 and s+2 missed-coordinate layers. With exactly one top anchor,
the first boundary layer is either of size at most one or an affine line
priced by the sharper outside-core cap 484. With no top anchor, an
intersecting pair of boundary missed sets synchronizes the whole layer;
otherwise those missed sets are pairwise disjoint and there are at most
floor(e/(s+1))=3 of them.

The five exhaustive charges are

16486411, 16434204, 16433721, 16434203, 16433722.

Their maximum is below budget by 290804. At e=98232, the residue
resets to zero, so the theorem stops there without claiming an unsafe
certificate.

Residue-zero direction-class router

At the first residual support e=98232, fix one exact-boundary
explanation. Every other boundary explanation determines a nonzero
normalized codeword direction agreeing with the gauged direction on at
least A=32746 coordinates. Distinct directions have intrinsic agreement
sets meeting in at most K-1=5 coordinates. The constant-block Johnson
count therefore permits at most three direction classes. Each class and
the anchor lie on a nonzero affine codeword line, whose outside-core cap is
484; subtracting the repeated anchor gives

|D| <= 1+3*(484-1) = 1450.

The exact prefix through H-1 is 16432695. Hence an unsafe family must
put at least 343071 slopes on the synchronized top line. Total-core line
packing then forces a common core of size at least 67452=m-2. This is a
proved structural router, not by itself a safety or unsafety certificate at
e=98232.

Residue-zero common-core absorption

The router's near-maximal core contains at least 67447 coordinates inside
the gauged direction support. Two top anchors therefore synchronize every
assigned explanation of outside deficit at least
98232-67447+6=30791 onto the same affine line. All lower explanations
have outside agreement at least 36664, and one punctured ordinary-Johnson
count bounds their number by 26. Charging the high line once and using
the conservative owner factor e below gives

|Z| <= 981129 + 98232*26 = 3535161 < 16777215.

This contradiction pays Mersenne full-lift support e=98232, with margin
13242054.

Fixed-cutoff boundary-stack interval

Fixing the lower deficit cutoff h0=65200, price every exact intermediate
layer by the same normalized-direction class count and outside-core line
cap, while retaining the synchronized top line. The resulting compiler
pays directly through e=101149; for the final six supports, unsafety
forces enough top-line core for the preceding absorption argument. At the
endpoint e=101155,

forcing charge = 16667033,
top threshold  =   110183,
forced core    =    67446,
low list cap   =       28,
final bound    =  3813469.

Thus all 2,924 supports 98232<=e<=101155 are paid. At adjacent
e=101156, the fixed-cutoff forcing charge is 16951223, above budget by
174008; this is a method wall, not an unsafe certificate.

Residue-two repair at the fixed-cutoff wall

At e=101156, optimize the cutoff to h0=65258. The full fixed-cutoff
charge is 16895280, with top two boundary charges 284224 and
258385. Residue q=2 lets two top anchors synchronize both boundary
layers. Unsafety in that case forces common core m-2, and core absorption
gives 3813497.

With zero or one top anchor, the first boundary layer is either one affine
line of size at most 94742, has at most one member, or has pairwise-disjoint
missed sets and size at most three. The five exhaustive bounds are

3813497, 16705799, 16611058, 16705798, 16611059.

Their maximum leaves slack 71416, so e=101156 is safe. At adjacent
e=101157, the residue resets to zero; this is the next method frontier,
not an unsafe certificate.

Boundary direction-class affine-line bank

For every exact deficit layer, retain each normalized-direction class as
one affine explanation-line slot instead of closing it separately with the
outside-core cap. If J_h is the direction-class bound, padding absent
classes by anchor-only slots gives the exact identity

|D_h| = 1-J_h + sum_(j=1)^J_h |L_(h,j)|.

After summing the low prefix and all boundary layers, unsafety forces one
line slot above an explicit threshold. Total-core line packing then forces
a large common core on that line, and the existing core-absorption theorem
synchronizes every sufficiently high explanation onto it. No outside-core
denominator is used. With fixed cutoff h0=65272, exact replay gives

first e=101157: direct charge 6380798650, threshold 2350,
                forced core 67037, final bound 3813525;
last  e=124805: direct charge 33909422817, threshold 440,
                forced core 65220, final bound 16706559.

This pays all 23,649 supports 101157<=e<=124805 by absorption. At
adjacent e=124806, the exact low-list cap rises from 126 to 127 and the
bound becomes 16831491, exceeding budget by 54276. This is a method
wall, not an unsafe certificate.

Recursive affine-line peeling and inside-core packing

After r forced affine explanation lines have been removed and charged by
r*(N-m+1), rerun the exact-layer line bank on the residual family. If its
weighted prefix does not pay, unsafety forces another line. Total-core
absorption lowers the residual deficit ceiling when possible.

There is also a second termination invariant. A peeled parameterized line
has a codeword pair (a_i,b_i) and an inside common core of certified size
u_i. Distinct peeled lines have distinct codeword pairs, so their inside
cores meet in at most K-1=5 coordinates. Hence

sum_i u_i-C(r,2)*5 <= e.

A strict violation contradicts the assumed unsafe family. With the printed
guarded moving cutoff, exact replay pays all 5,393 supports
124806<=e<=130198: 3,837 terminate at the weighted prefix and 1,556 by
core packing, using at most five lines. At the last support,

37718+33617+28204+20729+12942-10*5 = 133160 > 130198.

At adjacent e=130199, nine legal peels give packing lower bound 126052.
The next residual target is 7947054, while the certified base charge is
8154082, so the current pigeonhole cannot force another line. This is a
method wall, not an unsafe certificate.

Joint-core charge for peeled lines

The removed-line charge can use the same geometry instead of paying the
worst-case N-m+1 independently. For r distinct parameterized lines
with actual total-core sizes g_i,

sum_i g_i <= S_r := min(r(m-1),e+C(r+1,2)(K-1)).

The single-line cap f(g)=(N-g)/(m-g) is increasing and convex. Endpoint
concentration therefore gives the exact joint charge

q=floor(S_r/(m-1)), z=S_r-q(m-1), Q=N-m+1,
L_r=rQ                                             if q=r,
L_r=floor(qQ+f(z)+(r-q-1)f(0))                    otherwise.

Using residual target B-L_r pays all 21 supports
130199<=e<=130219. At the endpoint, 13 lines give

18393+12*9736-C(13,2)*5 = 134835 > 130219.

At adjacent e=130220, the first 43 positive cores give only 97018.
The joint allowance then admits a second endpoint core, the next threshold
drops to 13, and its forced-core lower bound is zero. Later thresholds
cannot increase. This is a method wall, not an unsafe certificate.

Lower-aware joint-core charge

The joint envelope can retain every total-core lower bound forced when a
line was selected. Sort those lower bounds decreasingly and spend the common
core budget by filling the largest coordinate to (m-1), then the next.
Convexity of (f(g)=(N-g)/(m-g)) proves that this greedy vector maximizes the
total line charge subject to all lower bounds.

At (e=130220) and (e=130221), 37 removed lines have lower-bound runs
(15816cdot4,2046cdot33). The maximizing joint charge is only (609),
so one final threshold 20 is forced. The 38 inside cores then give

5*15811+33*2041-C(38,2)*5 = 142893 > e.

At adjacent (e=130222), the exact compiler reaches 288 peels. Its
maximizing allocation is (67453cdot5,1037,0cdot282), with charge
(4910044); the residual target (11867171) is below certified base
(12148280). This is a method wall, not an unsafe certificate.

Core-dichotomy capped charge

Fix absorption cutoff (b=65450). A selected line with actual total core
(gge e+10-b) synchronizes every explanation above (b), so the exact
weighted prefix through (b) plus one line is at most (5161307).
In the complementary branch, every peeled core has cap
(G_e=e+9-b); the lower-aware convex envelope is recomputed with that
individual ceiling.

The complementary branch closes (e=130222,130223) with fourteen
threshold-18 lines,

14*9736-C(14,2)*5 = 135849 > e,

and closes (e=130224,130225) with seventy threshold-16 lines,

70*2041-C(70,2)*5 = 130795 > e.

At adjacent (e=130226), the first threshold is 14 and has zero forced
core. After 14,763 capped zero-lower-bound peels, the next threshold is one.
This is a method wall, not an unsafe certificate.

Exact-layer slot-core incidence

Every recursive-bank slot in this interval has one exact-layer owner. If a
selected affine explanation line contains at least lambda>=2 members of
exact layer h and has inside common core u, off-core line incidences are
disjoint and therefore

lambda*h <= e+(lambda-1)u,
u >= ceil((lambda*h-e)/(lambda-1)).

The bound is monotone in the forced minimum slot size and minimum exact layer.
Using it in the capped-core branch makes three distinct selected lines violate
pairwise inside-core packing for every support 130226<=e<=130236. The
smallest printed packing bound is

3*43948-C(3,2)*5 = 131829 > 130229.

At adjacent e=130237, the bank forces only size-two shift-pair slots, with
inside core 807. The first-order packing expression has maximum
65529<e; after 7,583 lower bounds the capped charge reaches threshold one.
This is a method wall, not an unsafe certificate.

First-wall interpolation common-factor router

At e=130237, every selected affine explanation line gives a distinct
polynomial pair (a,b) in RS_6^2 agreeing with the received pair on at least
807 inside coordinates. After 2,704 removed lines the capped charge is only
132,203, so unsafety still forces line 2,705.

Let I_264 be the weight-(1,5,5) interpolation kernel through all 130,237
inside received points. Exact monomial counting gives

dim I_264 >= 131175-130237 = 938.

Every selected pair is a common F(X)-rational zero of this kernel: after
substitution, a kernel polynomial has degree at most 264 but at least 807
roots. If the kernel has no positive-(Y,Z)-degree common factor, two generic
members are coprime of (Y,Z)-degree at most 52. Affine Bezout then permits at
most 52^2=2704 common pairs, contradicting line 2,705.

Thus the coprime branch is paid. Every unsafe survivor forces a common factor
of positive (Y,Z) degree over the algebraic closure of F(X). This does not
yet classify that factor as a split pencil.

Common-factor mass concentration

The capped size-two bank actually forces 7,583 distinct polynomial-pair cores
before its threshold drops to one. If the full interpolation gcd has
(Y,Z)-degree d, dividing by it leaves a gcd-one cofactor family of degree
at most 52-d. Cofactor Bezout therefore permits at most (52-d)^2 selected
pairs off the factor, so

on-factor pairs >= 7583-(52-d)^2 >= 4982.

Every captured pair has an inside core of size at least 807, and distinct pair
cores intersect in at most five coordinates. Incidence Cauchy gives

factor points >= ceil(t*807^2/(807+5(t-1))) >= 126188.

Thus the received pair satisfies one degree-at-most-52 factor relation on at
least 126,188 of 130,237 inside coordinates, leaving at most 4,049 exceptions.
This is not a common core, and it does not assert irreducibility, rationality,
or split-pencil form.

Linear-factor projective-star classification

If the full interpolation gcd has (Y,Z)-degree one, write its primitive
equation over the algebraic closure as

P(X,Y,Z) = A(X)Y+B(X)Z+C(X).

The 4,982 captured degree-five sections form one polynomial-parameter family
(a_i,b_i)=(a_0+B t_i,b_0-A t_i), with
deg t_i <= 5-max(deg A,deg B). The received pair induces a scalar word
on which every t_i has at least 807 agreements. Ordinary Johnson gives
the exact caps

parameter degree s:  0    1    2    3    4       5
list cap J_s:       161  201  268  401  802  1632032

Thus 4,982 sections exclude every nonconstant A or B. After
projective rescaling the factor is defined over F, and all captured
affine explanation lines share one F-rational projective
slope-codeword center. The finite case is
(gamma_*,c_*)=(B/A,-C/A); when A=0, all lines share the direction
codeword -C/B, the center at infinity.

This classifies the degree-one branch as the primitive projective-star shape.
It does not pay the star population. The complementary common-factor branch
has (Y,Z)-degree at least two.

Common-factor weighted-degree bound

Let P be the primitive full gcd of the weight-(1,5,5),
degree-264 interpolation kernel, and let w be its weighted degree.
Division by P embeds the at-least-938-dimensional kernel into weighted
degree at most 264-w. Exact monomial counting gives

M(46)=935 < 938 <= 990=M(47),

so w<=217 and deg_(Y,Z) P<=43. In the higher-degree branch
d>=2, the existing cofactor Bezout and core-incidence bounds sharpen to

on-factor pairs >= 7583-(52-2)^2 = 5083,
factor points    >= 126266,
inside exceptions <= 3971.

The full gcd may be reducible. This removes degrees 44--52 but does not
classify a component or pay either remaining branch.

Base-field component descent

In the degree-2..43 branch, factor the radical of P geometrically.
The deployed field is F_(p^4) with p=2^31-1>43, so a component not
defined over F(X) has a distinct conjugate. Every F(X)-rational
selected pair on that component lies on the conjugate too; Bezout bounds
this population by the square of the component degree.

Summing over all non-base-field components loses at most d^2 pairs.
Therefore

pairs on F(X)-defined components
  >= 7583-(52-d)^2-d^2
  >= 5079.

One absolutely irreducible base-field component carries at least 132
selected pairs. The union of all base-field components contains at least
126,263 received inside points, leaving at most 3,974 exceptions. This is
a base-field normalization, not an irreducibility or split-pencil theorem.

Combining the low and high payments gives the revised top-rank routing:

KoalaBear q=14, h=14: e<=96150 or e>=992852
KoalaBear q=14, h=15: e<=96150 or e>=1044239
Mersenne  q=6,  h=6:  e<=130236 or e>=1037876
Mersenne  q=6,  h=7:  e<=130236 or e>=1044242

The full-lift residual intervals are now
96151<=e<=1044238 and 130237<=e<=1044241.

Validation

python3 experimental/verify_mca_affine_span_incidence_counterexample_v1.py
python3 experimental/verify_mca_affine_span_incidence_counterexample_v1_independent.py
python3 experimental/verify_mca_proper_subspace_occupancy_compiler_v1.py
python3 experimental/verify_mca_full_explanation_lifted_rank_gauge_dichotomy_v1.py
python3 experimental/verify_mca_sparse_direction_punctured_johnson_profile_v1.py
python3 experimental/verify_mca_sparse_direction_near_johnson_gram_rank_v1.py
python3 experimental/verify_mca_sparse_direction_mean_centered_gram_profile_v1.py
python3 experimental/verify_mca_sparse_direction_terminal_deficit_line_payment_v1.py
python3 experimental/verify_mca_sparse_direction_top_third_affine_line_payment_v1.py
python3 experimental/verify_mca_full_lift_top_third_common_core_payment_v1.py
python3 experimental/verify_mca_full_lift_top_third_global_line_payment_v1.py
python3 experimental/verify_mca_full_lift_mean_centered_global_line_profile_v1.py
python3 experimental/verify_mca_full_lift_boundary_anchor_continuation_v1.py
python3 experimental/verify_mca_full_lift_two_boundary_layer_continuation_v1.py
python3 experimental/verify_mca_full_lift_residue_zero_direction_router_v1.py
python3 experimental/audit_mca_full_lift_residue_zero_direction_router_v1.py
python3 experimental/verify_mca_full_lift_residue_zero_core_absorption_v1.py
python3 experimental/audit_mca_full_lift_residue_zero_core_absorption_v1.py
python3 experimental/verify_mca_full_lift_fixed_cutoff_boundary_stack_v1.py
cc -O2 -std=c11 -Wall -Wextra -Werror experimental/verify_mca_full_lift_fixed_cutoff_boundary_stack_v1.c -o /tmp/verify_m31_boundary_stack
/tmp/verify_m31_boundary_stack
python3 experimental/verify_mca_full_lift_fixed_cutoff_q2_anchor_repair_v1.py
python3 experimental/audit_mca_full_lift_fixed_cutoff_q2_anchor_repair_v1.py
python3 experimental/verify_mca_full_lift_boundary_line_bank_absorption_v1.py
python3 experimental/audit_mca_full_lift_boundary_line_bank_absorption_v1.py
cc -O2 -std=c11 -Wall -Wextra -Werror experimental/verify_mca_full_lift_boundary_line_bank_absorption_v1.c -o /tmp/verify_m31_line_bank
/tmp/verify_m31_line_bank
python3 experimental/verify_mca_full_lift_recursive_line_peeling_core_packing_v1.py
python3 experimental/audit_mca_full_lift_recursive_line_peeling_core_packing_v1.py
cc -O2 -std=c11 -Wall -Wextra -Werror experimental/verify_mca_full_lift_recursive_line_peeling_core_packing_v1.c -o /tmp/verify_m31_recursive_line_peeling
/tmp/verify_m31_recursive_line_peeling
python3 experimental/verify_mca_full_lift_joint_core_charge_peeling_v1.py
python3 experimental/audit_mca_full_lift_joint_core_charge_peeling_v1.py
python3 experimental/verify_mca_full_lift_lower_aware_joint_core_charge_v1.py
python3 experimental/audit_mca_full_lift_lower_aware_joint_core_charge_v1.py
python3 experimental/verify_mca_full_lift_core_dichotomy_capped_charge_v1.py
python3 experimental/audit_mca_full_lift_core_dichotomy_capped_charge_v1.py
python3 experimental/verify_mca_full_lift_exact_layer_slot_core_packing_v1.py
python3 experimental/audit_mca_full_lift_exact_layer_slot_core_packing_v1.py
python3 experimental/verify_mca_full_lift_interpolation_common_factor_router_v1.py
python3 experimental/audit_mca_full_lift_interpolation_common_factor_router_v1.py
python3 experimental/verify_mca_full_lift_common_factor_mass_router_v1.py
python3 experimental/audit_mca_full_lift_common_factor_mass_router_v1.py
python3 experimental/verify_mca_full_lift_linear_factor_projective_star_router_v1.py
python3 experimental/audit_mca_full_lift_linear_factor_projective_star_router_v1.py
python3 experimental/verify_mca_full_lift_common_factor_weighted_degree_bound_v1.py
python3 experimental/audit_mca_full_lift_common_factor_weighted_degree_bound_v1.py
python3 experimental/verify_mca_full_lift_common_factor_base_field_descent_v1.py
python3 experimental/audit_mca_full_lift_common_factor_base_field_descent_v1.py
cc -O2 -std=c11 -Wall -Wextra -Werror experimental/verify_mca_full_lift_joint_core_charge_peeling_v1.c -o /tmp/verify_m31_joint_charge
/tmp/verify_m31_joint_charge
latexmk -pdf -interaction=nonstopmode -halt-on-error \
  -output-directory=/tmp/rs-mca-pr1165-build experimental/grande_finale.tex
git diff --check origin/main...HEAD

All forty-seven verifier commands pass. The Johnson checker scans 129,144 official
support values exactly, checks two independent profile-coarsening controls,
and rejects both hostile constant mutations. The centered-Gram checker adds
311 exact post-Johnson support checks, an explicit finite block control, and
two mutations. The PSD mean-centered checker adds 46 newly paid exact profiles. The
terminal and top-third line checkers add the complete e<d branch payment,
a grouped-floor implementation and a sharp triple-overlap control. The full-lift common-core checker adds uniform KoalaBear prefix maxima, five
direct Mersenne cells, and a sharp total-core model. The global-line checker
scans all 58,933 paid-support cells, reconstructs both adjacent sign walls,
and rejects four further mutations. The full-prefix checker scans 528 newly
paid supports and every deficit threshold, reconstructs the theorem-sign and
budget adjacent walls, and rejects four hostile mutations. The boundary-anchor checker independently
recomputes both 65k-cap endpoint profiles and rejects four hostile mutations. The residue-two checker reconstructs five exhaustive top/boundary cases, the outside-core cap 484, the disjoint missed-set cap 3, and four hostile mutations. The residue-zero checker reconstructs the three direction classes, boundary cap 1450, strict top threshold 343071, and forced core m-2; an independent rational-arithmetic audit checks the same endpoint without importing the profile implementation. The core-absorption checker reconstructs the inside-core threshold 67447, synchronization cutoff 30791, low-list cap 26, and contradiction bound 3535161; a second rational-arithmetic audit independently checks the same payment. The fixed-cutoff endpoint verifier rejects four mutations, while its independent constant-memory C replay checks all 2,925 supports, including 2,918 direct payments, six absorption payments, and the adjacent wall. The fixed-cutoff q2 checker reconstructs all 65,258 prefix caps, 2,181 boundary charges, the unsafe-core threshold, and five exhaustive cases, rejecting five mutations; an independent constant audit checks the same payment. The boundary line-bank endpoint checker performs 6,578 exact checks and rejects five hostile mutations; its independent audit reconstructs the endpoint constants, while a constant-memory C replay checks all 23,650 support values, including 23,649 absorption payments and the adjacent method wall. The recursive-peeling endpoint checker performs 100 exact checks and rejects five hostile mutations; its independent audit reconstructs the profile, first packing, last packing, and adjacent-wall records, while a constant-memory C replay checks all 5,394 support values and the exact 3,837/1,556 termination census. The joint-charge checker scans all 21 newly paid supports and rejects five hostile mutations; its independent rational audit reconstructs both endpoint packings and the zero-core wall, while a constant-memory C replay checks the exact line-count census. The lower-aware checker reconstructs both 38-line payments and the 288-line adjacent wall, rejects four hostile mutations, and has an independent exact-rational ledger audit. The core-dichotomy checker reconstructs the high-core absorption bound, all four capped-core packing payments, and the 14,763-line threshold-one wall; it rejects four hostile mutations and has a separate exact-rational audit. The exact-layer checker recomputes all eleven new three-line payments and the adjacent size-two shift-pair wall in 161 checks; an independently structured 193-check rational audit reconstructs the same endpoint ledger. The interpolation router checks the 938-dimensional kernel count, the 2,705-line forcing threshold, and the 2,704 Bezout cap with four hostile mutations; an independent 1,450-check enumeration reconstructs its monomial and charge arithmetic. The factor-mass checker reconstructs the 7,583-line supply and the uniform 126,188-point concentration with four hostile mutations; an independent audit checks all 52 possible factor degrees. The linear-factor checker reconstructs all six exact Johnson caps and rejects three hostile mutations; an independent exact-division audit checks the same projective-star split. The weighted-degree checker reconstructs the exact 935/990 quotient threshold and rejects four hostile mutations; an independent enumeration checks all quotient degrees 0 through 264 and factor degrees 2 through 43. The base-field descent checker scans every factor degree and rejects four hostile mutations; an independent audit verifies every integer degree partition through 43.
The earlier
checkers retain
their counterexample, 616 zero-normal, 540 toy-family, 625 gauge, and all
31 codimension-one extension controls. The manuscript builds successfully
to a 116-page PDF in an isolated output directory.

[scottdhughes]

Successor #1166 is now open and ready on exact head d4d6537. It preserves and independently replays #1165, then adds the distinct support-local theta refinement, arbitrary-rank gauge, and conditional Koala rank/exception router. Its isolated math and custody reviews are GREEN; deployed v4 ledger movement remains zero.