M12 complete-original candidate, version5 (internally reviewed; no external review)
Claim: In the exact uniform accepted ensemble of M12, Algorithm1 fails with
probability at most 2 m1 2^{-d} + m1 2^{-w} + 2^{1-w}, for sufficiently large
m1 and every nonempty admissible ensemble with w>=1. Thus the stated regime
has success probability1-o(1). This does not assert the same sampling law for
the original sequential generator.

LOWER BLOCKS
Use the exact derivation in R02/M12-accepted-law-v1.txt. Write m=m1 in the
following upper-code argument (m2 retains its original meaning elsewhere).
With k=g+d,z=n-k,h=m2-z=d-w, acceptance requires full-rank C and a unique
u=(f,b) with (F|D)u=1_m. In the quotient by im C, the lower matrix is uniform
subject to (Abar|Bbar)u=0, an event of probability2^{-h}. For f!=0, Bbar is
uniform h-by-d; for f=0 it is uniform subject to Bbar b=0. Rank failure is
at most2^{1-w}. If f=0 and rank Bbar=h, the radical image contains Db=1_m,
and the attack succeeds. If f!=0 and rank is full, its kernel is a uniform
w-subspace, independent of D. For every nonzero row of D the probability
that the row vanishes on this kernel is <=2^{-w}. It remains to bound the
chance that an accepted D has a zero row in the branch f!=0.

WHY UPPER ACCEPTANCE DOES NOT ADD A HIDDEN CODE WEIGHT
Let V=F2^m with its standard symmetric bilinear form B. A doubly-even code
D is totally isotropic, and it lies in the even-weight hyperplane 1^perp.
For fixed D the nonsingular quotient U=D^perp/D has dimension m-2d. Its
canonical vector is c=1+D, since B(x,x)=B(c,x) for all quotient vectors.
In the case 1 not in D, this vector is nonzero, and U is a nonalternating
nondegenerate symmetric bilinear space. Over F2 such a space is determined
up to isometry by its dimension. One elementary proof splits off norm-one
vectors; if an alternating plane remains, <1> plus that plane is congruent
to I3, and this eliminates the alternating summand. Every isometry preserves
the uniquely defined canonical vector c.

The possible F modulo D are ordered bases of nondegenerate g-subspaces of U
containing c. Their number consequently depends only on (m,d,g), not on D.
Each basis has exactly2^{dg} lifts into D^perp, all with the same Gram matrix.
The condition 1 in col(F|D) is exactly c in col Fbar. Ordered bases for D
also have a constant multiplicity. R02 shows lower-block acceptance is the
same factor2^{-h} for every such upper block. Therefore, CONDITIONAL on
1 not in D, D is uniform among doubly-even d-subspaces excluding1. If this
class has zero acceptance weight, only the already successful f=0 branch
is present. This argument does not presume independence of F and D.

EXACT CODE COUNTS
Let N(m,d) count doubly-even d-subspaces of F2^m, and N0(m,d) count those
not containing1. Missing a specified coordinate is exactly a code of length
m-1, so its conditional probability is N(m-1,d)/N0(m,d).
Put E=1^perp and q(x)=wt(x)/2 mod2 on E. Its polar form is B restricted to E.
For a nondegenerate quadratic space of dimension2h and sign e in {+1,-1},
write
 O_e(h,d)=product_{r=0}^{d-1}
   [2^{2(h-r)-1}+e2^{h-r-1}-1]/[2^{d-r}-1],
with O(h,0)=1 and impossible dimensions interpreted as0. Also write
 S(h,d)=product_{r=0}^{d-1}[2^{2(h-r)}-1]/[2^{d-r}-1].
The former counts totally singular subspaces, the latter symplectic isotropic
subspaces. To derive the first, extend an r-dimensional singular space: its
perpendicular quotient has dimension2(h-r), unchanged sign, and
2^{2(h-r)-1}+e2^{h-r-1} zeros. Each zero has2^r lifts; exclude the existing
2^r vectors, then divide the ordered-basis count by product_r(2^d-2^r).
The symplectic formula follows identically, with every quotient vector allowed.
The zero count is the elementary quadratic Gauss sum; it can also be checked
by multiplying counts for hyperbolic/anisotropic planes.

If m is odd: h=(m-1)/2, e=+ for m=1,7 mod8 and e=- for m=3,5 mod8.
Then N=N0=O_e(h,d). The sign follows from
sum_{x even}(-1)^{wt(x)/2}=Re(1+i)^m=e2^h.
If m=0 mod4: h=(m-2)/2,e=(-1)^{m/4}; the radical <1> of E is singular.
Codes avoiding it are the2^d linear sections of a singular d-space of E/<1>,
and codes containing it correspond to singular (d-1)-spaces. Thus
 N0=2^d O_e(h,d), N=2^d O_e(h,d)+O_e(h,d-1).
