Certified minimal memory for a divisor-residue presence observable modulo 30

UNREVIEWED STANDALONE MATHEMATICS PREPRINT. This seven-page article develops BC-MOD30 into a self-contained account of a precisely defined divisor-residue presence observable. Its source snapshots were already released in the companion to 10.5281/zenodo.23981308; this is a focused exposition with fresh reproducibility checks, not a claim of a newly discovered general automata theory. For words over the eight units modulo 30, the output counts distinct unordered residue pairs represented by complementary nonempty proper selections of labelled factor occurrences. Repeated occurrences and equal residue pairs are treated explicitly. The article proves the exact semantic recurrence, the supplied-factorisation interpretation and a certificate-based minimality theorem: 147 reachable semantic states and 1176 transitions admit exactly 101 future-output classes. Access words and 5050 separating suffixes certify the quotient and its lower bound among all deterministic output machines with this contract; suffixes of length at most two suffice. A separate elementary proof of the classical zero-sum constant D(C2 x C4)=5 yields the universal optimal threshold of six occurrences for equality between full and proper sub-product supports. The five-letter witness (7,7,7,11,17), realised by 64141, establishes sharpness. This saturation result is distinct from 101-state minimality. Fresh Python verification passed the states, transitions, quotient witnesses, 3002 multisets and 8007 integers at most 30029 coprime to 30. Regeneration reproduced the principal certificate byte for byte. Historical Lean S4/S5 sources and receipts are preserved with their original scope; no fresh Lean compilation or remote CI was run for this article. The elementary written proof is not represented as a newly compiled Lean proof. The companion contains exact source snapshots, fresh logs, reproducibility instructions, the article authoring source, a provenance map and checksums. Standard automata and finite-group zero-sum methods are credited to Moore, Nerode and Olson. No originality, priority, independent human peer review, factorisation algorithm, primality speedup, asymptotic average, Riemann-hypothesis result or industrial performance claim is established. Alexandre Couret, independent researcher, Rasigueres, France; ORCID 0009-0000-8246-7146. Substantial AI assistance was used; the named author is responsible for the deposited statements. No new blanket reuse licence is granted; existing explicit notices retain their scope.