Digitally bordered integer matrices: determinants, 3-adic distributions, and rational generating functions

Given an integer matrix A of order n, form M by appending the digital roots of the row sums, the column sums and the total sum. The determinant is always divisible by 9. We prove an exact identity det M = 9 tau det A - 81 c^T adj(A) r with explicit carries, show that the adjugate of M has rank one modulo 9, and show that k iterated expansions produce the factor 9^k. If the entries of A are Haar-distributed in the 3-adic integers, the carry tau is exactly uniform modulo 9 and independent of A modulo 9. Consequently P(81 divides det M) = 1 - (8/9) Q_n - (4/9) R_n, which equals 18281/59049 for n = 3 and tends to about 0.31540. Conditioning on the digits of A modulo 9 reduces the full law of the 3-adic valuation of det M to a finite average of Igusa-type generating functions, parametrised by the Smith invariants of a matrix built from those digits. The n = 1 law is closed; the n = 2 law is a rational function certified by exhaustive enumeration of all 6561 digital matrices. The algebraic core is formalised in Lean 4 and checked with AXLE. We do not claim cryptographic content, nor priority for the classical p-adic determinant laws. The record contains the English version (main file), a faithful Portuguese version, and the supplementary archive (Python scripts, figures, data, and Lean 4 files checked with the AXLE verifier for the algebraic identities of the bordered determinant, the adjugate, the iteration, and the carry splitting).