M12: exact conditional law of the lower blocks
Let k=g+d, z=n-k, h=m2-z=d-w. Fix T=(F|D), whose k columns are independent:
F has nondegenerate Gram matrix and is orthogonal to independent D. The
upper part of H is (T|0). Full column rank of H is EQUIVALENT to rank C=z.
Indeed, any vector in ker H first has its first k coordinates zero, and its
last z coordinates lie in ker C.

An accepted secret exists only if 1_m1 belongs to col T. When it does, write
T u=1, with u=(f,b) nonzero and unique. Conditional on full-rank C, let
pi:F2^m2 -> F2^m2/im C be the quotient, dimension h. Secret existence is
equivalent to Rbar u=0, where Rbar=pi(A|B). Before conditioning Rbar is a
uniform h-by-k matrix. The acceptance probability is exactly 2^{-h}, independent
of T,u and of the full-rank C. Therefore:
 1. T has the uniform constrained law CONDITIONED on 1 in col T.
 2. C is uniform among full-column-rank matrices, independently of T.
 3. Rbar is uniform among matrices annihilating u; its lifts have equal counts.
This removes an acceptance-bias ambiguity without asserting independence
between F and D.

If f!=0, Bbar is an unrestricted uniform h-by-d matrix: the constraint fixes
one A-column after the others are chosen. If f=0, then D b=1, and Bbar is
uniform among h-by-d matrices killing fixed nonzero b. A union bound over
nonzero left null vectors gives rank-failure probability <2^{-w} in the first
case, and <2^{1-w} in the second. These are finite-size bounds, not asymptotic
product approximations.

Conditional on rank Bbar=h, Gross--Hangleiter Corollary3 identifies the radical
image as D ker Bbar (embedded in the first m1 rows), of dimension w. In the
f=0 case it contains D b=1, hence has full support with certainty. In the f!=0
case ker Bbar is a uniform w-subspace of F2^d. For any nonzero row functional
ell of D, its probability of vanishing on this subspace is
 product_{j=0}^{w-1}(2^{d-1}-2^j)/(2^d-2^j) <=2^{-w}.
Consequently failure <=2^{1-w}+m1 2^{-w}+Pr(D lacks full support | accepted,
1 not in col D). The last probability is NOT replaced by an independent
uniform-matrix estimate. Its accepted upper-block law still requires a
quadratic-space counting argument (doubly-even totally singular subspaces,
including the canonical all-ones radical when m1 is even).

This is the conditional-law component. The completed upper-code counting
argument and asymptotic theorem are in proof.txt in this candidate bundle.
