Decidable bounded search yields n<=r<N and ell0<7 with A_(ell0,r)!=0, while A_(ell,k)=0 for all ell<7,k<r. Minimality is across all seven nodes, not just zero.
Method: native-search. Induction: none. Risk: routine.
This is a human-readable planning contract, not a parsed kernel formula or accepted proof.