Gyires's permanent inequality for structured matrices

The preprint includes nonnegative circulants of orders five, six, and seven; all-order permutation polynomials aI+bQ+cQ²; all-order four-block matrices; one exceptional column or row; and all rank-at-most-two doubly stochastic matrices through order fifteen. It also proves structural, scalar, polynomial, deletion, balancing, local, and counting results. Exact counterexamples identify failed auxiliary assertions. Only the principal order-five claims have complete Lean proofs. The broader arguments have incomplete Lean verification. The unrestricted conjecture remains outside these results.