If m=2 mod4: h=(m-2)/2 and q(1)=1. Each symplectic isotropic subspace of
E/<1> has a UNIQUE q-zero lift, because adding1 toggles q. Thus N=N0=S(h,d).

UNIFORM SHORTENING BOUND
These formulas give N(m-1,d)/N0(m,d)<=2*2^{-d} for all sufficiently large
m and every nonzero denominator. Explicitly:
 - For m=0 mod4 the ratio is exactly2^{-d}.
 - For m=2 mod4 it is (2^{h-d}+e)/(2^h+e), with e=(-1)^{(m-2)/4},
   by telescoping the factors; this is <=2*2^{-d}.
 - For odd m, put h=(m-1)/2 and use the same sign e as above. For m=1 mod4
   the ratio is [2^{2h-d-1}+e2^{h-1}-1]/[2^{2h-1}+e2^{h-1}-1].
   For m=3 mod4 it is [2^{2h-d-1}-e2^{h-1}]/[2^{2h-1}-e2^{h-1}].
   Each is <=2*2^{-d} for h>=2 and admissible d<=h. These identities follow
   directly from the products, or by counting vectors of the relevant
   quadratic type in D^perp. The small bounded dimensions are irrelevant to
   the asymptotic regime and are covered separately by the exhaustive check.
The union bound over m coordinates now gives Pr(D lacks support)<=2m2^{-d}.

ATTACK AND OBFUSCATION
If Bbar has full row rank, elementary column elimination removes A and
identifies H ker(H^T H) with (D ker Bbar,0). Indeed the eliminated Gram matrix
has invertible F^TF block, and the remaining lower block R=(B|C) is full row
rank; ker(R^T R)=ker R since R^T is injective. Projection of ker R onto the
D coordinates is ker Bbar, injectively because C has full column rank.
With complete support this image has support exactly the first m1 rows.
Algorithm1 solves Hs=1_support, which has the unique accepted secret because
H has full column rank. Under row permutation P and invertible column Q,
the radical image becomes P H ker(H^T H), and the secret becomes Q^{-1}s.
Thus success is invariant under the prescribed obfuscation.

Combining rank failure, support failure within a full-support D, and missing
code coordinates proves the stated bound. The hypotheses d-log2m1->infinity
and w-log2m1->infinity make every term tend to zero. No product-formula
approximation or sequential-sampling assumption is used.

REVIEW STATUS
Complete-original candidate, not yet externally checked. The exact count
checker exhausts small doubly-even codes and tests the ratio formulas, but
does not replace the argument for arbitrary dimensions. Review particularly
the classification/lift multiplicities and all parity-dependent counting cases.

M12 symbolic audit and slightly stronger failure constant.
Factor the orthogonal-space extension factor as
 f_e(h)=2^(2h-1)+e2^(h-1)-1=(2^h-e)(2^(h-1)+e).
Write O_e(h,d)=product_(r=0)^(d-1) f_e(h-r)/(2^(d-r)-1).
This makes every shortening ratio in the candidate telescope explicitly.

m=0 mod4: N(m-1,d)/N0(m,d)=2^-d because the quadratic sign and h agree.
m=2 mod4: O_e(h,d)/S(h,d) telescopes to
 (2^(h-d)+e)/(2^h+e).
Odd m=3 mod4: S(h-1,d)/O_e(h,d) telescopes to
 (2^(h-d)-e)/(2^h-e), equivalent to the earlier expanded formula.
Odd m=1 mod4: using the two radical branches at length m-1 gives
 [2^d O_e(h-1,d)+O_e(h-1,d-1)]/O_e(h,d)
 =[2^d f_e(h-d)+(2^d-1)]/f_e(h)
 =[2^(2h-d-1)+e2^(h-1)-1]/[2^(2h-1)+e2^(h-1)-1].

For h>=2 and admissible d<=h all these ratios are <=2*2^-d, improving
the previous deliberately loose4. In the last formula, if e=-1 bound the
numerator by its first term and the denominator below by half its first
term. If e=+1, the numerator is at most twice its first term since d<=h,
and the denominator at least its first term. The other fractions obey the
same factor-two bound immediately from2^(h-d)>=1 and2^h-1>=2^(h-1).
Zero denominator cases carry no accepted weight and are not divided by.

Consequently for sufficiently large admissible m1 the exact uniform-accepted
M12 failure bound can be strengthened to
 2 m1 2^-d + m1 2^-w +2^(1-w).
The asymptotic success regime is unchanged. This audit removes the earlier
phrase 'identities follow from products' as a proof obligation by displaying
the cancellations, including the singular-radical parity case.
